Hessian coercivity from the Polyak-Łojasiewicz condition

Proves that the Hessian of a C² function is μ-coercive on normal directions to the minimizer set, given the μ-PL condition.

This file provides the bridge from global PolyakLojasiewicz to the core Hessian bounds proved in MorseBott.HessianPL. The unique content here:

1. PL_to_local_MuPL: converts global PL on U to local MuPL at a minimizer
2. hessianQuadForm_eq_hessian: bridges hessianQuadForm to second Fréchet derivative
3. hessian_normal_bound_from_PL: Hessian ≥ μ on normal directions (main export)
4. PL_gradient_hessian_bound: gradient-form export

theorem PLAcceleratedNesterovLean.hessian_normal_bound_from_PL {d : ℕ} (f : E d → ℝ) (μ : ℝ) (U : Set (E d)) (hPL : PolyakLojasiewicz f μ U) (hU_open : IsOpen U) (S : Set (E d)) (hS : S = argminSet f) (hS_sub : S ⊆ U) (_hgrad_zero : ∀ x ∈ S, gradient f x = 0) (π : E d → E d) (_hπ_proj : ∀ x ∈ U, π x ∈ S ∧ dist x (π x) = Metric.infDist x S) (m : E d) (hmS : m ∈ S) (hf_C2 : ContDiffAt ℝ 2 f m) (hπ_sa : ∀ (u v : E d), inner ℝ ((fderiv ℝ π m) u) v = inner ℝ u ((fderiv ℝ π m) v)) (hMB : ∀ (w : E d), ↑(fderiv ℝ (fderiv ℝ f) m) w = 0 → w ∈ (↑(fderiv ℝ π m)).range) (ξ : E d) (hξ_normal : (fderiv ℝ π m) ξ = 0) : hessianQuadForm f m ξ ≥ μ * ‖ξ‖ ^ 2

Normal Hessian bound from PL: For m ∈ argminSet f and ξ with Dπ(m)ξ = 0 (normal direction), the Hessian quadratic form satisfies hessianQuadForm f m ξ ≥ μ · ‖ξ‖².

The proof combines:

1. PL → local MuPL at m
2. hessianQuadForm = hessian (bridge via Riesz representation)
3. ξ ∈ (hessKer f m)⊥ via self-adjointness of Dπ(m) + Morse-Bott condition
4. Rayleigh quotient coercivity on (hessKer)⊥

The Morse-Bott condition (hMB) states ker(D²f(m)) ⊆ range(Dπ(m)), i.e., every direction of zero Hessian curvature is tangent to the minimizer set. Combined with self-adjointness of Dπ(m) (which holds for smooth nearest-point projections), this gives ker(Dπ(m)) ⊆ (hessKer f m)⊥, so normal directions lie in the orthogonal complement of the Hessian kernel where μ-coercivity holds.

theorem PLAcceleratedNesterovLean.PL_gradient_hessian_bound {d : ℕ} (f : E d → ℝ) (μ : ℝ) (U : Set (E d)) (hPL : PolyakLojasiewicz f μ U) (hU_open : IsOpen U) (m : E d) (hf : ContDiffAt ℝ 2 f m) (hmS : m ∈ argminSet f) (hmU : m ∈ U) (v : E d) : μ * inner ℝ ((fderiv ℝ (gradient f) m) v) v ≤ ‖(fderiv ℝ (gradient f) m) v‖ ^ 2

Under PL on U at a minimizer m, μ⟨D(∇f)(m) v, v⟩ ≤ ‖D(∇f)(m) v‖² for all v. Gradient-form export of the core PL Hessian bound.