Helpers for single-phase convergence proof

Helper lemmas for the local convergence argument, covering initial Lyapunov bounds and phase transitions.

Lemmas provided

1. lyapunov_initial_bound — Lyap(x₀, v=0) ≤ C·dist² for L-smooth f
2. gen_at_every_phase — gen theorem at any m ∈ S for any phase k ≥ 1

1. Initial Lyapunov bound

theorem PLAcceleratedNesterovLean.lyapunov_initial_bound {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (hμ' : 0 < μ') (π : E d → E d) (f : E d → ℝ) (η : ℝ) (_hη_pos : 0 < η) (_hμη : μ' * η < 1) (hbdd : BddBelow (Set.range f)) (_hP_norm : ∀ (v : E d), ‖P v‖ ≤ ‖v‖) (m : E d) (hm : m ∈ argminSet f) (_hπ_in_S : ∀ (x : E d), π x ∈ argminSet f) (hπ_near : ∀ (x : E d), dist x (π x) ≤ dist x m) (C_f : ℝ) (_hC_f : 0 < C_f) (hf_bound : ∀ (x₀ : E d), f x₀ - f m ≤ C_f * dist x₀ m ^ 2) (x₀ : E d) : lyapunovOfState P μ' π f η { x := x₀, v := 0 } ≤ (C_f + μ' / 2) * dist x₀ m ^ 2

For L-smooth f with ∇f(m)=0, the initial state (x₀, v=0) has Lyapunov bounded by C·dist(x₀,m)². Uses that f(x₀)-f* ≤ Lyap and ‖x₀-π(x₀)‖ ≤ dist(x₀,m).

2. Gen theorem at arbitrary phase and base point

theorem PLAcceleratedNesterovLean.gen_at_every_phase {d : ℕ} (hd : 0 < d) (L : NNReal) (hL : 0 < ↑L) (μ : ℝ) (hμ : 0 < μ) (hμ_le_L : μ ≤ ↑L) (f : E d → ℝ) (S : Set (E d)) (hrange : S = argminSet f) (U : Set (E d)) (hTub : IsTubularNeighborhoodOfSubmanifold S U) (hPL : PolyakLojasiewicz f μ U) (hC2 : ContDiffOn ℝ 2 f U) (hLip : LipschitzOnWith L (gradient f) U) (π : E d → E d) (hπ_on_U : ∀ x ∈ U, π x ∈ S ∧ dist x (π x) = Metric.infDist x S) (hπ_fix : ∀ x ∈ S, π x = x) (hπ_in_S : ∀ (x : E d), π x ∈ S) (hgrad_zero : ∀ x ∈ S, gradient f x = 0) (m : E d) (hm : m ∈ S) (k : ℕ) (hk : 1 ≤ k) : have η := 1 / ↑L; have P := fderiv ℝ π m; have ρ_gen := (1 - √(muOfPhase μ k * η)) / (1 + √(muOfPhase μ k * η)); ∃ (Ω : Set (E d)) (δ : ℝ) (r_ball : ℝ) (C_coer : ℝ), IsOpen Ω ∧ m ∈ Ω ∧ Ω ⊆ U ∧ 0 < δ ∧ 0 < r_ball ∧ 0 < C_coer ∧ Metric.ball m r_ball ⊆ Ω ∧ (∀ (x : E d), P (P x) = P x) ∧ (∀ (v : E d), ‖P v‖ ≤ ‖v‖) ∧ muOfPhase μ k * η < 1 ∧ (∀ (s : NesterovState d), s.x ∈ Ω → s.lookahead η ∈ Ω → ‖s.v‖ ^ 2 + muOfPhase μ k * ‖normalDispOfState π η s‖ ^ 2 ≤ C_coer * lyapunovOfState P (muOfPhase μ k) π f η s) ∧ ∀ (s₀ : NesterovState d), s₀.x ∈ Metric.ball m δ → s₀.lookahead η ∈ Metric.ball m δ → lyapunovOfState P (muOfPhase μ k) π f η s₀ ≤ δ ^ 2 → (∀ (j : ℕ), (nesterovSeqGen f η ρ_gen s₀ j).x ∈ Ω ∧ (nesterovSeqGen f η ρ_gen s₀ j).lookahead η ∈ Ω) ∧ (∀ (j : ℕ), (nesterovSeqGen f η ρ_gen s₀ j).x ∈ Metric.ball m r_ball ∧ (nesterovSeqGen f η ρ_gen s₀ j).lookahead η ∈ Metric.ball m r_ball) ∧ (∀ (j : ℕ), lyapunovOfState P (muOfPhase μ k) π f η (nesterovSeqGen f η ρ_gen s₀ (j + 1)) ≤ (1 - (1 - thetaOfPhase k) * √(muOfPhase μ k * η)) ^ (j + 1) * lyapunovOfState P (muOfPhase μ k) π f η s₀) ∧ ∀ (j : ℕ) (t : ℝ), 0 ≤ t → t ≤ 1 → π ((nesterovSeqGen f η ρ_gen s₀ j).lookahead η) + t • ((nesterovSeqGen f η ρ_gen s₀ j).lookahead η - π ((nesterovSeqGen f η ρ_gen s₀ j).lookahead η)) ∈ U

The gen theorem works at any m ∈ S for any phase k ≥ 1. This is just local_convergence_at_base_point_gen applied with phase-k parameters. Also exports C_coer, projector properties, and coercivity bound.