Finite Maxima of Sub-Gaussian Variables #

Deterministic soft-max inequalities and the expected maximum bound for a finite sub-Gaussian family.

Main definitions #

This module introduces no new definitions.

theorem LeanPool.measure_finset_sup_ge_le_sum {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {u : ℝ} {s : Finset ι} (hs : s.Nonempty) :

μ {ω : Ω | u ≤ s.sup' hs fun (i : ι) => X i ω} ≤ ∑ i ∈ s, μ {ω : Ω | u ≤ X i ω}

Union bound for maximum over finset: P(max_i X_i ≥ u) ≤ Σ_i P(X_i ≥ u).

theorem LeanPool.exp_mul_sup'_le_sum {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) (f : ι → ℝ) (t : ℝ) :

Real.exp (t * s.sup' hs f) ≤ ∑ i ∈ s, Real.exp (t * f i)

Scaled soft-max: exp(t · sup' f) ≤ ∑ exp(t · fᵢ).

theorem LeanPool.exp_sup'_le_sum {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) (f : ι → ℝ) :

Real.exp (s.sup' hs f) ≤ ∑ i ∈ s, Real.exp (f i)

Soft-max bound: exp(sup' f) ≤ ∑ exp(fᵢ).

theorem LeanPool.abs_sup'_le_sum {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) (f : ι → ℝ) :

|s.sup' hs f| ≤ ∑ i ∈ s, |f i|

Bound |sup' f| ≤ ∑ |fᵢ| for finite sets.

theorem LeanPool.sup'_le_sum_abs {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) {f : ι → ℝ} :

s.sup' hs f ≤ ∑ i ∈ s, |f i|

Upper bound sup' f ≤ ∑ |fᵢ| for finite sets.

theorem LeanPool.expected_max_subGaussian {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {σ : ℝ} (hσ : 0 < σ) {s : Finset ι} (hs : s.Nonempty) (hs_card : 2 ≤ s.card) (hX_sgb : ∀ i ∈ s, ∀ (t : ℝ), ProbabilityTheory.cgf (X i) μ t ≤ t ^ 2 * σ ^ 2 / 2) (hX_int_exp : ∀ i ∈ s, ∀ (t : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :

∫ (ω : Ω), s.sup' hs fun (i : ι) => X i ω ∂μ ≤ σ * √(2 * Real.log ↑s.card)

Expected maximum over finset of sub-Gaussian random variables via MGF method. E[max_i X_i] ≤ σ · √(2 log n) where n = |s|.