Hessian coercivity from PŁ — main theorems

Proves muPL_norm_sq_bound and hessian_coercive_on_orthogonal_of_MuPL_impl, establishing that the Hessian is μ-coercive on ker(Hess)⊥ under the PŁ condition.

theorem PLAcceleratedNesterovLean.muPL_norm_sq_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ v : E) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) (hPL : MuPL f μ x₀) : μ * ((hessian f x₀) v) v ≤ ‖(hessian f x₀) v‖ ^ 2

Under μ-PŁ at a local minimum, μ · H(v,v) ≤ ‖Hv‖² for all v.

theorem PLAcceleratedNesterovLean.hessian_coercive_on_orthogonal_of_MuPL_impl {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ : E) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) (hPL : MuPL f μ x₀) (v : E) : v ∈ (hessianKer f x₀)ᗮ → ((hessian f x₀) v) v ≥ μ * ‖v‖ ^ 2

Main theorem: Under μ-PŁ at a local minimizer, the Hessian is μ-coercive on the orthogonal complement of its kernel.