Implicit Function Theorem Application

Proves ift_gives_graph: under Hessian coercivity on the normal space, the critical set near x₀ is locally a C¹ graph over ker(Hess f(x₀)).

theorem PLAcceleratedNesterovLean.ift_gives_graph_impl {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ : E) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hgrad : fderiv ℝ f x₀ = 0) (hcoer : ∀ v ∈ (hessianKer f x₀)ᗮ, ((hessian f x₀) v) v ≥ μ * ‖v‖ ^ 2) : ∃ (U : Set E) (_ : U ∈ nhds x₀) (φ : ↥(hessianKer f x₀) → ↥(hessianKer f x₀)ᗮ), ContDiffAt ℝ 1 φ 0 ∧ φ 0 = 0 ∧ fderiv ℝ φ 0 = 0 ∧ ∀ x ∈ U, (∀ (w : ↥(hessianKer f x₀)ᗮ), (fderiv ℝ f x) ↑w = 0) ↔ ↑((hessianKer f x₀)ᗮ.orthogonalProjectionOnto (x - x₀)) = ↑(φ ((hessianKer f x₀).orthogonalProjectionOnto (x - x₀)))

theorem PLAcceleratedNesterovLean.ift_gives_graph_impl₂ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ : E) (hμ : 0 < μ) (hf : ContDiffAt ℝ 3 f x₀) (hgrad : fderiv ℝ f x₀ = 0) (hcoer : ∀ v ∈ (hessianKer f x₀)ᗮ, ((hessian f x₀) v) v ≥ μ * ‖v‖ ^ 2) : ∃ (U : Set E) (_ : U ∈ nhds x₀) (φ : ↥(hessianKer f x₀) → ↥(hessianKer f x₀)ᗮ), ContDiffAt ℝ 2 φ 0 ∧ φ 0 = 0 ∧ fderiv ℝ φ 0 = 0 ∧ ∀ x ∈ U, (∀ (w : ↥(hessianKer f x₀)ᗮ), (fderiv ℝ f x) ↑w = 0) ↔ ↑((hessianKer f x₀)ᗮ.orthogonalProjectionOnto (x - x₀)) = ↑(φ ((hessianKer f x₀).orthogonalProjectionOnto (x - x₀)))

C³ version: when f is C³ at x₀, the IFT gives a C² graph.