Helper: Sub-Gaussian MGF properties from boundedness

theorem hoeffding_subgaussian_mgf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (_hab : a < b) (hXm : Measurable X) (hXa : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hXb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hmean : ∫ (ω : Ω), X ω ∂μ = 0) : ProbabilityTheory.HasSubgaussianMGF X ((‖b - a‖₊ / 2) ^ 2) μ

For bounded mean-zero random variables, derive the Hoeffding MGF bound and exponential integrability using Mathlib's hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero.

Hoeffding's Inequality — Sum Form

The sum form states: for independent mean-zero bounded random variables Xᵢ ∈ [aᵢ, bᵢ], we have P(∑ Xᵢ > t) ≤ exp(-2t²/∑(bᵢ-aᵢ)²).

This is the core result from which the sample-mean form follows.

theorem hoeffding_sum_upper_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {a b : Fin n → ℝ} (hab : ∀ (i : Fin n), a i < b i) (hXm : ∀ (i : Fin n), Measurable (X i)) (hXi : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hXa : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, a i ≤ X i ω) (hXb : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b i) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hX_indep : ProbabilityTheory.iIndepFun X μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∑ i : Fin n, X i ω > t} ≤ ENNReal.ofReal (Real.exp (-(2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2)))

Hoeffding's inequality (upper tail, sum form). For independent mean-zero Xᵢ ∈ [aᵢ, bᵢ] a.s., and t > 0: P(∑ᵢ Xᵢ > t) ≤ exp(-2t² / ∑ᵢ(bᵢ - aᵢ)²).

theorem hoeffding_sum_lower_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {a b : Fin n → ℝ} (hab : ∀ (i : Fin n), a i < b i) (hXm : ∀ (i : Fin n), Measurable (X i)) (hXi : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hXa : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, a i ≤ X i ω) (hXb : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b i) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hX_indep : ProbabilityTheory.iIndepFun X μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∑ i : Fin n, X i ω < -t} ≤ ENNReal.ofReal (Real.exp (-(2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2)))

Hoeffding's inequality (lower tail, sum form). For independent mean-zero Xᵢ ∈ [aᵢ, bᵢ] a.s., and t > 0: P(∑ᵢ Xᵢ < -t) ≤ exp(-2t² / ∑ᵢ(bᵢ - aᵢ)²).

Hoeffding's Inequality — Sample Mean Form (Theorem 1.9)

The sample-mean form: for independent Xᵢ ∈ [aᵢ, bᵢ] (not necessarily centered), P(X̄ - E(X̄) > t) ≤ exp(-2n²t²/∑(bᵢ-aᵢ)²).

This follows from the sum form by noting that X̄ - E(X̄) > t iff ∑(Xᵢ - E[Xᵢ]) > nt, and the centered variables Yᵢ = Xᵢ - E[Xᵢ] are mean-zero, bounded, and independent.

theorem theorem_1_9_hoeffding_inequality {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {a b : Fin n → ℝ} (hab : ∀ (i : Fin n), a i < b i) (hXm : ∀ (i : Fin n), Measurable (X i)) (hXi : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hXa : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, a i ≤ X i ω) (hXb : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b i) (hmean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hX_indep : ProbabilityTheory.iIndepFun X μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∑ i : Fin n, X i ω > t} ≤ ENNReal.ofReal (Real.exp (-(2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2))) ∧ μ {ω : Ω | ∑ i : Fin n, X i ω < -t} ≤ ENNReal.ofReal (Real.exp (-(2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2)))

Theorem 1.9 — Hoeffding's inequality (combined). For independent random variables Xᵢ ∈ [aᵢ, bᵢ] a.s. with aᵢ < bᵢ, the centered sum satisfies both tail bounds:

P(∑ᵢ Xᵢ > t) ≤ exp(-2t² / ∑ᵢ(bᵢ - aᵢ)²) P(∑ᵢ Xᵢ < -t) ≤ exp(-2t² / ∑ᵢ(bᵢ - aᵢ)²)

where the Xᵢ are assumed to be centered (mean zero). For general (uncentered) variables, apply this to Yᵢ = Xᵢ - E[Xᵢ].

Hoeffding's Inequality — Sample Mean Form (Theorem 1.9 proper)

The textbook states Hoeffding's inequality for the sample mean: for independent Xᵢ ∈ [aᵢ, bᵢ] (not necessarily centered), P(X̄ - E(X̄) > t) ≤ exp(-2n²t²/∑(bᵢ-aᵢ)²) where X̄ = (1/n)∑ᵢ Xᵢ.

The proof centers the variables: Yᵢ = Xᵢ - E[Xᵢ] are mean-zero, bounded in [aᵢ - E[Xᵢ], bᵢ - E[Xᵢ]] (so bᵢ - aᵢ is preserved), and independent. Since X̄ - E(X̄) > t ↔ ∑Yᵢ > nt, we apply the sum form with threshold nt.

theorem hoeffding_sample_mean_upper_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {X : Fin n → Ω → ℝ} {a b : Fin n → ℝ} (hab : ∀ (i : Fin n), a i < b i) (hXm : ∀ (i : Fin n), Measurable (X i)) (hXi : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hXa : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, a i ≤ X i ω) (hXb : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | (∑ i : Fin n, X i ω) / ↑n - (∑ i : Fin n, ∫ (ω' : Ω), X i ω' ∂μ) / ↑n > t} ≤ ENNReal.ofReal (Real.exp (-(2 * ↑n ^ 2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2)))

Hoeffding's inequality (upper tail, sample mean form). For independent Xᵢ ∈ [aᵢ, bᵢ] a.s. with n > 0: P(X̄ - E[X̄] > t) ≤ exp(-2n²t² / ∑ᵢ(bᵢ - aᵢ)²), where X̄ = (1/n)∑ Xᵢ, i.e., X̄ - E[X̄] = (∑ Xᵢ)/n - (∑ E[Xᵢ])/n.

theorem hoeffding_sample_mean_lower_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {X : Fin n → Ω → ℝ} {a b : Fin n → ℝ} (hab : ∀ (i : Fin n), a i < b i) (hXm : ∀ (i : Fin n), Measurable (X i)) (hXi : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hXa : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, a i ≤ X i ω) (hXb : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | (∑ i : Fin n, X i ω) / ↑n - (∑ i : Fin n, ∫ (ω' : Ω), X i ω' ∂μ) / ↑n < -t} ≤ ENNReal.ofReal (Real.exp (-(2 * ↑n ^ 2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2)))

Hoeffding's inequality (lower tail, sample mean form). For independent Xᵢ ∈ [aᵢ, bᵢ] a.s. with n > 0: P(X̄ - E[X̄] < -t) ≤ exp(-2n²t² / ∑ᵢ(bᵢ - aᵢ)²).

theorem theorem_1_9_sample_mean {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {X : Fin n → Ω → ℝ} {a b : Fin n → ℝ} (hab : ∀ (i : Fin n), a i < b i) (hXm : ∀ (i : Fin n), Measurable (X i)) (hXi : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hXa : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, a i ≤ X i ω) (hXb : ∀ (i : Fin n), ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b i) (hX_indep : ProbabilityTheory.iIndepFun X μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | (∑ i : Fin n, X i ω) / ↑n - (∑ i : Fin n, ∫ (ω' : Ω), X i ω' ∂μ) / ↑n > t} ≤ ENNReal.ofReal (Real.exp (-(2 * ↑n ^ 2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2))) ∧ μ {ω : Ω | (∑ i : Fin n, X i ω) / ↑n - (∑ i : Fin n, ∫ (ω' : Ω), X i ω' ∂μ) / ↑n < -t} ≤ ENNReal.ofReal (Real.exp (-(2 * ↑n ^ 2 * t ^ 2 / ∑ i : Fin n, (b i - a i) ^ 2)))

Theorem 1.9 — Hoeffding's inequality (sample mean form). Let X₁,...,Xₙ be n independent random variables with Xᵢ ∈ [aᵢ, bᵢ] a.s. Let X̄ = (1/n) ∑ᵢ Xᵢ. Then for any t > 0:

P(X̄ - E[X̄] > t) ≤ exp(-2n²t² / ∑ᵢ(bᵢ - aᵢ)²) P(X̄ - E[X̄] < -t) ≤ exp(-2n²t² / ∑ᵢ(bᵢ - aᵢ)²)

Here X̄ - E[X̄] is expressed as (∑ Xᵢ)/n - (∑ E[Xᵢ])/n.