Bernoulli sampling lemma#1240

Draft

hoheinzollern wants to merge 73 commits intomath-comp:masterfrom

hoheinzollern:sampling

Commits on May 2, 2025

tentative definition of Lp-spaces
affeldt-aist
committed
extended reals

hoheinzollern
authored and
affeldt-aist
committed
WIP

CohenCyril
authored and
affeldt-aist
committed
norms

hoheinzollern
authored and
affeldt-aist
committed
ae improvements

CohenCyril
authored and
affeldt-aist
committed
improvements

hoheinzollern
authored and
affeldt-aist
committed
compressions

CohenCyril
authored and
affeldt-aist
committed
inclusion of lp spaces

hoheinzollern
authored and
affeldt-aist
committed
make it compile on top of master
affeldt-aist
committed
wip

hoheinzollern
authored and
affeldt-aist
committed
proved one property of ess_sup
affeldt-aist
committed
ess_supM
affeldt-aist
committed
do w.o. measure_is_zero
affeldt-aist
committed
only one admit left in lspace.v
affeldt-aist
committed
typo
affeldt-aist
committed
ess_supD
affeldt-aist
committed
wip (#26)

hoheinzollern
authored and
affeldt-aist
committed
refactor essential_supremum / infimum theory

CohenCyril
authored and
affeldt-aist
committed
fix CI
affeldt-aist
committed
changelog
affeldt-aist
committed
doc, renamings, minor fixes
affeldt-aist
committed
move Module ProperNotations
affeldt-aist
committed
removed `lspace.v` and moved its theory to `hoelder.v` (#30)

hoheinzollern
authored and
affeldt-aist
committed
renaming to distinguish real-valued functions
affeldt-aist
committed
generalized cantelli and use of lfun

hoheinzollern
authored and
affeldt-aist
committed
integrable -> lfun & simplifications (#31)

hoheinzollern
authored and
affeldt-aist
committed
slight generalization of lfun_sum, not requiring a finite measure

hoheinzollern
authored and
affeldt-aist
committed
introduce the oppr_closed machinery
affeldt-aist
committed
rm lfun_sum, lfun0
affeldt-aist
committed
Use HB.instance instead of direct Canonical

proux01
authored and
affeldt-aist
committed
rm all casts but cantelli
affeldt-aist
committed
fix
affeldt-aist
committed
Lnorm_ge0 and Lnorm_eq0_eq0 need not be specialized
affeldt-aist
committed
oppr_Lnorm not needed (?)
affeldt-aist
committed

Commits on May 7, 2025

interval instances

proux01
authored and
hoheinzollern
committed
expectation of product

affeldt-aist
authored and
hoheinzollern
committed
remark 2.15

affeldt-aist
authored and
hoheinzollern
committed
a sampling theorem

affeldt-aist
authored and
hoheinzollern
committed
axiom about composition of RVs proved

affeldt-aist
authored and
hoheinzollern
committed
wip

affeldt-aist
authored and
hoheinzollern
committed
wip
hoheinzollern
committed
rm dRV

affeldt-aist
authored and
hoheinzollern
committed
reduce Axiom taylor_ln_le to Axiom expR2_le8

t6s
authored and
hoheinzollern
committed
measurable_tnth, pro

affeldt-aist
authored and
hoheinzollern
committed
mprod
hoheinzollern
committed
cons is measurable

affeldt-aist
authored and
hoheinzollern
committed
integration over iterated product (wip)

affeldt-aist
authored and
hoheinzollern
committed
add integrability assumption to integraal_mpro

t6s
authored and
hoheinzollern
committed
one admit in bernoulli_trial_mmt_gen_fun
hoheinzollern
committed
integrable_sum_ord, integral_sum (wip)

affeldt-aist
authored and
hoheinzollern
committed
independence of product
hoheinzollern
committed
integral_mpro

authored and
hoheinzollern
committed
move expectation of product out of Bernoulli section

affeldt-aist
authored and
hoheinzollern
committed
attempt at product of random variables using pushforward
hoheinzollern
committed
Lemma expR2_le8

t6s
authored and
hoheinzollern
committed
memo, renaming

affeldt-aist
authored and
hoheinzollern
committed
HARD part done

t6s
authored and
hoheinzollern
committed
splitting sampling_wip.v

affeldt-aist
authored and
hoheinzollern
committed
introduced type bernoulliRV
hoheinzollern
committed
rm tuple_sum, tuple_prod

affeldt-aist
authored and
hoheinzollern
committed
bernoulli_trial -> bool_trial_value

affeldt-aist
authored and
hoheinzollern
committed
split the sampling theorem in two sections

affeldt-aist
authored and
hoheinzollern
committed
exp2_le8 simplified
hoheinzollern
committed
remove unused lemmas from probability.v

affeldt-aist
authored and
hoheinzollern
committed
analytical argument

t6s
authored and
hoheinzollern
committed
progress
hoheinzollern
committed
add integral_pushforward

affeldt-aist
authored and
hoheinzollern
committed
doc and nix
hoheinzollern
committed
removing independence.v
hoheinzollern
committed

Commits on Jun 24, 2025