Theorems · Inductive type · probability

ProbabilityTheory.HasSubgaussianMGF

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

A random variable X has a sub-Gaussian moment-generating function with parameter c with respect to a measure μ if for all t : ℝ, exp (t * X) is μ-integrable and the moment-generating function of X is bounded by exp (c * t ^ 2 / 2) for all t : ℝ. This implies in particular that X has expectation 0. This is equivalent to Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ()), as proved in HasSubgaussianMGF_iff_kernel. Properties about sub-Gaussian moment-generating functions should be proved first for Kernel.HasSubgaussianMGF when possible.

Defined in

Mathlib.Probability.Moments.SubGaussian

Cited by

36 results in Mathlib

Foundations

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