Bennett / Bernstein sub-gamma concentration

Variance-sensitive (Bernstein/Freedman-style) concentration, which Mathlib currently lacks: Mathlib has the sub-Gaussian MGF (HasSubgaussianMGF, the base of Azuma/Hoeffding) but not the sub-gamma / Bernstein one. When the conditional variance V is much smaller than the squared range b², the sub-Gaussian tail exp(−ε²/2b²) is far too weak; the correct bound is the variance-based exp(−ε²/(2(V+cε))).

This file develops that from scratch, Mathlib-only:

• Contrib.Bennett.HasSubgammaMGF X V c μ — the sub-gamma MGF bound mgf ≤ exp(V t²/(2(1−ct))) (the variance-based analogue of HasSubgaussianMGF, recovered at c = 0).
• Contrib.Bennett.subgamma_tail — the Bernstein tail P(X ≥ ε) ≤ exp(−ε²/(2(V+cε))), via the Chernoff bound at the optimal parameter t* = ε/(V+cε).
• Contrib.Bennett.exp_mul_le_bennett_quadratic — the pointwise quadratic majorant exp(tx) ≤ 1 + tx + x²(exp(tb)−1−tb)/b² for x ≤ b.
• Contrib.Bennett.exp_sub_one_sub_le_bernstein — exp(u) − 1 − u ≤ u²/(2(1−u/3)) for 0 ≤ u < 3.
• Contrib.Bennett.mgf_le_bennett — Bennett's MGF inequality for a centered, upper-bounded variable.
• Contrib.Bennett.hasSubgammaMGF_of_bounded_above — a centered variable bounded above by b with second moment ≤ V is sub-gamma with variance factor V and scale b/3.

Sorry-free and axiom-clean [propext, Classical.choice, Quot.sound].

def Contrib.Bennett.HasSubgammaMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (V c : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

Sub-gamma MGF bound. X has a sub-gamma MGF with variance factor V and scale c if mgf X μ t ≤ exp(V t²/(2(1−ct))) for 0 ≤ t and ct < 1. This is the variance-based (Bernstein) analogue of HasSubgaussianMGF; when c = 0, every nonnegative parameter is in the effective domain. It is the martingale-summable object underlying Freedman's inequality.

Equations

• Contrib.Bennett.HasSubgammaMGF X V c μ = ∀ (t : ℝ), 0 ≤ t → c * t < 1 → ProbabilityTheory.mgf X μ t ≤ Real.exp (V * t ^ 2 / (2 * (1 - c * t)))

theorem Contrib.Bennett.subgamma_tail {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V c ε : ℝ} (h : HasSubgammaMGF X V c μ) (hV : 0 < V) (hc : 0 < c) (hε : 0 ≤ ε) (hint : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (ε / (V + c * ε) * X ω)) μ) : μ.real {ω : Ω | ε ≤ X ω} ≤ Real.exp (-ε ^ 2 / (2 * (V + c * ε)))

Bernstein tail from the sub-gamma MGF. If X has a sub-gamma MGF with V > 0, c > 0, then P(X ≥ ε) ≤ exp(−ε²/(2(V + cε))). The optimal Chernoff parameter is t* = ε/(V+cε), at which the exponent is exactly −ε²/(2(V+cε)).

theorem Contrib.Bennett.exp_mul_le_bennett_quadratic {t b x : ℝ} (ht : 0 ≤ t) (hb : 0 < b) (hx : x ≤ b) : Real.exp (t * x) ≤ 1 + t * x + x ^ 2 * (Real.exp (t * b) - 1 - t * b) / b ^ 2

The pointwise quadratic majorant underlying Bennett's MGF inequality.

theorem Contrib.Bennett.exp_sub_one_sub_le_bernstein {u : ℝ} (hu0 : 0 ≤ u) (hu3 : u < 3) : Real.exp u - 1 - u ≤ u ^ 2 / (2 * (1 - u / 3))

The elementary exponential remainder estimate which converts Bennett's bound to Bernstein's sub-gamma bound.

theorem Contrib.Bennett.mgf_le_bennett {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {V b t : ℝ} (hbpos : 0 < b) (ht : 0 ≤ t) (hX0 : ∫ (x : Ω), X x ∂μ = 0) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hvar : ∫ (x : Ω), (fun (ω : Ω) => X ω ^ 2) x ∂μ ≤ V) (hXint : MeasureTheory.Integrable X μ) (hXsqint : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) (hexpint : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : ProbabilityTheory.mgf X μ t ≤ Real.exp (V * (Real.exp (t * b) - 1 - t * b) / b ^ 2)

Bennett's MGF inequality. A centered random variable bounded above by b > 0, whose second moment is at most V, has the Bennett exponential-moment bound.

theorem Contrib.Bennett.hasSubgammaMGF_of_bounded_above {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {V b : ℝ} (hbpos : 0 < b) (hX0 : ∫ (x : Ω), X x ∂μ = 0) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hvar : ∫ (x : Ω), (fun (ω : Ω) => X ω ^ 2) x ∂μ ≤ V) (hXint : MeasureTheory.Integrable X μ) (hXsqint : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) (hexpint : ∀ (t : ℝ), 0 ≤ t → t < 3 / b → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : HasSubgammaMGF X V (b / 3) μ

A bounded-above centered random variable with second moment at most V is sub-gamma with variance factor V and scale b / 3.