Lyapunov Coercivity

The Lyapunov function L_n controls the physical quantities ‖v_n‖² + μ'‖e_n‖² and the potential Ψ(x_n). The constants depend only on a = √(μ'·η).

theorem PLAcceleratedNesterovLean.lyapunov_coercivity_gen {d : ℕ} (_hd : 0 < d) (f : E d → ℝ) (L : NNReal) (_hL : 0 < ↑L) (μ' : ℝ) (hμ' : 0 < μ') (η : ℝ) (_hη : η = 1 / ↑L) (hη_pos : 0 < η) (hμη_lt1 : μ' * η < 1) (S : Set (E d)) (_hM_argmin : S = argminSet f) (π : E d → E d) (_hπ_proj : ∀ x ∈ S, π x = x) (hπ_in_S : ∀ (x : E d), π x ∈ S) (P : E d →L[ℝ] E d) (_hP_idem : ∀ (x : E d), P (P x) = P x) (_hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_ortho : ∀ (v : E d), ‖v‖ ^ 2 = ‖P v‖ ^ 2 + ‖v - P v‖ ^ 2) (Ω : Set (E d)) (hπ_metric : ∀ x ∈ Ω, dist x (π x) = Metric.infDist x S) (hQG : ∀ x ∈ Ω, f x - fStar f ≥ μ' / 2 * Metric.infDist x S ^ 2) : ∃ (C_coer : ℝ) (C_Ψ : ℝ), 0 < C_coer ∧ 0 < C_Ψ ∧ ∀ (s : NesterovState d), have Ln := lyapunovOfState P μ' π f η s; s.x ∈ Ω → s.lookahead η ∈ Ω → ‖s.v‖ ^ 2 + μ' * ‖normalDispOfState π η s‖ ^ 2 ≤ C_coer * Ln ∧ psi f μ' S s.x ≤ C_Ψ * Ln

State-based coercivity of the Lyapunov function.

Whenever x_n, x'_n ∈ Ω, the Lyapunov function controls: (1) ‖v_n‖² + μ'‖e_n‖² ≤ C_coer · L_n (2) Ψ(x_n) ≤ C_Ψ · L_n

This version is state-based: it quantifies over arbitrary NesterovStates rather than sequence indices.

theorem PLAcceleratedNesterovLean.lyapunov_coercivity {d : ℕ} (_hd : 0 < d) (f : E d → ℝ) (L : NNReal) (_hL : 0 < ↑L) (μ' : ℝ) (hμ' : 0 < μ') (η : ℝ) (_hη : η = 1 / ↑L) (hη_pos : 0 < η) (hμη_lt1 : μ' * η < 1) (ρ : ℝ) (_hρ : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η))) (S : Set (E d)) (_hM_argmin : S = argminSet f) (π : E d → E d) (_hπ_proj : ∀ x ∈ S, π x = x) (hπ_in_S : ∀ (x : E d), π x ∈ S) (P : E d →L[ℝ] E d) (_hP_idem : ∀ (x : E d), P (P x) = P x) (_hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y)) (hP_ortho : ∀ (v : E d), ‖v‖ ^ 2 = ‖P v‖ ^ 2 + ‖v - P v‖ ^ 2) (Ω : Set (E d)) (hπ_metric : ∀ x ∈ Ω, dist x (π x) = Metric.infDist x S) (hQG : ∀ x ∈ Ω, f x - fStar f ≥ μ' / 2 * Metric.infDist x S ^ 2) : ∃ (C_coer : ℝ) (C_Ψ : ℝ), 0 < C_coer ∧ 0 < C_Ψ ∧ ∀ (x₁ : E d) (n : ℕ), have s := nesterovSeq f η ρ x₁ n; have Ln := lyapunov P μ' π f η ρ x₁ n; s.x ∈ Ω → s.lookahead η ∈ Ω → ‖s.v‖ ^ 2 + μ' * ‖normalDisp π f η ρ x₁ n‖ ^ 2 ≤ C_coer * Ln ∧ psi f μ' S s.x ≤ C_Ψ * Ln

Coercivity of the Lyapunov function.

Whenever x_n, x'_n ∈ Ω, the Lyapunov function controls: (1) ‖v_n‖² + μ'‖e_n‖² ≤ C_coer · L_n (2) Ψ(x_n) ≤ C_Ψ · L_n