Chernoff Bounds

Exponential-moment tail bounds, including the optimized sub-Gaussian tail estimate.

Main definitions

This module introduces no new definitions.

Main results

• chernoff_bound_cgf: a tail bound expressed through the cumulant generating function.
• chernoff_bound_subGaussian: the optimized sub-Gaussian specialization.

theorem LeanPool.chernoff_bound_cgf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {ε t : ℝ} (ht : 0 ≤ t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (μ {ω : Ω | ε ≤ X ω}).toReal ≤ Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)

Chernoff bound via cgf: For any t ≥ 0, P(X ≥ ε) ≤ exp(cgf(t) - t·ε).

theorem LeanPool.chernoff_bound_subGaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {σ u : ℝ} (hσ : 0 < σ) (hu : 0 < u) (h_sgb : ∀ (t : ℝ), ProbabilityTheory.cgf X μ t ≤ t ^ 2 * σ ^ 2 / 2) (h_int : ∀ (t : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : (μ {ω : Ω | u ≤ X ω}).toReal ≤ Real.exp (-u ^ 2 / (2 * σ ^ 2))

Chernoff bound optimized for sub-Gaussian random variables. If cgf(X, t) ≤ t²σ²/2, then P(X ≥ u) ≤ exp(-u²/(2σ²)).