Conditional Hoeffding lemma (conditionally sub-Gaussian martingale increment)

The conditional analogue of Mathlib's hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero: a random variable a.s. bounded in [a,b] whose conditional expectation given a sub-σ-algebra m is 0 is conditionally sub-Gaussian with parameter (b−a)²/4. This is the martingale-increment bound that feeds Azuma (measure_sum_ge_le_of_hasCondSubgaussianMGF) to yield McDiarmid's bounded-differences inequality. Mathlib has the unconditional version but not this conditional one.

• Contrib.ConditionalHoeffding.hasCondSubgaussianMGF_of_mem_Icc.

The proof lifts the unconditional Hoeffding bound through the conditional-expectation kernel condExpKernel μ m.

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

theorem Contrib.ConditionalHoeffding.hasCondSubgaussianMGF_of_mem_Icc {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ} {X : Ω → ℝ} (hXm : Measurable X) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) (hmean : μ[X | m] =ᵐ[μ] 0) : ProbabilityTheory.HasCondSubgaussianMGF m hm X ⟨(b - a) ^ 2 / 4, ⋯⟩ μ

Conditional Hoeffding. A variable a.s. in [a,b] with conditional expectation 0 given m is conditionally sub-Gaussian with parameter (b−a)²/4.