The Morse index

This file defines the Hessian quadratic form of a real-valued function on a real normed space and, in finite dimensions, its Morse index: the negative index of inertia of the Hessian. Thus the index is the maximal dimension of a subspace on which the Hessian is negative-definite.

The Hessian quadratic form used here is

v ↦ fderiv ℝ (fderiv ℝ f) x v v.

Some statements of the Morse lemma put a factor 2⁻¹ in front of this form. That positive factor does not change its negative index, by QuadraticForm.sigNeg_smul_of_pos. In particular the convention agrees with the normal form in TauCeti.Analysis.Calculus.Morse.NormalForm.

The definition is made at every point, not only at a critical point, since the index of the Hessian is meaningful there and this keeps regularity and criticality hypotheses on the results that use them. It follows Mathlib's total sigNeg, whose value is defined to be zero outside finite dimensions; all results interpreting the value as a Morse-theoretic index assume finite dimension. At a nondegenerate critical point the Hessian quadratic form is nondegenerate, so its positive and negative indices add to the dimension. Consequently index zero is equivalent to a positive-definite Hessian and full index is equivalent to a negative-definite Hessian.

The index depends only on the germ of the function and is invariant under a twice continuously differentiable change of coordinates with invertible derivative. Finally, Sylvester's law of inertia puts the Hessian into a diagonal normal form with weights ±1; the number of negative weights is exactly the Morse index. This supplies the integer grading of critical points needed by the Morse complex in Lane M of the analytic Heegaard Floer roadmap.

Main declarations

• TauCeti.hessianQuadraticForm: the quadratic form defined by the Hessian at a point.
• TauCeti.morseIndex: the negative index of inertia of the Hessian quadratic form.
• TauCeti.morseIndex_comp: invariance under a change of coordinates.
• TauCeti.IsNondegenerateCriticalPoint.hessianQuadraticForm_nondegenerate: the Hessian quadratic form at a nondegenerate critical point is nondegenerate.
• TauCeti.IsNondegenerateCriticalPoint.hessianQuadraticForm_posDef_iff_morseIndex_eq_zero: index zero characterizes a positive-definite Hessian at a nondegenerate critical point.
• TauCeti.IsNondegenerateCriticalPoint.exists_hessianQuadraticForm_equivalent_weightedSumSquares: the Hessian has a diagonal ±1 normal form.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 1.
• J. Milnor, Morse Theory, Princeton University Press, 1963, §2.
• Heegaard Floer homology roadmap, Lane M, "Morse homology".

noncomputable def TauCeti.hessianQuadraticForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) : QuadraticForm ℝ E

The Hessian quadratic form of f at x, sending v to the second derivative of f at x evaluated twice on v. The definition uses Mathlib's totalized Fréchet derivative, so no regularity hypothesis is needed to form it.

Equations

• TauCeti.hessianQuadraticForm f x = LinearMap.BilinMap.toQuadraticMap (fderiv ℝ (fderiv ℝ f) x).toBilinForm

@[simp]

theorem TauCeti.hessianQuadraticForm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x v : E) : (hessianQuadraticForm f x) v = ((fderiv ℝ (fderiv ℝ f) x) v) v

The Hessian quadratic form evaluates the second derivative twice on the same vector.

@[simp]

theorem TauCeti.associated_hessianQuadraticForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : QuadraticMap.associated (hessianQuadraticForm f x) = (fderiv ℝ (fderiv ℝ f) x).toBilinForm

For a twice continuously differentiable function, the bilinear form associated to its Hessian quadratic form is its second derivative.

theorem TauCeti.hessianQuadraticForm_congr_of_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} (hfg : f =ᶠ[nhds x] g) : hessianQuadraticForm f x = hessianQuadraticForm g x

The Hessian quadratic form depends only on the germ of the function at the point.

@[simp]

theorem TauCeti.hessianQuadraticForm_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) : hessianQuadraticForm (-f) x = -hessianQuadraticForm f x

Negating a function negates its Hessian quadratic form.

theorem TauCeti.hessianQuadraticForm_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → ℝ} {φ : F → E} {b : F} (hf : ContDiffAt ℝ 2 f (φ b)) (hφ : ContDiffAt ℝ 2 φ b) (hcrit : fderiv ℝ f (φ b) = 0) : hessianQuadraticForm (f ∘ φ) b = QuadraticMap.comp (hessianQuadraticForm f (φ b)) ↑(fderiv ℝ φ b)

At a critical point the Hessian quadratic form pulls back along the derivative of a C² change of variables.

theorem ContinuousLinearMap.hessianQuadraticForm_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → ℝ} (L : F →L[ℝ] E) {b : F} (hf : ContDiffAt ℝ 2 f (L b)) : TauCeti.hessianQuadraticForm (f ∘ ⇑L) b = QuadraticMap.comp (TauCeti.hessianQuadraticForm f (L b)) ↑L

The Hessian quadratic form pulls back along a continuous linear map.

noncomputable def TauCeti.morseIndex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) : ℕ

The Morse index of f at x is the negative index of inertia of its Hessian quadratic form. In finite dimensions it is equivalently the maximal dimension of a subspace on which the Hessian is negative-definite. Following Mathlib's sigNeg, its value is defined to be zero in infinite dimensions; the Morse-theoretic results below assume finite dimension.

Equations

• TauCeti.morseIndex f x = sigNeg (TauCeti.hessianQuadraticForm f x)

theorem TauCeti.morseIndex_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} : morseIndex f x = sigNeg (hessianQuadraticForm f x)

The Morse index is the negative index of inertia of the Hessian quadratic form.

theorem TauCeti.morseIndex_congr_of_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {x : E} (hfg : f =ᶠ[nhds x] g) : morseIndex f x = morseIndex g x

The Morse index depends only on the germ of the function at the point.

theorem TauCeti.morseIndex_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → ℝ} {φ : F → E} {b : F} (hf : ContDiffAt ℝ 2 f (φ b)) (hφ : ContDiffAt ℝ 2 φ b) (hcrit : fderiv ℝ f (φ b) = 0) (hinv : (fderiv ℝ φ b).IsInvertible) : morseIndex (f ∘ φ) b = morseIndex f (φ b)

The Morse index is invariant under a C² change of coordinates with invertible derivative. Criticality is needed because it removes the first-order term from the second-order chain rule.

theorem TauCeti.IsNondegenerateCriticalPoint.hessianQuadraticForm_nondegenerate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : QuadraticMap.Nondegenerate

At a nondegenerate critical point, the Hessian quadratic form is nondegenerate.

theorem TauCeti.morseIndex_le_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] : morseIndex f x ≤ Module.finrank ℝ E

The Morse index is at most the dimension of the ambient space.

theorem TauCeti.morseIndex_neg_add_morseIndex_eq_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : QuadraticMap.Nondegenerate) : morseIndex (-f) x + morseIndex f x = Module.finrank ℝ E

If the Hessian is nondegenerate, the Morse indices of a function and its negation add to the dimension of the ambient space.

theorem TauCeti.IsNondegenerateCriticalPoint.sigPos_hessianQuadraticForm_add_morseIndex_eq_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : sigPos (hessianQuadraticForm f x) + morseIndex f x = Module.finrank ℝ E

At a nondegenerate critical point, the positive index of the Hessian and the Morse index add to the dimension of the ambient space.

theorem TauCeti.IsNondegenerateCriticalPoint.morseIndex_neg_add_morseIndex_eq_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : morseIndex (-f) x + morseIndex f x = Module.finrank ℝ E

At a nondegenerate critical point, the Morse indices of a function and its negation add to the dimension of the ambient space.

theorem TauCeti.IsNondegenerateCriticalPoint.hessianQuadraticForm_posDef_iff_morseIndex_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : QuadraticMap.PosDef (hessianQuadraticForm f x) ↔ morseIndex f x = 0

At a nondegenerate critical point, the Hessian is positive-definite exactly when the Morse index is zero.

theorem TauCeti.IsNondegenerateCriticalPoint.neg_hessianQuadraticForm_posDef_iff_morseIndex_eq_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : QuadraticMap.PosDef (-hessianQuadraticForm f x) ↔ morseIndex f x = Module.finrank ℝ E

At a nondegenerate critical point, the Hessian is negative-definite exactly when the Morse index is the dimension of the ambient space.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_hessianQuadraticForm_equivalent_weightedSumSquares {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : ∃ (w : Fin (Module.finrank ℝ E) → ℝ), (∀ (i : Fin (Module.finrank ℝ E)), w i = -1 ∨ w i = 1) ∧ QuadraticMap.Equivalent (hessianQuadraticForm f x) (QuadraticMap.weightedSumSquares ℝ w)

At a nondegenerate critical point, the Hessian quadratic form has a diagonal normal form with every weight equal to -1 or 1. The returned equivalence can be passed to QuadraticForm.sigNeg_of_equiv_weightedSumSquares to count the negative weights by the Morse index, after rewriting with morseIndex_def. This is Sylvester's law of inertia applied to the Hessian.