From f915b2acaaae30d0717013d28f556b30ba334d0f Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 17 Oct 2026 08:03:03 +0000 Subject: [PATCH] perf(FormalLearningTheory): simplify growth and minimax proofs --- .../Complexity/FiniteSupportUC.lean | 12 +++--- .../Complexity/Rademacher.lean | 28 ++++++++----- .../Complexity/Symmetrization.lean | 42 +++++++++++++++---- .../PureMath/ApproxMinimax.lean | 26 +++++------- 4 files changed, 68 insertions(+), 40 deletions(-) diff --git a/LeanPool/FormalLearningTheory/Complexity/FiniteSupportUC.lean b/LeanPool/FormalLearningTheory/Complexity/FiniteSupportUC.lean index b6e8bec46b..99c134b79e 100644 --- a/LeanPool/FormalLearningTheory/Complexity/FiniteSupportUC.lean +++ b/LeanPool/FormalLearningTheory/Complexity/FiniteSupportUC.lean @@ -326,7 +326,8 @@ theorem finite_support_vc_approx ne_top_of_le_ne_top (by simp [measure_univ]) (measure_mono (Set.subset_univ _)) have h1 := MeasureTheory.measure_compl (DiscreteMeasurableSpace.forall_measurableSet _) hfin - simp_all + rw [h1, measure_univ] + exact tsub_pos_of_lt hbad_lt_one -- Sub-step 2: Witness extraction with all-Sum.inl guarantee -- D = PMF.toMeasure (μ.toPMF.map Sum.inl) is supported on range Sum.inl. -- So the product measure is supported on {xs | ∀ i, xs i ∈ range Sum.inl}. @@ -359,7 +360,7 @@ theorem finite_support_vc_approx have hsub : allInlᶜ ⊆ ⋃ i : Fin Tnat, {xs | xs i ∉ Set.range Sum.inl} := by intro xs hxs simp only [allInl, Set.mem_compl_iff, Set.mem_ofPred_eq, not_forall] at hxs - simp_all + simpa only [Set.mem_iUnion, Set.mem_ofPred_eq] using hxs have hzero : ∀ i : Fin Tnat, Measure.pi (fun _ => D) {xs | xs i ∉ Set.range Sum.inl} = 0 := by intro i @@ -391,12 +392,13 @@ theorem finite_support_vc_approx _ ≤ Measure.pi (fun _ => D) (badᶜ ∩ allInl) + Measure.pi (fun _ => D) allInlᶜ := MeasureTheory.measure_union_le _ _ - simp_all + exact (not_le_of_gt hcompl_pos) + (by simpa only [h0, hallInl_compl_zero, add_zero] using this) -- Extract witness from badᶜ ∩ allInl have hne : (badᶜ ∩ allInl).Nonempty := by by_contra h rw [Set.not_nonempty_iff_eq_empty] at h - simp_all + exact (ne_of_gt hinter_pos) (by rw [h, measure_empty]) obtain ⟨xs, hxs_good, hxs_inl⟩ := hne -- hxs_good : xs ∈ badᶜ, i.e., xs ∉ bad have hxs_not_bad : xs ∉ bad := hxs_good @@ -422,7 +424,7 @@ theorem finite_support_vc_approx congr 1 apply Finset.sum_congr rfl; intro i _ simp only [zeroOneLoss, hhs_eq i, extendBool] - split_ifs <;> simp_all + cases a (hs i) <;> rfl rw [htrue_eq] at hdev rw [hemp_eq] at hdev rw [← boolTestExpectation_empirical_eq_avg hTpos hs a] at hdev diff --git a/LeanPool/FormalLearningTheory/Complexity/Rademacher.lean b/LeanPool/FormalLearningTheory/Complexity/Rademacher.lean index 62e1fd67bc..8d396b442b 100644 --- a/LeanPool/FormalLearningTheory/Complexity/Rademacher.lean +++ b/LeanPool/FormalLearningTheory/Complexity/Rademacher.lean @@ -673,12 +673,14 @@ private theorem ncard_restrictions_le_sum_choose_set {X : Type u} simp [Finset.mem_inter, Finset.mem_filter, hy'T] have h2 : (⟨y', hy'S⟩ : ↥S) ∈ t_sub ↔ g' ⟨y', hy'S⟩ = true := by simp [t_sub, Finset.mem_filter, hy'T] - simp_all + rw [hTA] at h1 + exact h1.symm.trans h2 -- g' ⟨y', hy'S⟩ = g ⟨y', hyTval⟩ since y' ∈ Tval have h_g'_eq : g' ⟨y', hy'S⟩ = g ⟨y', hyTval⟩ := by simp only [g', dite_eq_left hyTval] -- Combine: c y' = f ⟨y',hy'S⟩ and f = true ↔ g = true - simp_all + rw [hcf_y, ← h_g'_eq] + exact Bool.eq_iff_iff.mpr h_f_iff_g' -- Step 5: Fintype.card ↥S = S.card have h5 : Fintype.card ↥S = S.card := Fintype.card_coe S -- Combine @@ -1600,13 +1602,14 @@ private theorem analytical_log_sqrt_bound (d m : ℕ) (ε : ℝ) have h_mid : 2 / t + 2 * Real.log t / t ≤ 2 / t + 4 / Real.sqrt t := by have : 2 * Real.log t / t ≤ 4 * Real.sqrt t / t := by apply div_le_div_of_nonneg_right _ (le_of_lt ht_pos) - nlinarith [h_log_t_bound, Real.sqrt_nonneg t] + linarith only [h_log_t_bound] have h_sq : 4 * Real.sqrt t / t = 4 / Real.sqrt t := by rw [div_eq_div_iff (ne_of_gt ht_pos) (ne_of_gt (Real.sqrt_pos.mpr ht_pos))] -- Goal: 4 * √t * √t = 4 * t rw [show 4 * Real.sqrt t * Real.sqrt t = 4 * (Real.sqrt t * Real.sqrt t) by ring] rw [Real.mul_self_sqrt (le_of_lt ht_pos)] - linarith [this, h_sq.symm.le] + rw [h_sq] at this + exact add_le_add (le_refl _) this -- Need: 2/t + 4/√t < ε². -- From t > 32/ε⁴: 2/t < ε⁴/16 and 4/√t < 4ε²/√32 = ε²/√2. -- Total < ε⁴/16 + ε²/√2 < ε² (since ε ≤ 1 and 1 / 16 + 1/√2 < 1). @@ -1619,7 +1622,7 @@ private theorem analytical_log_sqrt_bound (d m : ℕ) (ε : ℝ) ≤ ↑(⌈32 * (↑d + 1) / ε ^ 4⌉₊) := Nat.le_ceil _ _ < (m : ℝ) := by exact_mod_cast (by omega : ⌈32 * ((d : ℝ) + 1) / ε ^ 4⌉₊ < m) rw [div_lt_iff₀ hε4_pos] at hceil - nlinarith + linarith only [hceil] -- Bound 4/√t: √t > 4√2/ε² (since t > 32/ε⁴), so 4/√t < ε²/√2 have h_sqrt_t_lower : 4 * Real.sqrt 2 / ε ^ 2 < Real.sqrt t := by rw [Real.lt_sqrt (by positivity)] @@ -1639,14 +1642,17 @@ private theorem analytical_log_sqrt_bound (d m : ℕ) (ε : ℝ) -- Need: 2 * 16 = 32 < ε² * t -- From h_t_large: 32 / ε⁴ < t, so ε² * (32 / ε⁴) < ε² * t -- ε² * (32 / ε⁴) = 32 / ε², and 32 / ε² ≥ 32 (since ε² ≤ 1) - have hε2_le : ε ^ 2 ≤ 1 := by nlinarith [_hε1] + have hε2_le : ε ^ 2 ≤ 1 := by nlinarith only [hε, _hε1] have h1 : ε ^ 2 * (32 / ε ^ 4) < ε ^ 2 * t := mul_lt_mul_of_pos_left h_t_large hε2_pos have h2 : ε ^ 2 * (32 / ε ^ 4) = 32 / ε ^ 2 := by field_simp have h3 : (32 : ℝ) ≤ 32 / ε ^ 2 := by - rw [le_div_iff₀ hε2_pos]; nlinarith - linarith + rw [le_div_iff₀ hε2_pos] + linarith only [hε2_le] + calc 2 * 16 = (32 : ℝ) := by norm_num + _ ≤ 32 / ε ^ 2 := h3 + _ < ε ^ 2 * t := h2 ▸ h1 -- ε²/16 + ε²/√2 < ε²: show 1 / 16 + 1/√2 < 1 -- √2 > 4 / 3, so 1/√2 < 3 / 4, so 1 / 16 + 1/√2 < 1 / 16 + 3 / 4 = 13 / 16 < 1 have h_sqrt2_bound : (4 : ℝ) / 3 < Real.sqrt 2 := by @@ -1654,9 +1660,11 @@ private theorem analytical_log_sqrt_bound (d m : ℕ) (ε : ℝ) norm_num have h_inv_sqrt2 : ε ^ 2 / Real.sqrt 2 < 3 * ε ^ 2 / 4 := by rw [div_lt_div_iff₀ (Real.sqrt_pos.mpr (by norm_num : (0:ℝ) < 2)) (by norm_num : (0:ℝ) < 4)] - nlinarith [h_sqrt2_bound] + calc ε ^ 2 * 4 = (3 * ε ^ 2) * (4 / 3) := by ring + _ < (3 * ε ^ 2) * Real.sqrt 2 := + mul_lt_mul_of_pos_left h_sqrt2_bound (by positivity) -- Combine: 2/t + 4/√t < ε²/16 + ε²/√2 < ε²/16 + 3ε²/4 = 13ε²/16 < ε² - linarith [h_mid, h_2_over_t, h_4_over_sqrt, h_inv_sqrt2] + linarith only [h_mid, h_2_over_t, h_4_over_sqrt, h_inv_sqrt2, hε2_pos] /-- VCDim finite → Rademacher vanishes uniformly. The bound m₀ depends only on d and ε, NOT on D. -/ diff --git a/LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean b/LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean index 9c0cb89a2f..af5962508f 100644 --- a/LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean +++ b/LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean @@ -1483,8 +1483,9 @@ private lemma growth_exp_le_delta_large_v {X : Type u} have hgf_cast : (↑(GrowthFunction X C (2 * m)) : ℝ) ≤ (2 : ℝ) ^ (2 * m) := by exact_mod_cast hgf_trivial rw [ht_def] - nlinarith [hgf_cast, hexp_le, Real.exp_pos (-(↑m * ε ^ 2 / 8)), - show 0 < ↑((v + 1).factorial) / t ^ (v + 1) by positivity] + exact mul_le_mul + (mul_le_mul_of_nonneg_left hgf_cast (by norm_num)) hexp_le + (Real.exp_pos (-(↑m * ε ^ 2 / 8))).le (by positivity) suffices hchain2 : 4 * (2 : ℝ) ^ (2 * m) * ↑((v + 1).factorial) ≤ δ * t ^ (v + 1) by have ht_pow_pos := pow_pos ht_pos (v + 1) have hdiv : 4 * (2 : ℝ) ^ (2 * m) * ↑((v + 1).factorial) / t ^ (v + 1) ≤ δ := by @@ -1521,7 +1522,11 @@ private lemma growth_exp_le_delta_large_v {X : Type u} rw [div_le_div_iff_of_pos_right (pow_pos (by norm_num : (0:ℝ) < 8) (v + 1))] have hstep1 : 4 * (2 : ℝ) ^ (2 * m) * ↑((v + 1).factorial) * (8 : ℝ) ^ (v + 1) ≤ (16 : ℝ) ^ (v + 1) * (↑v + 1) ^ (v + 1) := by - nlinarith [h_pow_bound, hfact_le, pow_pos (show (0:ℝ) < 16 by norm_num) (v + 1)] + calc 4 * (2 : ℝ) ^ (2 * m) * ↑((v + 1).factorial) * (8 : ℝ) ^ (v + 1) + = (4 * (2 : ℝ) ^ (2 * m) * (8 : ℝ) ^ (v + 1)) * ↑((v + 1).factorial) := by + ring + _ ≤ (16 : ℝ) ^ (v + 1) * (↑v + 1) ^ (v + 1) := + mul_le_mul h_pow_bound hfact_le (Nat.cast_nonneg _) (by positivity) have hstep2 : (16 : ℝ) ^ (v + 1) * (↑v + 1) ^ (v + 1) ≤ (16 * Real.exp 1 * (↑v + 1)) ^ (v + 1) * ↑m ^ v := by rw [mul_pow, mul_pow] @@ -1529,7 +1534,12 @@ private lemma growth_exp_le_delta_large_v {X : Type u} one_le_mul_of_one_le_of_one_le hexp_pow_ge_1 hm_pow_ge_1 have h16pos := pow_pos (show (0:ℝ) < 16 by norm_num) (v + 1) have hv1pos := pow_pos hv1_pos (v + 1) - nlinarith [mul_le_mul_of_nonneg_left h1 (mul_nonneg (le_of_lt h16pos) (le_of_lt hv1pos))] + calc (16 : ℝ) ^ (v + 1) * (↑v + 1) ^ (v + 1) + ≤ ((16 : ℝ) ^ (v + 1) * (↑v + 1) ^ (v + 1)) * + (Real.exp 1 ^ (v + 1) * ↑m ^ v) := + le_mul_of_one_le_right (mul_nonneg h16pos.le hv1pos.le) h1 + _ = (16 : ℝ) ^ (v + 1) * Real.exp 1 ^ (v + 1) * + (↑v + 1) ^ (v + 1) * ↑m ^ v := by ring have hstep3 : (16 * Real.exp 1 * (↑v + 1)) ^ (v + 1) * ↑m ^ v ≤ δ * ↑m ^ (v + 1) * (ε ^ 2) ^ (v + 1) := by have hmul : ↑m ^ v * (16 * Real.exp 1 * (↑v + 1)) ^ (v + 1) ≤ @@ -1607,8 +1617,10 @@ theorem growth_exp_le_delta {X : Type u} le_trans (by linarith) (mul_le_mul_of_nonneg_left hv_pow_ge_1 (Real.exp_pos 1).le) have hkey : 2 * ↑((v + 1).factorial) ≤ Real.exp 1 * ↑v ^ v * (↑v + 1) ^ (v + 1) := by - nlinarith [hfact_le, h_2_le_ev, Nat.cast_nonneg (α := ℝ) ((v + 1).factorial), - pow_pos hv1_pos (v + 1)] + calc 2 * (↑((v + 1).factorial) : ℝ) ≤ 2 * (↑v + 1) ^ (v + 1) := + mul_le_mul_of_nonneg_left hfact_le (by norm_num) + _ ≤ Real.exp 1 * ↑v ^ v * (↑v + 1) ^ (v + 1) := + mul_le_mul_of_nonneg_right h_2_le_ev (pow_nonneg hv1_pos.le _) have hKeps : K * ε ^ 2 * ↑v ^ (v + 1) = 16 * Real.exp 1 * ↑v ^ v := by have : K * (↑v * ε ^ 2) = 16 * Real.exp 1 := by rw [hK_def] @@ -1617,7 +1629,9 @@ theorem growth_exp_le_delta {X : Type u} = K * (↑v * ε ^ 2) * ↑v ^ v := by rw [pow_succ]; ring _ = 16 * Real.exp 1 * ↑v ^ v := by rw [this] have hstepA : 32 * ↑((v + 1).factorial) ≤ - K * ε ^ 2 * ↑v ^ (v + 1) * (↑v + 1) ^ (v + 1) := by nlinarith [hkey, hKeps] + K * ε ^ 2 * ↑v ^ (v + 1) * (↑v + 1) ^ (v + 1) := by + rw [hKeps] + linarith only [hkey] have hstepB : K * ε ^ 2 * ↑v ^ (v + 1) * (↑v + 1) ^ (v + 1) * K ^ v ≤ ε ^ 2 * (↑m * δ) := by have : K * ε ^ 2 * ↑v ^ (v + 1) * (↑v + 1) ^ (v + 1) * K ^ v = @@ -1652,7 +1666,7 @@ theorem growth_exp_le_delta {X : Type u} · -- Part 2: 2 * log 2 ≤ m * ε² have hlog2_le_1 : Real.log 2 ≤ 1 := by rw [Real.log_le_iff_le_exp (by norm_num : (0 : ℝ) < 2)]; linarith - suffices h : 2 ≤ ↑m * ε ^ 2 by nlinarith + suffices h : 2 ≤ ↑m * ε ^ 2 by linarith only [h, hlog2_le_1] by_cases hcase : ε ^ 2 ≤ 16 * Real.exp 1 * (↑v + 1) · have hbase_ge_1 : 1 ≤ 16 * Real.exp 1 * (↑v + 1) / ε ^ 2 := by rw [le_div_iff₀ hε2]; linarith @@ -1662,7 +1676,17 @@ theorem growth_exp_le_delta {X : Type u} have : 16 * Real.exp 1 * (↑v + 1) / ε ^ 2 ≤ ↑m * δ := by linarith [hm_delta] have : 16 * Real.exp 1 * (↑v + 1) ≤ ↑m * δ * ε ^ 2 := by rwa [div_le_iff₀ hε2] at this - nlinarith + have hconstant : (2 : ℝ) ≤ 16 * Real.exp 1 * (↑v + 1) := by + calc (2 : ℝ) ≤ 16 * 2 * 2 := by norm_num + _ ≤ 16 * Real.exp 1 * (↑v + 1) := + mul_le_mul (mul_le_mul_of_nonneg_left he_ge_2 (by norm_num)) + hv1_ge_2 (by norm_num) (by positivity) + have hscaled : (↑m : ℝ) * δ * ε ^ 2 ≤ ↑m * ε ^ 2 := by + calc (↑m : ℝ) * δ * ε ^ 2 = (↑m * ε ^ 2) * δ := by ring + _ ≤ (↑m * ε ^ 2) * 1 := + mul_le_mul_of_nonneg_left hδ1.le (by positivity) + _ = ↑m * ε ^ 2 := mul_one _ + exact hconstant.trans (this.trans hscaled) · push Not at hcase have hm_ge_1 : (1 : ℝ) ≤ ↑m := Nat.one_le_cast.mpr hm have hbase_ge_two : (2 : ℝ) ≤ 16 * Real.exp 1 * (↑v + 1) := by diff --git a/LeanPool/FormalLearningTheory/PureMath/ApproxMinimax.lean b/LeanPool/FormalLearningTheory/PureMath/ApproxMinimax.lean index bb2ab4f9da..2b51dcc929 100644 --- a/LeanPool/FormalLearningTheory/PureMath/ApproxMinimax.lean +++ b/LeanPool/FormalLearningTheory/PureMath/ApproxMinimax.lean @@ -516,7 +516,7 @@ private lemma hitRate_from_potential Real.log_pow] at h0 simpa [mul_comm, mul_left_comm, mul_assoc] using h0 have hlog_up : Real.log (1 - η * v) ≤ -η * v := - by linarith [Real.log_le_sub_one_of_pos hbasev] + by linarith only [Real.log_le_sub_one_of_pos hbasev] have hlog_down : -η / (1 - η) ≤ Real.log (1 - η) := by have h := Real.one_sub_inv_le_log_of_pos hbase have hne : 1 - η ≠ 0 := by linarith @@ -531,20 +531,11 @@ private lemma hitRate_from_potential -- Hence H * log(1-η) ≤ log N - T*η*v -- Since log(1-η) < 0 (as 0 < η < 1), -log(1-η) > 0 -- So H * (-log(1-η)) ≥ -log N + T*η*v = T*η*v - log N - by_cases hv_sign : 0 ≤ v - · nlinarith [mul_nonneg hTreal_nonneg (mul_nonneg (le_of_lt hη) hv_sign)] - · push Not at hv_sign - -- v < 0 means T*η*v - log N < 0 ≤ H*(-log(1-η)) - have hlog_neg : Real.log (1 - η) < 0 := Real.log_neg (by linarith) (by linarith) - have h_rhs_nn : 0 ≤ (H : ℝ) * (-Real.log (1 - η)) := mul_nonneg hHnonneg (by linarith) - have hTreal_pos : (0 : ℝ) < T := by exact_mod_cast hTpos - have h_Tηv_neg : (T : ℝ) * η * v < 0 := by - have := mul_neg_of_pos_of_neg hη hv_sign - nlinarith - linarith [Real.log_natCast_nonneg N] + have hscaled := mul_le_mul_of_nonneg_left hlog_up hTreal_nonneg + linarith only [hlog, hscaled] have hcoef : -Real.log (1 - η) ≤ η / (1 - η) := by have : -η / (1 - η) = -(η / (1 - η)) := by ring - linarith + linarith only [hlog_down, this] have hanti' : (T : ℝ) * η * v - Real.log (N : ℝ) ≤ (H : ℝ) * (η / (1 - η)) := @@ -570,14 +561,17 @@ private lemma hitRate_from_potential ((H : ℝ) * η) / (η * T) = (H : ℝ) / T := by field_simp [show η ≠ 0 from ne_of_gt hη, hTne]; try ring simpa [hsimpL, hsimpR] using hdiv - have hterm1 : v - ε / 4 ≤ (1 - η) * v := by nlinarith [hηsmall, hv1] + have hterm1 : v - ε / 4 ≤ (1 - η) * v := by + linarith only [hηsmall, mul_le_of_le_one_right hη.le hv1] have hlog_nonneg : 0 ≤ Real.log (N : ℝ) := Real.log_natCast_nonneg N have haux : Real.log (N : ℝ) ≤ (ε / 4) * (η * T) := (div_le_iff₀ hηTpos).mp hlargeT have hterm2 : ((1 - η) * Real.log (N : ℝ)) / (η * T) ≤ ε / 4 := by apply (div_le_iff₀ hηTpos).2 - nlinarith [haux, hlog_nonneg] - linarith + calc (1 - η) * Real.log (N : ℝ) ≤ 1 * Real.log (N : ℝ) := + mul_le_mul_of_nonneg_right (by linarith only [hη]) hlog_nonneg + _ ≤ (ε / 4) * (η * T) := by simpa only [one_mul] using haux + linarith only [hterm1, hterm2, hrate0, hη, hηsmall] /-- **Genuine approximate minimax via MWU regret extraction.** If every column mixture admits a pure row with expected payoff ≥ v,