State-Based Lyapunov Contraction #
Generalization of lyapunov_contraction (Main.lean) to arbitrary NesterovState,
supporting nonzero initial velocity. Used by GenLocalArgument.lean.
theorem
PLAcceleratedNesterovLean.lyapunov_contraction_gen
{d : ℕ}
(_hd : 0 < d)
(f : E d → ℝ)
(L : NNReal)
(hL : 0 < ↑L)
(μ' : ℝ)
(hμ' : 0 < μ')
(θ : ℝ)
(hθ_pos : 0 < θ)
(hθ_lt1 : θ < 1)
(η : ℝ)
(hη : η = 1 / ↑L)
(hη_pos : 0 < η)
(ρ : ℝ)
(hρ : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η)))
(S : Set (E d))
(hM_argmin : S = argminSet f)
(π : E d → E d)
(_hπ_in_S : ∀ (x : E d), π x ∈ S)
(_hπ_proj : ∀ x ∈ S, π x = x)
(hgrad_zero : ∀ x ∈ S, gradient f x = 0)
(P : E d →L[ℝ] E d)
(m_star : E d)
(hm_star : m_star ∈ S)
(ε : ℝ)
(hε_pos : 0 < ε)
(hε_bound : ε * η ≤ √(μ' * η))
(hμη_lt1 : μ' * η < 1)
(U_plus : Set (E d))
(hU_open : IsOpen U_plus)
(hm_star_Up : m_star ∈ U_plus)
(hf_diff_on : DifferentiableOn ℝ f U_plus)
(hf_lip : LipschitzOnWith L (gradient f) U_plus)
(hStrAim : ∀ x ∈ U_plus, inner ℝ (gradient f x) (x - π x) ≥ f x - fStar f + μ' / 2 * ‖x - π x‖ ^ 2)
(hHess_lower : ∀ x ∈ U_plus, ∀ (ξ : E d), hessianQuadForm f x ξ ≥ -ε * ‖ξ‖ ^ 2)
(_hπ_kills_normal : ∀ x ∈ U_plus, (fderiv ℝ π (π x)) (x - π x) = 0)
(hP_self_adj : ∀ (x y : E d), inner ℝ (P x) y = inner ℝ x (P y))
(hP_idem : ∀ (x : E d), P (P x) = P x)
(hSegment :
∀ (x z : E d),
x ∈ U_plus →
z ∈ U_plus →
(∀ (t : ℝ), 0 ≤ t → t ≤ 1 → (1 - t) • z + t • x ∈ U_plus) →
inner ℝ (gradient f x) (x - z) ≥ f x - f z - ε / 2 * ‖x - z‖ ^ 2)
(R_abs : ℝ)
(hR_abs : 0 < R_abs)
(h_curv_absorb :
∀ (s₀ : NesterovState d) (n : ℕ),
(nesterovSeqGen f η ρ s₀ n).x ∈ Metric.ball m_star R_abs →
(nesterovSeqGen f η ρ s₀ n).lookahead η ∈ Metric.ball m_star R_abs →
lyapunovOfState P μ' π f η (nesterovSeqGen f η ρ s₀ n) ≤ R_abs ^ 2 →
have sn := nesterovSeqGen f η ρ s₀ n;
have gn := gradient f (sn.lookahead η);
have en := sn.lookahead η - π (sn.lookahead η);
have ξn := curvatureErrorOfState (⇑P) π f η ρ sn;
have un1 := auxVarOfState P μ' π η (nesterovStep f η ρ sn);
have wn := un1 - √μ' • ξn;
have δ_curv := √μ' * inner ℝ wn ξn + √μ' ^ 2 / 2 * ‖ξn‖ ^ 2;
have a := √(μ' * η);
have Ln := lyapunovOfState P μ' π f η sn;
have proj_err := a * |inner ℝ gn (P en)|;
δ_curv + proj_err ≤ θ * a * Ln)
:
∃ (Ω : Set (E d)) (Ω_plus : Set (E d)) (R : ℝ),
IsOpen Ω ∧ IsOpen Ω_plus ∧ 0 < R ∧ m_star ∈ Ω ∧ Ω ⊆ Ω_plus ∧ Ω_plus ⊆ U_plus ∧ ∀ (s₀ : NesterovState d) (n : ℕ),
have s := nesterovSeqGen f η ρ s₀ n;
have s' := nesterovSeqGen f η ρ s₀ (n + 1);
have Ln := lyapunovOfState P μ' π f η s;
have Ln' := lyapunovOfState P μ' π f η s';
have a := √(μ' * η);
s.x ∈ Ω →
s.lookahead η ∈ Ω →
Ln ≤ R ^ 2 → Ln' ≤ (1 - (1 - θ) * a) * Ln ∧ s'.x ∈ Ω_plus ∧ s'.lookahead η ∈ Ω_plus
Public theorem wrapper for lyapunovContractionGenProof.