Helper lemmas for Hessian coercivity from PŁ

These lemmas support the proof of hessian_coercive_on_orthogonal_of_MuPL in Submanifold.lean. The proof uses the Rayleigh quotient minimizer approach: the minimum of H(w,w) on the unit sphere of ker(H)⊥ is attained at an eigenvector, and PŁ forces this minimum to be ≥ μ.

theorem PLAcceleratedNesterovLean.taylor_ray_isLittleO_pl {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x₀ v : E) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) : (fun (t : ℝ) => f (x₀ + t • v) - f x₀ - t ^ 2 / 2 * ((hessian f x₀) v) v) =o[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ 2

Taylor expansion of a C² function along a ray from a local minimum: f(x₀ + t•v) - f(x₀) = (t²/2) · H(v,v) + o(t²) as t → 0⁺. (Copy of taylor_ray_isLittleO from HessianCoercive.lean.)

theorem PLAcceleratedNesterovLean.hessian_symmetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x₀ : E) (hf : ContDiffAt ℝ 2 f x₀) (v w : E) : ((hessian f x₀) v) w = ((hessian f x₀) w) v

The Hessian of a C² function is symmetric: H(v,w) = H(w,v).

theorem PLAcceleratedNesterovLean.hessian_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x₀ v : E) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) : 0 ≤ ((hessian f x₀) v) v

At a local minimum, the Hessian is positive semi-definite: H(v,v) ≥ 0.

theorem PLAcceleratedNesterovLean.mem_hessianKer_of_zero_quad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x₀ v : E) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) (hzero : ((hessian f x₀) v) v = 0) : v ∈ hessianKer f x₀

For a PSD symmetric Hessian, if H(v,v) = 0 then v ∈ ker(H).