Geometric helper: ε-net inner product bound

theorem exists_net_inner_ge_half_norm {d : ℕ} {N : Finset (EuclideanSpace ℝ (Fin d))} (hN_net : IsEpsilonNet (Metric.closedBall 0 1) (↑N) (1 / 2)) (x : EuclideanSpace ℝ (Fin d)) (hx : x ≠ 0) : ∃ z ∈ N, inner ℝ z x ≥ 1 / 2 * ‖x‖

For a 1/2-net N of the unit ball and any nonzero vector x, there exists z ∈ N with ⟪z, x⟫ ≥ (1/2)‖x‖.

Proof: Let θ = x/‖x‖ be the unit direction of x. Since θ ∈ B₂, there exists z ∈ N with ‖θ - z‖ ≤ 1/2. Then: ‖x‖ = ⟪θ, x⟫ = ⟪z, x⟫ + ⟪θ-z, x⟫ ≤ ⟪z, x⟫ + (1/2)‖x‖ So ⟪z, x⟫ ≥ (1/2)‖x‖.

Event containment via ε-net reduction

theorem event_containment_net {d : ℕ} {N : Finset (EuclideanSpace ℝ (Fin d))} (hN_net : IsEpsilonNet (Metric.closedBall 0 1) (↑N) (1 / 2)) (x : EuclideanSpace ℝ (Fin d)) (t : ℝ) (ht : 0 < t) (hθ_exists : ∃ (θ : EuclideanSpace ℝ (Fin d)), ‖θ‖ ≤ 1 ∧ inner ℝ θ x > t) : ∃ z ∈ ↑N, inner ℝ z x > t / 2

If some θ ∈ B₂ achieves ⟪θ, x⟫ > t (with t > 0), then some z ∈ N achieves ⟪z, x⟫ > t/2.

Proof: From ⟪θ, x⟫ > t and ‖θ‖ ≤ 1, we get ‖x‖ ≥ ⟪θ, x⟫ > t (Cauchy-Schwarz). By the geometric helper, ∃ z ∈ N with ⟪z, x⟫ ≥ (1/2)‖x‖ > t/2.

Main theorem

theorem theorem_1_19_tail_bound {d : ℕ} (hd : 0 < d) {Ω : Type u_1} [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 (tail bound version): For a sub-Gaussian random vector X ∈ ℝ^d, P(max_{θ ∈ B₂} θᵀX > t) ≤ 6^d · exp(-t²/(8σ²)).

Here "sub-Gaussian random vector" means every unit-ball projection is sub-Gaussian: for all a with ‖a‖ ≤ 1, the scalar ⟪a, X⟫ is sub-Gaussian with parameter σ².

Proof: By the ε-net argument with a 1/2-net from Lemma 1.18, the event {∃θ ∈ B₂, ⟪θ,X⟫ > t} is contained in {∃z ∈ N, ⟪z,X⟫ > t/2}. Applying the union bound and Lemma 1.3 to each net element gives P ≤ |N| · exp(-(t/2)²/(2σ²)) ≤ 6^d · exp(-t²/(8σ²)).

Expectation and high-probability bounds

theorem theorem_1_19_expectation_bound {d : ℕ} (hd : 0 < d) {Ω : Type u_1} {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 (expectation form). E[max_{θ ∈ B₂} θᵀX] ≤ 4σ√d for a sub-Gaussian random vector X with variance proxy σ².

Since max_{θ ∈ B₂} θᵀX(ω) = ‖X(ω)‖ (the supremum of the inner product over the unit ball equals the Euclidean norm), the statement simplifies to E[‖X‖] ≤ 4√σ² · √d.

Proof outline (from Rigollet):

1. Let N be a 1/2-net of B₂ with |N| ≤ 6^d.
2. For every θ ∈ B₂, write θ = z + x with z ∈ N and ‖x‖ ≤ 1/2.
3. max_{θ∈B₂} θᵀX ≤ max_{z∈N} zᵀX + (1/2) max_{θ∈B₂} θᵀX.
4. Rearranging: max_{θ∈B₂} θᵀX ≤ 2 max_{z∈N} zᵀX.
5. By Theorem 1.14 (expectation form): E[max_{z∈N} zᵀX] ≤ σ√(2 log|N|) ≤ σ√(2d log 6).
6. Therefore E[‖X‖] ≤ 2σ√(2d log 6) ≤ 4σ√d since 2 log 6 < 4.

theorem norm_gt_exists_inner_gt {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (t : ℝ) (ht : 0 < t) (hxt : ‖x‖ > t) : ∃ (θ : EuclideanSpace ℝ (Fin d)), ‖θ‖ ≤ 1 ∧ inner ℝ θ x > t

For any nonzero x with ‖x‖ > t > 0, there exists a unit vector θ with ⟪θ, x⟫ > t. Take θ = x / ‖x‖.

theorem theorem_1_19_high_prob {d : ℕ} (hd : 0 < d) {Ω : Type u_1} {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 (high probability form). With probability at least 1 - δ: ‖X‖ ≤ 4σ√d + 2σ√(2 log(1/δ)).

Since max_{θ ∈ B₂} θᵀX(ω) = ‖X(ω)‖, this gives a high-probability upper bound on ‖X‖.

Proof outline (from Rigollet):

1. From the tail bound (theorem_1_19_tail_bound): P(‖X‖ > t) ≤ 6^d · exp(-t²/(8σ²)).
2. Set 6^d · exp(-t²/(8σ²)) ≤ δ, which gives t² ≥ 8σ² (d log 6 + log(1/δ)).
3. Taking t = √(8 log 6) · σ · √d + 2σ · √(2 log(1/δ)) suffices.
4. Since √(8 log 6) < 4, we can use t = 4σ√d + 2σ√(2 log(1/δ)).