Sub-exponential random variables

A real random variable is sub-exponential with parameter K when its centered exponential moments exist and are bounded by exp (K ^ 2 * t ^ 2) for |t| ≤ 1 / K. Independent centered variables with a common parameter satisfy a two-sided Bernstein tail bound.

References

• R. Vershynin, High-Dimensional Probability, Cambridge University Press (2018), §2.7.

structure TauCeti.Probability.HasSubexponentialMGF {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (K : ℝ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : Prop

A real random variable is sub-exponential with parameter K if K > 0, it is integrable, and its centered exponential moments are integrable and bounded by exp (K ^ 2 * t ^ 2) for every |t| ≤ 1 / K.

• parameter_pos : 0 < K
• integrable : MeasureTheory.Integrable X μ
• integrable_exp_mul_centered (t : ℝ) : |t| ≤ K⁻¹ → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * (X ω - ∫ (x : Ω), X x ∂μ))) μ
• centered_mgf_le (t : ℝ) : |t| ≤ K⁻¹ → ProbabilityTheory.mgf (fun (ω : Ω) => X ω - ∫ (x : Ω), X x ∂μ) μ t ≤ Real.exp (K ^ 2 * t ^ 2)

theorem TauCeti.Probability.HasSubexponentialMGF.center {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {K : ℝ} (h : HasSubexponentialMGF X K μ) : HasSubexponentialMGF (fun (ω : Ω) => X ω - ∫ (x : Ω), X x ∂μ) K μ

Centering a sub-exponential random variable preserves its parameter.

theorem TauCeti.Probability.HasSubexponentialMGF.neg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {K : ℝ} (h : HasSubexponentialMGF X K μ) : HasSubexponentialMGF (-X) K μ

Negating a sub-exponential variable preserves its parameter.

theorem ProbabilityTheory.iIndepFun.mgf_sum_le_exp_of_hasSubexponentialMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {s : Finset ι} {K t : ℝ} (hX : ∀ i ∈ s, TauCeti.Probability.HasSubexponentialMGF (X i) K μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (ht : |t| ≤ K⁻¹) : mgf (fun (ω : Ω) => ∑ i ∈ s, X i ω) μ t ≤ Real.exp (↑s.card * K ^ 2 * t ^ 2)

The MGF of a finite sum of independent, centered sub-exponential variables is bounded by the product of their individual quadratic MGF bounds.

theorem ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_hasSubexponentialMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {s : Finset ι} {K t : ℝ} (hK : 0 < K) (hX : ∀ i ∈ s, TauCeti.Probability.HasSubexponentialMGF (X i) K μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (ht : 0 < t) : μ.real {ω : Ω | t ≤ ∑ i ∈ s, X i ω} ≤ Real.exp (-t ^ 2 / (4 * (↑s.card * K ^ 2 + K * t)))

One-sided sub-exponential Bernstein inequality. For independent centered variables with common parameter K, this bounds the upper tail of a finite sum.

theorem ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_hasSubexponentialMGF {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {s : Finset ι} {K t : ℝ} (hK : 0 < K) (hX : ∀ i ∈ s, TauCeti.Probability.HasSubexponentialMGF (X i) K μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (ht : 0 < t) : μ.real {ω : Ω | t ≤ |∑ i ∈ s, X i ω|} ≤ 2 * Real.exp (-t ^ 2 / (4 * (↑s.card * K ^ 2 + K * t)))

Sub-exponential Bernstein inequality. If the Xᵢ, i ∈ s, are independent, centered and sub-exponential with common parameter K, then for t > 0

P(|∑ i ∈ s, Xᵢ| ≥ t) ≤ 2 * exp (-t^2 / (4 * (|s| * K^2 + K * t))).

The constants follow directly from the centered MGF bound E exp (λ Xᵢ) ≤ exp (K ^ 2 * λ ^ 2) for |λ| ≤ 1 / K.