diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean index 1f60fe7cc9..39620fb254 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean @@ -44,10 +44,14 @@ private theorem contraction_factor_bounds {μ' η θ : ℝ} (hμ' : 0 < μ') (h have ha_lt1 : Real.sqrt (μ' * η) < 1 := by calc Real.sqrt (μ' * η) < Real.sqrt 1 := Real.sqrt_lt_sqrt (le_of_lt hμη_pos) hμη_lt1 _ = 1 := Real.sqrt_one - have hc_pos : 0 < 1 - (1 - θ) * Real.sqrt (μ' * η) := by - nlinarith [mul_pos (sub_pos.mpr hθ_lt1) ha_pos] - have hc_lt1 : 1 - (1 - θ) * Real.sqrt (μ' * η) < 1 := by - nlinarith [mul_pos (sub_pos.mpr hθ_lt1) ha_pos] + have hprod_lt1 : (1 - θ) * Real.sqrt (μ' * η) < 1 := by + calc (1 - θ) * Real.sqrt (μ' * η) ≤ 1 * Real.sqrt (μ' * η) := + mul_le_mul_of_nonneg_right (sub_le_self 1 hθ_pos.le) ha_pos.le + _ = Real.sqrt (μ' * η) := one_mul _ + _ < 1 := ha_lt1 + have hc_pos : 0 < 1 - (1 - θ) * Real.sqrt (μ' * η) := sub_pos.mpr hprod_lt1 + have hc_lt1 : 1 - (1 - θ) * Real.sqrt (μ' * η) < 1 := + sub_lt_self 1 (mul_pos (sub_pos.mpr hθ_lt1) ha_pos) refine ⟨le_of_lt hc_pos, le_of_lt hc_lt1, ?_⟩ calc Real.sqrt (1 - (1 - θ) * Real.sqrt (μ' * η)) < Real.sqrt 1 := Real.sqrt_lt_sqrt (le_of_lt hc_pos) hc_lt1 @@ -101,27 +105,28 @@ private theorem bootstrap_displacement_induction {d : ℕ} (hvel : B * Real.sqrt (Lf 0) ≤ r / 4) (n : ℕ) : (X n ∈ Ω ∧ Y n ∈ Ω) ∧ (dist (X n) m_star < r ∧ dist (Y n) m_star < r) ∧ Lf n ≤ c ^ n * Lf 0 := by - have hr_pos : 0 < r := by linarith [dist_nonneg (x := X 0) (y := m_star)] + have hr_pos : 0 < r := by linarith only [hX0, dist_nonneg (x := X 0) (y := m_star)] -- While the displacement-sum bound holds, the look-ahead stays within `r / 2` of `m_star`. have hY_half : ∀ k, dist (Y k) m_star ≤ dist (Y 0) m_star + A * Real.sqrt (Lf 0) * (Finset.range k).sum (fun j => Real.sqrt c ^ j) → dist (Y k) m_star < r / 2 := by intro k hk - linarith [geometric_displacement_le hA hsqrt_c_lt1 hdisp k] + linarith only [hk, hY0, geometric_displacement_le hA hsqrt_c_lt1 hdisp k] have hinv : ∀ n, dist (X n) m_star < r ∧ Lf n ≤ c ^ n * Lf 0 ∧ dist (Y n) m_star ≤ dist (Y 0) m_star + A * Real.sqrt (Lf 0) * (Finset.range n).sum (fun k => Real.sqrt c ^ k) := by intro n induction n with | zero => - refine ⟨by linarith, by simp only [pow_zero, one_mul, le_refl], ?_⟩ + refine ⟨by linarith only [hX0, hr_pos], by simp only [pow_zero, one_mul, le_refl], ?_⟩ simp only [Finset.range_zero, Finset.sum_empty, mul_zero, add_zero, le_refl] | succ n ih => obtain ⟨hXn, hLn, hYn⟩ := ih have hXn_Ω : X n ∈ Ω := hball_Ω (Metric.mem_ball.mpr hXn) - have hYn_Ω : Y n ∈ Ω := hball_Ω (Metric.mem_ball.mpr (by linarith [hY_half n hYn])) + have hYn_Ω : Y n ∈ Ω := + hball_Ω (Metric.mem_ball.mpr (by linarith only [hr_pos, hY_half n hYn])) have hLn_le : Lf n ≤ Lf 0 := by have := mul_le_of_le_one_left hL0_nonneg (pow_le_one₀ hc_nonneg hc_le_one (n := n)) - linarith + exact hLn.trans this have hLn_R : Lf n ≤ R ^ 2 := le_trans hLn_le hL0_R have hsqrt_Ln : Real.sqrt (Lf n) ≤ Real.sqrt c ^ n * Real.sqrt (Lf 0) := by calc Real.sqrt (Lf n) ≤ Real.sqrt (c ^ n * Lf 0) := Real.sqrt_le_sqrt hLn @@ -138,7 +143,7 @@ private theorem bootstrap_displacement_induction {d : ℕ} rw [hY_step n]; exact dist_add_le_dist_add_norm _ _ _ _ ≤ (dist (Y 0) m_star + A * Real.sqrt (Lf 0) * (Finset.range n).sum (fun k => Real.sqrt c ^ k)) + - A * Real.sqrt (Lf 0) * Real.sqrt c ^ n := by linarith + A * Real.sqrt (Lf 0) * Real.sqrt c ^ n := add_le_add hYn hH_geom _ = dist (Y 0) m_star + A * Real.sqrt (Lf 0) * (Finset.range (n + 1)).sum (fun k => Real.sqrt c ^ k) := by rw [Finset.sum_range_succ]; ring @@ -150,12 +155,12 @@ private theorem bootstrap_displacement_induction {d : ℕ} refine ⟨?_, ?_, hYn1⟩ · calc dist (X (n + 1)) m_star ≤ dist (Y (n + 1)) m_star + ‖V (n + 1)‖ := by rw [hX_eq (n + 1)]; exact dist_sub_le_dist_add_norm _ _ _ - _ < r := by linarith [hY_half (n + 1) hYn1] + _ < r := by linarith only [hr_pos, hV_small, hY_half (n + 1) hYn1] · calc Lf (n + 1) ≤ c * Lf n := hcontract n hXn_Ω hYn_Ω hLn_R _ ≤ c * (c ^ n * Lf 0) := mul_le_mul_of_nonneg_left hLn hc_nonneg _ = c ^ (n + 1) * Lf 0 := by ring obtain ⟨hXn, hLn, hYn⟩ := hinv n - have hYn_lt : dist (Y n) m_star < r := by linarith [hY_half n hYn] + have hYn_lt : dist (Y n) m_star < r := by linarith only [hr_pos, hY_half n hYn] exact ⟨⟨hball_Ω (Metric.mem_ball.mpr hXn), hball_Ω (Metric.mem_ball.mpr hYn_lt)⟩, ⟨hXn, hYn_lt⟩, hLn⟩ @@ -246,7 +251,7 @@ private theorem bootstrapTotalDisplacementProof contraction_factor_bounds hμ' hη_pos hμη_lt1 hθ_pos hθ_lt1 set a := Real.sqrt (μ' * η) with ha_def set c := 1 - (1 - θ) * a with hc_def - have h1_sub_sqrt_c_pos : (0 : ℝ) < 1 - Real.sqrt c := by linarith + have h1_sub_sqrt_c_pos : (0 : ℝ) < 1 - Real.sqrt c := sub_pos.mpr hsqrt_c_lt1 -- ── Step 1: Get r from Ω being open at m⋆ ────────────────────────────── obtain ⟨r, hr_pos, hball_Ω⟩ := Metric.isOpen_iff.mp hΩ_open m_star hm_star_Ω -- ── Step 2: Displacement bound constant ───────────────────────────────── @@ -262,14 +267,14 @@ private theorem bootstrapTotalDisplacementProof hΨ_cont hΨ_zero T hT_pos -- ── Step 5: Set α = min(α₁, r/4) ─────────────────────────────────────── set α := min α₁ (r / 4) with hα_def - refine ⟨α, lt_min hα₁_pos (by linarith), fun x₁ hx₁ => ?_⟩ + refine ⟨α, lt_min hα₁_pos (by linarith only [hr_pos]), fun x₁ hx₁ => ?_⟩ -- ── Base‑case setup ───────────────────────────────────────────────────── have hx₁_ball : x₁ ∈ Metric.ball m_star α₁ := Metric.ball_subset_ball (min_le_left α₁ (r / 4)) hx₁.1 have hx₁_dist : dist x₁ m_star < r / 4 := lt_of_lt_of_le (Metric.mem_ball.mp hx₁.1) (min_le_right α₁ (r / 4)) have hx₁_Ω : x₁ ∈ Ω := by - apply hball_Ω; exact Metric.mem_ball.mpr (by linarith) + apply hball_Ω; exact Metric.mem_ball.mpr (by linarith only [hr_pos, hx₁_dist]) have hx₁_U : x₁ ∈ U := hx₁.2 -- Ψ(x₁) < T² have hΨ_small : psi f μ' S x₁ < T ^ 2 := @@ -285,11 +290,11 @@ private theorem bootstrapTotalDisplacementProof rw [dist_eq_norm] at hπ_dist rw [norm_smul, Real.norm_of_nonneg (Real.sqrt_nonneg μ')] rw [mul_pow, Real.sq_sqrt (le_of_lt hμ'), hπ_dist] - linarith [sq_nonneg ((1 + Real.sqrt (μ' * η)) ^ 2 / (2 * (1 - Real.sqrt (μ' * η))))] + linarith only [] -- L 0 ≤ T² ≤ R² have hL0_le_T2 : L 0 ≤ T ^ 2 := le_of_lt (lt_of_le_of_lt hL0_le_Ψ hΨ_small) have hT_le_R : T ≤ R := min_le_left R _ - have hL0_bound : L 0 ≤ R ^ 2 := le_trans hL0_le_T2 (by nlinarith) + have hL0_bound : L 0 ≤ R ^ 2 := hL0_le_T2.trans (pow_le_pow_left₀ hT_pos.le hT_le_R 2) -- L 0 ≥ 0 have hL0_nonneg : (0 : ℝ) ≤ L 0 := by have hmin : ∀ y, f m_star ≤ f y := by @@ -301,7 +306,7 @@ private theorem bootstrapTotalDisplacementProof change 0 ≤ lyapunov P μ' π f η ρ x₁ 0 simp only [lyapunov, nesterovSeq, auxVar, normalDisp, NesterovState.lookahead, map_zero, smul_zero, sub_self, zero_add, add_zero, norm_zero] - linarith [sq_nonneg ‖Real.sqrt μ' • (x₁ - π x₁)‖] + linarith only [h1, sq_nonneg ‖Real.sqrt μ' • (x₁ - π x₁)‖] -- Key bound: √(L 0) ≤ T have hsqrt_L0_le_T : Real.sqrt (L 0) ≤ T := by calc Real.sqrt (L 0) ≤ Real.sqrt (T ^ 2) := Real.sqrt_le_sqrt hL0_le_T2 @@ -421,7 +426,7 @@ private theorem bootstrapTotalDisplacementGenProof contraction_factor_bounds hμ' hη_pos hμη_lt1 hθ_pos hθ_lt1 set a := Real.sqrt (μ' * η) with ha_def set c := 1 - (1 - θ) * a with hc_def - have h1_sub_sqrt_c_pos : (0 : ℝ) < 1 - Real.sqrt c := by linarith + have h1_sub_sqrt_c_pos : (0 : ℝ) < 1 - Real.sqrt c := sub_pos.mpr hsqrt_c_lt1 -- ── Step 1: Get r from Ω being open at m⋆ ────────────────────────────── obtain ⟨r, hr_pos, hball_Ω⟩ := Metric.isOpen_iff.mp hΩ_open m_star hm_star_Ω -- ── Step 2: Displacement bound constant ───────────────────────────────── @@ -430,7 +435,7 @@ private theorem bootstrapTotalDisplacementGenProof -- ── Step 3: Choose δ so that iterates stay within ball(m⋆, r) ⊆ Ω ────── set δ := min R (min (r / 4) (r / (4 * K))) with hδ_def have hδ_pos : (0 : ℝ) < δ := by - apply lt_min hR; apply lt_min (by linarith) (by positivity) + apply lt_min hR; apply lt_min (by linarith only [hr_pos]) (by positivity) have hδ_le_R : δ ≤ R := min_le_left R _ have hδ_le_r4 : δ ≤ r / 4 := le_trans (min_le_right R _) (min_le_left _ _) have hδ_le_rK : δ ≤ r / (4 * K) := le_trans (min_le_right R _) (min_le_right _ _) @@ -442,7 +447,7 @@ private theorem bootstrapTotalDisplacementGenProof lt_of_lt_of_le (Metric.mem_ball.mp hs₀_la) hδ_le_r4 -- L₀ ≤ R² have hL₀_R : lyapunovOfState P μ' π f η s₀ ≤ R ^ 2 := - le_trans hL₀_small (by nlinarith [hδ_le_R]) + hL₀_small.trans (pow_le_pow_left₀ hδ_pos.le hδ_le_R 2) -- L₀ ≥ 0 have hbdd : BddBelow (Set.range f) := by refine ⟨f m_star, ?_⟩ diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Core.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Core.lean index fcf022fcde..6b29600946 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Core.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Core.lean @@ -7,11 +7,8 @@ module public import Mathlib.Basic.Real.Basic import LeanPool.PLAcceleratedNesterovLean.Convergence.Coercivity.Step2 -import Mathlib.Algebra.Order.Algebra -import Mathlib.Analysis.SpecialFunctions.Pow.NNReal -import Mathlib.Data.Sym.Sym2.Init -import Mathlib.Tactic.NormNum.GCD -import Mathlib.Tactic.Positivity.Finset +import Mathlib.Tactic.Linarith.Frontend +import Mathlib.Tactic.Ring.RingNF /-! # Coercivity Core Bound @@ -42,14 +39,11 @@ theorem coercivity_core_bound (hV_ub : V ≤ A + T) : (1 - a) ^ 2 * (V ^ 2 + μ' * E ^ 2) ≤ 60 * Ln := by -- Key facts - have h1a : (0 : ℝ) < 1 - a := by linarith + have h1a : (0 : ℝ) < 1 - a := sub_pos.mpr ha_lt1 have h1a_sq_le : (1 - a) ^ 2 ≤ 1 := by - have : (1 - a) ^ 2 = 1 - 2 * a + a ^ 2 := by ring - have : a ^ 2 ≤ a := by - calc a ^ 2 = a * a := by ring - _ ≤ a * 1 := by exact mul_le_mul_of_nonneg_left ha_lt1.le ha_nn - _ = a := mul_one a - linarith + simpa only [one_pow] using pow_le_pow_left₀ h1a.le (sub_le_self 1 ha_nn) 2 + have ha_sq_le : a ^ 2 ≤ 1 := by + simpa only [one_pow] using pow_le_pow_left₀ ha_nn ha_lt1.le 2 have h1a_sq_nn : (0 : ℝ) ≤ (1 - a) ^ 2 := sq_nonneg _ -- B = s·E set B := s * E with hB_def @@ -62,13 +56,12 @@ theorem coercivity_core_bound _ = s * D + s * r * V := by ring _ = s * D + a * V := by rw [hsr] _ ≤ s * D + a * (A + T) := by - have : V ≤ A + T := hV_ub - linarith [mul_le_mul_of_nonneg_left this ha_nn] + exact add_le_add le_rfl (mul_le_mul_of_nonneg_left hV_ub ha_nn) -- Resolve coupled system: A ≤ U + B, B ≤ sD + a(A+T) have hB_res := resolve_coupled_bounds A B T U (s * D) a ha_nn ha_lt1 hA_ub hBE hU_nn (mul_nonneg hs_nn hD_nn) hT_nn have hBr : (1 - a) * B ≤ s * D + a * U + a * T := by - have h := (le_div_iff₀ h1a).mp hB_res; linarith + exact (mul_comm (1 - a) B).trans_le ((le_div_iff₀ h1a).mp hB_res) -- Square: ((1-a)B)² = (1-a)²μ'E² have hLHS : ((1 - a) * B) ^ 2 = (1 - a) ^ 2 * (μ' * E ^ 2) := by rw [hB_def, show μ' = s ^ 2 from hs_sq.symm]; ring @@ -81,36 +74,25 @@ theorem coercivity_core_bound have h1 : 0 ≤ (s * D - a * U) ^ 2 := sq_nonneg _ have h2 : 0 ≤ (s * D - a * T) ^ 2 := sq_nonneg _ have h3 : 0 ≤ (a * U - a * T) ^ 2 := sq_nonneg _ - have e1 : (s * D - a * U) ^ 2 = s^2*D^2 - 2*s*D*a*U + a^2*U^2 := by ring - have e2 : (s * D - a * T) ^ 2 = s^2*D^2 - 2*s*D*a*T + a^2*T^2 := by ring - have e3 : (a * U - a * T) ^ 2 = a^2*U^2 - 2*a^2*U*T + a^2*T^2 := by ring - have lhs : (s * D + a * U + a * T) ^ 2 = - s^2*D^2 + a^2*U^2 + a^2*T^2 + 2*s*D*a*U + 2*s*D*a*T + 2*a^2*U*T := by ring - rw [lhs]; linarith [e1 ▸ h1, e2 ▸ h2, e3 ▸ h3] + linarith only [h1, h2, h3] -- a²X² ≤ X² from (1-a²)X² ≥ 0 - have ha2U : a ^ 2 * U ^ 2 ≤ U ^ 2 := by - have : 0 ≤ (1 - a ^ 2) * U ^ 2 := - mul_nonneg (by have := mul_le_mul_of_nonneg_left ha_lt1.le ha_nn; linarith [sq_nonneg a]) - (sq_nonneg U) - linarith - have ha2T : a ^ 2 * T ^ 2 ≤ T ^ 2 := by - have : 0 ≤ (1 - a ^ 2) * T ^ 2 := - mul_nonneg (by have := mul_le_mul_of_nonneg_left ha_lt1.le ha_nn; linarith [sq_nonneg a]) - (sq_nonneg T) - linarith + have ha2U : a ^ 2 * U ^ 2 ≤ U ^ 2 := + (mul_le_mul_of_nonneg_right ha_sq_le (sq_nonneg U)).trans_eq (one_mul _) + have ha2T : a ^ 2 * T ^ 2 ≤ T ^ 2 := + (mul_le_mul_of_nonneg_right ha_sq_le (sq_nonneg T)).trans_eq (one_mul _) -- Core: (1-a)²μ'E² ≤ 18Ln have he_mult : (1 - a) ^ 2 * (μ' * E ^ 2) ≤ 18 * Ln := by have h1 : ((1 - a) * B) ^ 2 ≤ 3 * (s ^ 2 * D ^ 2 + U ^ 2 + T ^ 2) := by - linarith [hBr_sq, hRHS, ha2U, ha2T] + linarith only [hBr_sq, hRHS, ha2U, ha2T] rw [hs_sq] at h1 - linarith [hLHS] + linarith only [h1, hLHS, hD_le, hU_le, hT_le] -- A² ≤ 2(U²+μ'E²) have hperp_sq : A ^ 2 ≤ 2 * (U ^ 2 + μ' * E ^ 2) := by have h1 : A ≤ U + B := hA_ub - have h1sq : A ^ 2 ≤ (U + B) ^ 2 := sq_le_sq' (by linarith [hA_nn]) h1 + have h1sq : A ^ 2 ≤ (U + B) ^ 2 := pow_le_pow_left₀ hA_nn h1 2 have h2 := dist_bound_from_v_e U B hU_nn hB_nn have h3 : B ^ 2 = μ' * E ^ 2 := by rw [hB_def, show μ' = s ^ 2 from hs_sq.symm]; ring - linarith + linarith only [h1sq, h2, h3] -- (1-a)²·A² ≤ 40Ln have hA_mult : (1 - a) ^ 2 * A ^ 2 ≤ 40 * Ln := by -- (1-a)²A² ≤ A² ≤ 2(U²+μ'E²) ≤ 2(2Ln + 18Ln/(1-a)²) @@ -120,19 +102,19 @@ theorem coercivity_core_bound 2 * ((1 - a) ^ 2 * U ^ 2) + 2 * ((1 - a) ^ 2 * (μ' * E ^ 2)) := by have : (1 - a) ^ 2 * A ^ 2 ≤ (1 - a) ^ 2 * (2 * (U ^ 2 + μ' * E ^ 2)) := mul_le_mul_of_nonneg_left hperp_sq h1a_sq_nn - linarith + linarith only [this] have step2 : (1 - a) ^ 2 * U ^ 2 ≤ U ^ 2 := le_of_le_of_eq (mul_le_mul_of_nonneg_right h1a_sq_le (sq_nonneg U)) (one_mul _) - linarith + linarith only [step1, step2, he_mult, hU_le] -- (1-a)²T² ≤ 2Ln have hT_mult : (1 - a) ^ 2 * T ^ 2 ≤ 2 * Ln := by have : (1 - a) ^ 2 * T ^ 2 ≤ 1 * T ^ 2 := mul_le_mul_of_nonneg_right h1a_sq_le (sq_nonneg T) - linarith + linarith only [this, hT_le] -- Combine: (1-a)²(V²+μ'E²) = (1-a)²T² + (1-a)²A² + (1-a)²μ'E² ≤ 2+40+18 = 60Ln have h_expand : (1 - a) ^ 2 * (V ^ 2 + μ' * E ^ 2) = (1 - a) ^ 2 * T ^ 2 + (1 - a) ^ 2 * A ^ 2 + (1 - a) ^ 2 * (μ' * E ^ 2) := by rw [hv_orth]; ring - linarith + linarith only [h_expand, hT_mult, hA_mult, he_mult] end PLAcceleratedNesterovLean diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Main.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Main.lean index 6a8ca61c07..a24483e6ad 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Main.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Main.lean @@ -78,7 +78,7 @@ theorem lyapunov_coercivity_gen calc a < Real.sqrt 1 := Real.sqrt_lt_sqrt (le_of_lt (mul_pos hμ' hη_pos)) hμη_lt1 _ = 1 := Real.sqrt_one - have h1a : (0 : ℝ) < 1 - a := by linarith + have h1a : (0 : ℝ) < 1 - a := sub_pos.mpr ha_lt1 have h1a_sq : (0 : ℝ) < (1 - a) ^ 2 := pow_pos h1a 2 -- C_coer = 60/(1-a)², C_Ψ = 2 refine ⟨60 / (1 - a) ^ 2, 2, div_pos (by norm_num) h1a_sq, two_pos, ?_⟩ @@ -100,11 +100,10 @@ theorem lyapunov_coercivity_gen have hV_nn : 0 ≤ ‖s.v‖ := norm_nonneg _ -- Lyapunov setup have hlam_pos : 0 < (1 + a) ^ 2 / (2 * (1 - a)) := - div_pos (by positivity) (by linarith) + div_pos (by positivity) (mul_pos two_pos h1a) have hgap_nn : 0 ≤ f s.x - fStar f := by - linarith [hQG s.x hx, - mul_nonneg (div_nonneg (le_of_lt hμ') two_pos.le) - (sq_nonneg (Metric.infDist s.x S))] + exact (mul_nonneg (div_nonneg hμ'.le two_pos.le) + (sq_nonneg (Metric.infDist s.x S))).trans (hQG s.x hx) -- Lyapunov bounds have hgap_le : f s.x - fStar f ≤ Ln := lyapunov_gap_bound (f s.x - fStar f) (U ^ 2) ((1 + a) ^ 2 / (2 * (1 - a))) @@ -112,11 +111,11 @@ theorem lyapunov_coercivity_gen have hu_le : U ^ 2 ≤ 2 * Ln := lyapunov_u_bound (f s.x - fStar f) (U ^ 2) ((1 + a) ^ 2 / (2 * (1 - a))) (T ^ 2) Ln hgap_nn (sq_nonneg _) hlam_pos (sq_nonneg _) rfl - have hLn_nn : 0 ≤ Ln := by linarith [hu_le, sq_nonneg U] + have hLn_nn : 0 ≤ Ln := hgap_nn.trans hgap_le have hPv_le : T ^ 2 ≤ 2 * Ln := by have hlam_ge : (1 : ℝ) / 2 ≤ (1 + a) ^ 2 / (2 * (1 - a)) := by - rw [div_le_div_iff₀ (by norm_num : (0 : ℝ) < 2) (by linarith : (0 : ℝ) < 2 * (1 - a))] - nlinarith [sq_nonneg a] + rw [div_le_div_iff₀ two_pos (mul_pos two_pos h1a)] + linarith only [ha_nn, sq_nonneg a] have hPv_bound := lyapunov_Pv_bound (f s.x - fStar f) (U ^ 2) ((1 + a) ^ 2 / (2 * (1 - a))) (T ^ 2) Ln hgap_nn (sq_nonneg _) hlam_pos (sq_nonneg _) rfl calc T ^ 2 ≤ Ln / ((1 + a) ^ 2 / (2 * (1 - a))) := hPv_bound @@ -124,7 +123,9 @@ theorem lyapunov_coercivity_gen apply div_le_div_of_nonneg_left hLn_nn (by norm_num : (0 : ℝ) < 1 / 2) hlam_ge _ = 2 * Ln := by ring -- QG at x_n: μ'·D² ≤ 2Ln - have hD_sq : μ' * D ^ 2 ≤ 2 * Ln := by nlinarith [hQG s.x hx] + have hD_sq : μ' * D ^ 2 ≤ 2 * Ln := by + dsimp only [D] + linarith only [hQG s.x hx, hgap_le] -- A ≤ U + √μ'·E (from u = P⊥v + √μ'·e) have hperp : A ≤ U + Real.sqrt μ' * EE := by have h := perp_v_bound_from_u (auxVarOfState P μ' π η s) @@ -146,7 +147,7 @@ theorem lyapunov_coercivity_gen rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg η)] _ = dist s.x (π s.x) + Real.sqrt η * ‖s.v‖ := by rw [dist_eq_norm] _ = D + Real.sqrt η * ‖s.v‖ := by rw [hD_def, hπ_metric s.x hx] - linarith + exact h_eq.trans_le (h_le.trans h_tri) -- ‖v‖ ≤ A + T (triangle) have hV_ub : ‖s.v‖ ≤ A + T := by have := norm_add_le (s.v - P s.v) (P s.v) @@ -165,23 +166,23 @@ theorem lyapunov_coercivity_gen hPv_le hu_le hD_sq hv_ortho hperp hE_tri hV_ub -- Convert: goal is ‖v‖²+μ'E² ≤ 60/(1-a)²·Ln, i.e., (1-a)²(‖v‖²+μ'E²) ≤ 60Ln rw [div_mul_eq_mul_div, le_div_iff₀ h1a_sq] - linarith [hcore] + linarith only [hcore] · -- (2) Ψ(x_n) ≤ 2 · L_n have hqg := hQG s.x hx have hgap_nn : 0 ≤ f s.x - fStar f := by have := mul_nonneg (div_nonneg (le_of_lt hμ') two_pos.le) (sq_nonneg (Metric.infDist s.x S)) - linarith + exact this.trans hqg have hlam_pos : 0 < (1 + a) ^ 2 / (2 * (1 - a)) := - div_pos (by positivity) (by linarith) + div_pos (by positivity) (mul_pos two_pos h1a) have hpsi_le : psi f μ' S s.x ≤ 2 * (f s.x - fStar f) := by - simp only [psi]; linarith + simp only [psi]; linarith only [hqg] have hgap_le_Ln : f s.x - fStar f ≤ Ln := lyapunov_gap_bound (f s.x - fStar f) (‖auxVarOfState P μ' π η s‖ ^ 2) ((1 + a) ^ 2 / (2 * (1 - a))) (‖P s.v‖ ^ 2) Ln hgap_nn (sq_nonneg _) hlam_pos (sq_nonneg _) rfl - linarith + linarith only [hpsi_le, hgap_le_Ln] /-- **Coercivity of the Lyapunov function.** diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step1.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step1.lean index 57dcc0a6b1..722873418b 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step1.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step1.lean @@ -34,7 +34,7 @@ theorem lyapunov_gap_bound (gap u_sq lam Pv_sq L : ℝ) (_hgap : 0 ≤ gap) (hu : 0 ≤ u_sq) (hlam : 0 < lam) (hPv : 0 ≤ Pv_sq) (hL : L = gap + u_sq / 2 + lam * Pv_sq) : gap ≤ L := by - nlinarith [mul_nonneg (le_of_lt hlam) hPv] + linarith only [hL, hu, mul_nonneg hlam.le hPv] /-- Variant: gap ≤ L when λ ≥ 0 (weak inequality, handles a = 1 edge case). Unfolds the Lyapunov definition directly; requires √(μ'·η) ≤ 1. @@ -45,9 +45,9 @@ theorem gap_le_lyapunovOfState_of_sqrt_le {d : ℕ} (P : E d →L[ℝ] E d) (μ' f s.x - fStar f ≤ lyapunovOfState P μ' π f η s := by simp only [lyapunovOfState] have hlam_nn : 0 ≤ (1 + Real.sqrt (μ' * η)) ^ 2 / (2 * (1 - Real.sqrt (μ' * η))) := - div_nonneg (sq_nonneg _) (by nlinarith) - nlinarith [sq_nonneg ‖auxVarOfState P μ' π η s‖, - mul_nonneg hlam_nn (sq_nonneg ‖P s.v‖)] + div_nonneg (sq_nonneg _) (by linarith only [ha_le1]) + exact (le_add_of_nonneg_right (div_nonneg (sq_nonneg _) (by norm_num))).trans + (le_add_of_nonneg_right (mul_nonneg hlam_nn (sq_nonneg _))) /-- Variant: gap ≤ L when λ ≥ 0 (weak inequality, handles a = 1 edge case). Unfolds the Lyapunov definition directly; requires √(μ'·η) ≤ 1. -/ @@ -63,7 +63,7 @@ theorem lyapunov_u_bound (gap u_sq lam Pv_sq L : ℝ) (hgap : 0 ≤ gap) (_hu : 0 ≤ u_sq) (hlam : 0 < lam) (hPv : 0 ≤ Pv_sq) (hL : L = gap + u_sq / 2 + lam * Pv_sq) : u_sq ≤ 2 * L := by - nlinarith [mul_nonneg (le_of_lt hlam) hPv] + linarith only [hgap, hL, mul_nonneg hlam.le hPv] /-- From the Lyapunov definition, ‖Pv‖² ≤ L/λ. -/ theorem lyapunov_Pv_bound (gap u_sq lam Pv_sq L : ℝ) @@ -71,7 +71,7 @@ theorem lyapunov_Pv_bound (gap u_sq lam Pv_sq L : ℝ) (hL : L = gap + u_sq / 2 + lam * Pv_sq) : Pv_sq ≤ L / lam := by rw [le_div_iff₀ hlam] - nlinarith + linarith only [hgap, hu, hL] /-- Triangle inequality on u = Pperp_v + √μ' · e gives ‖Pperp_v‖ ≤ ‖u‖ + √μ'·‖e‖. -/ theorem perp_v_bound_from_u (u Pperp_v e : E d) (sqrtmu : ℝ) diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step2.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step2.lean index 0c53e30276..df32b19c59 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step2.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Step2.lean @@ -6,11 +6,7 @@ Authors: Max Obreiter, Tobias Steinbrecher, Robert Foerster module public import Mathlib.Basic.Real.Basic -import Mathlib.Algebra.Order.Algebra -import Mathlib.Analysis.SpecialFunctions.Pow.NNReal -import Mathlib.Data.Sym.Sym2.Init -import Mathlib.Tactic.NormNum.GCD -import Mathlib.Tactic.Positivity.Finset +import Mathlib.Tactic.Linarith.Frontend /-! # Coercivity Step 2: Resolve Coupled Bounds on A_n and B_n @@ -47,11 +43,11 @@ theorem resolve_coupled_bounds (A B T c₁ c₂ a : ℝ) (hB : B ≤ c₂ + a * (A + T)) (_hc₁ : 0 ≤ c₁) (_hc₂ : 0 ≤ c₂) (_hT : 0 ≤ T) : B ≤ (c₂ + a * c₁ + a * T) / (1 - a) := by - have h1 : B ≤ c₂ + a * (c₁ + B + T) := by nlinarith - have h2 : (1 - a) * B ≤ c₂ + a * c₁ + a * T := by nlinarith - have h3 : (0 : ℝ) < 1 - a := by linarith - rw [le_div_iff₀ h3] - nlinarith + have h1 : B ≤ c₂ + a * (c₁ + B + T) := + hB.trans (add_le_add le_rfl + (mul_le_mul_of_nonneg_left (add_le_add hA le_rfl) ha_nn)) + have h2 : (1 - a) * B ≤ c₂ + a * c₁ + a * T := by linarith only [h1] + exact (le_div_iff₀ (sub_pos.mpr ha_lt)).mpr ((mul_comm B (1 - a)).trans_le h2) /-- After resolving the coupled system, get a bound on A. -/ theorem resolve_coupled_A_bound (A B c₁ c₂_prime : ℝ) @@ -59,11 +55,11 @@ theorem resolve_coupled_A_bound (A B c₁ c₂_prime : ℝ) (hB : B ≤ c₂_prime) (_hc₁ : 0 ≤ c₁) : A ≤ c₁ + c₂_prime := by - linarith + exact hA.trans (add_le_add le_rfl hB) /-- For Ψ: dist(x, M)² ≤ 2(η‖v‖² + ‖e‖²) from (a+b)² ≤ 2(a²+b²). -/ theorem dist_bound_from_v_e (a b : ℝ) (_ha : 0 ≤ a) (_hb : 0 ≤ b) : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2) := by - nlinarith [sq_nonneg (a - b)] + linarith only [sq_nonneg (a - b)] end PLAcceleratedNesterovLean diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Algebraic.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Algebraic.lean index 4a724f5ad4..a96dfce216 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Algebraic.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Algebraic.lean @@ -121,67 +121,52 @@ theorem curv_absorption_algebraic (habs : ε₁ * (C_wh / 2 + sm ^ 2 / 2 * C_h + sa * C_ge) ≤ θ * sa) : sm * @inner ℝ _ _ wn ξn + sm ^ 2 / 2 * ‖ξn‖ ^ 2 + sa * |@inner ℝ _ _ gn Pen| ≤ θ * sa * Ln := by - have hCS1 := real_inner_le_norm wn ξn - have hCS2 := abs_real_inner_le_norm gn Pen - have hξ_nn := norm_nonneg ξn; have hhn_nn := norm_nonneg hn - have hen_nn := norm_nonneg en; have hwn_nn := norm_nonneg wn; have hgn_nn := norm_nonneg gn + have hε₁_nn : 0 ≤ ε₁ := hε₁_pos.le have hsm2_nn : 0 ≤ sm ^ 2 / 2 := by positivity - have hε₁_nn : 0 ≤ ε₁ := le_of_lt hε₁_pos + have hε₁_sq : ε₁ ^ 2 ≤ ε₁ := by + simpa only [sq, mul_one] using mul_le_mul_of_nonneg_left hε₁_le1 hε₁_nn have hξ_sq : ‖ξn‖ ^ 2 ≤ ε₁ * ‖hn‖ ^ 2 := by - have h1 : ‖ξn‖ ≤ ε₁ * ‖hn‖ := hξ - have h2 : ‖ξn‖ ^ 2 ≤ (ε₁ * ‖hn‖) ^ 2 := sq_le_sq' (by linarith [hξ_nn]) h1 - have h3 : (ε₁ * ‖hn‖) ^ 2 = ε₁ ^ 2 * ‖hn‖ ^ 2 := by ring - have h4 : ε₁ ^ 2 ≤ ε₁ := by - calc ε₁ ^ 2 = ε₁ * ε₁ := by ring - _ ≤ ε₁ * 1 := mul_le_mul_of_nonneg_left hε₁_le1 hε₁_nn - _ = ε₁ := mul_one _ - calc ‖ξn‖ ^ 2 ≤ ε₁ ^ 2 * ‖hn‖ ^ 2 := by linarith - _ ≤ ε₁ * ‖hn‖ ^ 2 := mul_le_mul_of_nonneg_right h4 (sq_nonneg _) - -- Term 1: sm*⟨w,ξ⟩ ≤ ε₁/2 * C_wh * Ln + calc + ‖ξn‖ ^ 2 ≤ (ε₁ * ‖hn‖) ^ 2 := + (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hε₁_nn (norm_nonneg _))).mpr hξ + _ = ε₁ ^ 2 * ‖hn‖ ^ 2 := mul_pow _ _ _ + _ ≤ ε₁ * ‖hn‖ ^ 2 := mul_le_mul_of_nonneg_right hε₁_sq (sq_nonneg _) + -- Young's inequality bounds the mixed term before scaling by ε₁. + have hyoung : 2 * (sm * ‖wn‖) * ‖hn‖ ≤ sm ^ 2 * ‖wn‖ ^ 2 + ‖hn‖ ^ 2 := by + simpa only [mul_pow] using two_mul_le_add_sq (sm * ‖wn‖) ‖hn‖ have hterm1 : sm * @inner ℝ _ _ wn ξn ≤ ε₁ / 2 * (C_wh * Ln) := by - have h1 : sm * @inner ℝ _ _ wn ξn ≤ sm * (‖wn‖ * ‖ξn‖) := - mul_le_mul_of_nonneg_left hCS1 hsm_nn - have h2 : ‖ξn‖ ≤ ε₁ * ‖hn‖ := hξ - have h3 : ‖wn‖ * ‖ξn‖ ≤ ‖wn‖ * (ε₁ * ‖hn‖) := - mul_le_mul_of_nonneg_left h2 (norm_nonneg _) - have h5 : 2 * (sm * ‖wn‖ * ‖hn‖) ≤ sm ^ 2 * ‖wn‖ ^ 2 + ‖hn‖ ^ 2 := by - have := sq_nonneg (sm * ‖wn‖ - ‖hn‖) - have : (sm * ‖wn‖ - ‖hn‖) ^ 2 = sm^2 * ‖wn‖^2 - 2*sm*‖wn‖*‖hn‖ + ‖hn‖^2 := by ring - linarith - -- sm * (‖w‖ * ‖ξ‖) ≤ sm * ‖w‖ * (ε₁ * ‖h‖) = ε₁ * (sm*‖w‖*‖h‖) ≤ ε₁/2 * (sm²‖w‖²+‖h‖²) - have h6 : sm * (‖wn‖ * ‖ξn‖) ≤ ε₁ * (sm * ‖wn‖ * ‖hn‖) := by - calc sm * (‖wn‖ * ‖ξn‖) ≤ sm * (‖wn‖ * (ε₁ * ‖hn‖)) := - mul_le_mul_of_nonneg_left h3 hsm_nn - _ = ε₁ * (sm * ‖wn‖ * ‖hn‖) := by ring - have h7 : ε₁ * (sm * ‖wn‖ * ‖hn‖) ≤ ε₁ / 2 * (sm ^ 2 * ‖wn‖ ^ 2 + ‖hn‖ ^ 2) := by - linarith [mul_le_mul_of_nonneg_left h5 hε₁_nn] - have h8 : ε₁ / 2 * (sm ^ 2 * ‖wn‖ ^ 2 + ‖hn‖ ^ 2) ≤ ε₁ / 2 * (C_wh * Ln) := by - apply mul_le_mul_of_nonneg_left hwh; linarith - linarith - -- Term 2: sm²/2 * ‖ξ‖² ≤ ε₁ * sm²/2 * C_h * Ln + calc + sm * @inner ℝ _ _ wn ξn ≤ sm * (‖wn‖ * ‖ξn‖) := + mul_le_mul_of_nonneg_left (real_inner_le_norm _ _) hsm_nn + _ ≤ sm * (‖wn‖ * (ε₁ * ‖hn‖)) := + mul_le_mul_of_nonneg_left + (mul_le_mul_of_nonneg_left hξ (norm_nonneg _)) hsm_nn + _ = ε₁ / 2 * (2 * (sm * ‖wn‖) * ‖hn‖) := by ring + _ ≤ ε₁ / 2 * (sm ^ 2 * ‖wn‖ ^ 2 + ‖hn‖ ^ 2) := + mul_le_mul_of_nonneg_left hyoung (div_nonneg hε₁_nn (by norm_num)) + _ ≤ ε₁ / 2 * (C_wh * Ln) := + mul_le_mul_of_nonneg_left hwh (div_nonneg hε₁_nn (by norm_num)) have hterm2 : sm ^ 2 / 2 * ‖ξn‖ ^ 2 ≤ ε₁ * (sm ^ 2 / 2 * (C_h * Ln)) := by - have h2a : sm ^ 2 / 2 * ‖ξn‖ ^ 2 ≤ sm ^ 2 / 2 * (ε₁ * ‖hn‖ ^ 2) := - mul_le_mul_of_nonneg_left hξ_sq hsm2_nn - have h2b : sm ^ 2 / 2 * (ε₁ * ‖hn‖ ^ 2) = ε₁ * (sm ^ 2 / 2 * ‖hn‖ ^ 2) := by ring - have h2c : sm ^ 2 / 2 * ‖hn‖ ^ 2 ≤ sm ^ 2 / 2 * (C_h * Ln) := - mul_le_mul_of_nonneg_left hh_sq hsm2_nn - linarith [mul_le_mul_of_nonneg_left h2c hε₁_nn] - -- Term 3: sa*|⟨g,Pe⟩| ≤ ε₁ * sa * C_ge * Ln + calc + sm ^ 2 / 2 * ‖ξn‖ ^ 2 ≤ sm ^ 2 / 2 * (ε₁ * ‖hn‖ ^ 2) := + mul_le_mul_of_nonneg_left hξ_sq hsm2_nn + _ = ε₁ * (sm ^ 2 / 2 * ‖hn‖ ^ 2) := by ring + _ ≤ ε₁ * (sm ^ 2 / 2 * (C_h * Ln)) := + mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left hh_sq hsm2_nn) hε₁_nn have hterm3 : sa * |@inner ℝ _ _ gn Pen| ≤ ε₁ * (sa * (C_ge * Ln)) := by - have h3a : |@inner ℝ _ _ gn Pen| ≤ ‖gn‖ * (ε₁ * ‖en‖) := by - calc |@inner ℝ _ _ gn Pen| ≤ ‖gn‖ * ‖Pen‖ := hCS2 - _ ≤ ‖gn‖ * (ε₁ * ‖en‖) := by - exact mul_le_mul_of_nonneg_left hPe hgn_nn - have h3d : sa * |@inner ℝ _ _ gn Pen| ≤ sa * (‖gn‖ * (ε₁ * ‖en‖)) := - mul_le_mul_of_nonneg_left h3a (le_of_lt hsa_pos) - have h3e : sa * (‖gn‖ * (ε₁ * ‖en‖)) = ε₁ * (sa * (‖gn‖ * ‖en‖)) := by ring - have h3c : sa * (‖gn‖ * ‖en‖) ≤ sa * (C_ge * Ln) := - mul_le_mul_of_nonneg_left hge (le_of_lt hsa_pos) - linarith [mul_le_mul_of_nonneg_left h3c hε₁_nn] - -- Assembly: total ≤ ε₁ * K * Ln ≤ θ*sa * Ln + calc + sa * |@inner ℝ _ _ gn Pen| ≤ sa * (‖gn‖ * ‖Pen‖) := + mul_le_mul_of_nonneg_left (abs_real_inner_le_norm _ _) hsa_pos.le + _ ≤ sa * (‖gn‖ * (ε₁ * ‖en‖)) := + mul_le_mul_of_nonneg_left + (mul_le_mul_of_nonneg_left hPe (norm_nonneg _)) hsa_pos.le + _ = ε₁ * (sa * (‖gn‖ * ‖en‖)) := by ring + _ ≤ ε₁ * (sa * (C_ge * Ln)) := + mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left hge hsa_pos.le) hε₁_nn have htotal : sm * @inner ℝ _ _ wn ξn + sm ^ 2 / 2 * ‖ξn‖ ^ 2 + sa * |@inner ℝ _ _ gn Pen| ≤ - ε₁ * ((C_wh / 2 + sm ^ 2 / 2 * C_h + sa * C_ge) * Ln) := by linarith - linarith [mul_le_mul_of_nonneg_right habs hLn_nn] + ε₁ * ((C_wh / 2 + sm ^ 2 / 2 * C_h + sa * C_ge) * Ln) := by + linarith only [hterm1, hterm2, hterm3] + linarith only [htotal, mul_le_mul_of_nonneg_right habs hLn_nn] end PLAcceleratedNesterovLean diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Assembly.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Assembly.lean index 18c2a70b76..74763403b5 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Assembly.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/CurvAbsorb/Assembly.lean @@ -47,12 +47,12 @@ private theorem existsScaledRadius (a b c e M : ℝ) ∃ radius > 0, radius ≤ a ∧ M * radius < b ∧ M * radius < c ∧ M * radius < e := by let δ := min (min (min a b) c) e have hδ : 0 < δ := lt_min (lt_min (lt_min ha hb) hc) he - have hden : 0 < M + 1 := by linarith + have hden : 0 < M + 1 := by linarith only [hM] let radius := δ / (M + 1) have hradius : 0 < radius := div_pos hδ hden have hscaled : (M + 1) * radius = δ := mul_div_cancel₀ _ (ne_of_gt hden) have hsmall : M * radius < δ := by nlinarith - have hle : radius ≤ δ := div_le_self (le_of_lt hδ) (by linarith) + have hle : radius ≤ δ := div_le_self (le_of_lt hδ) (by linarith only [hM]) have hδa : δ ≤ a := (min_le_left _ _).trans ((min_le_left _ _).trans (min_le_left _ _)) have hδb : δ ≤ b := (min_le_left _ _).trans ((min_le_left _ _).trans (min_le_right _ _)) have hδc : δ ≤ c := (min_le_left _ _).trans (min_le_right _ _) @@ -71,7 +71,8 @@ private theorem orthogonalCombinationBound (P : E →L[ℝ] E) have h1 : ‖(1 - sa) • (v - P v)‖ ≤ ‖v - P v‖ := by rw [norm_smul, Real.norm_eq_abs] calc |1 - sa| * ‖v - P v‖ ≤ 1 * ‖v - P v‖ := by - gcongr; rw [abs_le]; exact ⟨by linarith [hsa_pos], by linarith [hsa_lt1]⟩ + gcongr; rw [abs_le] + exact ⟨by linarith only [hsa_pos, hsa_lt1], by linarith only [hsa_pos, hsa_lt1]⟩ _ = ‖v - P v‖ := one_mul _ have hPv_sub : ‖v - P v‖ ≤ ‖v‖ := by rw [← Real.sqrt_sq (norm_nonneg v), ← Real.sqrt_sq (norm_nonneg (v - P v))] @@ -94,7 +95,7 @@ private theorem orthogonalCombinationBound (P : E →L[ℝ] E) have hh1 : ‖(1 - sa) • (v - P v)‖ ≤ ‖v‖ := h1.trans hPv_sub have hh3 : Real.sqrt η * ‖gn - P gn‖ ≤ Real.sqrt η * ‖gn‖ := mul_le_mul_of_nonneg_left hPg_sub (Real.sqrt_nonneg η) - linarith [hsm_e, hη_g, hh1, hh3] + linarith only [h1, hPv_sub, hsm_e, hη_g, hh3, hh1] _ ≤ Cv * Real.sqrt Ln + sm * (Ce * Real.sqrt Ln) + Real.sqrt η * (Cg * Real.sqrt Ln) := by gcongr _ = (Cv + sm * Ce + Real.sqrt η * Cg) * Real.sqrt Ln := by ring @@ -200,10 +201,10 @@ private theorem curvAbsorbAssemblyFamily {ι : Type*} obtain ⟨δ_diff, hδ_diff_pos, hπ_diff_ball⟩ := hπ_diff_near -- Expansion factor: dist(πx, m*) ≤ 2·dist(x, m*), dist(x'n1, m*) ≤ (1+Ch)·R let M := 2 + Ch + 1 - have hM_ge3 : (3 : ℝ) ≤ M := by linarith [hCh_nn] + have hM_ge3 : (3 : ℝ) ≤ M := by linarith only [hCh_nn] obtain ⟨R₀, hR₀_pos, hR₀_le_δUp, hMR₀_lt_δU, hMR₀_lt_δDπ, hMR₀_lt_δdiff⟩ := existsScaledRadius δ_Up δ_U δ_Dπ δ_diff M hδ_Up_pos hδ_U_pos hδ_Dπ_pos hδ_diff_pos - (by linarith) + (by linarith only [hsa_pos, hsa_lt1, hCh_nn]) refine ⟨R₀, hR₀_pos, ?_⟩ intro i hsx hslx hLn_le -- Abbreviations @@ -236,16 +237,16 @@ private theorem curvAbsorbAssemblyFamily {ι : Type*} rw [hnd] at hcoer -- ‖v‖² ≤ C_coer·Ln, ‖e‖² ≤ C_coer/μ'·Ln have hv_sq : ‖sn.v‖ ^ 2 ≤ C_coer * Ln := by - have := mul_nonneg (le_of_lt hμ') (sq_nonneg ‖en‖); linarith + have := mul_nonneg (le_of_lt hμ') (sq_nonneg ‖en‖); linarith only [hcoer, this] have he_sq : ‖en‖ ^ 2 ≤ C_coer / μ' * Ln := by - have h1 : μ' * ‖en‖ ^ 2 ≤ C_coer * Ln := by have := sq_nonneg ‖sn.v‖; linarith + have h1 : μ' * ‖en‖ ^ 2 ≤ C_coer * Ln := by + have := sq_nonneg ‖sn.v‖ + linarith only [hcoer, this] rw [div_mul_eq_mul_div] - exact (le_div_iff₀ hμ').mpr (by linarith) + exact (le_div_iff₀ hμ').mpr (by linarith only [h1]) -- Ln ≥ 0 - have hLn_nn : (0 : ℝ) ≤ Ln := by - have h1 := sq_nonneg ‖sn.v‖ - have h2 := mul_nonneg (le_of_lt hμ') (sq_nonneg ‖en‖) - exact nonneg_of_mul_nonneg_left (by linarith) hC_coer + have hLn_nn : (0 : ℝ) ≤ Ln := + nonneg_of_mul_nonneg_right ((sq_nonneg ‖sn.v‖).trans hv_sq) hC_coer -- √Ln ≤ R₀ have hLn_sqrt : Real.sqrt Ln ≤ R₀ := by calc Real.sqrt Ln ≤ Real.sqrt (R₀ ^ 2) := Real.sqrt_le_sqrt hLn_le @@ -287,7 +288,7 @@ private theorem curvAbsorbAssemblyFamily {ι : Type*} have := (hπ_on_U x'n hx'n_U).2 have hπe : dist x'n (π x'n) ≤ dist x'n mstar := this ▸ Metric.infDist_le_dist_of_mem hmstar - linarith [dist_triangle (π x'n) x'n mstar, dist_comm (π x'n) x'n] + linarith only [hd1, hπe, dist_triangle (π x'n) x'n mstar, dist_comm (π x'n) x'n] -- ── x'_{n+1} ∈ B(mstar, (1+Ch)·R₀) ── have hx'n1_eq : (nesterovStep f η ρ sn).lookahead η = x'n + hn := by change (nesterovStep f η ρ sn).lookahead η = @@ -297,19 +298,19 @@ private theorem curvAbsorbAssemblyFamily {ι : Type*} have hd1 := Metric.mem_ball.mp hslx have hhn_le : ‖hn‖ ≤ Ch * R₀ := le_trans hhn_bound (mul_le_mul_of_nonneg_left hLn_sqrt hCh_nn) - linarith [dist_triangle (x'n + hn) x'n mstar, - show dist (x'n + hn) x'n = ‖hn‖ from by rw [dist_eq_norm, add_sub_cancel_left]] + linarith only [hd1, hhn_le, dist_triangle (x'n + hn) x'n mstar, + show dist (x'n + hn) x'n = ‖hn‖ from by rw [dist_eq_norm, add_sub_cancel_left]] -- Both points in Dπ-controlled region (dist < M·R₀) have hMR₀_ge_2R₀ : 2 * R₀ ≤ M * R₀ := - mul_le_mul_of_nonneg_right (by linarith [hM_ge3]) (le_of_lt hR₀_pos) + mul_le_mul_of_nonneg_right (by linarith only [hM_ge3]) hR₀_pos.le have hMR₀_ge_1ChR₀ : (1 + Ch) * R₀ ≤ M * R₀ := - mul_le_mul_of_nonneg_right (by linarith [hCh_nn]) (le_of_lt hR₀_pos) + mul_le_mul_of_nonneg_right (by linarith only [hsa_pos, hsa_lt1, hCh_nn]) (le_of_lt hR₀_pos) have hπx'n_ctrl : dist (π x'n) mstar < M * R₀ := by - linarith [hπx'n_dist] + linarith only [hπx'n_dist, hMR₀_ge_2R₀] have hx'n_ctrl : dist x'n mstar < M * R₀ := by - have := Metric.mem_ball.mp hslx; linarith + have := Metric.mem_ball.mp hslx; linarith only [hR₀_pos, hMR₀_ge_2R₀, this] have hx'n1_ctrl : dist (x'n + hn) mstar < M * R₀ := by - linarith [hx'n1_dist] + linarith only [hR₀_pos, hx'n1_dist] -- ‖Dπ(π(x'n)) - P‖ ≤ ε₁ have hDπ_πx'n : ‖fderiv ℝ π (π x'n) - P‖ ≤ ε₁ := (hDπ_in_MR₀ (π x'n) hπx'n_ctrl).1 @@ -370,7 +371,7 @@ private theorem curvAbsorbAssemblyFamily {ι : Type*} hge θ hθ_pos apply le_trans (mul_le_mul_of_nonneg_left (show _ ≤ K from ?_) (le_of_lt hε₁_pos)) hε₁K_le dsimp [K] - linarith + linarith only [hsa_pos, hsa_lt1] /-- A uniform curvature-absorption radius for Nesterov sequences with zero initial velocity. -/ theorem curv_absorb_assembly diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean index 5633de7b58..4e4bba90d3 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean @@ -14,7 +14,6 @@ import LeanPool.PLAcceleratedNesterovLean.MorseBott.Bridge import LeanPool.PLAcceleratedNesterovLean.MorseBott.Submanifold import Mathlib.Analysis.Calculus.Deriv.Add import Mathlib.Analysis.Calculus.Deriv.Mul -import Mathlib.Analysis.InnerProductSpace.Calculus /-! @@ -243,8 +242,8 @@ private theorem hessianQuadForm_ge_of_unit_sphere {d : ℕ} {f : E d → ℝ} {x simp only [hessianQuadForm, map_smul, real_inner_smul_left, real_inner_smul_right] ring rw [hhomog] - have hc_sq_nonneg : (0 : ℝ) ≤ c ^ 2 := sq_nonneg c - nlinarith [hbound₀, hc_sq_nonneg] + exact (mul_comm a (c ^ 2)).trans_le + (mul_le_mul_of_nonneg_left hbound₀ (sq_nonneg c)) /-- Local compactness of `S` near `m⋆`: some closed ball piece of `S` is compact. -/ private theorem exists_compact_local_piece {d : ℕ} {S U : Set (E d)} diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/FlatCaseArithmetic.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/FlatCaseArithmetic.lean index 5bd312f6f7..3907344a25 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/FlatCaseArithmetic.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/FlatCaseArithmetic.lean @@ -6,12 +6,8 @@ Authors: Max Obreiter, Tobias Steinbrecher, Robert Foerster module public import Mathlib.Basic.Real.Basic -import Mathlib.Data.Rat.Cast.Order import Mathlib.Tactic.FieldSimp import Mathlib.Tactic.Linarith.Frontend -import Mathlib.Tactic.NormNum.Abs -import Mathlib.Tactic.NormNum.DivMod -import Mathlib.Tactic.NormNum.OfScientific /-! # Flat-Case Lyapunov Contraction: Arithmetic Core @@ -105,7 +101,7 @@ theorem flat_case_arithmetic : Fn1 + wn_sq / 2 + Tn1 ≤ (1 - a) * (Fn + Un / 2 + Tn) + a * proj_error := by -- Positivity of 1-a - have h1a : (0 : ℝ) < 1 - a := by linarith + have h1a : (0 : ℝ) < 1 - a := sub_pos.mpr ha_lt1 -- Clear the division in Tn: 2·(1-a)·Tn = (1+a)²·PVsq have hTn' : 2 * (1 - a) * Tn = (1 + a) ^ 2 * PVsq := by rw [hTn]; field_simp @@ -118,18 +114,20 @@ theorem flat_case_arithmetic -- Scale aiming by a > 0: a·ip_PperpG_en ≥ a·(Fnprime + μ/2·Esq − proj_error) have h_aim_sc : a * ip_PperpG_en ≥ a * Fnprime + a * (μ / 2) * Esq - a * proj_error := by have := mul_le_mul_of_nonneg_left h_aiming (le_of_lt ha_pos) - nlinarith + linarith only [this] -- Coefficient of PperpVsq: (1-a)·(a − εη)·PperpVsq ≥ 0 have hc_ppv : (1 - a) * (a - εη) * PperpVsq ≥ 0 := by - apply mul_nonneg _ hPperpVsq_nn - apply mul_nonneg <;> linarith + exact mul_nonneg (mul_nonneg h1a.le (sub_nonneg.mpr hεη_le)) hPperpVsq_nn -- Coefficient of PVsq: (3a + a² − (1-a)·εη)·PVsq ≥ 0 have hc_pv : (3 * a + a ^ 2 - (1 - a) * εη) * PVsq ≥ 0 := by - apply mul_nonneg _ hPVsq_nn; nlinarith [sq_nonneg a] + apply mul_nonneg _ hPVsq_nn + have hεη_scaled := mul_le_mul_of_nonneg_left hεη_le h1a.le + have ha_nonneg : 0 ≤ a := hεη_nn.trans hεη_le + linarith only [ha_nonneg, hεη_scaled, sq_nonneg a] -- Coefficient of PGsq: a·η·PGsq ≥ 0 - have hc_pg : a * η * PGsq ≥ 0 := by - simp_all + have hc_pg : a * η * PGsq ≥ 0 := + mul_nonneg (mul_nonneg ha_pos.le hη_pos.le) hPGsq_nn -- Main closure: combine all bounds and coefficient signs - nlinarith [hTn', h_descent, h_seg_sc, h_aim_sc, hc_ppv, hc_pv, hc_pg] + linarith only [hTn', h_descent, h_seg_sc, h_aim_sc, hc_ppv, hc_pv, hc_pg] end PLAcceleratedNesterovLean diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/GenMain.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/GenMain.lean index 3547dbfe5a..075336c134 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/GenMain.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/GenMain.lean @@ -44,7 +44,8 @@ private theorem descent_at_lookahead {d : ℕ} (f : E d → ℝ) (x'n : E d) (hx'_r09 : dist x'n m_star < r₀ / 9) : f (x'n - η • gradient f x'n) ≤ f x'n - η / 2 * ‖gradient f x'n‖ ^ 2 := by have hdist_nn := dist_nonneg (x := x'n) (y := m_star) - have hx'_Up : x'n ∈ U_plus := hball_sub (Metric.mem_ball.mpr (by linarith)) + have hx'_Up : x'n ∈ U_plus := + hball_sub (Metric.mem_ball.mpr (by linarith only [hx'_r09, hdist_nn])) have hgrad_lip' : ‖gradient f x'n‖ ≤ (↑L : ℝ) * dist x'n m_star := by have h := hf_lip.dist_le_mul x'n hx'_Up m_star hm_star_Up rwa [hg_zero, dist_zero_right] at h @@ -73,9 +74,9 @@ private theorem descent_at_lookahead {d : ℕ} (f : E d → ℝ) ≤ dist (x'n + t • (-(((1 : ℝ) / (↑L : ℝ)) • gradient f x'n))) x'n + dist x'n m_star := dist_triangle _ _ _ - _ ≤ 2 * dist x'n m_star := by linarith [h_step_bound] - _ < 2 * (r₀ / 9) := by linarith [hx'_r09] - _ < r₀ := by linarith + _ ≤ 2 * dist x'n m_star := by linarith only [h_step_bound] + _ < 2 * (r₀ / 9) := by linarith only [hx'_r09] + _ < r₀ := by linarith only [hx'_r09, hdist_nn] exact lsmooth_descent_at f L hL hU_open hf_diff_on hf_lip x'n hx'_Up hseg_x'n η hη /-- The gradient step moves the position by at most the distance of the look-ahead point @@ -101,11 +102,11 @@ private theorem nesterovStep_dist_le_two_mul {d : ℕ} (f : E d → ℝ) ≤ dist (x'n - η • gradient f x'n) x'n + dist x'n m_star := dist_triangle _ _ _ _ = η * ‖gradient f x'n‖ + dist x'n m_star := by rw [h_step_dist] _ ≤ η * ((L : ℝ) * dist x'n m_star) + dist x'n m_star := by - linarith [mul_le_mul_of_nonneg_left hgrad_lip (le_of_lt hη_pos)] + linarith only [hη_pos, hgrad_lip, mul_le_mul_of_nonneg_left hgrad_lip (le_of_lt hη_pos)] _ = 2 * dist x'n m_star := by have : η * ((L : ℝ) * dist x'n m_star) = dist x'n m_star := by rw [← mul_assoc, hηL, one_mul] - linarith + linarith only [this] /-- Distance bound for the next look-ahead point. Uses the identity `x'_{n+1} = (1+ρ)·x_{n+1} - ρ·x_n` and the triangle inequality: @@ -145,19 +146,20 @@ private theorem nesterovStep_lookahead_dist_lt {d : ℕ} (f : E d → ℝ) _ ≤ ‖(1 + ρ) • (sn1.x - m_star)‖ + ‖ρ • (sn.x - m_star)‖ := norm_sub_le _ _ _ = (1 + ρ) * ‖sn1.x - m_star‖ + ρ * ‖sn.x - m_star‖ := by - rw [norm_smul, norm_smul, Real.norm_eq_abs, abs_of_pos (by linarith : (0:ℝ) < 1 + ρ), + rw [norm_smul, norm_smul, Real.norm_eq_abs, + abs_of_pos (by linarith only [hρ_pos] : (0:ℝ) < 1 + ρ), Real.norm_eq_abs, abs_of_pos hρ_pos] _ = (1 + ρ) * dist sn1.x m_star + ρ * dist sn.x m_star := by simp only [dist_eq_norm] _ < (1 + ρ) * (2 * r) + ρ * r := by have h1 : (1 + ρ) * dist sn1.x m_star < (1 + ρ) * (2 * r) := - mul_lt_mul_of_pos_left hx1 (by linarith : (0:ℝ) < 1 + ρ) + mul_lt_mul_of_pos_left hx1 (by linarith only [hρ_pos, hρ_lt1] : (0:ℝ) < 1 + ρ) have h2 : ρ * dist sn.x m_star < ρ * r := mul_lt_mul_of_pos_left hx hρ_pos - linarith + linarith only [h1, h2] _ < 5 * r := by have h3 : ρ * r < r := mul_lt_of_lt_one_left hr_pos hρ_lt1 - linarith + linarith only [h3] /-- **Flat-case assembly.** The heart of the Lyapunov contraction in the flat case: with `w = (1-a)·P⊥v + √μ'·e - √η·P⊥g`, combining descent, aiming, the segment estimate @@ -221,12 +223,12 @@ private theorem flat_case_bound {d : ℕ} (P : E d →L[ℝ] E d) rw [inner_smul_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg η), mul_pow, Real.sq_sqrt (le_of_lt hη_pos)] at h1 rw [h_ip_decomp, hV_pyth] at h1 - linarith + linarith only [h1] -- Aiming: ⟨P⊥g, e⟩ ≥ Fnprime + μ'/2·‖e‖² − |⟨g, Pe⟩| (projector-freezing error) have h_aiming_arith : @inner ℝ _ _ (g - P g) e ≥ Fnprime + μ' / 2 * ‖e‖ ^ 2 - abs (@inner ℝ _ _ g (P e)) := by have hle := le_abs_self (@inner ℝ _ _ g (P e)) - linarith [h_ipGE_decomp] + linarith only [h_aim, h_ipGE_decomp, hle] -- w norm identity (with √μ'·√η = a) have hwn_sq_arith : ‖w‖ ^ 2 = (1 - a) ^ 2 * ‖v - P v‖ ^ 2 + μ' * ‖e‖ ^ 2 + @@ -295,18 +297,20 @@ private theorem lyapunovOfState_step_le {d : ℕ} (f : E d → ℝ) set x'n := sn.lookahead η with hx'n set gn := gradient f x'n with hgn have ha_pos : 0 < a := Real.sqrt_pos_of_pos (mul_pos hμ' hη_pos) - have hρ_pos : 0 < ρ := by rw [hρ]; apply div_pos <;> linarith + have hρ_pos : 0 < ρ := by + rw [hρ] + exact div_pos (sub_pos.mpr ha_lt1) (by linarith only [ha_pos]) have hgap_nn : 0 ≤ f sn.x - fStar f := sub_nonneg.mpr (ciInf_le hbdd sn.x) have hgap'_nn : 0 ≤ f sn1.x - fStar f := sub_nonneg.mpr (ciInf_le hbdd sn1.x) -- Parameter positivity - have h1a_pos : (0 : ℝ) < 1 + a := by linarith + have h1a_pos : (0 : ℝ) < 1 + a := by linarith only [hθ_pos, hθ_lt1, ha_pos] have h1a_ne : (1 + a : ℝ) ≠ 0 := ne_of_gt h1a_pos - have h1ma_ne : (1 - a : ℝ) ≠ 0 := ne_of_gt (by linarith) + have h1ma_ne : (1 - a : ℝ) ≠ 0 := ne_of_gt (by linarith only [ha_lt1]) -- λ = (1+a)²/(2(1-a)) > 0 have hlam_pos : (0 : ℝ) < (1 + a) ^ 2 / (2 * (1 - a)) := - div_pos (sq_pos_of_pos h1a_pos) (by linarith) + div_pos (sq_pos_of_pos h1a_pos) (by linarith only [ha_lt1]) -- Ln ≥ 0 have hLn_nn : 0 ≤ lyapunovOfState P μ' π f η sn := by simp only [lyapunovOfState] @@ -314,7 +318,7 @@ private theorem lyapunovOfState_step_le {d : ℕ} (f : E d → ℝ) le_of_lt hlam_pos have h1 := sq_nonneg ‖auxVarOfState P μ' π η sn‖ have h2 := mul_nonneg hlam_nn (sq_nonneg ‖P sn.v‖) - linarith + linarith only [hgap_nn, h1, h2] -- ══════════════ Tangential velocity identity ══════════════ -- P is a CLM, so P(sn1.v) = ρ • (P sn.v - √η • P gn) have hPv1 : P sn1.v = ρ • (P sn.v - Real.sqrt η • P gn) := by @@ -380,15 +384,16 @@ private theorem lyapunovOfState_step_le {d : ℕ} (f : E d → ℝ) rw [hTn1_val] refine flat_case_bound P hP_self_adj hP_idem μ' η ε a hμ' hη_pos hε_pos hε_bound rfl ha_lt1 sn.v gn (x'n - π x'n) wn hwn_eq Fn Fn1 (f x'n - fStar f) hgap_nn hgap'_nn - (sub_nonneg.mpr (ciInf_le hbdd x'n)) (by linarith [h_descent]) (by linarith [h_aim]) ?_ - rw [← h_diff_eq]; linarith [h_seg] + (sub_nonneg.mpr (ciInf_le hbdd x'n)) (by linarith only [h_descent]) + (by linarith only [h_aim]) ?_ + rw [← h_diff_eq]; linarith only [h_seg] -- ── Final assembly ── apply two_step_contraction_general a θ _ _ (δ_curv + a * abs (@inner ℝ _ _ gn (P (x'n - π x'n)))) ha_pos ha_lt1 hθ_pos hθ_lt1 hLn_nn · -- Goal: Ln' ≤ (1-a) * Ln + (δ_curv + proj_err_n) rw [hLn'_eq, hLn_eq] - linarith [h_Un1_half, h_flat] + linarith only [h_Un1_expand, hδ_def, h_flat, h_Un1_half] · -- Goal: (δ_curv + proj_err_n) ≤ θ * a * Ln exact h_absorb @@ -477,7 +482,7 @@ theorem lyapunov_contraction_of_state obtain ⟨r₀, hr₀_pos, hball_sub⟩ : ∃ r₀ > 0, Metric.ball m_star r₀ ⊆ U_plus := by exact Metric.isOpen_iff.mp hU_open m_star hm_star_Up -- Auxiliary inequalities for the chosen radii - have hr₀9 : (0 : ℝ) < r₀ / 9 := by linarith + have hr₀9 : (0 : ℝ) < r₀ / 9 := by linarith only [hr₀_pos] have hR_min : (0 : ℝ) < min (r₀ / 9) R_abs := lt_min hr₀9 hR_abs -- Ω = B(m⋆, min(r₀/9, R_abs)) — ensures iterates are in B(m⋆, R_abs) for the absorption have hΩ_sub_r09 : Metric.ball m_star (min (r₀ / 9) R_abs) ⊆ @@ -488,8 +493,8 @@ theorem lyapunov_contraction_of_state Metric.ball_subset_ball (min_le_right _ _) have hΩ_sub_Ωp : Metric.ball m_star (min (r₀ / 9) R_abs) ⊆ Metric.ball m_star (2 * r₀ / 3) := - hΩ_sub_r09.trans (Metric.ball_subset_ball (by linarith)) - have h23_le : 2 * r₀ / 3 ≤ r₀ := by linarith + hΩ_sub_r09.trans (Metric.ball_subset_ball (by linarith only [hr₀_pos])) + have h23_le : 2 * r₀ / 3 ≤ r₀ := by linarith only [hr₀_pos] have hΩp_sub_Up : Metric.ball m_star (2 * r₀ / 3) ⊆ U_plus := (Metric.ball_subset_ball h23_le).trans hball_sub -- Provide the existential witnesses: @@ -523,7 +528,9 @@ theorem lyapunov_contraction_of_state calc a = Real.sqrt (μ' * η) := rfl _ < Real.sqrt 1 := Real.sqrt_lt_sqrt hle hμη_lt1 _ = 1 := Real.sqrt_one - have hρ_pos : 0 < ρ := by rw [hρ]; apply div_pos <;> linarith + have hρ_pos : 0 < ρ := by + rw [hρ] + exact div_pos (sub_pos.mpr ha_lt1) (by linarith only [ha_pos]) -- Step 1 (Descent): f(x_{n+1}) ≤ f(x'_n) − (η/2)·‖g_n‖² have h_descent := descent_at_lookahead f L hL η hη U_plus hU_open hf_diff_on hf_lip m_star hm_star_Up hg_zero_mstar r₀ hball_sub (sn.lookahead η) hx'_ball_r09 @@ -542,7 +549,8 @@ theorem lyapunov_contraction_of_state intro t ht0 ht1 exact hΩp_sub_Up (hΩ_sub_Ωp ((convex_ball m_star (min (r₀ / 9) R_abs)) hx_in hx'_in - (by linarith : (0 : ℝ) ≤ 1 - t) ht0 (by linarith : (1 : ℝ) - t + t = 1))) + (by linarith only [ht1] : (0 : ℝ) ≤ 1 - t) ht0 + (by linarith only [] : (1 : ℝ) - t + t = 1))) -- Derive Ln ≤ R_abs² from Ln ≤ (min(r₀/9, R_abs))² ≤ R_abs² have hLn_le_Rabs : Ln ≤ R_abs ^ 2 := by calc Ln ≤ (min (r₀ / 9) R_abs) ^ 2 := hLn_bound @@ -555,13 +563,15 @@ theorem lyapunov_contraction_of_state (h_curv_absorb (hΩ_sub_Rabs hx_in) (hΩ_sub_Rabs hx'_in) hLn_le_Rabs) case x_next_in => rw [Metric.mem_ball] - exact h_sn1_dist.trans_lt (by linarith) + exact h_sn1_dist.trans_lt (by linarith only [hr₀_pos, hx'_ball_r09]) case x'_next_in => rw [Metric.mem_ball] have hρ_lt1 : ρ < 1 := by - rw [hρ]; rw [div_lt_one (by linarith : (0 : ℝ) < 1 + a)]; linarith + rw [hρ, div_lt_one (by linarith only [ha_pos] : (0 : ℝ) < 1 + a)] + linarith only [ha_pos] exact (nesterovStep_lookahead_dist_lt f η ρ hη_pos hρ_pos hρ_lt1 m_star (r₀ / 9) sn - hx_ball_r09 (h_sn1_dist.trans_lt (by linarith))).trans_le (by linarith) + hx_ball_r09 (h_sn1_dist.trans_lt (by linarith only [hx'_ball_r09]))).trans_le + (by linarith only [hr₀_pos]) /-- **State-based Lyapunov contraction along `nesterovSeqGen`.** diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/Step3.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/Step3.lean index 93106b8b9f..f88504b798 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/Step3.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/Step3.lean @@ -6,7 +6,6 @@ Authors: Max Obreiter, Tobias Steinbrecher, Robert Foerster module public import Mathlib.Analysis.Real.Sqrt -import LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.Step1 /-! # Lyapunov Contraction Step 3: Algebraic Assembly Lemmas @@ -105,12 +104,15 @@ theorem leading_coeff_slack_lower (a F U V : ℝ) -- § 2. Lambda-rho identity and tangential coefficient -- ════════════════════════════════════════════════════════════════════════════ -/-- λρ² = (1-a)/2. Already in Step1; re-exported for convenience. -/ +/-- λρ² = (1-a)/2. The direct calculation keeps this scalar module +independent of the analytic descent lemmas. -/ theorem lambda_rho_sq' (a ρ lam : ℝ) (ha_ne : 1 + a ≠ 0) (ha_pos : 1 - a ≠ 0) (hρ : ρ = (1 - a) / (1 + a)) (hlam : lam = (1 + a) ^ 2 / (2 * (1 - a))) : - lam * ρ ^ 2 = (1 - a) / 2 := - lambda_rho_sq a ρ lam ha_ne ha_pos hρ hlam + lam * ρ ^ 2 = (1 - a) / 2 := by + subst hρ + subst hlam + field_simp -- ════════════════════════════════════════════════════════════════════════════ -- § 3. Flat-case function-value bound diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/MainTheoremInternal.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/MainTheoremInternal.lean index aa90b87b73..4963d263e5 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/MainTheoremInternal.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/MainTheoremInternal.lean @@ -622,7 +622,7 @@ theorem nesterov_pl_accelerated_rate_embedded exact div_pos (Real.sqrt_pos_of_pos (div_pos hμ hL)) (by norm_num) have hθ_le : θ ≤ Real.sqrt (μ / ↑L) / 8 := by dsimp only [θ] - nlinarith [Real.sqrt_nonneg (μ / ↑L)] + linarith only [Real.sqrt_nonneg (μ / ↑L)] obtain ⟨U_tub, _hU_tub_open, _hS_sub_tub, hU_tub_sub, hGenTub⟩ := exists_general_tubular_subneighborhood M ι hι U hU_open hS_sub have hf_C2_tub : ContDiffOn ℝ 2 f U_tub := hf_C2.mono hU_tub_sub @@ -685,7 +685,7 @@ theorem nesterov_pl_accelerated_rate_c3_internal exact div_pos (Real.sqrt_pos_of_pos (div_pos hμ hL)) (by norm_num) have hθ_le : θ ≤ Real.sqrt (μ / ↑L) / 8 := by dsimp only [θ] - nlinarith [Real.sqrt_nonneg (μ / ↑L)] + linarith only [Real.sqrt_nonneg (μ / ↑L)] obtain ⟨U_tub, _hU_tub_open, _hS_sub_tub, hU_tub_sub, _hGenTub, hTub_sub⟩ := exists_tubular_subneighborhood_of_c3_pl hd hU_open hS_sub hPL hf_C3 have hf_C2_tub : ContDiffOn ℝ 2 f U_tub := diff --git a/LeanPool/PLAcceleratedNesterovLean/Convergence/NesterovConvergence.lean b/LeanPool/PLAcceleratedNesterovLean/Convergence/NesterovConvergence.lean index 98fd214243..4a87ede304 100644 --- a/LeanPool/PLAcceleratedNesterovLean/Convergence/NesterovConvergence.lean +++ b/LeanPool/PLAcceleratedNesterovLean/Convergence/NesterovConvergence.lean @@ -58,22 +58,27 @@ private lemma rate_bound_case_small {θ a : ℝ} have h_exp_lb : 1 - a + a ^ 2 / 4 ≤ Real.exp (-a) := by have h := @Real.one_sub_div_pow_le_exp_neg 2 a (by simp; linarith : a ≤ ↑(2 : ℕ)) simp only [Nat.cast_ofNat] at h - nlinarith [sq_nonneg (1 - a / 2)] - nlinarith + linarith only [h] + have ha_nn : 0 ≤ a := by linarith only [hθ_nn, hθ_le] + linarith only [h_exp_lb, mul_le_mul_of_nonneg_right hθ_le ha_nn] /-- For θ ≤ 1/4 and a ≥ 2: (1−θ)√(1−θ) ≥ 1/2, so rate ≤ 1−a/2 ≤ 0 ≤ exp(−a). -/ private lemma rate_bound_case_large {θ a : ℝ} (_hθ_nn : 0 ≤ θ) (hθ_le : θ ≤ 1 / 4) (ha_ge2 : 2 ≤ a) : 1 - (1 - θ) * Real.sqrt (1 - θ) * a ≤ Real.exp (-a) := by - have h1θ_nn : (0 : ℝ) ≤ 1 - θ := by linarith - have h1θ_ge : (3 : ℝ)/4 ≤ 1 - θ := by linarith + have h1θ_nn : (0 : ℝ) ≤ 1 - θ := by linarith only [hθ_le] + have h1θ_ge : (3 : ℝ)/4 ≤ 1 - θ := by linarith only [hθ_le] have h_sqrt_lb : Real.sqrt (1 - θ) ≥ 2/3 := by rw [ge_iff_le, ← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2/3)] - exact Real.sqrt_le_sqrt (by nlinarith [sq_nonneg (2:ℝ)]) - have h_prod : (1 - θ) * Real.sqrt (1 - θ) ≥ 1/2 := by nlinarith - have h1 : (1 - θ) * Real.sqrt (1 - θ) * a ≥ 1 := by nlinarith - linarith [Real.exp_pos (-a)] + exact Real.sqrt_le_sqrt (by linarith only [hθ_le]) + have h_prod : (1 - θ) * Real.sqrt (1 - θ) ≥ 1/2 := by + linarith only [mul_le_mul h1θ_ge h_sqrt_lb + (by norm_num : (0 : ℝ) ≤ 2/3) h1θ_nn] + have h1 : (1 - θ) * Real.sqrt (1 - θ) * a ≥ 1 := by + have ha_nn : 0 ≤ a := by linarith only [ha_ge2] + linarith only [ha_ge2, mul_le_mul_of_nonneg_right h_prod ha_nn] + linarith only [h1, Real.exp_pos (-a)] -- Scalar comparison with the retuning parameter θ explicit. /-- If `0 < θ ≤ min (√(μ/L)/8) (1/4)`, then the retuned one-step factor from @@ -87,7 +92,7 @@ theorem nesterov_rate_bound_theta 1 - (1 - θ) * Real.sqrt (muOfTheta μ θ * (1 / ↑L)) ≤ Real.exp (-(1 / Real.sqrt (↑L / μ))) := by set a := Real.sqrt (μ / ↑L) with ha_def - have h1θ_nn : 0 ≤ 1 - θ := by linarith + have h1θ_nn : 0 ≤ 1 - θ := by linarith only [hθ_le_quarter] have ha_pos : 0 < a := Real.sqrt_pos_of_pos (div_pos hμ hL) have h_prod_eq : muOfTheta μ θ * (1 / ↑L) = (μ / ↑L) * (1 - θ) := by change μ * (1 - θ) * (1 / ↑L) = μ / ↑L * (1 - θ) @@ -97,20 +102,22 @@ theorem nesterov_rate_bound_theta rw [ha_def, one_div, ← Real.sqrt_inv, inv_div] rw [h_target_eq] have h_sqrt_lb : Real.sqrt (1 - θ) ≥ 1 - θ := by - have hle : (1 - θ) ^ 2 ≤ 1 - θ := by nlinarith [mul_nonneg hθ_pos.le h1θ_nn] + have hle : (1 - θ) ^ 2 ≤ 1 - θ := by + linarith only [mul_nonneg hθ_pos.le h1θ_nn] calc (1 : ℝ) - θ = Real.sqrt ((1 - θ) ^ 2) := (Real.sqrt_sq h1θ_nn).symm _ ≤ Real.sqrt (1 - θ) := Real.sqrt_le_sqrt hle have h_prod_lb : (1 - θ) * Real.sqrt (1 - θ) ≥ 1 - 2 * θ := by - nlinarith [mul_le_mul_of_nonneg_left h_sqrt_lb h1θ_nn, sq_nonneg θ] + linarith only [mul_le_mul_of_nonneg_left h_sqrt_lb h1θ_nn, sq_nonneg θ] have h_rate_ub : 1 - (1 - θ) * (a * Real.sqrt (1 - θ)) ≤ 1 - (1 - 2 * θ) * a := by have : (1 - θ) * (a * Real.sqrt (1 - θ)) = (1 - θ) * Real.sqrt (1 - θ) * a := by ring - rw [this]; nlinarith + rw [this] + exact sub_le_sub_left (mul_le_mul_of_nonneg_right h_prod_lb ha_pos.le) 1 by_cases ha2 : a ≤ 2 - · linarith [rate_bound_case_small hθ_pos.le hθ_le ha_pos ha2] + · exact h_rate_ub.trans (rate_bound_case_small hθ_pos.le hθ_le ha_pos ha2) · push Not at ha2 - linarith [rate_bound_case_large hθ_pos.le hθ_le_quarter ha2.le] + linarith only [rate_bound_case_large hθ_pos.le hθ_le_quarter ha2.le] -- The local assembly uses the full Lyapunov argument and rate conversion. /-! ## State-position local theorem family -/ @@ -268,7 +275,7 @@ theorem nesterov_convergence_at_base_point_position_params have hL₀_le_two_gap : L₀ ≤ 2 * (f x₀ - fStar f) := by rw [show L₀ = (f x₀ - fStar f) + μ' / 2 * ‖x₀ - π x₀‖ ^ 2 from (hlyap_eq_psi x₀)] - nlinarith + linarith only [hQG₀_norm] have hsqrt_pos : 0 < Real.sqrt (μ' * η) := Real.sqrt_pos_of_pos (by positivity) have hr_pos : 0 < r := by simp only [hr_def] @@ -324,7 +331,7 @@ theorem nesterov_convergence_at_base_point_position_params (Real.exp (-(1 / Real.sqrt (↑L / μ)))) ^ k := by apply mul_le_mul_of_nonneg_left · exact pow_le_pow_left₀ (le_of_lt hr_pos) hr_le_exp k - · nlinarith + · exact mul_nonneg (by norm_num) hgap₀_nn _ = 2 * Real.exp (-(↑k / Real.sqrt (↑L / μ))) * (f x₀ - fStar f) := by rw [h_exp_pow] ring diff --git a/LeanPool/PLAcceleratedNesterovLean/MorseBott/GradAlign.lean b/LeanPool/PLAcceleratedNesterovLean/MorseBott/GradAlign.lean index ff7ae6876f..1a474209c2 100644 --- a/LeanPool/PLAcceleratedNesterovLean/MorseBott/GradAlign.lean +++ b/LeanPool/PLAcceleratedNesterovLean/MorseBott/GradAlign.lean @@ -37,8 +37,8 @@ variable {E : Type*} omit [FiniteDimensional ℝ E] in private lemma hasDerivAt_line' (x v : E) (t : ℝ) : HasDerivAt (fun s => x + s • v) v t := by - have := (hasDerivAt_id t).smul_const v - simp_all + simpa only [id_eq, one_smul, hasDerivAt_const_add_iff] using + (hasDerivAt_id t).smul_const v omit [FiniteDimensional ℝ E] in private lemma hasDerivAt_f_line' {f : E → ℝ} {x v : E} {t : ℝ} @@ -57,8 +57,7 @@ private lemma hasDerivAt_fderiv_line_eval' {f : E → ℝ} {x v : E} {t : ℝ} ((hf.fderiv_right le_rfl).differentiableAt one_ne_zero).hasFDerivAt.comp_hasDerivAt t (hasDerivAt_line' x v t) - have h := hΦ.clm_apply (hasDerivAt_const t v) - simp_all + simpa only [map_zero, add_zero] using hΦ.clm_apply (hasDerivAt_const t v) omit [FiniteDimensional ℝ E] in private lemma taylor_remainder_bound' {f : E → ℝ} {x v : E} @@ -76,8 +75,8 @@ private lemma taylor_remainder_bound' {f : E → ℝ} {x v : E} have hb : ∀ s ∈ Ico (0:ℝ) 1, ‖hessian f (x + s • v) v v‖ ≤ C * ‖v‖ ^ 2 := fun s hs => hbound s ⟨hs.1, le_of_lt hs.2⟩ - have h := norm_image_sub_le_of_norm_deriv_le_segment' hd hb - simp_all + simpa only [zero_smul, add_zero, sub_zero] using + norm_image_sub_le_of_norm_deriv_le_segment' hd hb have hk_deriv : ∀ s ∈ Icc (0:ℝ) 1, HasDerivWithinAt (fun s => f (x + s • v) - f x - s * (fderiv ℝ f x v)) @@ -99,10 +98,10 @@ private lemma taylor_remainder_bound' {f : E → ℝ} {x v : E} calc ‖fderiv ℝ f (x + s • v) v - fderiv ℝ f x v‖ ≤ C * ‖v‖ ^ 2 * (s - 0) := h1 _ ≤ C * ‖v‖ ^ 2 * 1 := - mul_le_mul_of_nonneg_left (by linarith [hs.2]) (mul_nonneg hC (sq_nonneg _)) + mul_le_mul_of_nonneg_left (by linarith only [hs, hs.2]) (mul_nonneg hC (sq_nonneg _)) _ = C * ‖v‖ ^ 2 := mul_one _ - have hmvt2 := norm_image_sub_le_of_norm_deriv_le_segment_01' hk_deriv hk_bound - simp_all + simpa only [one_smul, one_mul, zero_smul, add_zero, sub_self, zero_mul, sub_zero] + using norm_image_sub_le_of_norm_deriv_le_segment_01' hk_deriv hk_bound -- ═══════════════════════════════════════════════════════════════ -- § Main theorem diff --git a/LeanPool/PLAcceleratedNesterovLean/MorseBott/HessianPL/Main.lean b/LeanPool/PLAcceleratedNesterovLean/MorseBott/HessianPL/Main.lean index 60d5a69c07..cf4a76f64e 100644 --- a/LeanPool/PLAcceleratedNesterovLean/MorseBott/HessianPL/Main.lean +++ b/LeanPool/PLAcceleratedNesterovLean/MorseBott/HessianPL/Main.lean @@ -51,7 +51,7 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) set Hvv := H v v set normHv := ‖H v‖ set gap := μ * Hvv - normHv ^ 2 with hgap_def - have hgap_pos : 0 < gap := by linarith + have hgap_pos : 0 < gap := by linarith only [h_contra] -- Derivative of fderiv at x₀ is the hessian have hhess_deriv : HasFDerivAt (fderiv ℝ f) H x₀ := ((hf.fderiv_right le_rfl).differentiableAt one_ne_zero).hasFDerivAt @@ -59,7 +59,7 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) -- Gradient approximation: fderiv ℝ f (x₀ + h) - H h =o[𝓝 0] h have hgrad_o : (fun h => fderiv ℝ f (x₀ + h) - H h) =o[𝓝 (0 : E)] fun h => h := by have := hasFDerivAt_iff_isLittleO_nhds_zero.mp hhess_deriv - simp_all + simpa only [hdf0, sub_zero] using this -- Compose with ray t ↦ t • v have hray_tend : Tendsto (fun t : ℝ => t • v) (𝓝 0) (𝓝 (0 : E)) := by rw [show (0 : E) = (0 : ℝ) • v from (zero_smul ℝ v).symm] @@ -74,7 +74,7 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) have htend : Tendsto (fun t : ℝ => x₀ + t • v) (𝓝 0) (𝓝 x₀) := by have key : Tendsto (fun t : ℝ => x₀ + t • v) (𝓝 0) (𝓝 (x₀ + (0 : ℝ) • v)) := tendsto_const_nhds.add (tendsto_id.smul tendsto_const_nhds) - simp_all + simpa only [zero_smul, add_zero] using key exact (htend.eventually hPL).filter_mono nhdsWithin_le_nhds -- Taylor bound have hTaylor := taylor_ray_isLittleO_pl f x₀ v hf hmin @@ -94,7 +94,7 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) -- Taylor lower bound: f(x₀+tv) - f(x₀) ≥ t²/2 · Hvv - gap/(4μ) · t² rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (sq_nonneg t)] at hT have hT_lower : t ^ 2 / 2 * Hvv - gap / (4 * μ) * t ^ 2 ≤ - f (x₀ + t • v) - f x₀ := by linarith [abs_le.mp hT] + f (x₀ + t • v) - f x₀ := by linarith only [hT, abs_le.mp hT] -- Gradient upper bound: ‖fderiv(x₀+tv)‖ ≤ t·‖Hv‖ + ε'·t·‖v‖ have hG_upper : ‖fderiv ℝ f (x₀ + t • v)‖ ≤ t * normHv + ε' * t * ‖v‖ := by have h1 : ‖fderiv ℝ f (x₀ + t • v)‖ ≤ ‖t • H v‖ + @@ -109,7 +109,7 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) ≤ ε' * ‖t • v‖ := hG _ = ε' * (|t| * ‖v‖) := by rw [norm_smul, Real.norm_eq_abs] _ = ε' * (t * ‖v‖) := by rw [abs_of_pos ht_pos] - linarith [h1, h2, h3] + linarith only [h1, h2, h3] -- PŁ gives upper bound using gradient have hPL_upper : f (x₀ + t • v) - f x₀ ≤ (2 * μ)⁻¹ * (t * normHv + ε' * t * ‖v‖) ^ 2 := by @@ -117,7 +117,8 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) ≤ (2 * μ)⁻¹ * ‖fderiv ℝ f (x₀ + t • v)‖ ^ 2 := hPLt _ ≤ (2 * μ)⁻¹ * (t * normHv + ε' * t * ‖v‖) ^ 2 := by apply mul_le_mul_of_nonneg_left _ (by positivity) - exact sq_le_sq' (by linarith [norm_nonneg (fderiv ℝ f (x₀ + t • v))]) hG_upper + exact sq_le_sq' + (by linarith only [hG_upper, norm_nonneg (fderiv ℝ f (x₀ + t • v))]) hG_upper -- Combine and factor out t² have h_sq_factor : (t * normHv + ε' * t * ‖v‖) ^ 2 = t ^ 2 * (normHv + ε' * ‖v‖) ^ 2 := by ring @@ -127,14 +128,11 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) have hv_ne : v ≠ 0 := by intro h have : (H v) v = 0 := by simp only [h, map_zero] - linarith [show Hvv = (H v) v from rfl] + linarith only [hvv_pos, this, show Hvv = (H v) v from rfl] have hv_norm_pos : 0 < ‖v‖ := norm_pos_iff.mpr hv_ne have h_final : gap / 2 ≤ 2 * normHv * (ε' * ‖v‖) + (ε' * ‖v‖) ^ 2 := by - have h_combined : t ^ 2 / 2 * Hvv - gap / (4 * μ) * t ^ 2 ≤ - (2 * μ)⁻¹ * (t ^ 2 * (normHv + ε' * ‖v‖) ^ 2) := by - linarith [h_sq_factor ▸ hPL_upper] have h_factored : t ^ 2 * (Hvv / 2 - gap / (4 * μ)) ≤ - t ^ 2 * ((2 * μ)⁻¹ * (normHv + ε' * ‖v‖) ^ 2) := by linarith + t ^ 2 * ((2 * μ)⁻¹ * (normHv + ε' * ‖v‖) ^ 2) := by linarith only [hT_lower, hPL_upper] have h_div : Hvv / 2 - gap / (4 * μ) ≤ (2 * μ)⁻¹ * (normHv + ε' * ‖v‖) ^ 2 := le_of_mul_le_mul_left h_factored ht_sq_pos have h_eq1 : μ * (Hvv / 2 - gap / (4 * μ)) = μ * Hvv / 2 - gap / 4 := by @@ -143,11 +141,10 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) (normHv + ε' * ‖v‖) ^ 2 / 2 := by field_simp have h_mul_mu : μ * Hvv / 2 - gap / 4 ≤ (normHv + ε' * ‖v‖) ^ 2 / 2 := by have := mul_le_mul_of_nonneg_left h_div hμ.le - linarith [h_eq1, h_eq2] - have h_gap_eq : μ * Hvv = gap + normHv ^ 2 := by linarith [hgap_def] + linarith only [h_eq1, h_eq2, this] have h_expand : (normHv + ε' * ‖v‖) ^ 2 = normHv ^ 2 + 2 * normHv * (ε' * ‖v‖) + (ε' * ‖v‖) ^ 2 := by ring - linarith [h_expand] + linarith only [h_mul_mu, h_expand] -- But ε' is too small for this to hold have hε'v_bound : ε' * ‖v‖ < gap / (4 * (normHv + 1) * (gap + 1)) := by calc ε' * ‖v‖ @@ -160,9 +157,7 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) have hBlt1 : gap / (4 * (normHv + 1) * (gap + 1)) < 1 := by rw [div_lt_one (by positivity : (0:ℝ) < 4 * (normHv + 1) * (gap + 1))] have h_prod := mul_nonneg hNHv hgap_pos.le - have h_exp : 4 * (normHv + 1) * (gap + 1) = - 4 * normHv * gap + 4 * normHv + 4 * gap + 4 := by ring - linarith + linarith only [h_contra, hNHv, h_prod] have hδp : (0 : ℝ) < ε' * ‖v‖ := mul_pos hε'_pos hv_norm_pos have hδlt1 : ε' * ‖v‖ < 1 := lt_trans hε'v_bound hBlt1 have hstep1 : (ε' * ‖v‖) ^ 2 < ε' * ‖v‖ := by @@ -172,19 +167,21 @@ lemma muPL_norm_sq_bound (f : E → ℝ) (μ : ℝ) (x₀ v : E) (2 * normHv + 1) * (gap / (4 * (normHv + 1) * (gap + 1))) := by have h1 : 2 * normHv * (ε' * ‖v‖) ≤ 2 * normHv * (gap / (4 * (normHv + 1) * (gap + 1))) := - mul_le_mul_of_nonneg_left hε'v_bound.le (by linarith) + mul_le_mul_of_nonneg_left hε'v_bound.le (by linarith only [hNHv]) have h2 : (ε' * ‖v‖) ^ 2 < gap / (4 * (normHv + 1) * (gap + 1)) := lt_trans hstep1 hε'v_bound - linarith [show (2 * normHv + 1) * (gap / (4 * (normHv + 1) * (gap + 1))) = + linarith only [hε'v_bound, hstep1, h1, + show (2 * normHv + 1) * (gap / (4 * (normHv + 1) * (gap + 1))) = 2 * normHv * (gap / (4 * (normHv + 1) * (gap + 1))) + gap / (4 * (normHv + 1) * (gap + 1)) from by ring] - have hstep3 : (2 * normHv + 1) ≤ 2 * (normHv + 1) := by linarith + have hstep3 : (2 * normHv + 1) ≤ 2 * (normHv + 1) := by linarith only [] have hstep4 : 2 * (normHv + 1) * (gap / (4 * (normHv + 1) * (gap + 1))) = gap / (2 * (gap + 1)) := by field_simp; ring have hstep5 : gap / (2 * (gap + 1)) < gap / 2 := by rw [div_lt_div_iff₀ (by positivity : (0:ℝ) < 2 * (gap + 1)) two_pos] - linarith [mul_pos hgap_pos hgap_pos] - linarith [mul_le_mul_of_nonneg_right hstep3 hBp.le] + linarith only [hgap_pos, mul_pos hgap_pos hgap_pos] + linarith only [h_final, hε'v_bound, hδp, hstep2, hstep4, hstep5, + mul_le_mul_of_nonneg_right hstep3 hBp.le] -- ════════════════════════════════════════════════════════════════════════════ -- § F. Rayleigh quotient minimizer argument @@ -231,7 +228,8 @@ theorem hessian_coercive_on_orthogonal_of_MuPL_impl (f : E → ℝ) (μ : ℝ) ( rcases eq_or_lt_of_le hc_nonneg with hc0 | hc_pos · -- c = 0, so H(w₀,w₀) = 0, then w₀ ∈ ker(H), but w₀ ∈ ker(H)⊥ exfalso - have : w₀ ∈ K := mem_hessianKer_of_zero_quad f x₀ w₀ hf hmin (by linarith) + have : w₀ ∈ K := + mem_hessianKer_of_zero_quad f x₀ w₀ hf hmin (by linarith only [hc_nonneg, hc0]) have : w₀ ∈ K ⊓ K.orthogonal := ⟨this, hw₀_orth⟩ rw [K.orthogonal_disjoint.eq_bot] at this have hw0_ne : w₀ ≠ 0 := by rw [ne_eq, ← norm_eq_zero, hw₀_norm]; exact one_ne_zero @@ -255,8 +253,8 @@ theorem hessian_coercive_on_orthogonal_of_MuPL_impl (f : E → ℝ) (μ : ℝ) ( have hv_ne : (‖v‖ : ℝ) ≠ 0 := ne_of_gt hv_norm_pos have h2 : ‖v‖⁻¹ * (‖v‖⁻¹ * (H v) v) * ‖v‖ ^ 2 = (H v) v := by field_simp - linarith - linarith [mul_le_mul_of_nonneg_right hc_bound (sq_nonneg ‖v‖)] + linarith only [h1, h2] + linarith only [hc_bound, this, mul_le_mul_of_nonneg_right hc_bound (sq_nonneg ‖v‖)] -- Step 6: Prove μ ≤ c -- The minimizer w₀ is an eigenvector: H(w₀) = c · innerSL ℝ w₀ -- This gives ‖H(w₀)‖ = c, and then PŁ gives μ ≤ c. @@ -294,7 +292,7 @@ theorem hessian_coercive_on_orthogonal_of_MuPL_impl (f : E → ℝ) (μ : ℝ) ( have h0 : ‖w₀ + t • z‖ = 0 := by rw [htz, norm_zero] have h1 : ‖w₀ + t • z‖ ^ 2 = 0 := by rw [h0]; ring have h2 := hnorm_sq t - linarith [mul_nonneg (sq_nonneg t) (sq_nonneg ‖z‖)] + linarith only [h1, h2, mul_nonneg (sq_nonneg t) (sq_nonneg ‖z‖)] · have hw_in_S : (‖w₀ + t • z‖⁻¹ • (w₀ + t • z)) ∈ S := by constructor · exact K.orthogonal.smul_mem _ @@ -327,7 +325,7 @@ theorem hessian_coercive_on_orthogonal_of_MuPL_impl (f : E → ℝ) (μ : ℝ) ( intro t have h1 := hRQ t rw [hexpand] at h1 - linarith + linarith only [h1] -- If a ≠ 0, choosing t small with sign opposite to a gives contradiction -- t(2a + t(Hzz - c‖z‖²)) ≥ 0 for all t -- At t = 0: value = 0, derivative in t = 2a ≠ 0 @@ -350,8 +348,8 @@ theorem hessian_coercive_on_orthogonal_of_MuPL_impl (f : E → ℝ) (μ : ℝ) ( have h_sq := sq_nonneg (2 * d - 1) have h_sq_exp : (2 * d - 1) ^ 2 = 4 * d ^ 2 - 4 * d + 1 := by ring rw [h_sq_exp] at h_sq - have h_neg : d - 2 * den₂ < 0 := by linarith [sq_nonneg d] - linarith [mul_neg_of_pos_of_neg ha2 h_neg] + have h_neg : d - 2 * den₂ < 0 := by linarith only [hden₂_pos, ha2, h_sq, sq_nonneg d] + linarith only [h2, ha2, h_neg, mul_neg_of_pos_of_neg ha2 h_neg] -- Eigenvector equation: H(w₀) = c • innerSL ℝ w₀ have h_eig : H w₀ = c • innerSL ℝ w₀ := by ext e diff --git a/LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/IFT.lean b/LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/IFT.lean index 790a6ac0f2..aea5040caa 100644 --- a/LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/IFT.lean +++ b/LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/IFT.lean @@ -85,14 +85,7 @@ private lemma contDiff_adjoint [NormedAddCommGroup F₂] [InnerProductSpace ℝ F₂] [FiniteDimensional ℝ F₂] : ContDiff ℝ n (ContinuousLinearMap.adjoint : (F₁ →L[ℝ] F₂) → (F₂ →L[ℝ] F₁)) := - IsBoundedLinearMap.contDiff { - map_add := fun A B => by - simp_all - map_smul := fun c A => by - simp_all - bound := ⟨1, one_pos, fun A => by - simp_all⟩ - } + (ContinuousLinearMap.adjoint : (F₁ →L[ℝ] F₂) ≃ₗᵢ[ℝ] (F₂ →L[ℝ] F₁)).contDiff lemma optimalityEqn_contDiff {V : Submodule ℝ E} {φ : V → V.orthogonal}