Continuation of a nondegenerate critical point

A nondegenerate critical point of a C³ finite-dimensional family persists uniquely under a small change of the parameter. The critical point is obtained by applying the implicit function theorem to the spatial differential of the family. It depends locally C² on the parameter, remains nondegenerate with unchanged Morse index, and its critical value has the same first derivative as the family with the spatial variable held fixed at the original critical point.

The uniqueness assertion is local jointly in the parameter and spatial variables. Thus it rules out other critical points only in the neighbourhood on which the implicit function theorem applies; it makes no global assertion about the critical locus of a member of the family.

Main declaration

• TauCeti.IsNondegenerateCriticalPoint.exists_contDiffAt_criticalPoint_continuation: a local C² branch of nondegenerate critical points, unique near its base point.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 1.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_contDiffAt_criticalPoint_continuation {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace P] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : P × E → ℝ} {p : P} {x : E} (h : IsNondegenerateCriticalPoint (fun (y : E) => F (p, y)) x) (hF : ContDiffAt ℝ 3 F (p, x)) : ∃ (ψ : P → E), ψ p = x ∧ ContDiffAt ℝ 2 ψ p ∧ (∀ᶠ (q : P) in nhds p, IsNondegenerateCriticalPoint (fun (y : E) => F (q, y)) (ψ q)) ∧ (∀ᶠ (q : P) in nhds p, morseIndex (fun (y : E) => F (q, y)) (ψ q) = morseIndex (fun (y : E) => F (p, y)) x) ∧ (∀ᶠ (q : P × E) in nhds (p, x), fderiv ℝ (fun (y : E) => F (q.1, y)) q.2 = 0 ↔ ψ q.1 = q.2) ∧ ContDiffAt ℝ 2 (fun (q : P) => F (q, ψ q)) p ∧ fderiv ℝ (fun (q : P) => F (q, ψ q)) p = fderiv ℝ (fun (q : P) => F (q, x)) p

Continuation of a nondegenerate critical point.

Let F p x be a C³ family of real functions. A nondegenerate critical point x of the member at p extends to a C² branch ψ of nondegenerate critical points near p. This branch is the unique critical point near (p, x), and its Morse index is locally constant. The corresponding critical value is C², and its derivative at p is the derivative obtained by freezing the spatial variable at x.

The continuation function is total, as is Mathlib's implicit function, but all its characteristic properties are local at the base parameter.