[Paper Artifact] Bernoulli sampling theorem#1645

Open

hoheinzollern wants to merge 28 commits intomath-comp:masterfrom

hoheinzollern:sampling_20250619

Commits on Nov 22, 2025

Sampling theorem

hoheinzollern
authored and
affeldt-aist
committed
mfunM no longer needed

hoheinzollern
authored and
affeldt-aist
committed
removed finite_prod_fin_num and finite_prod_ge0

hoheinzollern
authored and
affeldt-aist
committed
removing subset_itvW_bound

hoheinzollern
authored and
affeldt-aist
committed
removed gtr0_derive1_homo and ger0_derive1_homo

hoheinzollern
authored and
affeldt-aist
committed
removed bigcup_mkord_ord

hoheinzollern
authored and
affeldt-aist
committed
removed measurability of tuples

hoheinzollern
authored and
affeldt-aist
committed
cleaning
affeldt-aist
committed
rm dup
affeldt-aist
committed
renaming
affeldt-aist
committed
rebase
affeldt-aist
committed
rm dead code, cleaning, rebase
affeldt-aist
committed
tuple_of_pair
affeldt-aist
committed
cleaning
affeldt-aist
committed
generalize ipro to sigma_finite

t6s
authored and
affeldt-aist
committed
cleaning
affeldt-aist
committed
rm dup code
affeldt-aist
committed
rebase
affeldt-aist
committed
remove preimage_set1

t6s
authored and
affeldt-aist
committed
ipro -> power_measure
affeldt-aist
committed
nitpicking
affeldt-aist
committed
Adding interval dependency to OPAM package

proux01
authored and
affeldt-aist
committed
[CI] Add interval dependency to mathcomp-analysis-stdlib

proux01
authored and
affeldt-aist
committed
moving sampling.v to analysis_stdlib/

hoheinzollern
authored and
affeldt-aist
committed
[CI] New attempt

proux01
authored and
affeldt-aist
committed
[CI] Further fix

proux01
authored and
affeldt-aist
committed
typo

hoheinzollern
authored and
affeldt-aist
committed
rm warnings
affeldt-aist
committed