Catalog/Sparsity/ChernoffBound/Contract.lean
| 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 |