Theorems · Theorem · probability

ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le

∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ (t : ℝ), ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun ω => Real.exp (t * X ω) | m] ω' ≤ Real.exp (↑c * t ^ 2 / 2)

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure