theorem exp_mul_one_add_le_exp_double (u : ℝ) : Real.exp u * (1 + u) ≤ Real.exp (2 * u)

exp(u) * (1 + u) ≤ exp(2 * u) for all u : ℝ. This is the final analytical step in the proof of Lemma 1.5: from exp(2σ²s²) · (1 + 2σ²s²) to exp(4σ²s²).

theorem integrable_pow_of_exp_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_exp_int : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) (k : ℕ) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ k) μ

If exp(s * X) is integrable for all s, then X^k is integrable for all k. Proof sketch: |x|^k ≤ k! · exp(|x|), and exp(|X|) is integrable since both exp(X) and exp(-X) are integrable by hypothesis. The bound |x|^k / k! ≤ exp(|x|) follows from Real.sum_le_exp_of_nonneg (each term of the Taylor series is nonneg for x ≥ 0, so each individual term is bounded by the full sum).

theorem mgf_taylor_interchange {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_exp_int : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) (s : ℝ) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ = ∑' (k : ℕ), s ^ k / ↑k.factorial * ∫ (ω : Ω), X ω ^ k ∂μ

Taylor expansion of MGF with dominated convergence interchange.

If exp(sX) is integrable for all s, then: E[exp(sX)] = Σ_k s^k/k! · E[X^k]

This uses:

• Real.exp x = Σ_k x^k/k! (NormedSpace.exp_eq_tsum_div via Real.exp_eq_exp_ℝ)
• MeasureTheory.integral_tsum to interchange ∫ and Σ
• integrable_pow_of_exp_integrable to verify integrability of each term
• The domination bound |Σ_{k≤N} (sX)^k/k!| ≤ exp(|sX|) for the DCT condition

theorem factorial_eq_double_factorial_mul (m : ℕ) (hm : 1 ≤ m) : (2 * m).factorial = (2 * m).doubleFactorial * (2 * m - 1).doubleFactorial

(2m)! = (2m)‼ * (2m-1)‼ for m ≥ 1. Proved by induction on m.

theorem factorial_two_mul_add_one_eq (m : ℕ) (hm : 1 ≤ m) : (2 * m + 1).factorial = (2 * m + 1) * (2 * m - 1).doubleFactorial * (2 ^ m * m.factorial)

(2m+1)! = (2m+1) * (2m-1)‼ * (2^m * m!) for m ≥ 1.

theorem gamma_factorial_ratio_le (n : ℕ) : 2 ≤ n → ↑n * Real.Gamma (↑n / 2) * ↑(n / 2).factorial ≤ ↑n.factorial

Gamma-factorial ratio bound (core mathematical fact). For n ≥ 2: n · Γ(n/2) · (n/2)! ≤ n!, where n/2 uses natural-number division.

Proof: • Even n = 2m (m ≥ 1): Γ(m) = (m-1)! by Real.Gamma_nat_eq_factorial, so LHS = 2m·(m-1)!·m! = 2·(m!)². Need 2·(m!)² ≤ (2m)!, i.e. C(2m,m) ≥ 2. This follows from Nat.two_pow_mul_factorial_le_factorial_two_mul. • Odd n = 2m+1 (m ≥ 1): Γ(m+½) = (2m-1)‼·√π/2^m by Real.Gamma_nat_add_half, so LHS = (2m+1)·(2m-1)‼·√π·m!/2^m = (2m+1)‼·√π·m!/2^m. RHS = (2m+1)! = (2m+1)‼·(2m)‼ = (2m+1)‼·2^m·m!. Need √π/2^m ≤ 2^m, i.e. √π ≤ 4^m. True since π < 4 (Real.pi_lt_four).

theorem exp_sub_one_le_mul_exp (u : ℝ) : Real.exp u - 1 ≤ u * Real.exp u

exp(u) - 1 ≤ u · exp(u) for all u : ℝ. Equivalent to 1 - u ≤ exp(-u), which follows from add_one_le_exp applied to -u.

theorem two_mul_exp_sub_one_le (u : ℝ) (_hu : 0 ≤ u) : 2 * (Real.exp u - 1) ≤ Real.exp u * (1 + u) - 1

2 · (exp(u) - 1) ≤ exp(u) · (1 + u) - 1 for u ≥ 0. Proof: exp(u)·(1+u) - 1 - 2·(exp(u)-1) = (u-1)·exp(u) + 1. For u ≥ 1: (u-1)·exp(u) ≥ 0 so result ≥ 1 ≥ 0. For 0 ≤ u < 1: (1-u)·exp(u) ≤ 1 by exp_sub_one_le_mul_exp.

theorem rpow_half_eq_sqrt_pow (x : ℝ) (hx : 0 < x) (n : ℕ) : x ^ (↑n / 2) = √x ^ n

x^((n:ℝ)/2) = (√x)^n for x > 0 (converts rpow to npow via sqrt).

theorem mul_sqrt_pow_eq (σsq s : ℝ) (_hσ : 0 < σsq) (hs : 0 < s) (n : ℕ) : s ^ n * √(2 * σsq) ^ n = √(2 * σsq * s ^ 2) ^ n

s^n * (√(2σsq))^n = (√(2σsq·s²))^n for s > 0, σsq > 0.

theorem series_term_bound_via_gamma (σsq s : ℝ) (hσ : 0 < σsq) (hs : 0 < s) (moments : ℕ → ℝ) (hmom : ∀ (k : ℕ), 1 ≤ k → |moments k| ≤ (2 * σsq) ^ (↑k / 2) * ↑k * Real.Gamma (↑k / 2)) (n : ℕ) (hn : 2 ≤ n) : s ^ n / ↑n.factorial * |moments n| ≤ √(2 * σsq * s ^ 2) ^ n / ↑(n / 2).factorial

Series term bound via gamma-factorial ratio (corrected). For n ≥ 2 with the moment bound, each term satisfies: s^n / n! · |moments(n)| ≤ (√u)^n / (n/2)! where u = 2σ²s² and (n/2) is natural-number division. Using (√u)^n correctly handles both even n (where (√u)^(2m) = u^m) and odd n (where (√u)^(2m+1) = u^m·√u).

theorem gamma_factorial_series_bound (σsq : ℝ) (hσ : 0 < σsq) (s : ℝ) (hs : 0 < s) (moments : ℕ → ℝ) (hmom_bound : ∀ (k : ℕ), 1 ≤ k → |moments k| ≤ (2 * σsq) ^ (↑k / 2) * ↑k * Real.Gamma (↑k / 2)) : ∑' (k : ℕ), s ^ (k + 2) / ↑(k + 2).factorial * |moments (k + 2)| ≤ Real.exp (2 * σsq * s ^ 2) * (1 + 2 * σsq * s ^ 2) - 1

Gamma-factorial series bound. For the series from Lemma 1.4 moment bounds in the MGF Taylor expansion: ∑ s^{k+2}/(k+2)! · |moments(k+2)| ≤ exp(u)·(1+u) - 1, where u = 2σ²s².

Proof strategy: bound each term using hmom_bound + gamma_factorial_ratio_le, showing each term ≤ u^m/m! where m = (k+2)/2. The map k ↦ (k+2)/2 hits each m ≥ 1 exactly twice, so the series ≤ 2·(exp(u) - 1) ≤ exp(u)·(1+u) - 1. Reference: Rigollet, Lemma 1.5; Boucheron–Lugosi–Massart §2.3.

theorem moment_bound_series_le (σsq : ℝ) (hσ : 0 < σsq) (s : ℝ) (hs : 0 < s) (moments : ℕ → ℝ) (hmom_bound : ∀ (k : ℕ), 1 ≤ k → |moments k| ≤ (2 * σsq) ^ (↑k / 2) * ↑k * Real.Gamma (↑k / 2)) (_hm0 : moments 0 = 1) (_hm1 : moments 1 = 0) : 1 + ∑' (k : ℕ), s ^ (k + 2) / ↑(k + 2).factorial * |moments (k + 2)| ≤ Real.exp (2 * σsq * s ^ 2) * (1 + 2 * σsq * s ^ 2)

theorem lemma_1_5_mgf_bound_from_tails {Ω : Type u_1} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (hP : MeasureTheory.IsProbabilityMeasure μ) {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX_int : MeasureTheory.Integrable X μ) (hX_mean : ∫ (ω : Ω), X ω ∂μ = 0) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σsq)))) (hX_exp_int : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) (s : ℝ) (hs : 0 < s) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (4 * σsq * s ^ 2)

Lemma 1.5 (Rigollet): Tail bound implies MGF bound.

If a random variable X satisfies the sub-Gaussian tail bound P[|X| > t] ≤ 2 exp(-t²/(2σ²)) for all t > 0 and has mean zero (E[X] = 0), then for any s > 0: E[exp(sX)] ≤ exp(4σ² s²).

Proof structure (4 steps, all fully proved): Step A: All moments E[|X|^k] are finite (integrable_pow_of_exp_integrable) ✓ Step B: Taylor+DCT interchange (mgf_taylor_interchange) ✓ Step C: Series bound via Lemma 1.4 (moment_bound_series_le) ✓ Step D: exp(u)·(1+u) ≤ exp(2u) (exp_mul_one_add_le_exp_double) ✓

theorem lemma_1_5_implies_subgaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX_int : MeasureTheory.Integrable X μ) (hX_mean : ∫ (ω : Ω), X ω ∂μ = 0) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σsq)))) (hX_exp_int : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) : IsSubGaussian X (8 * σsq) μ

Corollary: The tail bound condition (1.3) implies sub-Gaussianity with variance proxy 8σ² in the sense of Definition 1.2.

Note: The book's Lemma 1.5 gives exp(4σ²s²) which equals exp(8σ² · s²/2), so the variance proxy in the IsSubGaussian sense is 8σ².

theorem exp_integrable_of_subgaussian_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σsq)))) (s : ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ

If a random variable X satisfies the sub-Gaussian tail bound P[|X| > t] ≤ 2 exp(-t²/(2σ²)) for all t > 0, then exp(s * X) is integrable for all s ∈ ℝ.

This follows because E[exp(|s|·|X|)] is finite: using the layer cake formula, E[exp(c·|X|)] = 1 + c·∫₀^∞ exp(ct)·P[|X| > t] dt ≤ 1 + 2c·∫₀^∞ exp(ct - t²/(2σ²)) dt < ∞ (the latter is a Gaussian integral after completing the square).

The book (Rigollet, Section 1.2) does not provide an explicit proof of this step, invoking it implicitly via "the dominated convergence theorem."

theorem integrable_of_exp_integrable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_exp_int : ∀ (s : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X ω)) μ) : MeasureTheory.Integrable X μ

Integrability of X itself follows from integrability of exp(X): since |x| ≤ exp(|x|) ≤ exp(x) + exp(-x), if exp(X) and exp(-X) are integrable then X is integrable.

Bundled Lemma 1.5

We provide a single bundled theorem combining the MGF bound (for all s > 0) and the sub-Gaussianity conclusion.

theorem SubGaussianTailBound.tail_implies_mgf_and_subgaussian {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hX_mean : ∫ (ω : Ω), X ω ∂μ = 0) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σsq)))) : (∀ (s : ℝ), 0 < s → ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (4 * σsq * s ^ 2)) ∧ IsSubGaussian X (8 * σsq) μ

Lemma 1.5 (bundled). Under the sub-Gaussian tail bound hypothesis, a centered random variable satisfies both: (1) E[exp(sX)] ≤ exp(4σ²s²) for all s > 0, and (2) X is sub-Gaussian with variance proxy 8σ².

Note: The book (Rigollet, Section 1.2) assumes only the tail bound (1.3), measurability, and mean zero. MGF integrability is derived internally from the tail bound (see exp_integrable_of_subgaussian_tail).