theorem hoeffding_mgf_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (hab : a < b) (hXm : Measurable X) (hXa : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hXb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hmean : ∫ (ω : Ω), X ω ∂μ = 0) (s : ℝ) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (s ^ 2 * (b - a) ^ 2 / 8)

Hoeffding's Lemma (MGF bound): If X has mean zero and X ∈ [a, b] a.s., then E[exp(sX)] ≤ exp(s²(b-a)²/8) for all s : ℝ. This is the core MGF inequality.

theorem lemma_1_8_hoeffding {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (hab : a < b) (hXm : Measurable X) (hXi : MeasureTheory.Integrable X μ) (hXa : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hXb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hmean : ∫ (ω : Ω), X ω ∂μ = 0) : IsSubGaussian X ((b - a) ^ 2 / 4) μ

Hoeffding's Lemma (sub-Gaussian): If X has mean zero and X ∈ [a, b] a.s., then X is sub-Gaussian with variance proxy (b - a)² / 4. This means E[exp(sX)] ≤ exp(σ² s² / 2) where σ² = (b-a)²/4, i.e., E[exp(sX)] ≤ exp(s²(b-a)²/8).