Theorems · Theorem · probability

ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF

∀ {Ω : 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)) μ) →
          ProbabilityTheory.HasSubgaussianMGF (fun ω => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ

Let Y be a random process strongly adapted to a filtration ℱ, such that for all i : ℕ, Y i is conditionally sub-Gaussian with parameter cY i with respect to ℱ (i - 1). In particular, n ↦ ∑ i ∈ range n, Y i is a martingale. Then the sum ∑ i ∈ range n, Y i is sub-Gaussian with parameter ∑ i ∈ range n, cY i.

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

2 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsZeroOrProbabilityMeasure