Theorems · Theorem · probability

ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF

Deprecated since 2026-01-27Use ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF instead.

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ}
  {cY : ℕ → NNReal} {ℱ : MeasureTheory.Filtration ℕ mΩ} [inst_1 : MeasureTheory.IsZeroOrProbabilityMeasure μ],
  MeasureTheory.StronglyAdapted ℱ Y →
    ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) μ →
      ∀ (n : ℕ),
        (∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
          ∀ {ε : ℝ},
            0 ≤ ε →
              μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑(∑ i ∈ Finset.range n, cY i)))

Alias of ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF. Azuma-Hoeffding inequality for sub-Gaussian random variables.

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

0 results in Mathlib

Foundations

Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

StandardBorelSpaceMeasureTheory.IsZeroOrProbabilityMeasure