Skip to content

Optimize PLAcceleratedNesterovLean arithmetic proofs and imports #763

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 1 commit into
base: main
Choose a base branch
from
+257 −281
Open

Optimize PLAcceleratedNesterovLean arithmetic proofs and imports #763

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 26 additions & 21 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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⟩

Expand Down Expand Up @@ -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 ─────────────────────────────────
Expand All @@ -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 :=
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 ─────────────────────────────────
Expand All @@ -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 _ _)
Expand All @@ -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, ?_⟩
Expand Down
60 changes: 21 additions & 39 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Core.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)²)
Expand All @@ -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
31 changes: 16 additions & 15 deletions LeanPool/PLAcceleratedNesterovLean/Convergence/Coercivity/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, ?_⟩
Expand All @@ -100,31 +100,32 @@ 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)))
(T ^ 2) Ln hgap_nn (sq_nonneg _) hlam_pos (sq_nonneg _) rfl
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
_ ≤ Ln / (1 / 2) := by
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)
Expand All @@ -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)
Expand All @@ -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.**

Expand Down
Loading
Loading