def
IsSubGaussian
{Ω : Type u_1}
[MeasurableSpace Ω]
(X : Ω → ℝ)
(σsq : ℝ)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
:
A random variable X on a probability space is sub-Gaussian with variance proxy σsq
(representing σ²) if X is integrable, E[X] = 0,
exp(s * X) is integrable for all s, and
E[exp(sX)] ≤ exp(σsq * s² / 2) for all s : ℝ.
Instances For
theorem
IsSubGaussian.integrable
{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Ω → ℝ}
{σsq : ℝ}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(h : IsSubGaussian X σsq μ)
:
A sub-Gaussian random variable is integrable.
theorem
IsSubGaussian.mean_zero
{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Ω → ℝ}
{σsq : ℝ}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(h : IsSubGaussian X σsq μ)
:
A sub-Gaussian random variable has mean zero.
theorem
IsSubGaussian.exp_integrable
{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Ω → ℝ}
{σsq : ℝ}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(h : IsSubGaussian X σsq μ)
(s : ℝ)
:
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ
The exponential moment exp(s * X) is integrable for a sub-Gaussian random variable.
theorem
IsSubGaussian.mgf_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Ω → ℝ}
{σsq : ℝ}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(h : IsSubGaussian X σsq μ)
(s : ℝ)
:
A sub-Gaussian random variable satisfies the MGF bound for all s : ℝ.