Finite sub-Gaussian maximal inequality #

Finite maximal inequalities for weighted finite probability spaces. The module exposes the probability-facing wrapper around the finite MGF-to-supremum primitive used by the Dudley chaining layer.

source

theorem FormalSLT.Probability.SubGaussianFiniteMax.exp_finiteExpectation_le_of_jensen {Ω : Type u_1} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ (ω : Ω), 0 ≤ w ω) (hsum : ∑ ω : Ω, w ω = 1) (Z : Ω → ℝ) (lam : ℝ) :

Real.exp (lam * Covering.FiniteSubGaussianChaining.finiteExpectation w Z) ≤ Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Real.exp (lam * Z ω)

Finite Jensen for the exponential function in weighted-expectation form.

source

theorem FormalSLT.Probability.SubGaussianFiniteMax.subgaussian_finite_max {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] [Nonempty ι] (w : Ω → ℝ) (hw : ∀ (ω : Ω), 0 ≤ w ω) (hsum : ∑ ω : Ω, w ω = 1) (Y : ι → Ω → ℝ) (sigma : ℝ) (hsigma : 0 < sigma) (hmean : ∀ (i : ι), (Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Y i ω) = 0) (hmgf : ∀ (i : ι) (lam : ℝ), 0 ≤ lam → (Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Real.exp (lam * Y i ω)) ≤ Real.exp (lam ^ 2 * sigma ^ 2 / 2)) :

(Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Covering.FiniteSubGaussianChaining.finiteSup fun (i : ι) => Y i ω) ≤ sigma * √(2 * Real.log ↑(Fintype.card ι))

Finite maximal inequality for a one-sided sub-Gaussian family over a finite weighted probability space.

source

theorem FormalSLT.Probability.SubGaussianFiniteMax.subgaussian_finite_max_abs {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Fintype ι] [Nonempty ι] (w : Ω → ℝ) (hw : ∀ (ω : Ω), 0 ≤ w ω) (hsum : ∑ ω : Ω, w ω = 1) (Y : ι → Ω → ℝ) (sigma : ℝ) (hsigma : 0 < sigma) (hmean : ∀ (i : ι), (Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Y i ω) = 0) (hmgf_pos : ∀ (i : ι) (lam : ℝ), 0 ≤ lam → (Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Real.exp (lam * Y i ω)) ≤ Real.exp (lam ^ 2 * sigma ^ 2 / 2)) (hmgf_neg : ∀ (i : ι) (lam : ℝ), 0 ≤ lam → (Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Real.exp (lam * -Y i ω)) ≤ Real.exp (lam ^ 2 * sigma ^ 2 / 2)) :

(Covering.FiniteSubGaussianChaining.finiteExpectation w fun (ω : Ω) => Covering.FiniteSubGaussianChaining.finiteSup fun (i : ι) => |Y i ω|) ≤ sigma * √(2 * Real.log (2 * ↑(Fintype.card ι)))

Two-sided finite maximal inequality, proved by applying subgaussian_finite_max to the signed family indexed by Bool × ι.