theorem SubGaussianMoments.moment_bound {Ω : 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)))) (k : ℕ) (hk : 1 ≤ k) : ∫⁻ (ω : Ω), ENNReal.ofReal (|X ω| ^ ↑k) ∂μ ≤ ENNReal.ofReal ((2 * σsq) ^ (↑k / 2) * ↑k * Real.Gamma (↑k / 2))

Lemma 1.4 (Part 1): If a random variable X satisfies the sub-Gaussian tail bound P[|X| > t] ≤ 2 exp(-t²/(2σ²)), then its k-th absolute moment satisfies E[|X|^k] ≤ (2σ²)^{k/2} · k · Γ(k/2).

Stated using the Lebesgue integral (lintegral) for cleanest formulation with the layer cake formula.

theorem SubGaussianMoments.gamma_half_le_rpow (k : ℕ) (hk : 2 ≤ k) : Real.Gamma (↑k / 2) ≤ (↑k / 2) ^ (↑k / 2)

Stirling-type bound: Γ(k/2) ≤ (k/2)^{k/2} for k ≥ 2. Referenced but not proved in the textbook (line 554).

theorem SubGaussianMoments.log_div_le_inv_exp (x : ℝ) (hx : 0 < x) : Real.log x / x ≤ 1 / Real.exp 1

For any x > 0, log(x)/x ≤ 1/e. This follows from log(x) ≤ x/e, which is a consequence of log(t) ≤ t - 1 applied to t = x/e.

theorem SubGaussianMoments.rpow_inv_le_exp_inv_exp (k : ℕ) (hk : 2 ≤ k) : ↑k ^ (↑k)⁻¹ ≤ Real.exp (1 / Real.exp 1)

k^{1/k} ≤ e^{1/e} for k ≥ 2. Referenced but not proved in the textbook (line 554).

theorem SubGaussianMoments.kth_root_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (σ : ℝ) (hσ : 0 < σ) (k : ℕ) (hk : 2 ≤ k) (hX : Measurable X) (htail : ∀ (t : ℝ), 0 ≤ t → μ {ω : Ω | |X ω| ≥ t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σ ^ 2)))) : (∫ (ω : Ω), |X ω| ^ k ∂μ) ^ (↑k)⁻¹ ≤ σ * Real.exp (1 / Real.exp 1) * √↑k

Lemma 1.4, Part 2 (k-th root bound). For X with sub-Gaussian tail P[|X|>t] ≤ 2exp(-t²/(2σ²)), (E[|X|^k])^{1/k} ≤ σ · e^{1/e} · √k for k ≥ 2.

Proof: From Part 1, E[|X|^k] ≤ (2σ²)^{k/2} · k · Γ(k/2). Using Stirling/Gamma bounds: k·Γ(k/2) ≤ (k/e)^{k/2} · e, so E[|X|^k]^{1/k} ≤ σ√2 · (k·Γ(k/2))^{1/k} ≤ σ · e^{1/e} · √k.

theorem SubGaussianMoments.first_moment_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (σ : ℝ) (hσ : 0 < σ) (hX : Measurable X) (htail : ∀ (t : ℝ), 0 ≤ t → μ {ω : Ω | |X ω| ≥ t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σ ^ 2)))) : ∫ (ω : Ω), |X ω| ∂μ ≤ σ * √(2 * Real.pi)

Lemma 1.4, Part 3 (First moment bound). For X with sub-Gaussian tail, E[|X|] ≤ σ√(2π).

Proof: Apply Part 1 with k=1: E[|X|] ≤ (2σ²)^{1/2} · 1 · Γ(1/2) = σ√2 · √π = σ√(2π).

theorem SubGaussianMoments.subgaussian_moment_bounds {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (σ : ℝ) (hσ : 0 < σ) (hX : Measurable X) (htail : ∀ (t : ℝ), 0 ≤ t → μ {ω : Ω | |X ω| ≥ t} ≤ ENNReal.ofReal (2 * Real.exp (-t ^ 2 / (2 * σ ^ 2)))) : (∀ (k : ℕ), 2 ≤ k → (∫ (ω : Ω), |X ω| ^ k ∂μ) ^ (↑k)⁻¹ ≤ σ * Real.exp (1 / Real.exp 1) * √↑k) ∧ ∫ (ω : Ω), |X ω| ∂μ ≤ σ * √(2 * Real.pi)

Lemma 1.4 (bundled). Under the sub-Gaussian tail bound P[|X| ≥ t] ≤ 2exp(-t²/(2σ²)): (a) (E[|X|^k])^{1/k} ≤ σ · e^{1/e} · √k for k ≥ 2, and (b) E[|X|] ≤ σ√(2π).

Backward-compatible aliases

theorem lemma_1_4_moment_bound {Ω : 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)))) (k : ℕ) (hk : 1 ≤ k) : ∫⁻ (ω : Ω), ENNReal.ofReal (|X ω| ^ ↑k) ∂μ ≤ ENNReal.ofReal ((2 * σsq) ^ (↑k / 2) * ↑k * Real.Gamma (↑k / 2))

Alias for SubGaussianMoments.moment_bound for backward compatibility.