Bootstrap via Total Displacement Control

Starting from a sufficiently small neighborhood of m⋆ with zero initial velocity, all iterates remain in the controlled region Ω and the Lyapunov function decays geometrically.

theorem PLAcceleratedNesterovLean.bootstrap_total_displacement {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μη_lt1 : μ' * η < 1) (ρ : ℝ) (_hρ : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η))) (S : Set (E d)) (hM_argmin : S = argminSet f) (U : Set (E d)) (_hTub : IsTubularNeighborhoodOfSubmanifold S U) (π : E d → E d) (_hπ_in_S : ∀ (x : E d), π x ∈ S) (_hπ_proj : ∀ x ∈ S, π x = x) (hπ_metric : ∀ x ∈ U, dist x (π x) = Metric.infDist x S) (P : E d →L[ℝ] E d) (Ω : Set (E d)) (hΩ_open : IsOpen Ω) (hΩ_sub_U : Ω ⊆ U) (R : ℝ) (hR : 0 < R) (m_star : E d) (hm_star : m_star ∈ S) (hm_star_Ω : m_star ∈ Ω) (hΨ_cont : ContinuousAt (psi f μ' S) m_star) (hΨ_zero : psi f μ' S m_star = 0) (_hQG : ∀ x ∈ Ω, f x - fStar f ≥ μ' / 2 * Metric.infDist x S ^ 2) (hcontract : ∀ (x₁ : E d) (n : ℕ), have s := nesterovSeq f η ρ x₁ n; have Ln := lyapunov P μ' π f η ρ x₁ n; have Ln' := lyapunov P μ' π f η ρ x₁ (n + 1); have a := √(μ' * η); s.x ∈ Ω → s.lookahead η ∈ Ω → Ln ≤ R ^ 2 → Ln' ≤ (1 - (1 - θ) * a) * Ln) (C_h : ℝ) (hC_h : 0 < C_h) (hstep_bound : ∀ (x₁ : E d) (n : ℕ), have s := nesterovSeq f η ρ x₁ n; have Ln := lyapunov P μ' π f η ρ x₁ n; s.x ∈ Ω → s.lookahead η ∈ Ω → Ln ≤ R ^ 2 → ‖nesterovH f η ρ x₁ n‖ ≤ C_h * √η * √Ln) (C_mov : ℝ) (hC_mov : 0 < C_mov) (hvel_bound : ∀ (x₁ : E d) (n : ℕ), have s := nesterovSeq f η ρ x₁ n; have s' := nesterovSeq f η ρ x₁ (n + 1); have Ln := lyapunov P μ' π f η ρ x₁ n; s.x ∈ Ω → s.lookahead η ∈ Ω → Ln ≤ R ^ 2 → ‖√η • s'.v‖ ≤ C_mov * √Ln) : ∃ (α : ℝ), 0 < α ∧ ∀ x₁ ∈ Metric.ball m_star α ∩ U, (∀ (n : ℕ), (nesterovSeq f η ρ x₁ n).x ∈ Ω ∧ (nesterovSeq f η ρ x₁ n).lookahead η ∈ Ω) ∧ (∀ (n : ℕ), (nesterovSeq f η ρ x₁ n).x ∈ U) ∧ ∀ (n : ℕ), have a := √(μ' * η); lyapunov P μ' π f η ρ x₁ (n + 1) ≤ (1 - (1 - θ) * a) ^ (n + 1) * lyapunov P μ' π f η ρ x₁ 0

Public theorem wrapper for bootstrapTotalDisplacementProof.

theorem PLAcceleratedNesterovLean.bootstrap_total_displacement_gen {d : ℕ} (f : E d → ℝ) (μ' : ℝ) (hμ' : 0 < μ') (θ : ℝ) (hθ_pos : 0 < θ) (hθ_lt1 : θ < 1) (η : ℝ) (hη_pos : 0 < η) (hμη_lt1 : μ' * η < 1) (ρ : ℝ) (S : Set (E d)) (hM_argmin : S = argminSet f) (π : E d → E d) (P : E d →L[ℝ] E d) (Ω : Set (E d)) (hΩ_open : IsOpen Ω) (R : ℝ) (hR : 0 < R) (m_star : E d) (hm_star : m_star ∈ S) (hm_star_Ω : m_star ∈ Ω) (hcontract : ∀ (s₀ : NesterovState d) (n : ℕ), have s := nesterovSeqGen f η ρ s₀ n; s.x ∈ Ω → s.lookahead η ∈ Ω → lyapunovOfState P μ' π f η s ≤ R ^ 2 → lyapunovOfState P μ' π f η (nesterovSeqGen f η ρ s₀ (n + 1)) ≤ (1 - (1 - θ) * √(μ' * η)) * lyapunovOfState P μ' π f η s) (C_h : ℝ) (hC_h : 0 < C_h) (hstep_bound : ∀ (s₀ : NesterovState d) (n : ℕ), have s := nesterovSeqGen f η ρ s₀ n; s.x ∈ Ω → s.lookahead η ∈ Ω → lyapunovOfState P μ' π f η s ≤ R ^ 2 → ‖stepDispOfState f η ρ s‖ ≤ C_h * √η * √(lyapunovOfState P μ' π f η s)) (C_mov : ℝ) (hC_mov : 0 < C_mov) (hvel_bound : ∀ (s₀ : NesterovState d) (n : ℕ), have s := nesterovSeqGen f η ρ s₀ n; s.x ∈ Ω → s.lookahead η ∈ Ω → lyapunovOfState P μ' π f η s ≤ R ^ 2 → ‖√η • (nesterovSeqGen f η ρ s₀ (n + 1)).v‖ ≤ C_mov * √(lyapunovOfState P μ' π f η s)) : ∃ (δ : ℝ) (r_ball : ℝ), 0 < δ ∧ 0 < r_ball ∧ Metric.ball m_star r_ball ⊆ Ω ∧ ∀ (s₀ : NesterovState d), s₀.x ∈ Metric.ball m_star δ → s₀.lookahead η ∈ Metric.ball m_star δ → lyapunovOfState P μ' π f η s₀ ≤ δ ^ 2 → (∀ (n : ℕ), (nesterovSeqGen f η ρ s₀ n).x ∈ Ω ∧ (nesterovSeqGen f η ρ s₀ n).lookahead η ∈ Ω) ∧ (∀ (n : ℕ), (nesterovSeqGen f η ρ s₀ n).x ∈ Metric.ball m_star r_ball ∧ (nesterovSeqGen f η ρ s₀ n).lookahead η ∈ Metric.ball m_star r_ball) ∧ ∀ (n : ℕ), have a := √(μ' * η); lyapunovOfState P μ' π f η (nesterovSeqGen f η ρ s₀ (n + 1)) ≤ (1 - (1 - θ) * a) ^ (n + 1) * lyapunovOfState P μ' π f η s₀

Public theorem wrapper for bootstrapTotalDisplacementGenProof.