Theorems · Inductive type · probability

ProbabilityTheory.Kernel.HasSubgaussianMGF

{Ω : Type u_1} →
  {Ω' : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {mΩ' : MeasurableSpace Ω'} →
        (Ω → ℝ) →
          NNReal →
            ProbabilityTheory.Kernel Ω' Ω →
              autoParam (MeasureTheory.Measure Ω') ProbabilityTheory.Kernel.HasSubgaussianMGF._auto_1 → Prop

A random variable X has a sub-Gaussian moment-generating function with parameter c with respect to a kernel κ and a measure ν if for ν-almost all ω', for all t : ℝ, the moment-generating function of X with respect to κ ω' is bounded by exp (c * t ^ 2 / 2). This implies in particular that X has expectation 0.

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

36 results in Mathlib

Foundations

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