Theorems · Theorem · probability

ProbabilityTheory.HasCondSubgaussianMGF.cgf_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 μ →
    ∀ᵐ (ω' : Ω) ∂μ.trim hm,
      ∀ (t : ℝ), ProbabilityTheory.cgf X ((ProbabilityTheory.condExpKernel μ m) ω') t ≤ ↑c * t ^ 2 / 2

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure