Gradient Alignment Lemma

Under μ-PŁ at a local min x₀, proves fderiv(x) = 0 ↔ fderiv(x)|_{T⊥} = 0 for x near x₀. Uses Taylor remainder bounds and a Hessian perturbation argument.

theorem PLAcceleratedNesterovLean.gradient_alignment_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₀) : ∃ W ∈ nhds x₀, ∀ x ∈ W, fderiv ℝ f x = 0 ↔ ∀ (w : ↥(hessianKer f x₀)ᗮ), (fderiv ℝ f x) ↑w = 0