Local Fiberwise Geometry from PL near M

Given a base point m⋆ ∈ M and any μ' ∈ (0, μ), there exists a fiber-saturated open neighborhood U₊ of m⋆ with U₊ ⊂⊂ U, and ε > 0 with ε ≤ √(μ'/η), such that:

(a) Normal Hessian lower bound: ξᵀ D²f(x)ξ ≥ μ'‖ξ‖² for x ∈ U₊, ξ ∈ N_{π(x)}M (b) Quadratic growth: f(x) - f⋆ ≥ (μ'/2) dist(x, M)² (c) Strong aiming: ⟨∇f(x), x - π(x)⟩ ≥ f(x) - f⋆ + (μ'/2)‖x - π(x)‖² (d) Hessian lower bound: D²f(x) ≽ -εI

theorem PLAcceleratedNesterovLean.local_fiberwise_geometry {d : ℕ} (_hd : 0 < d) (f : E d → ℝ) (L : NNReal) (_hL : 0 < ↑L) (μ : ℝ) (hμ : 0 < μ) (μ' : ℝ) (hμ' : 0 < μ') (hμ'_lt : μ' < μ) (η : ℝ) (_hη : η = 1 / ↑L) (hη_pos : 0 < η) (S : Set (E d)) (hM_argmin : S = argminSet f) (U : Set (E d)) (hTub_sub : IsTubularNeighborhoodOfSubmanifold S U) (hPL : PolyakLojasiewicz f μ U) (hf_C2 : ContDiffOn ℝ 2 f U) (π : E d → E d) (hπ_proj : ∀ x ∈ U, π x ∈ S ∧ dist x (π x) = Metric.infDist x S) (hgrad_zero : ∀ x ∈ S, gradient f x = 0) (m_star : E d) (hm_star : m_star ∈ S) : ∃ (U_plus : Set (E d)) (ε : ℝ), IsOpen U_plus ∧ m_star ∈ U_plus ∧ IsCompact (closure U_plus) ∧ closure U_plus ⊆ U ∧ Convex ℝ U_plus ∧ 0 < ε ∧ ε ≤ √(μ' / η) ∧ (∀ x ∈ U_plus, ∀ (ξ : E d), (fderiv ℝ π (π x)) ξ = 0 → hessianQuadForm f x ξ ≥ μ' * ‖ξ‖ ^ 2) ∧ (∀ x ∈ U_plus, f x - fStar f ≥ μ' / 2 * Metric.infDist x S ^ 2) ∧ (∀ x ∈ U_plus, inner ℝ (gradient f x) (x - π x) ≥ f x - fStar f + μ' / 2 * ‖x - π x‖ ^ 2) ∧ (∀ x ∈ U_plus, ∀ (ξ : E d), hessianQuadForm f x ξ ≥ -ε * ‖ξ‖ ^ 2) ∧ (∀ (ξ : E d), (fderiv ℝ π m_star) ξ = 0 → hessianQuadForm f m_star ξ ≥ μ * ‖ξ‖ ^ 2) ∧ ∀ x ∈ U_plus, ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → π x + t • (x - π x) ∈ U

Public theorem wrapper for localFiberwiseGeometryProof.