Local Convergence Argument

This file contains the per-base-point local convergence argument, extracted from MainTheorem for build parallelism. For each m⋆ ∈ M, the theorem chain local_fiberwise_geometry, lyapunov_coercivity, motion_bounds_curvature_error, lyapunov_contraction, and bootstrap_total_displacement produces a ball around m⋆ where the Nesterov iterates converge at the accelerated rate exp(-k / √(L / ((1-θ)²·μ_minus))).

theorem PLAcceleratedNesterovLean.local_convergence_at_base_point {d : ℕ} (hd : 0 < d) (L : NNReal) (hL : 0 < ↑L) (μ : ℝ) (hμ : 0 < μ) (hμ_le_L : μ ≤ ↑L) (μ_minus : ℝ) (hμ_minus : 0 < μ_minus) (hμ_minus_lt : μ_minus < μ) (θ : ℝ) (hθ : 0 < θ) (hθ_lt1 : θ < 1) (f : E d → ℝ) (S : Set (E d)) (hrange : S = argminSet f) (U : Set (E d)) (hTub_sub : IsTubularNeighborhoodOfSubmanifold S U) (hPL : PolyakLojasiewicz f μ U) (hf_C2 : ContDiffOn ℝ 2 f U) (hf_lip : 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) (mstar : E d) (hmstar : mstar ∈ S) : have η := 1 / ↑L; have ρ := (1 - √(μ_minus * η)) / (1 + √(μ_minus * η)); ∃ (α : ℝ), 0 < α ∧ Metric.ball mstar α ⊆ U ∧ ∀ x₁ ∈ Metric.ball mstar α, (∀ (k : ℕ), (nesterovSeq f η ρ x₁ k).lookahead η ∈ U) ∧ HasAcceleratedRate f (fun (k : ℕ) => (nesterovSeq f η ρ x₁ k).lookahead η) (↑L) ((1 - θ) ^ 2 * μ_minus)

Public theorem wrapper for localConvergenceAtBasePointProof.