Catalog.Sparsity.ChernoffBound
Theorem
Theorem (Chernoff’s bound). Let \(X_1, \ldots, X_n\) be i.i.d. Bernoulli random variables with success probability \(p\). Let \(S = X_1 + \ldots + X_n\) and let \(\mu = np\) be the expected value of \(S\). Then for every \(\delta \in (0, 1)\), we have \[\Pr(|S - \mu| > \delta\mu) \leq 2\exp\!\left(-\frac{\delta^2\mu}{3}\right).\]
Review notes
The source (Theorem 3.3) cites this result without proof as a “classic variant of Chernoff’s bound”. The statement is reproduced faithfully.
Which variant.
This is the multiplicative Chernoff bound for \(\delta \in (0,1)\): two-sided (\(|S-\mu|\)), with constant \(1/3\) in the exponent. Many references state one-sided versions or use the constant \(1/2\); the \(1/3\) constant gives a slightly weaker bound but is standard in the combinatorics literature.
Implicit assumptions.
The source writes \(X_1,\ldots,X_n\) without specifying a probability space. The intended reading is: there is a common probability space on which the \(X_i\) are independent Bernoulli(\(p\)) random variables, and \(\Pr\) denotes the probability measure on that space.
Lean encoding choices.
- The probability space \((\Omega, \mu)\) is made explicit with
IsProbabilityMeasure\(\mu\). - The \(n\) random variables are indexed by
Fin nand take values in \(\mathbb{R}\). The Bernoulli condition is encoded as \(X_i(\omega) = 0 \lor X_i(\omega) = 1\) a.s., combined with \(\mathbb{E}[X_i] = p\). - Independence uses Mathlib’s
ProbabilityTheory.iIndepFun. - The hypothesis \(p \in [0,1]\) is included explicitly for readability, though it is redundant given the Bernoulli and mean conditions.
- The event set uses \(\le\) (non-strict) rather than the source’s \(>\); this is slightly stronger and matches Mathlib convention. The source statement follows immediately.
- The probability is expressed via \(\mu\)
.real, matching the convention in Mathlib’s sub-Gaussian framework (Mathlib.Probability.Moments.SubGaussian).
Proof scope.
The multiplicative Chernoff bound cannot be derived from Mathlib’s
sub-Gaussian/Hoeffding framework: Hoeffding gives
\(\exp(-2\delta^2 n p^2)\) (quadratic in \(p\)), while the Chernoff bound gives
\(\exp(-\delta^2 n p / 3)\) (linear in \(p\)). For Catalog.Sparsity.Densification,
where \(p \to 0\), the linear dependence is essential. The proof requires the
specific Bernoulli MGF analysis: \(\mathbb{E}[e^{t(X-p)}] \le
\exp((e^t - 1 - t)p)\), optimized over \(t\).
Catalog/Sparsity/ChernoffBound/Contract.lean (full)
| 1 | import Mathlib.Probability.Independence.Basic |
| 2 | import Mathlib.MeasureTheory.Integral.Bochner.Basic |
| 3 | |
| 4 | namespace Catalog.Sparsity.ChernoffBound |
| 5 | |
| 6 | /-- Theorem 3.3 (Chernoff's bound). For i.i.d. Bernoulli(p) random variables |
| 7 | X₁, ..., Xₙ with sum S and mean μ = np, for every δ ∈ (0, 1): |
| 8 | P(|S - μ| ≥ δμ) ≤ 2 exp(-δ²μ/3). -/ |
| 9 | axiom chernoffBound |
| 10 | {Ω : Type*} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} |
| 11 | [MeasureTheory.IsProbabilityMeasure μ] |
| 12 | {n : ℕ} {X : Fin n → Ω → ℝ} {p : ℝ} |
| 13 | (hp : p ∈ Set.Icc 0 1) |
| 14 | (hX_meas : ∀ i, Measurable (X i)) |
| 15 | (hX_indep : ProbabilityTheory.iIndepFun X μ) |
| 16 | (hX_bern : ∀ i, ∀ᵐ ω ∂μ, X i ω = 0 ∨ X i ω = 1) |
| 17 | (hX_mean : ∀ i, ∫ ω, X i ω ∂μ = p) |
| 18 | {δ : ℝ} (hδ : δ ∈ Set.Ioo 0 1) : |
| 19 | μ.real {ω | δ * (↑n * p) ≤ |(∑ i : Fin n, X i ω) - ↑n * p|} ≤ |
| 20 | 2 * Real.exp (-(δ ^ 2 * (↑n * p) / 3)) |
| 21 | |
| 22 | end Catalog.Sparsity.ChernoffBound |
| 23 |