LeanMachineLearning

1.32. ForMathlib.Probability.Moments.SubExponential🔗

From the authors

Sub-exponential random variables

A real random variable X has a sub-exponential moment generating function (mgf) with parameters (V, b) if for every t with b * |t| ≤ 1, exp (t * X) is integrable and mgf X μ t ≤ exp (V * t ^ 2 / 2). The range of t is written as b * |t| ≤ 1 (rather than |t| ≤ 1 / b) so that b = 0 imposes no restriction on t: the case b = 0 is exactly HasSubgaussianMGF (see Mathlib/Probability/Moments/SubGaussian.lean, whose structure this file follows).

As for sub-Gaussian variables, the notion is first defined with respect to a kernel and a measure (Kernel.HasSubexponentialMGF), then specialized to conditionally sub-exponential variables (HasCondSubexponentialMGF, the kernel being the conditional expectation kernel of a sub-σ-algebra) and to sub-exponential variables with respect to a measure (HasSubexponentialMGF, a constant kernel).

Main definitions

  • Kernel.HasSubexponentialMGF X V b κ ν: for every t with b * |t| ≤ 1, exp (t * X) is integrable with respect to κ ∘ₘ ν and, for ν-almost every ω', mgf X (κ ω') t ≤ exp (V * t ^ 2 / 2).

  • HasCondSubexponentialMGF m hm X V b μ: Kernel.HasSubexponentialMGF with respect to the conditional expectation kernel condExpKernel μ m and the measure μ.trim hm.

  • HasSubexponentialMGF X V b μ: for every t with b * |t| ≤ 1, exp (t * X) is μ-integrable and mgf X μ t ≤ exp (V * t ^ 2 / 2). This is equivalent to Kernel.HasSubexponentialMGF with a constant kernel (hasSubexponentialMGF_iff_kernel).

Main results

  • HasSubexponentialMGF.integral_eq_zero: a sub-exponential variable is integrable and centered.

  • HasSubexponentialMGF.const_mul, neg, mono, add, add_of_indepFun, sum_of_iIndepFun: stability under scaling, sums, and independent sums.

  • HasSubexponentialMGF.measure_ge_le, measure_le_le, measure_abs_ge_le: Bernstein-type tail bounds exp (-min (t ^ 2 / (2 * V)) (t / (2 * b))).

  • HasSubexponentialMGF.measure_sum_ge_le_of_iIndepFun, measure_abs_average_ge_le: Bernstein's inequality for sums and averages of independent sub-exponential variables.

  • hasSubexponentialMGF_of_abs_le_of_integral_eq_zero: a centered variable bounded by M with second moment at most v has parameters (3 * v / 2, M).

  • HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF and measure_sum_ge_le_of_hasCondSubexponentialMGF: a sum of conditionally sub-exponential martingale differences is sub-exponential, and the corresponding Azuma–Bernstein inequality.

Implementation notes

The parameters V and b are real numbers rather than ℝ≥0, which avoids coercions in the arithmetic of the applications. The Bernstein-type tail bounds do not assume 0 < V or 0 < b: when V ≤ 0 or b ≤ 0, the right-hand side exp (-min (t ^ 2 / (2 * V)) (t / (2 * b))) is at least 1 (with the convention x / 0 = 0) and the bound holds trivially. As in Kernel.HasSubgaussianMGF, the integrability condition of the kernel version is integrability with respect to κ ∘ₘ ν, not almost-everywhere integrability with respect to κ ω'.

Sub-exponential with respect to a kernel and a measure

Conditionally sub-exponential moment-generating function

Sub-exponential moment-generating function

Module LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential contains 107 exposed declarations.