Almost every linear perturbation of a function is Morse

Morse homology starts from a function all of whose critical points are nondegenerate, so the theory is empty until such functions are known to exist. This file proves that they are in fact generic: on an open subset U of a finite-dimensional real normed space E, for a twice continuously differentiable f : E → ℝ and almost every continuous linear functional a : E →L[ℝ] ℝ, every critical point of f - a in U is nondegenerate.

The mechanism is the equal-dimensional case of Sard's theorem, applied not to f but to its differential. Subtracting a linear functional changes the differential by a constant and leaves the second derivative alone, so

• x is a critical point of f - a exactly when fderiv ℝ f x = a, and
• the second derivative of f - a at x is that of f.

Hence f - a has a degenerate critical point in U exactly when a is a critical value of the map fderiv ℝ f : E → (E →L[ℝ] ℝ) taken on U; this is TauCeti.hasNondegenerateCriticalPointsOn_sub_iff, and it is the whole content of the argument. Domain and codomain of fderiv ℝ f have the same dimension, the continuous dual of a finite-dimensional space having the dimension of the space (ContinuousLinearMap.dual_finrank_eq), so TauCeti.addHaar_image_eq_zero_of_not_surjective_fderivWithin applies and the bad set of a is null. Note that only C² regularity of f is used: the map fderiv ℝ f is then merely differentiable, which is all the equal-dimensional Sard lemma asks for, and no higher-stratum Morse--Sard argument is needed.

The perturbation is written f - a rather than f + a; the two conventions differ by the sign of a, and subtraction makes the criticality condition read fderiv ℝ f x = a, so that the exceptional set is literally the set of critical values of fderiv ℝ f.

Nondegeneracy here is TauCeti.HasNondegenerateCriticalPointsOn, which asks nothing of f away from its critical points; the regularity hypothesis ContDiffOn ℝ 2 f U is carried separately, as TauCeti/Analysis/Calculus/Morse/Basic.lean explains.

Main declarations

• TauCeti.isNondegenerateCriticalPoint_sub_iff: a point at which f is C² is a nondegenerate critical point of f - a exactly when a is the differential of f there and the second derivative of f is invertible.
• TauCeti.hasNondegenerateCriticalPointsOn_sub_iff: f - a has nondegenerate critical points on U exactly when a is a regular value of fderiv ℝ f on U.
• TauCeti.ae_hasNondegenerateCriticalPointsOn_sub: almost every linear perturbation is Morse.
• TauCeti.dense_setOfPred_hasNondegenerateCriticalPointsOn_sub and TauCeti.exists_norm_lt_hasNondegenerateCriticalPointsOn_sub: the good perturbations are dense, so they can be taken arbitrarily small in the operator norm.
• TauCeti.ae_hasNondegenerateCriticalPointsOn_sub_inner, TauCeti.dense_setOfPred_hasNondegenerateCriticalPointsOn_sub_inner and TauCeti.exists_norm_lt_hasNondegenerateCriticalPointsOn_sub_inner: the same three statements on an inner product space, with the perturbation written ⟪v, ·⟫ as in the gradient formulation.
• TauCeti.finite_setOfPred_fderiv_sub_eq_zero: a perturbation that is Morse on U has only finitely many critical points on a compact subset of U.

References

• V. Guillemin and A. Pollack, Differential Topology, Prentice-Hall, 1974, Chapter 1, §7, where this genericity statement is proved in exactly this way.
• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 1.

Morse perturbations are the regular values of the differential

The effect of the perturbation on the first two derivatives follows from Mathlib's general calculus lemmas for derivatives of differences and constant shifts.

theorem TauCeti.isNondegenerateCriticalPoint_sub_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (a : E →L[ℝ] ℝ) : IsNondegenerateCriticalPoint (fun (y : E) => f y - a y) x ↔ fderiv ℝ f x = a ∧ (fderiv ℝ (fderiv ℝ f) x).IsInvertible

A point at which f is C² is a nondegenerate critical point of f - a exactly when the differential of f there is a and the second derivative of f there is invertible. Both conditions are about f alone: the perturbation only moves the differential, so it selects which points are critical without affecting whether they are degenerate.

theorem TauCeti.finite_setOfPred_fderiv_sub_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {U : Set E} {a : E →L[ℝ] ℝ} {K : Set E} (hK : IsCompact K) (hd : ∀ x ∈ K, DifferentiableAt ℝ f x) (hcont : ContinuousOn (fderiv ℝ f) K) (ha : HasNondegenerateCriticalPointsOn (fun (y : E) => f y - a y) U) (hKU : K ⊆ U) : {x : E | x ∈ K ∧ fderiv ℝ (fun (y : E) => f y - a y) x = 0}.Finite

A perturbation that is Morse on U has only finitely many critical points on a compact subset of U. Continuity of fderiv ℝ f on the compact set closes the critical locus, and nondegeneracy makes it discrete. The hypotheses are that K is compact and contained in U, that f is differentiable at each point of K, and that fderiv ℝ f is continuous on K; note that continuity of fderiv ℝ f does not by itself give differentiability, since fderiv is defined at points where f is not differentiable. The perturbation itself needs no regularity: it shifts the differential of f by the constant a, which disturbs neither the differentiability nor the continuity.

theorem TauCeti.hasNondegenerateCriticalPointsOn_sub_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {U : Set E} [FiniteDimensional ℝ E] (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) (a : E →L[ℝ] ℝ) : HasNondegenerateCriticalPointsOn (fun (y : E) => f y - a y) U ↔ a ∉ fderiv ℝ f '' {x : E | x ∈ U ∧ ¬Function.Surjective ⇑(fderiv ℝ (fderiv ℝ f) x)}

The perturbations that make f Morse are exactly the regular values of its differential. All critical points of f - a in U are nondegenerate if and only if a is not the value at a point of U of the differential fderiv ℝ f at which the second derivative fails to be surjective.

Genericity

theorem TauCeti.ae_hasNondegenerateCriticalPointsOn_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {U : Set E} [FiniteDimensional ℝ E] [MeasurableSpace (E →L[ℝ] ℝ)] [BorelSpace (E →L[ℝ] ℝ)] (ν : MeasureTheory.Measure (E →L[ℝ] ℝ)) [ν.IsAddHaarMeasure] (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) : ∀ᵐ (a : E →L[ℝ] ℝ) ∂ν, HasNondegenerateCriticalPointsOn (fun (y : E) => f y - a y) U

Almost every linear perturbation of a C² function is Morse. For a Haar measure ν on the continuous dual, for ν-almost every functional a the function f - a has only nondegenerate critical points on the open set U.

The exceptional set is the set of critical values on U of the differential fderiv ℝ f, a map between spaces of the same finite dimension, so it is null by the equal-dimensional case of Sard's theorem.

Only the dual carries a measurable structure in the statement, since that is where ν lives; the source E is measured only inside the proof, by Sard's lemma, and gets its Borel structure there.

theorem TauCeti.dense_setOfPred_hasNondegenerateCriticalPointsOn_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {U : Set E} [FiniteDimensional ℝ E] (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) : Dense {a : E →L[ℝ] ℝ | HasNondegenerateCriticalPointsOn (fun (y : E) => f y - a y) U}

The linear perturbations that make a C² function Morse on an open set are dense in the continuous dual. No measurable structure appears in the statement: the Haar measure that produces the density is an auxiliary object of the proof, which installs the Borel structure it needs.

theorem TauCeti.exists_norm_lt_hasNondegenerateCriticalPointsOn_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {U : Set E} [FiniteDimensional ℝ E] (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) {ε : ℝ} (hε : 0 < ε) : ∃ (a : E →L[ℝ] ℝ), ‖a‖ < ε ∧ HasNondegenerateCriticalPointsOn (fun (y : E) => f y - a y) U

A C² function is made Morse by an arbitrarily small linear perturbation: for every ε > 0 there is a continuous linear functional of operator norm less than ε whose subtraction leaves only nondegenerate critical points on U.

The gradient formulation

On a real inner product space the perturbations are usually written f - ⟪v, ·⟫, so that the gradient of the perturbed function is ∇f - v; the Riesz isometry carries the statement above to that form.

theorem TauCeti.ae_hasNondegenerateCriticalPointsOn_sub_inner {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {U : Set E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) : ∀ᵐ (v : E) ∂μ, HasNondegenerateCriticalPointsOn (fun (y : E) => f y - inner ℝ v y) U

Almost every perturbation by a linear form ⟪v, ·⟫ of a C² function is Morse. This is TauCeti.ae_hasNondegenerateCriticalPointsOn_sub transported along the Riesz isometry, which is a continuous linear equivalence and so carries null sets to null sets; the perturbed function has gradient ∇f - v, which is the shape the negative gradient flow is stated in.

No measurable structure on the dual appears in the statement: the Borel one is installed inside the proof, where the Haar measure of the dual is the auxiliary object being transported.

theorem TauCeti.dense_setOfPred_hasNondegenerateCriticalPointsOn_sub_inner {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) : Dense {v : E | HasNondegenerateCriticalPointsOn (fun (y : E) => f y - inner ℝ v y) U}

The vectors v for which subtracting ⟪v, ·⟫ makes a C² function Morse on an open set are dense. As above, the Haar measure witnessing the density is internal to the proof, so the statement mentions no measurable structure.

theorem TauCeti.exists_norm_lt_hasNondegenerateCriticalPointsOn_sub_inner {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) {ε : ℝ} (hε : 0 < ε) : ∃ (v : E), ‖v‖ < ε ∧ HasNondegenerateCriticalPointsOn (fun (y : E) => f y - inner ℝ v y) U

A C² function is made Morse by subtracting ⟪v, ·⟫ for an arbitrarily small v: for every ε > 0 there is a vector of norm less than ε whose associated linear form, subtracted, leaves only nondegenerate critical points on U. Equivalently, the gradient of f may be shifted by an arbitrarily small vector to make f Morse.