From e8ad5c422dde593d7cf1bc0edf0a0204d7fb5caf Mon Sep 17 00:00:00 2001
From: tukamilano <milanotukamoto@g.ecc.u-tokyo.ac.jp>
Date: Mon, 21 Sep 2026 15:01:51 +0900
Subject: [PATCH] remove duplicate theorem

---
 .../EmpiricalProcess/FunctionClass.lean       |  5 ++
 .../LearningTheory/Rademacher/Dudley.lean     |  1 +
 .../Rademacher/FiniteClass.lean               |  2 +
 .../Rademacher/LipschitzBall.lean             |  1 +
 .../Rademacher/LipschitzParameter.lean        |  2 +
 .../LearningTheory/Rademacher/OneStep.lean    |  1 +
 .../Concentration/HansonWright.lean           | 12 ----
 .../Probability/RandomMatrix/Basic.lean       | 21 ++----
 .../LeastSquares/Linear/MinimaxRate.lean      |  6 +-
 .../LeastSquares/LocalGaussianComplexity.lean | 65 ++++---------------
 .../LeastSquares/MasterErrorBound.lean        |  8 +--
 11 files changed, 36 insertions(+), 88 deletions(-)

diff --git a/StatsMLlib/LearningTheory/EmpiricalProcess/FunctionClass.lean b/StatsMLlib/LearningTheory/EmpiricalProcess/FunctionClass.lean
index 7370b28..a01eb27 100644
--- a/StatsMLlib/LearningTheory/EmpiricalProcess/FunctionClass.lean
+++ b/StatsMLlib/LearningTheory/EmpiricalProcess/FunctionClass.lean
@@ -26,6 +26,9 @@ metric structure are induced from StatsMLlib's canonical empirical space.
 
 universe v
 open scoped BigOperators
+
+namespace EmpiricalProcess.FunctionClass
+
 variable {𝒳 : Type v}
 variable {n : ℕ}
 
@@ -195,3 +198,5 @@ lemma empiricalFunctionSpace_totallyBounded [Fintype ι] :
       (Set.univ : Set (EmpiricalFunctionSpace F S)) :=
   Set.finite_univ.totallyBounded
 end
+
+end EmpiricalProcess.FunctionClass
diff --git a/StatsMLlib/LearningTheory/Rademacher/Dudley.lean b/StatsMLlib/LearningTheory/Rademacher/Dudley.lean
index f32bbb1..baa2a07 100644
--- a/StatsMLlib/LearningTheory/Rademacher/Dudley.lean
+++ b/StatsMLlib/LearningTheory/Rademacher/Dudley.lean
@@ -35,6 +35,7 @@ This module builds dyadic covers of `EmpiricalFunctionSpace` using `coveringFins
 universe v u
 open scoped BigOperators
 open Classical ProbabilityTheory
+open EmpiricalProcess.FunctionClass
 
 section Empirical
 variable {Z : Type v}
diff --git a/StatsMLlib/LearningTheory/Rademacher/FiniteClass.lean b/StatsMLlib/LearningTheory/Rademacher/FiniteClass.lean
index 4768b60..7b01af4 100644
--- a/StatsMLlib/LearningTheory/Rademacher/FiniteClass.lean
+++ b/StatsMLlib/LearningTheory/Rademacher/FiniteClass.lean
@@ -19,6 +19,7 @@ noncomputable section
 universe u v
 
 open MeasureTheory Real
+open EmpiricalProcess.FunctionClass
 
 variable {n : ℕ} {H : Type u} {𝒳 : Type v}
 
@@ -186,6 +187,7 @@ noncomputable section
 universe u v w
 
 open MeasureTheory ProbabilityTheory Real
+open EmpiricalProcess.FunctionClass
 open scoped ENNReal
 
 variable {n : ℕ}
diff --git a/StatsMLlib/LearningTheory/Rademacher/LipschitzBall.lean b/StatsMLlib/LearningTheory/Rademacher/LipschitzBall.lean
index a6742bb..13e6357 100644
--- a/StatsMLlib/LearningTheory/Rademacher/LipschitzBall.lean
+++ b/StatsMLlib/LearningTheory/Rademacher/LipschitzBall.lean
@@ -30,6 +30,7 @@ because the latter is dominated by the former on any sample.
 noncomputable section
 
 open MeasureTheory Real unitInterval ProbabilityTheory
+open EmpiricalProcess.FunctionClass
 
 namespace LipschitzBall
 
diff --git a/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean b/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean
index dc0732c..94300a1 100644
--- a/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean
+++ b/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean
@@ -21,6 +21,7 @@ noncomputable section
 universe u
 
 open MeasureTheory Real
+open EmpiricalProcess.FunctionClass
 
 variable {n : ℕ} {𝒳 : Type u}
 
@@ -369,6 +370,7 @@ noncomputable section
 universe u v
 
 open MeasureTheory ProbabilityTheory Real TopologicalSpace
+open EmpiricalProcess.FunctionClass
 open scoped ENNReal
 
 variable {n : ℕ}
diff --git a/StatsMLlib/LearningTheory/Rademacher/OneStep.lean b/StatsMLlib/LearningTheory/Rademacher/OneStep.lean
index 419d9c0..1657e59 100644
--- a/StatsMLlib/LearningTheory/Rademacher/OneStep.lean
+++ b/StatsMLlib/LearningTheory/Rademacher/OneStep.lean
@@ -31,6 +31,7 @@ noncomputable section
 universe u v
 
 open MeasureTheory Real
+open EmpiricalProcess.FunctionClass
 
 namespace ProbabilityTheory
 
diff --git a/StatsMLlib/Probability/Concentration/HansonWright.lean b/StatsMLlib/Probability/Concentration/HansonWright.lean
index 53bd67c..a787a35 100644
--- a/StatsMLlib/Probability/Concentration/HansonWright.lean
+++ b/StatsMLlib/Probability/Concentration/HansonWright.lean
@@ -3038,18 +3038,6 @@ lemma centeredQuadraticForm_eq_diagonal_add_offDiagonal {μ : Measure Ω}
   · intro i _
     exact hdiag_term_int i
 
-lemma hasSubgaussianMGF_mono_param {μ : Measure Ω} {X : Ω → ℝ} {c d : ℝ≥0}
-    (h : HasSubgaussianMGF X c μ) (hcd : (c : ℝ) ≤ d) :
-    HasSubgaussianMGF X d μ where
-  integrable_exp_mul t := h.integrable_exp_mul t
-  mgf_le t := by
-    have hmul : (c : ℝ) * t ^ 2 ≤ (d : ℝ) * t ^ 2 :=
-      mul_le_mul_of_nonneg_right hcd (sq_nonneg t)
-    calc
-      mgf X μ t ≤ exp ((c : ℝ) * t ^ 2 / 2) := h.mgf_le t
-      _ ≤ exp ((d : ℝ) * t ^ 2 / 2) := by
-          exact exp_le_exp.mpr (by linarith)
-
 /-- A finite independent linear combination of sub-Gaussian variables is sub-Gaussian. -/
 lemma hasSubgaussianMGF_finset_sum_const_mul_of_iIndepFun {ι : Type*} {μ : Measure Ω}
     {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {c : ι → ℝ≥0}
diff --git a/StatsMLlib/Probability/RandomMatrix/Basic.lean b/StatsMLlib/Probability/RandomMatrix/Basic.lean
index 8dbd52e..7d7241b 100644
--- a/StatsMLlib/Probability/RandomMatrix/Basic.lean
+++ b/StatsMLlib/Probability/RandomMatrix/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
 -/
 import StatsMLlib.Analysis.NormedSpace.CoveringNumber.Euclidean
+import StatsMLlib.LinearAlgebra.Matrix.SingularValue
 import StatsMLlib.Probability.Concentration.HansonWright
 import StatsMLlib.Probability.Independence.Grouping
 import StatsMLlib.Probability.Moments.Exponential
@@ -117,24 +118,12 @@ def sampleCovarianceDeviationOperatorNorm {m n : ℕ} (A : Matrix (Fin m) (Fin n
     ℝ :=
   matrixOperatorNorm (sampleCovarianceDeviation A)
 
-omit [MeasurableSpace Ω] in
-/-- The Euclidean linear map associated to `AᵀA` is `A† ∘ A`. -/
-lemma conjTranspose_mul_self_toEuclideanLin {m n : ℕ}
-    (A : Matrix (Fin m) (Fin n) ℝ) :
-    (A.conjTranspose * A).toEuclideanLin =
-      LinearMap.adjoint A.toEuclideanLin ∘ₗ A.toEuclideanLin := by
-  rw [← Matrix.toEuclideanLin_conjTranspose_eq_adjoint A]
-  simpa [Matrix.toEuclideanLin_eq_toLin_orthonormal] using Matrix.toLin_mul
-    (v₁ := (EuclideanSpace.basisFun (Fin n) ℝ).toBasis)
-    (v₂ := (EuclideanSpace.basisFun (Fin m) ℝ).toBasis)
-    (v₃ := (EuclideanSpace.basisFun (Fin n) ℝ).toBasis) A.conjTranspose A
-
 omit [MeasurableSpace Ω] in
 lemma inner_conjTranspose_mul_self_toEuclideanLin {m n : ℕ}
     (A : Matrix (Fin m) (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :
     inner ℝ ((A.conjTranspose * A).toEuclideanLin x) x =
       ‖A.toEuclideanLin x‖ ^ 2 := by
-  rw [conjTranspose_mul_self_toEuclideanLin]
+  rw [Matrix.conjTranspose_mul_self_toEuclideanLin]
   rw [LinearMap.comp_apply]
   rw [LinearMap.adjoint_inner_left]
   rw [real_inner_self_eq_norm_sq]
@@ -2226,7 +2215,7 @@ lemma upperTriangleQuadraticForm_hasSubgaussianMGF_of_norm_le_one {n : ℕ}
   have h :=
     upperTriangleQuadraticForm_hasSubgaussianMGF_explicit
       (A := A) (μ := μ) (K := K) h_indep hA_subG x
-  refine HansonWright.hasSubgaussianMGF_mono_param h ?_
+  refine hasSubgaussianMGF_mono_param h ?_
   change (((∑ p : UpperTriangleIndex n,
       Real.toNNReal (upperTriangleQuadraticCoeff x p ^ 2) *
         Real.toNNReal (K ^ 2)) : ℝ≥0) : ℝ) ≤ (2 * K) ^ 2
@@ -2268,7 +2257,7 @@ lemma inner_randomMatrix_hasSubgaussianMGF {m n : ℕ}
   have h :=
     inner_randomMatrix_hasSubgaussianMGF_explicit
       (A := A) (μ := μ) (K := K) h_indep hA_subG x y
-  refine HansonWright.hasSubgaussianMGF_mono_param h ?_
+  refine hasSubgaussianMGF_mono_param h ?_
   change (((∑ p : Fin m × Fin n,
       Real.toNNReal ((x p.2 * y p.1) ^ 2) * Real.toNNReal (K ^ 2)) : ℝ≥0) : ℝ) ≤
     K ^ 2 * ‖x‖ ^ 2 * ‖y‖ ^ 2
@@ -2287,7 +2276,7 @@ lemma inner_randomMatrix_hasSubgaussianMGF_of_norm_le_one {m n : ℕ}
   have h :=
     inner_randomMatrix_hasSubgaussianMGF (A := A) (μ := μ) (K := K)
       h_indep hA_subG x y
-  refine HansonWright.hasSubgaussianMGF_mono_param h ?_
+  refine hasSubgaussianMGF_mono_param h ?_
   change K ^ 2 * ‖x‖ ^ 2 * ‖y‖ ^ 2 ≤ K ^ 2
   have hx2 : ‖x‖ ^ 2 ≤ 1 := by
     nlinarith [norm_nonneg x, hx]
diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/Linear/MinimaxRate.lean b/StatsMLlib/Statistics/Regression/LeastSquares/Linear/MinimaxRate.lean
index ed649fb..e466cec 100644
--- a/StatsMLlib/Statistics/Regression/LeastSquares/Linear/MinimaxRate.lean
+++ b/StatsMLlib/Statistics/Regression/LeastSquares/Linear/MinimaxRate.lean
@@ -138,7 +138,7 @@ lemma linear_localizedBall_nonempty {δ : ℝ} (hδ : 0 ≤ δ)
       ext i; rfl
     rw [h_eq]
     have h_zero : empiricalNorm n (fun _ : Fin n => (0 : ℝ)) = 0 := by
-      unfold empiricalNorm
+      unfold EmpiricalProcess.empiricalNorm
       simp only [sq, mul_zero, sum_const_zero, mul_zero, Real.sqrt_zero]
     rw [h_zero]
     exact hδ
@@ -149,7 +149,7 @@ lemma empiricalNorm_smul_linear
     {c : ℝ} (hc : 0 ≤ c) :
     empiricalNorm n (fun i => c * @inner ℝ _ _ θ (x i)) =
     c * empiricalNorm n (fun i => @inner ℝ _ _ θ (x i)) := by
-  unfold empiricalNorm
+  unfold EmpiricalProcess.empiricalNorm
   have h_sq : ∀ i, (c * @inner ℝ _ _ θ (x i))^2 = c^2 * (@inner ℝ _ _ θ (x i))^2 := by
     intro i; ring
   simp_rw [h_sq]
@@ -267,7 +267,7 @@ lemma linear_bddAbove_at_radius (hn : 0 < n)
           apply mul_le_mul_of_nonneg_left _ (norm_nonneg w')
           -- ‖hx‖ ≤ √n · u from empiricalNorm h ≤ u
           have h_emp : empiricalNorm n (fun i => h (x i)) ≤ u := hh_norm
-          unfold empiricalNorm at h_emp
+          unfold EmpiricalProcess.empiricalNorm at h_emp
           have h_hx_norm : ‖hx‖ = Real.sqrt (∑ i, (h (x i))^2) := by
             simp only [hx, EuclideanSpace.norm_eq]
             congr 1
diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean b/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean
index e2e5e16..9fe1c8f 100644
--- a/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean
+++ b/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
 -/
 import Mathlib
+import StatsMLlib.LearningTheory.EmpiricalProcess.FunctionClass
 import StatsMLlib.Statistics.Regression.LeastSquares.Defs
 import StatsMLlib.Statistics.Regression.LeastSquares.SubGaussianity
 import StatsMLlib.Probability.Process.Dudley
@@ -19,7 +20,6 @@ of empirical processes over function classes.
 ## Main definitions
 
 * `evalAtSample`: Evaluation map embedding functions into finite-dimensional space
-* `empiricalDist`: Pseudo-metric on functions induced by empirical norm
 * `innerProductProcess`: The Gaussian process Z_v(w) = (1/n) Σᵢ wᵢvᵢ
 * `euclideanNorm`: L2 norm on Fin n → ℝ
 
@@ -65,31 +65,6 @@ This is the key embedding into the metric space structure. -/
 def evalAtSample (n : ℕ) (x : Fin n → X) (g : X → ℝ) : Fin n → ℝ :=
   fun i => g (x i)
 
-/-- The empirical distance between two functions is the empirical norm of their difference -/
-noncomputable def empiricalDist (n : ℕ) (x : Fin n → X) (g₁ g₂ : X → ℝ) : ℝ :=
-  empiricalNorm n (fun i => g₁ (x i) - g₂ (x i))
-
-/-- Empirical distance is non-negative -/
-lemma empiricalDist_nonneg (n : ℕ) (x : Fin n → X) (g₁ g₂ : X → ℝ) :
-    0 ≤ empiricalDist n x g₁ g₂ :=
-  empiricalNorm_nonneg n _
-
-/-- Empirical distance is symmetric -/
-lemma empiricalDist_comm (n : ℕ) (x : Fin n → X) (g₁ g₂ : X → ℝ) :
-    empiricalDist n x g₁ g₂ = empiricalDist n x g₂ g₁ := by
-  unfold empiricalDist empiricalNorm
-  congr 1
-  apply congr_arg
-  congr 1
-  ext i
-  ring
-
-/-- Empirical distance from a function to itself is zero -/
-lemma empiricalDist_self (n : ℕ) (x : Fin n → X) (g : X → ℝ) :
-    empiricalDist n x g g = 0 := by
-  unfold empiricalDist empiricalNorm
-  simp only [sub_self, sq, mul_zero, sum_const_zero, mul_zero, Real.sqrt_zero]
-
 /-- Norm on EuclideanSpace in terms of sum of squares -/
 lemma euclidean_norm_sq (n : ℕ) (a : EuclideanSpace ℝ (Fin n)) :
     ‖a‖ = Real.sqrt (∑ i : Fin n, (a i)^2) := by
@@ -123,7 +98,7 @@ lemma empiricalNorm_add_le (n : ℕ) (a b : Fin n → ℝ) :
 /-- Triangle inequality: ‖a - b‖ ≤ ‖a‖ + ‖b‖ for empirical norm -/
 lemma empiricalNorm_sub_le (n : ℕ) (a b : Fin n → ℝ) :
     empiricalNorm n (fun i => a i - b i) ≤ empiricalNorm n a + empiricalNorm n b := by
-  unfold empiricalNorm
+  unfold EmpiricalProcess.empiricalNorm
   by_cases hn : n = 0
   · simp [hn]
   have hn_pos : (0 : ℝ) < n := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)
@@ -141,20 +116,6 @@ lemma empiricalNorm_sub_le (n : ℕ) (a b : Fin n → ℝ) :
   rw [ha_norm, hb_norm, hab_norm]
   exact norm_sub_le a' b'
 
-/-- Empirical distance satisfies triangle inequality -/
-lemma empiricalDist_triangle (n : ℕ) (x : Fin n → X) (g₁ g₂ g₃ : X → ℝ) :
-    empiricalDist n x g₁ g₃ ≤ empiricalDist n x g₁ g₂ + empiricalDist n x g₂ g₃ := by
-  unfold empiricalDist empiricalNorm
-  -- Key: (g₁ - g₃) = (g₁ - g₂) + (g₂ - g₃), so use Minkowski
-  have h_sum_eq : ∑ i : Fin n, (g₁ (x i) - g₃ (x i))^2 =
-      ∑ i : Fin n, ((g₁ (x i) - g₂ (x i)) + (g₂ (x i) - g₃ (x i)))^2 := by
-    apply Finset.sum_congr rfl
-    intro i _
-    congr 1
-    ring
-  rw [h_sum_eq]
-  exact empiricalNorm_add_le n (fun i => g₁ (x i) - g₂ (x i)) (fun i => g₂ (x i) - g₃ (x i))
-
 /-! ## Localized Ball Diameter Bound -/
 
 /-- The diameter of a localized ball B_n(δ; H) is at most 2δ.
@@ -163,14 +124,14 @@ For g₁, g₂ ∈ B_n(δ), we have:
 ‖g₁ - g₂‖_n ≤ ‖g₁‖_n + ‖g₂‖_n ≤ δ + δ = 2δ -/
 lemma localizedBall_diam_bound (n : ℕ) (H : Set (X → ℝ)) (δ : ℝ) (x : Fin n → X)
     (g₁ g₂ : X → ℝ) (hg₁ : g₁ ∈ localizedBall H δ x) (hg₂ : g₂ ∈ localizedBall H δ x) :
-    empiricalDist n x g₁ g₂ ≤ 2 * δ := by
+    EmpiricalProcess.FunctionClass.empiricalDist x g₁ g₂ ≤ 2 * δ := by
   -- g₁ ∈ B_n(δ) means ‖g₁‖_n ≤ δ
   -- g₂ ∈ B_n(δ) means ‖g₂‖_n ≤ δ
   have hg₁_norm : empiricalNorm n (fun i => g₁ (x i)) ≤ δ := hg₁.2
   have hg₂_norm : empiricalNorm n (fun i => g₂ (x i)) ≤ δ := hg₂.2
   -- By triangle inequality: ‖g₁ - g₂‖_n ≤ ‖g₁‖_n + ‖g₂‖_n ≤ 2δ
-  unfold empiricalDist
-  calc empiricalNorm n (fun i => g₁ (x i) - g₂ (x i))
+  show EmpiricalProcess.empiricalNorm n (fun i => g₁ (x i) - g₂ (x i)) ≤ 2 * δ
+  calc EmpiricalProcess.empiricalNorm n (fun i => g₁ (x i) - g₂ (x i))
       ≤ empiricalNorm n (fun i => g₁ (x i)) + empiricalNorm n (fun i => g₂ (x i)) :=
         empiricalNorm_sub_le n (fun i => g₁ (x i)) (fun i => g₂ (x i))
     _ ≤ δ + δ := add_le_add hg₁_norm hg₂_norm
@@ -190,9 +151,7 @@ lemma localizedBall_diam (n : ℕ) (H : Set (X → ℝ)) (δ : ℝ) (hδ : 0 ≤
   -- dist(v₁, v₂) = empiricalDist n x g₁ g₂
   rw [dist_empiricalMetricImage]
   -- Use the pointwise bound
-  have h := localizedBall_diam_bound n H δ x g₁ g₂ hg₁ hg₂
-  unfold empiricalDist at h
-  exact h
+  exact localizedBall_diam_bound n H δ x g₁ g₂ hg₁ hg₂
 
 /-! ## Sub-Gaussian Bridge to EmpiricalSpace -/
 
@@ -301,7 +260,7 @@ lemma empiricalProcess_smul (n : ℕ) (x : Fin n → X) (α : ℝ) (g : X → 
 /-- Empirical norm scales by absolute value of the scalar -/
 lemma empiricalNorm_smul (n : ℕ) (α : ℝ) (f : Fin n → ℝ) :
     empiricalNorm n (α • f) = |α| * empiricalNorm n f := by
-  unfold empiricalNorm
+  unfold EmpiricalProcess.empiricalNorm
   simp only [Pi.smul_apply, smul_eq_mul, mul_pow]
   rw [← Finset.mul_sum]
   have h_rearrange : (n : ℝ)⁻¹ * (α ^ 2 * ∑ i, f i ^ 2) = α ^ 2 * ((n : ℝ)⁻¹ * ∑ i, f i ^ 2) := by
@@ -342,7 +301,7 @@ lemma zero_mem_localizedBall_of_starShaped (n : ℕ) (H : Set (X → ℝ)) (δ :
   · exact hH.1  -- 0 ∈ H from star-shaped property
   · -- ‖0‖_n = 0 ≤ δ
     simp only [Pi.zero_apply]
-    unfold empiricalNorm
+    unfold EmpiricalProcess.empiricalNorm
     simp only [sq, mul_zero, sum_const_zero, mul_zero, Real.sqrt_zero]
     exact hδ
 
@@ -429,7 +388,7 @@ lemma empiricalProcess_le_delta_norm (n : ℕ) (hn : 0 < n) (x : Fin n → X) (H
     inner_abs_le_norm_mul_norm' n w gx
   -- euclideanNorm gx = √(Σ gᵢ²), and empiricalNorm = √(n⁻¹ Σ gᵢ²), so euclideanNorm = √n * empiricalNorm
   have h_norm_gx_sq : (euclideanNorm n gx)^2 = n * (empiricalNorm n gx)^2 := by
-    unfold euclideanNorm empiricalNorm
+    unfold euclideanNorm EmpiricalProcess.empiricalNorm
     rw [sq_sqrt, sq_sqrt]
     · ring_nf
       rw [mul_inv_cancel₀ hn_ne, one_mul]
@@ -626,7 +585,7 @@ lemma gaussian_complexity_ratio_antitone (n : ℕ) (H : Set (X → ℝ)) (x : Fi
                   (√n * empiricalNorm n (fun i => g (x i))) := by
                 have heq : ∀ f : Fin n → ℝ, √(∑ i : Fin n, f i ^ 2) = √n * empiricalNorm n f := by
                   intro f
-                  unfold empiricalNorm
+                  unfold EmpiricalProcess.empiricalNorm
                   symm
                   calc √n * √((n : ℝ)⁻¹ * ∑ i : Fin n, f i ^ 2)
                       = √n * (√((n : ℝ)⁻¹) * √(∑ i : Fin n, f i ^ 2)) := by
@@ -830,7 +789,7 @@ lemma EmpiricalSpace.coord_sq_le (n : ℕ) (i : Fin n) (v : EmpiricalSpace n) :
     (v i)^2 ≤ n * (empiricalNorm n v)^2 := by
   have hn_pos : 0 < n := Fin.pos i
   have hn_ne : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn_pos)
-  unfold empiricalNorm
+  unfold EmpiricalProcess.empiricalNorm
   rw [sq_sqrt (by positivity : 0 ≤ (n : ℝ)⁻¹ * ∑ j : Fin n, (v j)^2)]
   have h_single : (v i : ℝ)^2 ≤ ∑ j : Fin n, (v j : ℝ)^2 := by
     exact Finset.single_le_sum (f := fun j => (v j : ℝ)^2) (fun j _ => sq_nonneg _) (Finset.mem_univ i)
@@ -1047,7 +1006,7 @@ lemma dudley_empiricalProcess (n : ℕ) (hn : 0 < n) (x : Fin n → X)
       have h_sum_sq : ∑ i, (g (x i))^2 ≤ n * D^2 := by
         have h1 : empiricalNorm n (fun i => g (x i)) = Real.sqrt ((n : ℝ)⁻¹ * ∑ i, (g (x i))^2) := rfl
         have h_norm_nonneg : 0 ≤ empiricalNorm n (fun i => g (x i)) := by
-          unfold empiricalNorm
+          unfold EmpiricalProcess.empiricalNorm
           positivity
         have h2 : (empiricalNorm n (fun i => g (x i)))^2 ≤ D^2 := by
           apply sq_le_sq'
diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/MasterErrorBound.lean b/StatsMLlib/Statistics/Regression/LeastSquares/MasterErrorBound.lean
index 0cc9298..035144a 100644
--- a/StatsMLlib/Statistics/Regression/LeastSquares/MasterErrorBound.lean
+++ b/StatsMLlib/Statistics/Regression/LeastSquares/MasterErrorBound.lean
@@ -69,7 +69,7 @@ constant sup_g ‖(σ/n) g(x₁,...,xₙ)‖₂ = σu/√n when restricted to 
 /-- The Euclidean norm of g(x₁,...,xₙ) equals √n · ‖g‖_n. -/
 lemma euclidean_norm_eq_sqrt_n_mul_empiricalNorm (hn : 0 < n) (g : X → ℝ) (x : Fin n → X) :
     Real.sqrt (∑ i, (g (x i))^2) = Real.sqrt n * empiricalNorm n (fun i => g (x i)) := by
-  unfold empiricalNorm
+  unfold EmpiricalProcess.empiricalNorm
   have hn_pos : (0 : ℝ) < n := Nat.cast_pos.mpr hn
   have hn_ne : (n : ℝ) ≠ 0 := ne_of_gt hn_pos
   -- RHS = √n * √(n⁻¹ * ∑ g²) = √(n * (n⁻¹ * ∑ g²)) = √(∑ g²) = LHS
@@ -441,7 +441,7 @@ lemma Z_le_sigma_mul_localComplexity (n : ℕ) (hn : 0 < n) (σ : ℝ) (H : Set
             · exact Real.sum_mul_le_sqrt_mul_sqrt Finset.univ w (fun i => h (x i))
           have h_norm : Real.sqrt (∑ i, (h (x i))^2) ≤ Real.sqrt n * u := by
             have hh_norm := hh.2
-            rw [empiricalNorm] at hh_norm
+            rw [EmpiricalProcess.empiricalNorm] at hh_norm
             -- From √((n⁻¹) * ∑ h(x)²) ≤ u, we get ∑ h(x)² ≤ n * u²
             have h_sum_nonneg : 0 ≤ ∑ i, (h (x i))^2 := Finset.sum_nonneg (fun i _ => sq_nonneg _)
             have h_sqrt_nonneg : 0 ≤ Real.sqrt ((n : ℝ)⁻¹ * ∑ i, (h (x i))^2) := Real.sqrt_nonneg _
@@ -688,7 +688,7 @@ theorem bad_event_probability_bound (hn : 0 < n) {σ δ_star u : ℝ}
       exact hsmul
     -- ‖g'‖_n = u
     have hg'_norm : empiricalNorm n (fun i => g' (x i)) = u := by
-      unfold empiricalNorm
+      unfold EmpiricalProcess.empiricalNorm
       have h_sum : ∑ k, (g' (x k))^2 = α^2 * ∑ k, (g (x k))^2 := by
         simp only [hg'_def, mul_pow]
         rw [Finset.mul_sum]
@@ -741,7 +741,7 @@ theorem bad_event_probability_bound (hn : 0 < n) {σ δ_star u : ℝ}
                 · exact Real.sum_mul_le_sqrt_mul_sqrt Finset.univ w (fun i => h (x i))
               have h_norm_eq : Real.sqrt (∑ i, (h (x i))^2) = Real.sqrt n * u := by
                 have hh_norm := hh.2
-                rw [empiricalNorm] at hh_norm
+                rw [EmpiricalProcess.empiricalNorm] at hh_norm
                 have h_sum : ∑ i, (h (x i))^2 = n * u^2 := by
                   have h_inner_nonneg : 0 ≤ (n : ℝ)⁻¹ * ∑ i, (h (x i))^2 := by positivity
                   have h_eq : (n : ℝ)⁻¹ * ∑ i, (h (x i))^2 = u^2 := by