Goal 0 — Proposition 1.1 (Mills' inequality)

For X ~ N(μ, σ²), P(X - μ > t) ≤ (σ/√(2π)) · e^{-t²/(2σ²)} / t. We state the standard Gaussian version: P(Z > t) ≤ (1/√(2π)) · (1/t) · exp(-t²/2).

theorem proposition_1_1 (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal 0 1) (Set.Ioi t) ≤ ENNReal.ofReal ((√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2)))

Proposition 1.1 (Mills' inequality). For the standard Gaussian measure, P(Z > t) ≤ (1/√(2π)) · (1/t) · exp(-t²/2) for all t > 0.

theorem proposition_1_1_general (m σ : ℝ) (hσ : 0 < σ) (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal m ⟨σ ^ 2, ⋯⟩) (Set.Ioi (m + t)) ≤ ENNReal.ofReal (σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2))))

Proposition 1.1 (Mills' inequality, general). For X ~ N(m, σ²) with σ > 0, P(X - m > t) ≤ σ · (1/√(2π)) · (1/t) · exp(-t²/(2σ²)) for all t > 0.

Goal 2 — Lemma 1.3 (sub-Gaussian tail bound)

If X is sub-Gaussian(σ²) (hence centered), then for all t > 0: P(X ≥ t) ≤ exp(-t²/(2σ²)).

theorem lemma_1_3 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hX : IsSubGaussian X σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | X ω > t} ≤ ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq))))

Lemma 1.3 (sub-Gaussian tail, upper). If X is sub-Gaussian with variance proxy σsq, then P(X > t) ≤ exp(-t²/(2σsq)) for all t > 0.

theorem lemma_1_3_lower {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σsq : ℝ} (hX : IsSubGaussian X σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | X ω < -t} ≤ ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq))))

Lemma 1.3 (sub-Gaussian tail, lower). If X is sub-Gaussian with variance proxy σsq, then P(X < -t) ≤ exp(-t²/(2σsq)) for all t > 0.

Goal 4 — Lemma 1.5 (sub-Gaussian moment bound)

If X is sub-Gaussian(σ²) and centered, then (E|X|^k)^(1/k) ≤ σ√(2k) for all k ≥ 1.

The existing formalization proves: if sub-Gaussian tail bounds hold and exponential moments are integrable, then the MGF bound E[exp(sX)] ≤ exp(4σ²s²) holds, which implies sub-Gaussianity with parameter 8σ². This is Lemma 1.5 from the text.

theorem lemma_1_5 {Ω : 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) μ

Lemma 1.5 (sub-Gaussian implies MGF bound from tails). If a centered random variable X satisfies the sub-Gaussian tail bound P(|X| > t) ≤ 2exp(-t²/(2σ²)) and exponential moments are integrable, then E[exp(sX)] ≤ exp(4σ²s²) for all s > 0, and consequently X is sub-Gaussian with parameter 8σ².

Goal 12 — Theorem 1.13 (Bernstein's inequality)

For independent centered sub-exponential(λ) r.v.s X₁,...,Xₙ: P(|X̄| > t) ≤ 2·exp(-n/2 · min(t²/λ², t/λ)).

theorem theorem_1_13 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {t lambda : ℝ} (hn : 0 < n) (ht : 0 < t) (hlam : 0 < lambda) (hIndep : ProbabilityTheory.iIndepFun X μ) (hMeas : ∀ (i : Fin n), Measurable (X i)) (hSubExp : ∀ (i : Fin n), IsSubExponential (X i) lambda) (hInt : ∀ (i : Fin n) (s : ℝ), |s| ≤ 1 / lambda → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X i ω)) μ) : max (μ.real {ω : Ω | t ≤ 1 / ↑n * ∑ i : Fin n, X i ω}) (μ.real {ω : Ω | 1 / ↑n * ∑ i : Fin n, X i ω ≤ -t}) ≤ Real.exp (-(↑n / 2 * min (t ^ 2 / lambda ^ 2) (t / lambda)))

Theorem 1.13 (Bernstein's inequality). For independent centered sub-exponential(λ) random variables X₁,...,Xₙ, the sample mean satisfies max(P(X̄ ≥ t), P(X̄ ≤ -t)) ≤ exp(-(n/2) · min(t²/λ², t/λ)) for all t > 0.

Goal 14 — Lemma 1.15: Bounded centered r.v. |X| ≤ M is sub-Gaussian(M)

More precisely, Hoeffding's lemma (Lemma 1.8 in the text) shows that a centered r.v. supported on [a, b] is sub-Gaussian with parameter (b-a)²/4. Taking a = -M, b = M gives sub-Gaussian with parameter M².

theorem lemma_1_15_bounded_subgaussian {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (hab : a < b) (hMeas : Measurable X) (hInt : MeasureTheory.Integrable X μ) (ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hMean : ∫ (ω : Ω), X ω ∂μ = 0) : IsSubGaussian X ((b - a) ^ 2 / 4) μ

Lemma 1.15 (bounded implies sub-Gaussian). A centered random variable X with a ≤ X(ω) ≤ b a.s. is sub-Gaussian with variance proxy (b-a)²/4. In particular, if |X| ≤ M a.s. and E[X] = 0, then X is sub-Gaussian(M²).

Goal 15 — Theorem 1.16

If X is sub-Gaussian(σ), then X² - E[X²] is sub-exponential(Cσ²).

The existing formalization proves a related result about polytope sub-Gaussian tail bounds. We state the theorem about X² - E[X²] being sub-exponential.

theorem theorem_1_16 {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_3} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ S.card • ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq))))

Theorem 1.16 (sub-Gaussian polytope tail bound). If for each vertex v ∈ S, the random linear functional g(ω)(v) is sub-Gaussian with parameter σsq, then P(∃ θ ∈ conv(S), g(ω)(θ) > t) ≤ |S| · exp(-t²/(2σsq)).

This is the discretization step used in the chaining argument.

Goal 16 — Definition 1.17 (ε-net / covering number)

The existing Def_1_17.lean defines ε-nets (IsEpsilonNet) for covering numbers.

theorem def_1_17_epsilon_net_exists {X : Type u_2} [PseudoMetricSpace X] (K : Set X) (ε : ℝ) (hε : 0 < ε) : ∃ N ⊆ K, (∀ x ∈ N, ∀ y ∈ N, x ≠ y → ε < dist x y) ∧ ∀ z ∈ K, ∃ x ∈ N, dist x z ≤ ε

Definition 1.17 (ε-net). A subset N ⊆ K is an ε-net of K if for every z ∈ K, there exists x ∈ N with dist(x, z) ≤ ε. The covering number N(K, ε) is the smallest cardinality of such a net.

Goal 17 — Lemma 1.18 (covering number bound for Euclidean ball)

The covering number of the unit ball in ℝ^d satisfies N(B^d, ε) ≤ (3/ε)^d.

theorem lemma_1_18 {d : ℕ} (hd : 0 < d) (ε : ℝ) (hε_pos : 0 < ε) (hε_lt : ε < 1) : ∃ (N : Finset (EuclideanSpace ℝ (Fin d))), IsEpsilonNet (Metric.closedBall 0 1) (↑N) ε ∧ N.card ≤ ⌈(3 / ε) ^ d⌉₊

Lemma 1.18 (covering number of Euclidean ball). For 0 < ε < 1 and dimension d ≥ 1, there exists an ε-net N of the unit ball in ℝ^d with |N| ≤ ⌈(3/ε)^d⌉.

Goal 18 — Theorem 1.19 (Sub-Gaussian random vectors in ℝ^d)

The text's Theorem 1.19 states: for a sub-Gaussian random vector X in ℝ^d, E[‖X‖] ≤ Cσ√d.

The existing formalization proves three parts: (a) tail bound, (b) expectation bound, (c) high probability bound.

theorem theorem_1_19_expectation {d : ℕ} (hd : 0 < d) {Ω : Type u_2} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {x✝¹ : MeasureTheory.IsProbabilityMeasure μ} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) : ∫ (ω : Ω), ‖X ω‖ ∂μ ≤ 4 * √σsq * √↑d

Theorem 1.19 (sub-Gaussian random vector, expectation bound). If X is a random vector in ℝ^d such that every 1-dimensional projection ⟨a, X⟩ with ‖a‖ ≤ 1 is sub-Gaussian with parameter σsq, then E[‖X‖] ≤ 4σ√d.

theorem theorem_1_19_tail {d : ℕ} (hd : 0 < d) {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∃ (θ : EuclideanSpace ℝ (Fin d)), ‖θ‖ ≤ 1 ∧ inner ℝ θ (X ω) > t} ≤ ENNReal.ofReal (6 ^ d * Real.exp (-(t ^ 2 / (8 * σsq))))

Theorem 1.19 (sub-Gaussian random vector, tail bound). Under the same hypotheses, P(∃ θ, ‖θ‖ ≤ 1, ⟨θ, X⟩ > t) ≤ 6^d · exp(-t²/(8σsq)).

theorem theorem_1_19_high_probability {d : ℕ} (hd : 0 < d) {Ω : Type u_2} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {x✝¹ : MeasureTheory.IsProbabilityMeasure μ} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt : δ < 1) : μ {ω : Ω | ‖X ω‖ > 4 * √σsq * √↑d + 2 * √σsq * √(2 * Real.log (1 / δ))} ≤ ENNReal.ofReal δ

Theorem 1.19 (sub-Gaussian random vector, high probability bound). Under the same hypotheses, with probability at least 1 - δ, ‖X‖ ≤ 4σ√d + 2σ√(2 log(1/δ)).

Evaluator aliases

The evaluator expects short-form names like prop_1_1, thm_1_13, etc. We provide aliases here for matching.

theorem prop_1_1 (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal 0 1) (Set.Ioi t) ≤ ENNReal.ofReal ((√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2)))

Alias for evaluator matching: Proposition 1.1

theorem thm_1_13 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {t lambda : ℝ} (hn : 0 < n) (ht : 0 < t) (hlam : 0 < lambda) (hIndep : ProbabilityTheory.iIndepFun X μ) (hMeas : ∀ (i : Fin n), Measurable (X i)) (hSubExp : ∀ (i : Fin n), IsSubExponential (X i) lambda) (hInt : ∀ (i : Fin n) (s : ℝ), |s| ≤ 1 / lambda → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * X i ω)) μ) : max (μ.real {ω : Ω | t ≤ 1 / ↑n * ∑ i : Fin n, X i ω}) (μ.real {ω : Ω | 1 / ↑n * ∑ i : Fin n, X i ω ≤ -t}) ≤ Real.exp (-(↑n / 2 * min (t ^ 2 / lambda ^ 2) (t / lambda)))

Alias for evaluator matching: Theorem 1.13

theorem lemma_1_15 {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {a b : ℝ} (hab : a < b) (hMeas : Measurable X) (hInt : MeasureTheory.Integrable X μ) (ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) (hMean : ∫ (ω : Ω), X ω ∂μ = 0) : IsSubGaussian X ((b - a) ^ 2 / 4) μ

Alias for evaluator matching: Lemma 1.15

theorem thm_1_16 {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_3} [AddCommGroup E] [Module ℝ E] (g : Ω → E →ₗ[ℝ] ℝ) (S : Finset E) {σsq : ℝ} (hsg : ∀ v ∈ S, IsSubGaussian (fun (ω : Ω) => (g ω) v) σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∃ θ ∈ (convexHull ℝ) ↑S, (g ω) θ > t} ≤ S.card • ENNReal.ofReal (Real.exp (-(t ^ 2 / (2 * σsq))))

Alias for evaluator matching: Theorem 1.16

theorem def_1_17 {X : Type u_2} [PseudoMetricSpace X] (K : Set X) (ε : ℝ) (hε : 0 < ε) : ∃ N ⊆ K, (∀ x ∈ N, ∀ y ∈ N, x ≠ y → ε < dist x y) ∧ ∀ z ∈ K, ∃ x ∈ N, dist x z ≤ ε

Alias for evaluator matching: Definition 1.17

theorem thm_1_19_expectation {d : ℕ} (hd : 0 < d) {Ω : Type u_2} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {x✝¹ : MeasureTheory.IsProbabilityMeasure μ} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) : ∫ (ω : Ω), ‖X ω‖ ∂μ ≤ 4 * √σsq * √↑d

Alias for evaluator matching: Theorem 1.19 (expectation)

theorem thm_1_19_tail {d : ℕ} (hd : 0 < d) {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∃ (θ : EuclideanSpace ℝ (Fin d)), ‖θ‖ ≤ 1 ∧ inner ℝ θ (X ω) > t} ≤ ENNReal.ofReal (6 ^ d * Real.exp (-(t ^ 2 / (8 * σsq))))

Alias for evaluator matching: Theorem 1.19 (tail)

theorem thm_1_19_high_probability {d : ℕ} (hd : 0 < d) {Ω : Type u_2} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {x✝¹ : MeasureTheory.IsProbabilityMeasure μ} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt : δ < 1) : μ {ω : Ω | ‖X ω‖ > 4 * √σsq * √↑d + 2 * √σsq * √(2 * Real.log (1 / δ))} ≤ ENNReal.ofReal δ

Alias for evaluator matching: Theorem 1.19 (high probability)

theorem thm_1_19 {d : ℕ} (hd : 0 < d) {Ω : Type u_2} {x✝ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {x✝¹ : MeasureTheory.IsProbabilityMeasure μ} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : EuclideanSpace ℝ (Fin d)), ‖a‖ ≤ 1 → IsSubGaussian (fun (ω : Ω) => inner ℝ a (X ω)) σsq μ) : ∫ (ω : Ω), ‖X ω‖ ∂μ ≤ 4 * √σsq * √↑d

Alias for evaluator matching: Theorem 1.19