remove unresolvable theorem number

StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean

@@ -1224,7 +1224,7 @@ theorem entropy_le_half_gradient {n : ℕ} (h : (Fin n → Bool) → ℝ) :
 ## Part 6: Main Theorem - Bernoulli Log-Sobolev Inequality
 -/
 
-/-- The Bernoulli log-Sobolev inequality (Theorem 5.1).
+/-- The Bernoulli log-Sobolev inequality.
 
 For any function h : {±1}^n → ℝ,
   Ent_μ(h²) ≤ (1/2) · E_μ[Σⱼ (h(ε) - h(flip_j ε))²]

StatsMLlib/Probability/Process/Dudley.lean

@@ -1079,7 +1079,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
     (dn.nets K).sup' (hnet_nonempty K) (fun u => X u ω)
 
   -- ══════════════════════════════════════════════════════════════════════════════
-  -- SECTION 2: CORE BOUND (Lemma 4.2)
+  -- SECTION 2: CORE BOUND
   -- 𝔼[Y_K] ≤ 6√2 · σ · dyadicRHS(K+1), via dudley_chaining_bound_core.
   -- ══════════════════════════════════════════════════════════════════════════════
 
@@ -1103,7 +1103,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
   -- proj_K(tₙ) → tₙ, hence X(proj_K(tₙ)) → X(tₙ), and X(proj_K(tₙ)) ≤ Y_K.
   -- ══════════════════════════════════════════════════════════════════════════════
 
-  -- Lemma 4.3: proj_K(tₙ) → tₙ as K → ∞
+  -- proj_K(tₙ) → tₙ as K → ∞
   have h_proj_tendsto : ∀ n, Filter.Tendsto (fun K => proj K n) Filter.atTop (nhds (t n)) := by
     intro n
     rw [Metric.tendsto_atTop]
@@ -1131,7 +1131,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
       _ = |dyadicScale D K - 0| := by simp [abs_of_pos (dyadicScale_pos hD K)]
       _ < ε := hN K hK
 
-  -- Lemma 4.4: X(proj_K(tₙ))(ω) → X(tₙ)(ω) by path continuity
+  -- X(proj_K(tₙ))(ω) → X(tₙ)(ω) by path continuity
   have h_X_tendsto : ∀ n ω, Filter.Tendsto (fun K => X (proj K n) ω) Filter.atTop (nhds (X (t n) ω)) := by
     intro n ω
     have h_cont_at := (hcont ω).continuousAt (x := ⟨t n, ht_mem n⟩)
@@ -1142,7 +1142,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
       exact h_proj_tendsto n
     exact h_cont_at.tendsto.comp h_proj_sub_tendsto
 
-  -- Lemma 4.5: X(proj_K(tₙ))(ω) ≤ Y_K(ω)
+  -- X(proj_K(tₙ))(ω) ≤ Y_K(ω)
   have h_le_Y : ∀ K n ω, X (proj K n) ω ≤ Y K ω := by
     intro K n ω
     exact Finset.le_sup' (fun u => X u ω) (h_proj_mem K n)
@@ -1152,7 +1152,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
   -- Y_K is bounded below pointwise, integrable for K ≥ 1, and liminf Y_K ≠ +∞ a.e.
   -- ══════════════════════════════════════════════════════════════════════════════
 
-  -- Lemma 4.6: Y_K bounded below via convergence of X(proj_K(t₀))
+  -- Y_K bounded below via convergence of X(proj_K(t₀))
   have h_Y_bdd_below : ∀ ω, Filter.IsBoundedUnder (· ≥ ·) Filter.atTop (fun K => Y K ω) := by
     intro ω
     have h_tendsto := h_X_tendsto 0 ω
@@ -1186,7 +1186,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
       calc |(dn.nets K).sup' (hnet_nonempty K) (fun u => X u ω)|
         _ ≤ ∑ u ∈ dn.nets K, |X u ω| := abs_sup'_le_sum (hnet_nonempty K) (fun u => X u ω)
 
-  -- Lemma 4.7: liminf Y_K(ω) < +∞ a.e. via uniform L¹ bounds
+  -- liminf Y_K(ω) < +∞ a.e. via uniform L¹ bounds
   have h_Y_liminf_ne_top : ∀ᵐ ω ∂μ,
       Filter.liminf (fun K => (Y K ω : EReal)) Filter.atTop ≠ ⊤ := by
 
@@ -1434,7 +1434,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
     exact (EReal.coe_ne_top R) (le_antisymm h_liminf_le_R le_top).symm
 
   -- ══════════════════════════════════════════════════════════════════════════════
-  -- SECTION 5: POINTWISE BOUND (Lemma 4.8)
+  -- SECTION 5: POINTWISE BOUND
   -- For a.e. ω: sup_n X(tₙ)(ω) ≤ liminf_K Y_K(ω) via tendsto_le_liminf_of_le'.
   -- ══════════════════════════════════════════════════════════════════════════════
   have h_pointwise : ∀ᵐ ω ∂μ, ∀ n, X (t n) ω ≤ Filter.liminf (fun K => Y K ω) Filter.atTop := by
@@ -1464,7 +1464,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
       exact h_liminf_ge_0
 
   -- ══════════════════════════════════════════════════════════════════════════════
-  -- SECTION 6: FATOU'S LEMMA (Lemma 4.9)
+  -- SECTION 6: FATOU'S LEMMA
   -- ∫ sup_n X(tₙ) ≤ liminf_K ∫ Y_K using shifted-Fatou: Z_K = Y_K - g ≥ 0 where
   -- g = inf_K X(proj_K(0)). The shift g is integrable via telescoping bound.
   -- ══════════════════════════════════════════════════════════════════════════════
@@ -2268,7 +2268,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
     exact le_trans h_step1 h_fatou_Y
 
   -- ══════════════════════════════════════════════════════════════════════════════
-  -- SECTION 7: UPPER BOUND FOR LIMINF (Lemma 4.10)
+  -- SECTION 7: UPPER BOUND FOR LIMINF
   -- liminf((6√2)σ * dyadicRHS) ≤ (12√2)σ * entropyIntegral via δf(δ) → 0.
   -- ══════════════════════════════════════════════════════════════════════════════
 
@@ -2481,7 +2481,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A :
       _ = (12 * Real.sqrt 2) * σ * entropyIntegral s D := h_liminf_eq
 
   -- ══════════════════════════════════════════════════════════════════════════════
-  -- SECTION 8: INTEGRAL BOUNDED BELOW (Lemma 4.11)
+  -- SECTION 8: INTEGRAL BOUNDED BELOW
   -- ∫ Y_K ≥ 0 via centering: ∫ X u = 0 for all u ∈ s.
   -- ══════════════════════════════════════════════════════════════════════════════
 

StatsMLlib/Probability/Process/TruncatedDudley.lean

@@ -64,7 +64,7 @@ def localOsc (X : α → ℝ) (T : Set α) (δ : ℝ) : ℝ :=
   sSup {X x - X y | (x ∈ T) (y ∈ T) (_ : dist x y ≤ δ)}
 
 /-
-Lemma 1.1: One-step discretization bound.
+One-step discretization bound.
 Fix δ > 0 and let U be a finite centered δ-net of T. Then
 sup_{θ, θ' ∈ T} (X_θ - X_θ') ≤ 2 sup_{d(γ, γ') ≤ δ} (X_γ - X_γ') + 2 max_{u ∈ U} |X_u - X_u0|.
 -/
@@ -179,7 +179,7 @@ lemma mgf_max_bound {α : Type*} [MeasurableSpace α]
     _ = M * Real.exp (σ_sq * t^2 / 2) := by simp
 
 /-
-Lemma 1.2: Metric entropy bound for sub-Gaussian maxima.
+Metric entropy bound for sub-Gaussian maxima.
 Let Y_1, ..., Y_M be mean-zero sub-Gaussian random variables with parameter σ^2.
 Then E[max Y_k] ≤ σ * sqrt(2 * log M).
 -/

StatsMLlib/Probability/RandomMatrix/Basic.lean

@@ -106,7 +106,7 @@ def randomMatrix {m n : ℕ} (A : Fin m → Fin n → Ω → ℝ) (ω : Ω) :
   fun i j => A i j ω
 
 omit [MeasurableSpace Ω] in
-/-- The empirical covariance deviation `m⁻¹ AᵀA - Iₙ` appearing in HDP Theorem 4.6.1. -/
+/-- The empirical covariance deviation `m⁻¹ AᵀA - Iₙ`. -/
 def sampleCovarianceDeviation {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
     Matrix (Fin n) (Fin n) ℝ :=
   ((m : ℝ)⁻¹) • (A.conjTranspose * A) - 1
@@ -503,7 +503,7 @@ structure MatrixBilinearNet (m n : ℕ) (ε : ℝ) where
 /--
 A centered matrix bilinear net: the net points themselves lie in the corresponding unit balls.
 This is the form naturally produced by finite coverings of the unit balls and used in the
-Section 4.4 net argument.
+operator-norm net argument.
 -/
 structure CenteredMatrixBilinearNet (m n : ℕ) (ε : ℝ) extends
     MatrixBilinearNet m n ε where
@@ -783,7 +783,7 @@ lemma matrixOperatorNorm_le_of_centered_bilinear_net {m n : ℕ} {ε u : ℝ}
   have hmul' : M * (1 - 2 * ε) ≤ u := by nlinarith
   exact (le_div_iff₀ hden).mpr (by simpa [M] using hmul')
 
-/-- The standard `ε = 1/4` matrix-net reduction used in HDP's proof of Theorem 4.4.3. -/
+/-- The standard `ε = 1/4` matrix-net reduction for the operator norm. -/
 lemma matrixOperatorNorm_le_two_mul_of_quarter_centered_bilinear_net {m n : ℕ} {u : ℝ}
     (A : Matrix (Fin m) (Fin n) ℝ) (N : CenteredMatrixBilinearNet m n (1 / 4))
     (hu : 0 ≤ u)
@@ -1046,7 +1046,7 @@ lemma matrixOperatorNorm_le_of_centered_quadratic_net {n : ℕ} {ε u : ℝ}
   have hmul' : M * (1 - 2 * ε) ≤ u := by nlinarith
   exact (le_div_iff₀ hden).mpr (by simpa [M] using hmul')
 
-/-- The standard `ε = 1/4` symmetric matrix-net reduction used in HDP Corollary 4.4.7. -/
+/-- The standard `ε = 1/4` matrix-net reduction for symmetric matrices. -/
 lemma matrixOperatorNorm_le_two_mul_of_quarter_centered_quadratic_net {n : ℕ} {u : ℝ}
     (A : Matrix (Fin n) (Fin n) ℝ) (hA_symm : A.IsSymm)
     (N : CenteredMatrixBilinearNet n n (1 / 4)) (hu : 0 ≤ u)
@@ -1482,7 +1482,7 @@ def HasSubGaussianVectorPsi2Bound {n : ℕ} (X : Ω → EuclideanSpace ℝ (Fin
     ∀ x : EuclideanSpace ℝ (Fin n), ‖x‖ = 1 →
       HasSubgaussianMGF (fun ω => inner ℝ (X ω) x) ⟨K ^ 2, sq_nonneg K⟩ μ
 
-/-- The HDP vector ψ₂ scale, defined as the infimum over admissible projection scales. -/
+/-- The vector ψ₂ scale, defined as the infimum over admissible projection scales. -/
 def subGaussianVectorPsi2Norm {n : ℕ} (X : Ω → EuclideanSpace ℝ (Fin n))
     (μ : Measure Ω) : ℝ :=
   sInf {K : ℝ | HasSubGaussianVectorPsi2Bound X μ K}
@@ -2027,7 +2027,7 @@ lemma hdpHansonWrightConstant_offdiag_quad :
   rfl
 
 omit [MeasurableSpace Ω] in
-/-- The absolute constant used in the vector norm lower tail for Exercise 4.42. -/
+/-- The absolute constant used in the vector norm lower tail. -/
 def randomVectorLowerTailConstant : ℝ :=
   1 / (64 * hdpHansonWrightConstant * exp 1 ^ 2)
 

StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean

@@ -157,7 +157,7 @@ lemma empiricalDist_triangle (n : ℕ) (x : Fin n → X) (g₁ g₂ g₃ : X →
 
 /-! ## Localized Ball Diameter Bound -/
 
-/-- **Lemma 5.1**: The diameter of a localized ball B_n(δ; H) is at most 2δ.
+/-- The diameter of a localized ball B_n(δ; H) is at most 2δ.
 
 For g₁, g₂ ∈ B_n(δ), we have:
 ‖g₁ - g₂‖_n ≤ ‖g₁‖_n + ‖g₂‖_n ≤ δ + δ = 2δ -/
@@ -176,7 +176,7 @@ lemma localizedBall_diam_bound (n : ℕ) (H : Set (X → ℝ)) (δ : ℝ) (x : F
     _ ≤ δ + δ := add_le_add hg₁_norm hg₂_norm
     _ = 2 * δ := by ring
 
-/-- **Lemma 5.1 (Metric.diam version)**: The diameter of the image of a localized ball
+/-- `Metric.diam` version: the diameter of the image of a localized ball
 under empiricalMetricImage is at most 2δ.
 
 This upgrades localizedBall_diam_bound from a pointwise bound to a Metric.diam statement. -/
@@ -1143,7 +1143,7 @@ lemma localizedBall_isStarShaped (n : ℕ) (H : Set (X → ℝ)) (δ : ℝ) (hδ
 
 /-- Local Gaussian complexity is bounded by entropy integral times (24√2)/√n.
 
-This is Lemma 5.2 from the plan: combines Dudley's bound with the |Z| ≤ 2·sup Z bound. -/
+Combines Dudley's bound with the |Z| ≤ 2·sup Z bound. -/
 lemma local_gaussian_complexity_bound (n : ℕ) (hn : 0 < n) (H : Set (X → ℝ))
     (δ : ℝ) (hδ : 0 < δ) (x : Fin n → X)
     (hH_star : IsStarShaped H)