The Morse lemma for a locally smooth function

TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart puts a globally smooth function in quadratic normal form near a nondegenerate critical point. The normal form only depends on the function near the point, and this file states it for a function that is smooth on a neighbourhood of the critical point only. This is the form in which the Morse lemma applies to the coordinate expressions of a function on a manifold, which are only defined on chart targets.

Main declarations

• TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn: the Morse lemma for a function smooth on a neighbourhood of a nondegenerate critical point, with a chart whose source lies in that neighbourhood.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Theorem 1.3.1.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {g : E → ℝ} {a : E} {U : Set E} (hU : U ∈ nhds a) (hg : ContDiffOn ℝ (↑⊤) g U) (h : IsNondegenerateCriticalPoint g a) : ∃ (ψ : OpenPartialHomeomorph E E), ψ.source ⊆ U ∧ a ∈ ψ.source ∧ ↑ψ a = 0 ∧ ContDiffOn ℝ (↑⊤) (↑ψ) ψ.source ∧ ContDiffOn ℝ (↑⊤) (↑ψ.symm) ψ.target ∧ ∀ y ∈ ψ.source, g y = g a + 2⁻¹ * ((fderiv ℝ (fderiv ℝ g) a) (↑ψ y)) (↑ψ y)

The Morse lemma for a locally smooth function. If g is smooth on a neighbourhood U of a nondegenerate critical point a, there is a chart ψ with source in U, sending a to 0, smooth in both directions, on whose source g is its Hessian quadratic form read in the chart.