Sard's theorem on the locus where the derivative vanishes

This file proves that a sufficiently smooth map between finite-dimensional real normed spaces sends the set of points at which its Fréchet derivative vanishes to a set of additive Haar measure zero, with no relation required between the two dimensions beyond a nontrivial target. Since a linear map onto a one-dimensional space is surjective exactly when it is nonzero, this is the full Morse--Sard theorem whenever the target is one-dimensional: the critical values of a smooth real-valued function on a finite-dimensional real normed space form a null set, and its regular values are dense.

The proof is Morse's stratification argument, run by induction on the dimension of the source and assembling the two estimates already available. Write Σ_i for the set of points at which the iterated derivatives of order 1 ≤ j ≤ i all vanish, and stratify Σ_1 as Σ_1 = Σ_K ∪ ⋃_{i < K} (Σ_i \ Σ_{i+1}) for a depth K large enough that finrank ℝ E < (K + 1) * finrank ℝ F.

• On the innermost stratum Σ_K, TauCeti.addHaar_image_eq_zero_of_iteratedFDeriv_eq_zero applies directly: enough derivatives vanish for the Hölder estimate to force nullity.
• Near a point of Σ_i \ Σ_{i+1}, TauCeti.exists_parametrization_iteratedFDeriv_eq_zero carries Σ_i by a C^r map θ out of a space of dimension finrank ℝ E - 1. Every point of Σ_1 in the image is a point where f ∘ θ has vanishing derivative, by the chain rule, so the inductive hypothesis in dimension finrank ℝ E - 1 applies to f ∘ θ and returns the local nullity of the image.

Both steps are local, and second countability of the source turns local nullity into global nullity through TauCeti.measure_image_null_of_locally_null.

Each descent step costs derivatives, since the parametrization θ is only as smooth as the implicit function theorem makes it; the regularity finrank ℝ E * finrank ℝ E + 1 recorded below is a convenient sufficient bound rather than the sharp one. Morse--Sard holds already for C^k maps with k ≥ max 1 (finrank ℝ E - finrank ℝ F + 1); recovering that sharp exponent needs a more careful induction than the one run here, and smooth maps satisfy every bound in sight.

The remaining stratum of the general Morse--Sard theorem, the set of critical points at which the derivative is nonzero but not surjective, is handled by a Fubini argument on a local fibration of the source in TauCeti.Analysis.Calculus.Sard.OutermostStratum, where the theorem itself is assembled; the results here are what that argument runs its induction against.

This is Lane F0 of the analytic Heegaard Floer roadmap, where finite-dimensional Sard is the prerequisite for Sard--Smale and hence for every transversality argument downstream.

Main results

• TauCeti.addHaar_image_eq_zero_of_fderiv_eq_zero: the image of a set of points at which the derivative vanishes is null, for a map that is C^k at those points with k large enough.
• TauCeti.ContDiff.addHaar_image_vanishingFDeriv_eq_zero: its global form for a smooth map.
• TauCeti.setOf_not_surjective_fderiv_eq_setOf_fderiv_eq_zero_of_finrank_eq_one: for a one-dimensional target, the critical locus is exactly the vanishing-derivative locus.

References

The stratification is the proof of Sard's theorem in J. Milnor, Topology from the Differentiable Viewpoint, Section 3, and M. Hirsch, Differential Topology, Chapter 3.

theorem TauCeti.addHaar_image_eq_zero_of_fderiv_eq_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] [Nontrivial F] (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → F} {s : Set E} {n : WithTop ℕ∞} (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n) (hf : ∀ x ∈ s, ContDiffAt ℝ n f x) (hs : ∀ x ∈ s, fderiv ℝ f x = 0) : ν (f '' s) = 0

Sard's theorem on the locus where the derivative vanishes. Let f be a map between finite-dimensional real normed spaces with nontrivial target, and let s be a set at each point of which f is C^n and the Fréchet derivative of f vanishes. If ((finrank ℝ E * finrank ℝ E + 1 : ℕ) : ℕ∞ω) ≤ n, then f '' s has additive Haar measure zero.

No relation between the two dimensions is required, beyond a nontrivial (positive-dimensional) target: the vanishing of the derivative, rather than a dimension count, is what the higher derivatives are used against. The smoothness bound is sufficient, not the sharp exponent of the Morse--Sard theorem.

theorem TauCeti.ContDiff.addHaar_image_vanishingFDeriv_eq_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] [Nontrivial F] (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → F} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n) : ν (f '' {x : E | fderiv ℝ f x = 0}) = 0

The image under a sufficiently smooth map with nontrivial target of the whole locus where its Fréchet derivative vanishes has additive Haar measure zero, with no relation required between the two finite dimensions.

theorem TauCeti.ContDiff.dense_compl_image_vanishingFDeriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] [Nontrivial F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → F} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n) : Dense (f '' {x : E | fderiv ℝ f x = 0})ᶜ

The complement of the image of the locus where the derivative of a sufficiently smooth map with nontrivial target vanishes is dense.

@[simp]

theorem TauCeti.setOf_not_surjective_fderiv_eq_setOf_fderiv_eq_zero_of_finrank_eq_one {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → F} (hF : Module.finrank ℝ F = 1) : {x : E | ¬Function.Surjective ⇑(fderiv ℝ f x)} = {x : E | fderiv ℝ f x = 0}

A linear map into a one-dimensional space is surjective exactly when it is nonzero, so the critical points of a map into such a space are the points where its derivative vanishes.