Auxiliary lemmas

theorem tsum_geometric_tail_le {r : ℝ} (hr0 : 0 ≤ r) (hr : r ≤ 1 / 2) : ∑' (k : ℕ), r ^ (k + 2) ≤ 2 * r ^ 2

Tail of geometric series: ∑_{k≥2} r^k ≤ 2r² when 0 ≤ r ≤ 1/2.

Part 1: Moment bound from exponential tail decay (Bochner integral formulation)

The proof uses the layer cake formula as a hypothesis: E[|X|^k] ≤ k · 2 · ∫₀^∞ t^{k-1} · exp(-2t/λ) dt

Then evaluates the integral using Γ function and bounds the result.

theorem lemma_1_10_moment_bound_exponential_tail (l : ℝ) (hl : 0 < l) (k : ℕ) (hk : 1 ≤ k) (moment_k : ℝ) (hlayer : moment_k ≤ ↑k * (2 * ∫ (t : ℝ) in Set.Ioi 0, t ^ (↑k - 1) * Real.exp (-(2 / l * t)))) : moment_k ≤ l ^ k * ↑k.factorial

Part 1b: Moment bound (lintegral formulation)

The full measure-theoretic statement using ∫⁻ and the layer cake formula.

theorem lemma_1_10_moment_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {lambda : ℝ} (hlam : 0 < lambda) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-2 * t / lambda))) (k : ℕ) (hk : 1 ≤ k) : ∫⁻ (ω : Ω), ENNReal.ofReal (|X ω| ^ ↑k) ∂μ ≤ ENNReal.ofReal (lambda ^ k * ↑k.factorial)

Part 2: Moment root bound

theorem lemma_1_10_moment_root_bound (l : ℝ) (hl : 0 < l) (k : ℕ) (hk : 1 ≤ k) (E : ℝ) (hE0 : 0 ≤ E) (hE : E ≤ l ^ k * ↑k.factorial) : E ^ (↑k)⁻¹ ≤ 2 * l * ↑k

Part 3: MGF bound

theorem lemma_1_10_mgf_bound (s l : ℝ) (hl : 0 < l) (M : ℝ) (hs : |s| ≤ 1 / (2 * l)) (hM : M ≤ 1 + ∑' (k : ℕ), (|s| * l) ^ (k + 2)) : M ≤ Real.exp (2 * s ^ 2 * l ^ 2)

theorem lemma_1_10_exp_bound (s l : ℝ) : 1 + 2 * s ^ 2 * l ^ 2 ≤ Real.exp (2 * s ^ 2 * l ^ 2)

Helper: 1 + x ≤ exp(x) applied to 2s²λ².

Part 3b: MGF bound (measure-theoretic statement)

This states Part 3 as an actual integral inequality over the probability space, using the centered hypothesis E[X] = 0 (which eliminates the k=1 Taylor term). The proof connects the Taylor expansion of the MGF to the moment bounds via dominated convergence (using integral_tsum for the interchange of sum and integral).

theorem mgf_taylor_dct_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {lambda s : ℝ} (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (lambda_pos : 0 < lambda) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-2 * t / lambda))) (hX_centered : ∫ (ω : Ω), X ω ∂μ = 0) (s_pos : 0 < s) (s_le : s ≤ 1 / (2 * lambda)) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ 1 + ∑' (k : ℕ), (s * lambda) ^ (k + 2)

For a centered random variable X with sub-exponential moments (from the tail bound), and for s > 0 with s ≤ 1/(2λ), the MGF integral satisfies: E[exp(sX)] ≤ 1 + Σ_{k≥2} (sλ)^k

The proof: (1) Taylor-expands exp(sX) = 1 + sX + Σ_{k≥2} (sX)^k/k!, (2) uses integral_tsum (dominated convergence) to interchange sum and integral, (3) uses the centered hypothesis E[X] = 0 to eliminate the k=1 term, and (4) bounds E[|X|^k]/k! ≤ λ^k from the moment bound E[|X|^k] ≤ λ^k k!.

theorem mgf_bound_pos {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {lambda : ℝ} (hlam : 0 < lambda) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-2 * t / lambda))) (hX_centered : ∫ (ω : Ω), X ω ∂μ = 0) (s : ℝ) (hs_pos : 0 < s) (s_le : s ≤ 1 / (2 * lambda)) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (2 * s ^ 2 * lambda ^ 2)

Helper: MGF bound for s > 0, proved using the Taylor-DCT bound and the geometric tail bound.

theorem lemma_1_10_mgf_bound_integral {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {lambda : ℝ} (hlam : 0 < lambda) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-2 * t / lambda))) (hX_centered : ∫ (ω : Ω), X ω ∂μ = 0) (s : ℝ) (hs : |s| ≤ 1 / (2 * lambda)) : ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (2 * s ^ 2 * lambda ^ 2)

Lemma 1.10 Part (iii) (measure-theoretic MGF bound). For a centered random variable X with sub-exponential tail P(|X| > t) ≤ 2exp(-2t/λ), we have E[exp(sX)] ≤ exp(2s²λ²) for all |s| ≤ 1/(2λ).

Proof outline. Taylor-expand exp(sX) = 1 + sX + Σ_{k≥2} (sX)^k/k!. By dominated convergence (proved via mgf_taylor_dct_bound), the integral commutes with the sum. The k=1 term vanishes since E[X] = 0. For k ≥ 2, bound E[|X|^k]/k! ≤ λ^k, giving E[exp(sX)] ≤ 1 + Σ_{k≥2}(sλ)^k ≤ 1 + 2(sλ)² ≤ exp(2s²λ²). The case s < 0 is handled by symmetry (replace X by -X); s = 0 is trivial.

Unified Lemma 1.10

Combines all three parts into a single theorem with proper probabilistic hypotheses, including the centered condition E[X] = 0.

theorem lemma_1_10 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {lambda : ℝ} (hlam : 0 < lambda) (hX_meas : MeasureTheory.AEStronglyMeasurable X μ) (hX_tail : ∀ (t : ℝ), 0 < t → μ {ω : Ω | |X ω| > t} ≤ ENNReal.ofReal (2 * Real.exp (-2 * t / lambda))) (hX_centered : ∫ (ω : Ω), X ω ∂μ = 0) : (∀ (k : ℕ), 1 ≤ k → ∫⁻ (ω : Ω), ENNReal.ofReal (|X ω| ^ ↑k) ∂μ ≤ ENNReal.ofReal (lambda ^ k * ↑k.factorial)) ∧ (∀ (k : ℕ), 1 ≤ k → ∀ (E_val : ℝ), 0 ≤ E_val → E_val ≤ lambda ^ k * ↑k.factorial → E_val ^ (↑k)⁻¹ ≤ 2 * lambda * ↑k) ∧ ∀ (s : ℝ), |s| ≤ 1 / (2 * lambda) → ∫ (ω : Ω), Real.exp (s * X ω) ∂μ ≤ Real.exp (2 * s ^ 2 * lambda ^ 2)

Lemma 1.10 (unified). Let X be a centered random variable with sub-Gaussian tail P(|X| > t) ≤ 2exp(-2t/λ). Then:

1. E[|X|^k] ≤ λ^k · k!
2. (E[|X|^k])^{1/k} ≤ 2λk
3. E[exp(sX)] ≤ exp(2s²λ²) for |s| ≤ 1/(2λ)