From accc1ca7817c83ebb0aba1da4a9133ee7303e2aa Mon Sep 17 00:00:00 2001 From: tukamilano Date: Mon, 21 Sep 2026 11:37:22 +0900 Subject: [PATCH] remove unresolvable theorem number --- .../Concentration/LogSobolev/Bernoulli.lean | 2 +- StatsMLlib/Probability/Process/Dudley.lean | 20 +++++++++---------- .../Probability/Process/TruncatedDudley.lean | 4 ++-- .../Probability/RandomMatrix/Basic.lean | 12 +++++------ .../LeastSquares/LocalGaussianComplexity.lean | 6 +++--- 5 files changed, 22 insertions(+), 22 deletions(-) diff --git a/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean b/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean index 829332b..cf532ac 100644 --- a/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean +++ b/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 ε))²] diff --git a/StatsMLlib/Probability/Process/Dudley.lean b/StatsMLlib/Probability/Process/Dudley.lean index e746a0a..535ac13 100644 --- a/StatsMLlib/Probability/Process/Dudley.lean +++ b/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. -- ══════════════════════════════════════════════════════════════════════════════ diff --git a/StatsMLlib/Probability/Process/TruncatedDudley.lean b/StatsMLlib/Probability/Process/TruncatedDudley.lean index d05b041..679d9d4 100644 --- a/StatsMLlib/Probability/Process/TruncatedDudley.lean +++ b/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). -/ diff --git a/StatsMLlib/Probability/RandomMatrix/Basic.lean b/StatsMLlib/Probability/RandomMatrix/Basic.lean index d602af9..8dbd52e 100644 --- a/StatsMLlib/Probability/RandomMatrix/Basic.lean +++ b/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) diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean b/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean index 64fa81d..e2e5e16 100644 --- a/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean +++ b/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)