The Morse lemma

Near a nondegenerate critical point a smooth function is, in suitable coordinates, exactly its Hessian quadratic form. This file proves that, for a real-valued smooth function on a Banach space, in the form TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart: there is a chart ψ at the critical point x, carrying x to 0, with both coordinate maps smooth on their domains, and with

f y = f x + 2⁻¹ * fderiv ℝ (fderiv ℝ f) x (ψ y) (ψ y)

on the whole of its source. Nondegeneracy is the one from TauCeti.Analysis.Calculus.Morse.Basic: the second derivative, read as a map from the space to its dual, is a linear homeomorphism. In finite dimensions that is the classical condition that the Hessian be a nondegenerate bilinear form, so this is the classical Morse lemma; in infinite dimensions it is the strong nondegeneracy of Morse theory on Banach and Hilbert manifolds, and the statement is the Morse--Palais lemma of Palais (1969).

The proof is Palais's. Write f (x + v) - f x - fderiv ℝ f x v = 2⁻¹ * B v v v, where B v is the averaged Hessian TauCeti.hessianAverage f x v, the average of the second derivative along the segment from x to x + v, weighted so that B 0 is the Hessian itself. Then B is a smooth family of symmetric continuous bilinear forms with B 0 invertible, so TauCeti.exists_congruence_of_symmetric_family produces a smooth family of operators R v, equal to the identity at v = 0, with B v w w' = B 0 (R v w) (R v w'). Taking w = w' = v turns the second-order term into the Hessian evaluated at φ v = R v v, and φ has derivative the identity at 0, so it is a chart by the inverse function theorem.

The weight 2 * (1 - t) is what makes B 0 the Hessian on the nose. Iterating the smooth Hadamard factorisation of TauCeti.Analysis.Calculus.Hadamard twice would also produce a smooth family with f (x + v) - f x = B v v v at a critical point, but its value at 0 is then the derivative of a parametrised integral rather than the Hessian, and it is not symmetric; both are needed here. The averaged Hessian and its Taylor formula are stated for a map into an arbitrary Banach space, nothing in them being special to real-valued functions; only the congruence and the Morse lemma itself need f real-valued.

The family R is manufactured from a square root: the operator C v = (B 0)⁻¹ ∘ B v is close to the identity for v close to 0, so it has a unique square root there (TauCeti.sqrtNearOne), and that square root is automatically self-adjoint for the pairing B 0, because the adjoint of a square root is a square root of the adjoint and the two are close to the identity. Self-adjointness is exactly what turns R v * R v = C v into the congruence identity.

This is Lane M of the analytic Heegaard Floer roadmap, which asks for Morse homology built the way Floer homology is built. The Morse lemma is what makes the local model of a Morse function available: the index of the critical point, the local handle structure, and the local form of the gradient flow are all read off it. Everything here is stated for C^∞ functions, which is the standing regularity of Morse theory; the refinement giving a C^k chart for a C^{k+2} function is not proved.

Main declarations

• TauCeti.hessianAverage: the averaged Hessian along a segment, normalised so that TauCeti.hessianAverage_zero identifies its value at 0 with the Hessian.
• TauCeti.map_add_eq_add_hessianAverage: the second-order Taylor formula it satisfies.
• TauCeti.exists_congruence_of_symmetric_family: a smooth family of symmetric continuous bilinear forms whose value at 0 is invertible is, near 0, the congruence of that value by a smooth family of operators equal to the identity at 0.
• TauCeti.IsNondegenerateCriticalPoint.exists_normal_form: the Morse lemma, in the form of a smooth map φ fixing 0 with derivative the identity there.
• TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart: the Morse lemma as a chart at the critical point.

References

• R. S. Palais, The Morse lemma for Banach spaces, Bull. Amer. Math. Soc. 75 (1969), 968--971, for the statement proved here: the theorem below asks only that E be a Banach space, which is that note's setting rather than the Hilbert one.
• R. S. Palais, Morse theory on Hilbert manifolds, Topology 2 (1963), 299--340, Section 2, for the proof by an operator square root used here.
• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, 1963, Lemma 2.2, for the classical finite-dimensional statement.
• M. Audin, M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 1.
• Heegaard Floer homology roadmap, Lane M, "Morse homology".

noncomputable def TauCeti.hessianAverage {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x v : E) : E →L[ℝ] E →L[ℝ] F

The averaged Hessian of f at x in the direction v: the average of the second derivative of f along the segment from x to x + v, against the weight 2 * (1 - t). The weight is normalised so that the value at v = 0 is the Hessian at x itself (TauCeti.hessianAverage_zero), while TauCeti.map_add_eq_add_hessianAverage says that f (x + v) differs from its first-order Taylor polynomial by 2⁻¹ • hessianAverage f x v v v.

Equations

• TauCeti.hessianAverage f x v = segmentAverage (fun (t : ℝ) => 2 * (1 - t)) (fderiv ℝ (fderiv ℝ f)) x v

theorem TauCeti.hessianAverage_eq_integral_Icc {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x : E) : hessianAverage f x = fun (v : E) => ∫ (t : ℝ) in Set.Icc 0 1, (2 * (1 - t)) • fderiv ℝ (fderiv ℝ f) (x + t • v)

The averaged Hessian as an integral over the compact unit interval, the shape in which the regularity theorem for parametrised integrals applies to it.

@[simp]

theorem TauCeti.hessianAverage_zero {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (x : E) : hessianAverage f x 0 = fderiv ℝ (fderiv ℝ f) x

At the basepoint the averaged Hessian is the Hessian: the weight 2 * (1 - t) has integral 1 over the unit interval.

theorem TauCeti.contDiff_hessianAverage {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (x : E) : ContDiff ℝ (↑⊤) (hessianAverage f x)

The averaged Hessian of a smooth function depends smoothly on the direction.

theorem TauCeti.hessianAverage_apply {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : ContDiff ℝ 2 f) (x v w w' : E) : ((hessianAverage f x v) w) w' = ∫ (t : ℝ) in 0..1, (2 * (1 - t)) • ((fderiv ℝ (fderiv ℝ f) (x + t • v)) w) w'

Evaluating the averaged Hessian on a pair of vectors commutes with the integral.

theorem TauCeti.hessianAverage_symm {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : ContDiff ℝ 2 f) (x v w w' : E) : ((hessianAverage f x v) w) w' = ((hessianAverage f x v) w') w

The averaged Hessian is a symmetric bilinear form, since each second derivative along the segment is.

theorem TauCeti.map_add_eq_add_hessianAverage {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} (hf : ContDiff ℝ 2 f) (x v : E) : f (x + v) = f x + (fderiv ℝ f x) v + 2⁻¹ • ((hessianAverage f x v) v) v

Taylor's formula to second order, with the remainder written as the averaged Hessian evaluated twice on the increment.

theorem TauCeti.exists_congruence_of_symmetric_family {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {B : E → E →L[ℝ] E →L[ℝ] ℝ} (hB : ContDiff ℝ (↑⊤) B) (hsymm : ∀ (v w w' : E), ((B v) w) w' = ((B v) w') w) (B₀ : E ≃L[ℝ] E →L[ℝ] ℝ) (hB₀ : ↑B₀ = B 0) : ∃ (R : E → E →L[ℝ] E) (U : Set E), IsOpen U ∧ 0 ∈ U ∧ R 0 = 1 ∧ ContDiffOn ℝ (↑⊤) R U ∧ ∀ v ∈ U, ∀ (w w' : E), (B₀ ((R v) w)) ((R v) w') = ((B v) w) w'

A smooth family B of symmetric continuous bilinear forms on a Banach space whose value at 0 is invertible is, near 0, the congruence of that value by a smooth family of continuous linear operators equal to the identity at 0: there is R with R 0 = 1 and B₀ (R v w) (R v w') = B v w w'.

This is the linear-algebraic heart of the Morse lemma, and it is where the square root of an operator close to the identity is used: the comparison operator C v = B₀⁻¹ ∘ B v is self-adjoint for the pairing B₀, hence so is its square root R v, hence B₀ (R v w) (R v w') = B₀ w ((R v * R v) w') = B₀ w (C v w') = B v w w'.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_normal_form {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} [CompleteSpace E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (h : IsNondegenerateCriticalPoint f x) : ∃ (φ : E → E) (U : Set E), IsOpen U ∧ 0 ∈ U ∧ φ 0 = 0 ∧ ContDiffOn ℝ (↑⊤) φ U ∧ HasFDerivAt φ (ContinuousLinearMap.id ℝ E) 0 ∧ ∀ v ∈ U, f (x + v) = f x + 2⁻¹ * ((fderiv ℝ (fderiv ℝ f) x) (φ v)) (φ v)

The Morse lemma. Near a nondegenerate critical point x of a smooth function f there is a smooth map φ, fixing 0 and with derivative the identity there, in terms of which f is exactly its Hessian quadratic form: f (x + v) = f x + 2⁻¹ * fderiv ℝ (fderiv ℝ f) x (φ v) (φ v) for v near 0.

TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart repackages this as a chart at x.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_morse_chart {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} [CompleteSpace E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (h : IsNondegenerateCriticalPoint f x) : ∃ (ψ : OpenPartialHomeomorph E E), x ∈ ψ.source ∧ ↑ψ x = 0 ∧ ContDiffOn ℝ (↑⊤) (↑ψ) ψ.source ∧ ContDiffOn ℝ (↑⊤) (↑ψ.symm) ψ.target ∧ ∀ y ∈ ψ.source, f y = f x + 2⁻¹ * ((fderiv ℝ (fderiv ℝ f) x) (↑ψ y)) (↑ψ y)

The Morse lemma, as a chart. At a nondegenerate critical point x of a smooth function f there is a chart ψ sending x to 0, smooth in both directions, on whose whole source f is its Hessian quadratic form read in that chart.