Sub-Gaussian Processes

This file defines sub-Gaussian processes and proves tail bounds needed for Dudley's entropy integral bound.

Main definitions

• IsSubGaussian: A scalar real random variable with Mathlib's sub-Gaussian MGF bound.
• subGaussianPsi2Norm: the least MGF sub-Gaussian scale, the ψ₂ scale used by the HDP-style Hanson-Wright wrapper.
• IsSubGaussianProcess: A stochastic process indexed by a pseudo-metric space satisfies the sub-Gaussian MGF bound for increments.

Main results

• subGaussian_tail_bound_one_sided: One-sided Chernoff bound P(X_s - X_t ≥ u).
• subGaussian_tail_bound: Two-sided tail bound P(|X_s - X_t| ≥ u).
• gaussian_tail_integral: The Gaussian tail integral ∫₀^∞ 2·exp(-r²/(2τ²)) dr = τ·√(2π).
• ae_eq_zero_of_mgf_le_one: MGF ≤ 1 for all λ implies Y = 0 a.e.
• IsSubGaussian.integrable: Scalar sub-Gaussian variables are integrable.
• hasSubgaussianMGF_of_subGaussianPsi2Norm_le: Extract an MGF certificate at any scale above the ψ₂ infimum.
• hasSubGaussianPsi2Bound_subGaussianPsi2Norm_of_pos: The positive ψ₂ infimum is an admissible scale.
• integrable_ciSup_abs_of_fintype_subGaussian: Finite suprema of absolute values of sub-Gaussian families are integrable.
• subGaussian_first_moment_bound: E[|X_s - X_t|] ≤ √(2π)·σ·d(s,t).
• subGaussian_finite_max_bound: E[max_{t∈T} X_t] ≤ σ·diam(T)·√(2 log|T|).

def LeanPool.IsSubGaussian {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (σ_sq : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

A real random variable is sub-Gaussian with variance proxy σ_sq if its moment generating function is bounded by the corresponding Gaussian moment generating function.

Equations

• LeanPool.IsSubGaussian X σ_sq μ = ∃ (h : 0 ≤ σ_sq), ProbabilityTheory.HasSubgaussianMGF X ⟨σ_sq, h⟩ μ

theorem LeanPool.hasSubgaussianMGF_mono_param {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {c d : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) (hcd : ↑c ≤ ↑d) : ProbabilityTheory.HasSubgaussianMGF X d μ

Monotonicity of the MGF sub-Gaussian parameter.

def LeanPool.HasSubGaussianPsi2Bound {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (K : ℝ) : Prop

An admissible ψ₂/MGF scale for a real random variable.

This is the MGF version of the sub-Gaussian ψ₂ scale used in this development: K is admissible when X has Gaussian MGF control with variance proxy K². For centered variables this scale is equivalent, up to universal constants, to the Orlicz ψ₂ norm used in HDP.

Equations

• LeanPool.HasSubGaussianPsi2Bound X μ K = (0 < K ∧ ProbabilityTheory.HasSubgaussianMGF X ⟨K ^ 2, ⋯⟩ μ)

noncomputable def LeanPool.subGaussianPsi2Norm {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ

The ψ₂ sub-Gaussian scale as the infimum of admissible MGF scales.

Equations

• LeanPool.subGaussianPsi2Norm X μ = sInf {K : ℝ | LeanPool.HasSubGaussianPsi2Bound X μ K}

def LeanPool.HasFiniteSubGaussianPsi2Norm {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : Prop

Finiteness of the ψ₂ scale: there is at least one admissible MGF scale.

Equations

• LeanPool.HasFiniteSubGaussianPsi2Norm X μ = ∃ (K : ℝ), LeanPool.HasSubGaussianPsi2Bound X μ K

theorem LeanPool.subGaussianPsi2Norm_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hfin : HasFiniteSubGaussianPsi2Norm X μ) : 0 ≤ subGaussianPsi2Norm X μ

theorem LeanPool.exists_hasSubGaussianPsi2Bound_lt {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {R : ℝ} (hfin : HasFiniteSubGaussianPsi2Norm X μ) (hR : subGaussianPsi2Norm X μ < R) : ∃ (K : ℝ), HasSubGaussianPsi2Bound X μ K ∧ K < R

theorem LeanPool.hasSubgaussianMGF_of_subGaussianPsi2Norm_lt {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {R : ℝ} (hfin : HasFiniteSubGaussianPsi2Norm X μ) (hR : subGaussianPsi2Norm X μ < R) : ProbabilityTheory.HasSubgaussianMGF X ⟨R ^ 2, ⋯⟩ μ

theorem LeanPool.hasSubgaussianMGF_of_subGaussianPsi2Norm_le {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {R : ℝ} (hfin : HasFiniteSubGaussianPsi2Norm X μ) (hR : subGaussianPsi2Norm X μ ≤ R) : ProbabilityTheory.HasSubgaussianMGF X ⟨R ^ 2, ⋯⟩ μ

theorem LeanPool.hasSubGaussianPsi2Bound_subGaussianPsi2Norm_of_pos {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hfin : HasFiniteSubGaussianPsi2Norm X μ) (hpos : 0 < subGaussianPsi2Norm X μ) : HasSubGaussianPsi2Bound X μ (subGaussianPsi2Norm X μ)

noncomputable def LeanPool.maxSubGaussianPsi2Norm {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} (X : Fin n → Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ

Maximum coordinate ψ₂ scale for a finite random vector. It is 0 for the empty index type.

Equations

• LeanPool.maxSubGaussianPsi2Norm X μ = if h : Finset.univ.Nonempty then Finset.univ.sup' h fun (i : Fin n) => LeanPool.subGaussianPsi2Norm (X i) μ else 0

theorem LeanPool.subGaussianPsi2Norm_le_maxSubGaussianPsi2Norm {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {X : Fin n → Ω → ℝ} {μ : MeasureTheory.Measure Ω} (i : Fin n) : subGaussianPsi2Norm (X i) μ ≤ maxSubGaussianPsi2Norm X μ

theorem LeanPool.integrable_pow_of_hasSubgaussianMGF {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {c : NNReal} {μ : MeasureTheory.Measure Ω} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) (m : ℕ) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ m) μ

Every polynomial moment of a globally sub-Gaussian random variable is integrable.

theorem LeanPool.IsSubGaussian.integrable_exp_mul {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {σ_sq : ℝ} {μ : MeasureTheory.Measure Ω} (h_sg : IsSubGaussian X σ_sq μ) (t : ℝ) : MeasureTheory.Integrable (fun (x : Ω) => Real.exp (t * X x)) μ

A sub-Gaussian random variable has integrable exponential tilts.

theorem LeanPool.IsSubGaussian.integrable {Ω : Type u_1} [MeasurableSpace Ω] {X : Ω → ℝ} {σ_sq : ℝ} {μ : MeasureTheory.Measure Ω} (h_sg : IsSubGaussian X σ_sq μ) : MeasureTheory.Integrable X μ

A sub-Gaussian real random variable is integrable.

theorem LeanPool.hasSubgaussianMGF_integral_eq_zero {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) : ∫ (ω : Ω), X ω ∂μ = 0

A random variable satisfying the global sub-Gaussian MGF bound is centered.

theorem LeanPool.integrable_ciSup_of_fintype {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} [Finite ι] [Nonempty ι] {Y : ι → Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h_int : ∀ (i : ι), MeasureTheory.Integrable (Y i) μ) : MeasureTheory.Integrable (fun (x : Ω) => ⨆ (i : ι), Y i x) μ

A finite supremum of integrable real-valued functions is integrable.

theorem LeanPool.integrable_ciSup_abs_of_fintype {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} [Finite ι] [Nonempty ι] {Y : ι → Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h_int : ∀ (i : ι), MeasureTheory.Integrable (Y i) μ) : MeasureTheory.Integrable (fun (x : Ω) => ⨆ (i : ι), |Y i x|) μ

A finite supremum of absolute values of integrable real-valued functions is integrable.

theorem LeanPool.integrable_ciSup_of_fintype_subGaussian {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} [Finite ι] [Nonempty ι] {Y : ι → Ω → ℝ} {σ_sq : ι → ℝ} {μ : MeasureTheory.Measure Ω} (h_sg : ∀ (i : ι), IsSubGaussian (Y i) (σ_sq i) μ) : MeasureTheory.Integrable (fun (x : Ω) => ⨆ (i : ι), Y i x) μ

A finite supremum of a sub-Gaussian family is integrable.

theorem LeanPool.integrable_ciSup_abs_of_fintype_subGaussian {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} [Finite ι] [Nonempty ι] {Y : ι → Ω → ℝ} {σ_sq : ι → ℝ} {μ : MeasureTheory.Measure Ω} (h_sg : ∀ (i : ι), IsSubGaussian (Y i) (σ_sq i) μ) : MeasureTheory.Integrable (fun (x : Ω) => ⨆ (i : ι), |Y i x|) μ

A finite supremum of absolute values of a sub-Gaussian family is integrable.

def LeanPool.IsSubGaussianProcess {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] (μ : MeasureTheory.Measure Ω) (X : A → Ω → ℝ) (σ : ℝ) : Prop

A stochastic process {X_θ : θ ∈ A} indexed by a pseudo-metric space A is sub-Gaussian with parameter σ if each increment has the corresponding sub-Gaussian MGF certificate.

Equations

• LeanPool.IsSubGaussianProcess μ X σ = ∀ (s t : A), ProbabilityTheory.HasSubgaussianMGF (fun (ω : Ω) => X s ω - X t ω) ⟨σ ^ 2 * dist s t ^ 2, ⋯⟩ μ

Basic properties of sub-Gaussian processes

theorem LeanPool.IsSubGaussianProcess.symm {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} {X : A → Ω → ℝ} {σ : ℝ} (h : IsSubGaussianProcess μ X σ) (s t : A) : ProbabilityTheory.HasSubgaussianMGF (fun (ω : Ω) => X t ω - X s ω) ⟨σ ^ 2 * dist t s ^ 2, ⋯⟩ μ

Swapping the two indices preserves the increment MGF certificate.

theorem LeanPool.IsSubGaussianProcess.integrable_exp_mul {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} {X : A → Ω → ℝ} {σ : ℝ} (h : IsSubGaussianProcess μ X σ) (s t : A) (l : ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * (X s ω - X t ω))) μ

Exponential integrability of every sub-Gaussian process increment.

theorem LeanPool.IsSubGaussianProcess.mgf_le {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} {X : A → Ω → ℝ} {σ : ℝ} (h : IsSubGaussianProcess μ X σ) (s t : A) (l : ℝ) : ∫ (x : Ω), (fun (ω : Ω) => Real.exp (l * (X s ω - X t ω))) x ∂μ ≤ Real.exp (l ^ 2 * σ ^ 2 * dist s t ^ 2 / 2)

Numerical MGF bound for a sub-Gaussian process increment.

theorem LeanPool.IsSubGaussianProcess.mono {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} {X : A → Ω → ℝ} {σ σ' : ℝ} (h : IsSubGaussianProcess μ X σ) (hσ : 0 ≤ σ) (hσ' : σ ≤ σ') : IsSubGaussianProcess μ X σ'

If σ ≤ σ', then σ-sub-Gaussian implies σ'-sub-Gaussian.

Tail bounds for sub-Gaussian processes

The key result is that sub-Gaussian increments have exponentially decaying tails.

theorem LeanPool.subGaussian_tail_bound_one_sided {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : A → Ω → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX : IsSubGaussianProcess μ X σ) (s t : A) (u : ℝ) (hu : 0 < u) (hd : 0 < dist s t) : (μ {ω : Ω | X s ω - X t ω ≥ u}).toReal ≤ Real.exp (-u ^ 2 / (2 * σ ^ 2 * dist s t ^ 2))

Chernoff bound: for any sub-Gaussian increment, P(X_s - X_t ≥ u) ≤ exp(-u²/(2σ²d(s,t)²)). This is the one-sided tail bound. Note: In a PseudoMetricSpace, we require dist s t > 0 explicitly (unlike MetricSpace where this follows from s ≠ t).

theorem LeanPool.subGaussian_tail_bound {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : A → Ω → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX : IsSubGaussianProcess μ X σ) (s t : A) (u : ℝ) (hu : 0 < u) (hd : 0 < dist s t) : (μ {ω : Ω | |X s ω - X t ω| ≥ u}).toReal ≤ 2 * Real.exp (-u ^ 2 / (2 * σ ^ 2 * dist s t ^ 2))

Two-sided tail bound for sub-Gaussian increments.

First moment bound for sub-Gaussian increments

theorem LeanPool.gaussian_tail_integral {τ : ℝ} (hτ : 0 < τ) : ∫ (r : ℝ) in Set.Ioi 0, 2 * Real.exp (-r ^ 2 / (2 * τ ^ 2)) = τ * √(2 * Real.pi)

The Gaussian integral ∫₀^∞ 2·exp(-r²/(2τ²)) dr = τ·√(2π) for τ > 0.

theorem LeanPool.ae_eq_zero_of_mgf_le_one {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} (hY_mgf : ∀ (l : ℝ), ∫ (x : Ω), (fun (ω : Ω) => Real.exp (l * Y ω)) x ∂μ ≤ 1) (hY_int_exp_pos : ∀ (l : ℝ), 0 < l → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ) (hY_int_exp_neg : ∀ l < 0, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ) : Y =ᵐ[μ] fun (x : Ω) => 0

A random variable with MGF bounded by 1 for all λ is zero a.s.

Key lemma for the degenerate case of sub-Gaussian processes with zero variance proxy.

theorem LeanPool.integral_abs_eq_zero_of_ae_eq_zero {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} (hY_ae : Y =ᵐ[μ] fun (x : Ω) => 0) : ∫ (ω : Ω), |Y ω| ∂μ = 0

If Y = 0 a.e., then ∫|Y| = 0.

theorem LeanPool.integral_abs_subGaussian_zero {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} (hY_mgf_le_one : ∀ (l : ℝ), ∫ (x : Ω), (fun (ω : Ω) => Real.exp (l * Y ω)) x ∂μ ≤ 1) (hY_int_exp : ∀ (l : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * Y ω)) μ) : ∫ (ω : Ω), |Y ω| ∂μ = 0

Integral of absolute value of sub-Gaussian increment with variance proxy 0.

theorem LeanPool.subGaussian_first_moment_bound {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : A → Ω → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX : IsSubGaussianProcess μ X σ) (s t : A) : ∫ (ω : Ω), |X s ω - X t ω| ∂μ ≤ √(2 * Real.pi) * σ * dist s t

Sub-Gaussian first moment bound: E[|X_s - X_t|] ≤ √(2π) · σ · d(s,t).

Proof sketch (via layer-cake formula):

1. From subGaussian_tail_bound: P(|X_s - X_t| ≥ r) ≤ 2·exp(-r²/(2σ²d(s,t)²))
2. By layer-cake: E[|X_s - X_t|] = ∫₀^∞ P(|X_s - X_t| ≥ r) dr
3. Computing: ∫₀^∞ 2·exp(-r²/(2τ²)) dr = τ·√(2π) where τ = σ·d(s,t)
4. Therefore: E[|X_s - X_t|] ≤ √(2π) · σ · d(s,t)

Maximum over finite sets

For Dudley's chaining argument, we need bounds on the expected maximum of a sub-Gaussian process over finite sets.

theorem LeanPool.iSup_subtype_eq_sup' {A : Type v} {T : Finset A} (hT : T.Nonempty) (f : A → ℝ) : ⨆ (t : ↥T), f ↑t = T.sup' hT f

For a finite nonempty set, the subtype iSup equals sup'. This avoids the issue with biSup and sSup ∅ for ℝ.

theorem LeanPool.biSup_eq_sup'_of_finset {A : Type v} {T : Finset A} (hT : T.Nonempty) (f : A → ℝ) (h_nonneg : ∃ t ∈ T, 0 ≤ f t) : ⨆ t ∈ T, f t = T.sup' hT f

For a finite set with at least one non-negative value, biSup equals sup'. The hypothesis is needed because sSup ∅ = 0 for ℝ.

theorem LeanPool.subGaussian_finite_max_bound {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : A → Ω → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX : IsSubGaussianProcess μ X σ) (T : Finset A) (hT : T.Nonempty) (hT_card : 2 ≤ T.card) (t₀ : A) (ht₀ : t₀ ∈ T) (hcenter : ∀ (ω : Ω), X t₀ ω = 0) (hdiam_pos : 0 < Metric.diam ↑T) : ∫ (x : Ω), (fun (ω : Ω) => ⨆ t ∈ T, X t ω) x ∂μ ≤ σ * Metric.diam ↑T * √(2 * Real.log ↑T.card)

E[max_{t ∈ T} X_t] ≤ σ · diam(T) · √(2 log |T|) for centered sub-Gaussian processes.

theorem LeanPool.subGaussian_finite_max_bound' {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : A → Ω → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX : IsSubGaussianProcess μ X σ) (T : Finset A) (hT : 2 ≤ T.card) (D : ℝ) (hD : 0 ≤ D) (hdiam : Metric.diam ↑T ≤ D) : ∃ C > 0, C ≤ √2 ∧ ∀ t₀ ∈ T, ∫ (x : Ω), (fun (ω : Ω) => ⨆ t ∈ T, X t ω - X t₀ ω) x ∂μ ≤ C * σ * D * √(Real.log ↑T.card)

Variant of subGaussian_finite_max_bound with diameter bound D and no fixed basepoint.

theorem LeanPool.subGaussian_process_centered {Ω : Type u_1} [MeasurableSpace Ω] {A : Type u_2} [PseudoMetricSpace A] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : A → Ω → ℝ} {σ : ℝ} (hX : IsSubGaussianProcess μ X σ) (s t : A) : ∫ (ω : Ω), X s ω - X t ω ∂μ = 0

Every increment of a sub-Gaussian process has zero mean.