Scalar Bernstein Inequality

This file contains generic scalar Bernstein CGF-to-tail infrastructure and the classical Bernstein inequality for finite independent sums of centered bounded real random variables.

Main results

• bernstein_one_sided_of_cgf_bound: a coarse one-sided sub-exponential tail bound from a local quadratic CGF estimate.
• bernstein_two_sided_of_cgf_bound: the corresponding two-sided bound.
• bernstein_mgf_le_of_centered_abs_le: one-variable Bernstein MGF bound.
• bernstein_cgf_le_of_centered_abs_le: one-variable Bernstein CGF bound.
• bernstein_cgf_sum_le: rational CGF bound for a finite independent sum.
• bernstein_one_sided_of_rational_cgf_bound: exact optimized Bernstein tail from a rational CGF estimate.
• bernstein_inequality_finset: scalar Bernstein inequality for a Finset.
• bernstein_inequality: [Fintype] convenience wrapper.

theorem LeanPool.bernstein_one_sided_of_cgf_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} {v b C t : ℝ} (hC : 0 < C) (hv : 0 < v) (hb : 0 < b) (hcgf : ∀ (l : ℝ), |l| ≤ (2 * C * b)⁻¹ → ProbabilityTheory.cgf Y μ l ≤ C * l ^ 2 * v) (hint : ∀ (l : ℝ), |l| ≤ (2 * C * b)⁻¹ → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ) (ht : 0 ≤ t) : (μ {ω : Ω | t ≤ Y ω}).toReal ≤ Real.exp (-(1 / (4 * C)) * min (t ^ 2 / v) (t / b))

A one-sided Bernstein tail bound from a local quadratic CGF estimate.

theorem LeanPool.bernstein_two_sided_of_cgf_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} {v b C t : ℝ} (hC : 0 < C) (hv : 0 < v) (hb : 0 < b) (hcgf : ∀ (l : ℝ), |l| ≤ (2 * C * b)⁻¹ → ProbabilityTheory.cgf Y μ l ≤ C * l ^ 2 * v) (hint : ∀ (l : ℝ), |l| ≤ (2 * C * b)⁻¹ → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ) (ht : 0 ≤ t) : (μ {ω : Ω | t ≤ |Y ω|}).toReal ≤ 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / v) (t / b))

A two-sided Bernstein tail bound from a local quadratic CGF estimate.

Exact scalar Bernstein CGF and tail infrastructure

theorem LeanPool.iIndepFun.integrable_exp_mul_finsetSum {Ω : Type u} [MeasurableSpace Ω] {ι : Type u_1} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (h_meas : ∀ (i : ι), AEMeasurable (X i) μ) {s : Finset ι} {t : ℝ} (h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * (∑ i ∈ s, X i) ω)) μ

theorem LeanPool.bernstein_mgf_le_of_centered_abs_le {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {b l : ℝ} (hX : AEMeasurable X μ) (hcenter : ∫ (ω : Ω), X ω ∂μ = 0) (hbound : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ b) (hl : 0 ≤ l) (hbl : b * l < 3) : ProbabilityTheory.mgf X μ l ≤ Real.exp (ProbabilityTheory.variance X μ * l ^ 2 / (2 * (1 - b * l / 3)))

Bernstein MGF bound for one centered, almost surely bounded real random variable.

theorem LeanPool.bernstein_cgf_le_of_centered_abs_le {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {b l : ℝ} (hX : AEMeasurable X μ) (hcenter : ∫ (ω : Ω), X ω ∂μ = 0) (hbound : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ b) (hl : 0 ≤ l) (hbl : b * l < 3) : ProbabilityTheory.cgf X μ l ≤ ProbabilityTheory.variance X μ * l ^ 2 / (2 * (1 - b * l / 3))

Bernstein CGF bound for one centered, almost surely bounded real random variable.

theorem LeanPool.bernstein_cgf_sum_le {Ω : Type u} [MeasurableSpace Ω] {ι : Type u_1} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (s : Finset ι) {X : ι → Ω → ℝ} {b v l : ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hcenter : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hbound : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ b) (hvar : ∑ i ∈ s, ProbabilityTheory.variance (X i) μ ≤ v) (hl : 0 ≤ l) (hbl : b * l < 3) : ProbabilityTheory.cgf (∑ i ∈ s, X i) μ l ≤ v * l ^ 2 / (2 * (1 - b * l / 3))

The CGF of a finite independent sum satisfies the rational Bernstein bound.

theorem LeanPool.bernstein_one_sided_of_rational_cgf_bound {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} {v b t : ℝ} (hv : 0 < v) (hb : 0 ≤ b) (ht : 0 ≤ t) (hcgf : ∀ (l : ℝ), 0 ≤ l → b * l < 3 → ProbabilityTheory.cgf Y μ l ≤ v * l ^ 2 / (2 * (1 - b * l / 3))) (hint : ∀ (l : ℝ), 0 ≤ l → b * l < 3 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ) : (μ {ω : Ω | t ≤ Y ω}).toReal ≤ Real.exp (-t ^ 2 / (2 * (v + b * t / 3)))

Exact one-sided Bernstein tail bound from a rational Bernstein CGF estimate.

theorem LeanPool.bernstein_inequality_finset {Ω : Type u} [MeasurableSpace Ω] {ι : Type u_1} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (s : Finset ι) {X : ι → Ω → ℝ} {b v t : ℝ} (hb : 0 ≤ b) (hv : 0 < v) (ht : 0 ≤ t) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hcenter : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (hbound : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ b) (hvar : ∑ i ∈ s, ProbabilityTheory.variance (X i) μ ≤ v) : (μ {ω : Ω | t ≤ (∑ i ∈ s, X i) ω}).toReal ≤ Real.exp (-t ^ 2 / (2 * (v + b * t / 3)))

Scalar Bernstein inequality for a finite set of independent centered bounded summands.

theorem LeanPool.bernstein_inequality {Ω : Type u} [MeasurableSpace Ω] {ι : Type u_1} [Fintype ι] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {b v t : ℝ} (hb : 0 ≤ b) (hv : 0 < v) (ht : 0 ≤ t) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hcenter : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0) (hbound : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ b) (hvar : ∑ i : ι, ProbabilityTheory.variance (X i) μ ≤ v) : (μ {ω : Ω | t ≤ (∑ i : ι, X i) ω}).toReal ≤ Real.exp (-t ^ 2 / (2 * (v + b * t / 3)))

Convenience [Fintype ι] wrapper for the scalar Bernstein inequality.