perf(FormalLearningTheory): simplify growth and minimax proofs

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

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,24 +1642,29 @@ 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
     rw [Real.lt_sqrt (by norm_num : (0:ℝ) ≤ 4 / 3)]
     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. -/

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,15 +1522,24 @@ 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]
     have h1 : (1 : ℝ) ≤ Real.exp 1 ^ (v + 1) * ↑m ^ v :=
       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

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,