Lemma 1.12: Square of sub-Gaussian is sub-exponential

Let X subG(σ²). Then Z = X² - E[X²] is sub-exponential: Z subE(16σ²).

The proof in the book uses:

1. Power series expansion of E[exp(sZ)]
2. Jensen's inequality (twice) to bound centered moments
3. Lemma 1.4 for moment bounds E[X^{2k}] ≤ (2σ²)^k · k!
4. Geometric series summation for |8sσ²| < 1
5. The inequality 1 + x ≤ exp(x)

This yields: E[exp(sZ)] ≤ 1 + 128s²σ⁴ ≤ exp(s²(16σ²)²/2) for |s| ≤ 1/(16σ²).

Auxiliary lemmas

theorem sq_le_exp_add_exp_neg (x : ℝ) : x ^ 2 ≤ Real.exp x + Real.exp (-x)

For all x ∈ ℝ, x² ≤ exp(x) + exp(-x).

Proof: By the Taylor expansion exp(y) ≥ 1 + y + y²/2 + y³/6 for y ≥ 0 (from Real.sum_le_exp_of_nonneg), applied to y = |x|, we get exp(|x|) ≥ 1 + |x| + x²/2 + |x|³/6 ≥ x² (using the algebraic fact |x|³ - 3|x|² + 6|x| + 6 ≥ 0 for |x| ≥ 0). Since exp(-|x|) > 0 and exp(x) + exp(-x) = exp(|x|) + exp(-|x|), we conclude x² ≤ exp(|x|) ≤ exp(x) + exp(-x).

theorem sq_integrable_of_exp_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX_int : MeasureTheory.Integrable X μ) (hX_exp : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ

If X has integrable exponential moments for all s, then X² is integrable. This uses the pointwise bound x² ≤ exp(x) + exp(-x).

Helper lemmas for the analytical MGF bound

theorem exp_le_one_add_abs_series (x : ℝ) : Real.exp x ≤ 1 + x + ∑' (k : ℕ), |x| ^ (k + 2) / ↑(k + 2).factorial

exp(x) ≤ 1 + x + Σ_{k≥0} |x|^(k+2)/(k+2)! for all x : ℝ. This follows because exp(x) = Σ_{k≥0} x^k/k! = 1 + x + Σ_{k≥2} x^k/k! and |x^k/k!| ≤ |x|^k/k! for all k.

theorem dct_interchange_exp_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Z : Ω → ℝ} (hZ_int : MeasureTheory.Integrable Z μ) (hZ_mean : ∫ (ω : Ω), Z ω ∂μ = 0) (hZ_exp : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (Z ω)) μ) (hZ_abs_exp : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp |Z ω|) μ) : ∫ (ω : Ω), Real.exp (Z ω) ∂μ ≤ 1 + ∑' (k : ℕ), ∫ (ω : Ω), |Z ω| ^ (k + 2) / ↑(k + 2).factorial ∂μ

Helper: The DCT interchange for the tail of the exp series applied to a centered random variable. The textbook cites this step by reference ("by the Dominated Convergence Theorem"). The interchange is fully proved using integral_tsum.

theorem subgaussian_even_moment_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX_int : MeasureTheory.Integrable X μ) (hX_mean : ∫ (ω : Ω), X ω ∂μ = 0) (hX_exp : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) (hX_mgf : ∀ (s : ℝ), ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (σsq * s ^ 2 / 2)) (k : ℕ) (hk : 1 ≤ k) : ∫ (ω : Ω), X ω ^ (2 * k) ∂μ ≤ 2 * (2 * σsq) ^ k * ↑k.factorial

Sub-Gaussian even moment bound (Rigollet, line 722, via Lemma 1.4). For X ~ subG(σ²): E[X^{2k}] ≤ 2 · (2σ²)^k · k!. Derived from the sub-Gaussian tail bound and the layer cake formula. Referenced in the textbook proof of Lemma 1.12.

theorem exp_abs_sq_centered_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX : IsSubGaussian X σsq μ) (s : ℝ) (hs : |s| ≤ 1 / (16 * σsq)) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp |s * (X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ)|) μ

Integrability of exp(|s*(X²-c)|) when X is sub-Gaussian and |s| is small.

Similar to exp_sq_centered_integrable, this is a technical condition for DCT. Since |s*(X²-c)| ≤ |s|*X² + |s|*c, the integrability reduces to that of exp(|s|*X²), which follows from the same moment bound argument. Cited by reference in the textbook (Rigollet, Lemma 1.12).

theorem exp_sq_centered_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX : IsSubGaussian X σsq μ) (s : ℝ) (hs : |s| ≤ 1 / (16 * σsq)) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * (X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ))) μ

Integrability of exp(s*(X²-c)) when X is sub-Gaussian and |s| is small.

This follows from exp_abs_sq_centered_integrable since exp(x) ≤ exp(|x|) for all x ∈ ℝ.

theorem dct_mgf_expansion {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX : IsSubGaussian X σsq μ) (s : ℝ) (hs : |s| ≤ 1 / (16 * σsq)) : ∫ (ω : Ω), Real.exp (s * (X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ)) ∂μ ≤ 1 + ∑' (k : ℕ), (|s| ^ (k + 2) * ∫ (ω : Ω), |X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ| ^ (k + 2) ∂μ) / ↑(k + 2).factorial

DCT MGF expansion (Rigollet, line 714).

For X ~ subG(σ²) and Z = X² - E[X²], the MGF can be bounded by its Taylor series with absolute values on the moments:

E[exp(sZ)] ≤ 1 + Σ_{k≥2} |s|^k · E[|Z|^k] / k!

The proof uses:

1. Taylor expansion: exp(x) = 1 + x + Σ_{k≥2} x^k/k!
2. E[Z] = 0, so the k=1 term vanishes
3. Dominated convergence theorem to interchange E and Σ
4. |E[Z^k]| ≤ E[|Z|^k] (Jensen on absolute value)

Reference: Rigollet, High-Dimensional Statistics, Lemma 1.12, line 714. The dominated convergence interchange is cited by reference.

theorem centering_moment_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX_int : MeasureTheory.Integrable X μ) (hX_sq_int : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ 2) μ) (k : ℕ) (hk : 1 ≤ k) : ∫ (ω : Ω), |X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ| ^ k ∂μ ≤ 2 ^ k * ∫ (ω : Ω), X ω ^ (2 * k) ∂μ

Jensen/centering bound (Rigollet, lines 718–720). For Z = X² - E[X²]: E[|Z|^k] ≤ 2^k · E[X^{2k}]. Uses |a-b|^k ≤ 2^{k-1}(|a|^k + |b|^k) and Jensen's inequality (E[X²])^k ≤ E[X^{2k}]. Referenced but not explicitly proved in the textbook.

theorem per_term_mgf_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX : IsSubGaussian X σsq μ) (s : ℝ) (k : ℕ) : (|s| ^ (k + 2) * ∫ (ω : Ω), |X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ| ^ (k + 2) ∂μ) / ↑(k + 2).factorial ≤ (8 * |s| * σsq) ^ (k + 2)

Per-term MGF bound (Rigollet, lines 718–722).

For X ~ subG(σ²) and Z = X² - E[X²], for each k ≥ 2: E[|Z|^k] ≤ (2k)! · σ^{2k} · 2^k

More precisely, the terms in the series satisfy: |s|^k · E[|Z|^k] / k! ≤ (8|s|σ²)^k

The proof combines:

1. Jensen/centering (line 718–720): |a-b|^k ≤ 2^{k-1}(|a|^k + |b|^k) and (E[X²])^k ≤ E[X^{2k}] (Jensen for convex x^k, k ≥ 2) giving E[|Z|^k] ≤ 2^k · E[X^{2k}]
2. Lemma 1.4 (line 722): E[X^{2k}] ≤ 2(2σ²)^k · k! → E[|Z|^k] ≤ 2^{k+1} · (2σ²)^k · k! → |s|^k · E[|Z|^k] / k! ≤ 2 · (4|s|σ²)^k ≤ (8|s|σ²)^k

Reference: Rigollet, High-Dimensional Statistics, Lemma 1.12, lines 718–722. The centering bound and Lemma 1.4 moment bound are now fully proved.

theorem geometric_series_bound (s σsq : ℝ) (hσ : 0 < σsq) (hs : |s| ≤ 1 / (16 * σsq)) : ∑' (k : ℕ), (8 * |s| * σsq) ^ (k + 2) ≤ 128 * s ^ 2 * σsq ^ 2

Geometric series bound (Rigollet, lines 724–726). For |s| ≤ 1/(16σ²), the geometric series Σ_{k≥2} (8|s|σ²)^k ≤ 128s²σ⁴. This uses the geometric series formula and the constraint 8|s|σ² ≤ 1/2.

Key theorem and main result

theorem analytical_mgf_bound_for_centered_square {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX : IsSubGaussian X σsq μ) (s : ℝ) (hs : |s| ≤ 1 / (16 * σsq)) : ∫ (ω : Ω), Real.exp (s * (X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ)) ∂μ ≤ 1 + 128 * s ^ 2 * σsq ^ 2

Analytical MGF bound from Lemma 1.12 proof.

For X ~ subG(σ²) and Z = X² - E[X²], for |s| ≤ 1/(16σ²): E[exp(sZ)] ≤ 1 + 128s²σ⁴

This combines:

• dct_mgf_expansion: E[exp(sZ)] ≤ 1 + Σ_{k≥2} |s|^k E[|Z|^k]/k! (DCT interchange)
• per_term_mgf_bound: |s|^k E[|Z|^k]/k! ≤ (8|s|σ²)^k (Jensen + Lemma 1.4)
• geometric_series_bound: Σ_{k≥2} (8|s|σ²)^k ≤ 128s²σ⁴ (geometric series)

Reference: Rigollet, High-Dimensional Statistics, Lemma 1.12, lines 714–726.

theorem lemma_1_12_square_subgaussian_is_subexponential {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX : IsSubGaussian X σsq μ) : IsSubExponential (fun (ω : Ω) => X ω ^ 2 - ∫ (ω' : Ω), X ω' ^ 2 ∂μ) (16 * σsq)

Lemma 1.12 (Square of sub-Gaussian is sub-exponential).

Let X subG(σ²). Then the random variable Z = X² - E[X²] is sub-exponential with parameter λ = 16σ², i.e., Z subE(16σ²).

The proof establishes:

• Positivity: 16σ² > 0 (from σ² > 0)
• Integrability: Z = X² - E[X²] is integrable (derived from sub-Gaussian via the bound x² ≤ exp(x) + exp(-x))
• Mean zero: E[Z] = E[X² - E[X²]] = 0 (by linearity of expectation)
• MGF bound: E[exp(sZ)] ≤ exp(s²(16σ²)²/2) for |s| ≤ 1/(16σ²) This follows from the analytical bound E[exp(sZ)] ≤ 1 + 128s²σ⁴ (from analytical_mgf_bound_for_centered_square) combined with the standard inequality 1 + x ≤ exp(x).