Theorems · Definition · probability

ProbabilityTheory.HasCondSubgaussianMGF

{Ω : Type u_1} →
  (m : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      m ≤ mΩ →
        [StandardBorelSpace Ω] →
          (Ω → ℝ) →
            NNReal →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasCondSubgaussianMGF._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop

A random variable X has a conditionally sub-Gaussian moment-generating function with parameter c with respect to a sigma-algebra m and a measure μ if for all t : ℝ, exp (t * X) is μ-integrable and the moment-generating function of X conditioned on m is almost surely bounded by exp (c * t ^ 2 / 2) for all t : ℝ. This implies in particular that X has expectation 0. The actual definition uses Kernel.HasSubgaussianMGF: HasCondSubgaussianMGF is defined as sub-Gaussian with respect to the conditional expectation kernel for m and the restriction of μ to the sigma-algebra m.

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

15 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure