Sub-Gaussian random variables #

This presentation of sub-Gaussian random variables is inspired by section 2.5 of [Ver18]. Let X be a random variable. Consider the following five properties, in which Kᵢ are positive reals,

(i) for all t ≥ 0, ℙ(|X| ≥ t) ≤ 2 * exp(-t^2 / K₁^2),
(ii) for all p : ℕ with 1 ≤ p, 𝔼[|X|^p]^(1/p) ≤ K₂ sqrt(p),
(iii) for all |t| ≤ 1/K₃, 𝔼[exp (t^2 * X^2)] ≤ exp (K₃^2 * t^2),
(iv) 𝔼[exp(X^2 / K₄)] ≤ 2,
(v) for all t : ℝ, 𝔼[exp (t * X)] ≤ exp (K₅ * t^2 / 2).

Properties (i) to (iv) are equivalent, in the sense that there exists a constant C such that if X satisfies one of those properties with constant K, then it satisfies any other one with constant at most CK.

If 𝔼[X] = 0 then properties (i)-(iv) are equivalent to (v) in that same sense. Property (v) implies that X has expectation zero.

The name sub-Gaussian is used by various authors to refer to any one of (i)-(v). We will say that a random variable has sub-Gaussian moment generating function (mgf) with constant K₅ to mean that property (v) holds with that constant. The function exp (K₅ * t^2 / 2) which appears in property (v) is the mgf of a Gaussian with variance K₅. That property (v) is the most convenient one to work with if one wants to prove concentration inequalities using Chernoff's method.

TODO: implement definitions for (i)-(iv) when it makes sense. For example the maximal constant K₄ such that (iv) is true is an Orlicz norm. Prove relations between those properties.

Conditionally sub-Gaussian random variables and kernels #

A related notion to sub-Gaussian random variables is that of conditionally sub-Gaussian random variables. A random variable X is conditionally sub-Gaussian in the sense of (v) with respect to a sigma-algebra m and a measure μ if for all t : ℝ, exp (t * X) is μ-integrable and the conditional mgf of X conditioned on m is almost surely bounded by exp (c * t^2 / 2) for some constant c.

As in other parts of Mathlib's probability library (notably the independence and conditional independence definitions), we express both sub-Gaussian and conditionally sub-Gaussian properties as special cases of a notion of sub-Gaussianity with respect to a kernel and a measure.

Main definitions #

Kernel.HasSubgaussianMGF: 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).
HasCondSubgaussianMGF: 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 : ℝ. 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.
HasSubgaussianMGF: 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 is equivalent to Kernel.HasSubgaussianMGF with a constant kernel. See HasSubgaussianMGF_iff_kernel.

Main statements #

measure_sum_ge_le_of_iIndepFun: Hoeffding's inequality for sums of independent sub-Gaussian random variables.
measure_sum_ge_le_of_HasCondSubgaussianMGF: the Azuma-Hoeffding inequality for sub-Gaussian random variables.

Implementation notes #

Definition of `Kernel.HasSubgaussianMGF` #

The definition of sub-Gaussian with respect to a kernel and a measure is the following:

structure Kernel.HasSubgaussianMGF (X : Ω → ℝ) (c : ℝ≥0)
    (κ : Kernel Ω' Ω) (ν : Measure Ω' := by volume_tac) : Prop where
  integrable_exp_mul : ∀ t, Integrable (fun ω ↦ exp (t * X ω)) (κ ∘ₘ ν)
  mgf_le : ∀ᵐ ω' ∂ν, ∀ t, mgf X (κ ω') t ≤ exp (c * t ^ 2 / 2)

An interesting point is that the integrability condition is not integrability of exp (t * X) with respect to κ ω' for ν-almost all ω', but integrability with respect to κ ∘ₘ ν. This is a stronger condition, as the weaker one did not allow to prove interesting results about the sum of two sub-Gaussian random variables.

For the conditional case, that integrability condition reduces to integrability of exp (t * X) with respect to μ.

Definition of `HasCondSubgaussianMGF` #

We define HasCondSubgaussianMGF as a special case of Kernel.HasSubgaussianMGF with the conditional expectation kernel for m, condExpKernel μ m, and the restriction of μ to m, μ.trim hm (where hm states that m is a sub-sigma-algebra). Note that condExpKernel μ m ∘ₘ μ.trim hm = μ. The definition is equivalent to the two conditions

for all t, exp (t * X) is μ-integrable,
for μ.trim hm-almost all ω, for all t, the mgf with respect to the the conditional distribution condExpKernel μ m ω is bounded by exp (c * t ^ 2 / 2).

For any t, we can write the mgf of X with respect to the conditional expectation kernel as a conditional expectation, (μ.trim hm)-almost surely: mgf X (condExpKernel μ m ·) t =ᵐ[μ.trim hm] μ[fun ω' ↦ exp (t * X ω') | m].

References #

R. Vershynin, High-dimensional probability: An introduction with applications in data science

Sub-Gaussian random variables #

Conditionally sub-Gaussian random variables and kernels #

Main definitions #

Main statements #

Implementation notes #

Definition of Kernel.HasSubgaussianMGF #

Definition of HasCondSubgaussianMGF #

References #

Sub-Gaussian with respect to a kernel and a measure #

Conditionally sub-Gaussian moment generating function #

Sub-Gaussian moment generating function #

Definition of `Kernel.HasSubgaussianMGF` #

Definition of `HasCondSubgaussianMGF` #