Skip to content

Bernoulli sampling theorem #1645

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 27 commits into
base: master
Choose a base branch
from

Conversation

hoheinzollern
Copy link
Member

@hoheinzollern hoheinzollern commented Jun 19, 2025

This PR contains the Bernoulli sampling theorem as described in the paper:

Formalizing concentration inequalities in Rocq: infrastructure and automation

by Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa

Much of the code leading up to this formalization has already been integrated through various PRs in MathComp and MathComp-Analysis where appropriate. See Figure 2 of the paper for a detailed explanation of the formalized theories developed for this PR, and the list below for references to the merged PRs.

Structure of the proof

The proof is inspired by Rajani's pen and paper proof.

One key lemma is mmt_gen_fun_expectation, which establishes the expectation of the moment generating function of a Bernoulli trial using the product probability measure.
Then follows the proof bernoulli_trial_mmt_gen_fun, which establishes that the moment generating function of a Bernoulli trial is the product of each moment generating function.

One key step in the above proofs is to show:

E n P [ i < n X i ] = i < n E P [ X i ]

i.e. that the expectation of the product of n random variables on the power measure of P is the product of the expectations of each variable with probability measure P.

To prove our final results, we need to establish a sequence of key analytical lemmas, namely:

  • exp2_le8: e 2 8 , inequality solved by using CoqInterval.
  • xlnx_lbound_i01: lower bound for x ln ( x ) in the interval ] 0 , 1 [ .
  • xlnx_ubound_i1y: upper bound for x ln ( x ) for x > 1 .

The proof itself is split into a sequence of intermediate (concentration) inequalities:

  • sampling_ineq1: Concentration inequality on a Bernoulli trial X , bounding the probability of X ( 1 + δ ) E n P [ X ] .
  • sampling_ineq2: Specialization of sampling_ineq1 using xlnx_lbound_i12
  • sampling_ineq3: Concentration inequality on a Bernoulli trial X , bounding the probability of X ( 1 δ ) E n P [ X ]
  • sampling_ineq4: Combines the previous two inequalities to obtain a bound on the probability of | X E n P [ X ] | δ E n P [ X ]

Finally, sampling is the main sampling theorem combining the above inequalities.

Notes on the current state of this PR

Much of this formalization has already been integrated in MathComp and MathComp-Analysis, and the goal of the current PR is to serve as a compendium to the paper. A few integration tasks currently remain:

  • first is the instantiation of semi-norms for Lp spaces, which, due to MathComp-Analysis aiming to be compatible with at least two version of MathComp, will not be integrated until support is dropped for MathComp 2.3. PR Lspace #1230 is meant to track the experiment of integrating Lp spaces in MathComp-Analysis with semi-norms, and is only compatible with MathComp 2.4 onwards.
  • second is that the theory of iterated product measures (here called power_measure), is not yet integrated into MathComp-Analysis as of version 1.12. The plan is to merge it into the next release.

As these elements get integrated into the main branches, this PR will shrink to contain only the Bernoulli sampling theorem.

PRs leading up to this one

This is a (somewhat complete) list of PRs to Analysis that have been branched out of this sampling theorem:

In additions to these PRs, this development contributed the following commits and PRs to MathComp:

@affeldt-aist affeldt-aist force-pushed the sampling_20250619 branch 4 times, most recently from bda9c53 to e04452c Compare June 28, 2025 10:27
@hoheinzollern hoheinzollern changed the title Sampling theorem Bernoulli sampling theorem Jul 8, 2025
@proux01
Copy link
Collaborator

proux01 commented Jul 9, 2025

CI green

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants