Sard's lemma in equal dimensions

This file proves the equal-dimensional case of Sard's theorem for maps between two possibly different finite-dimensional real normed spaces. A differentiable map sends any set on which its derivative is nowhere surjective to a set of additive Haar measure zero. In particular, the critical values of a differentiable map between spaces of equal dimension have measure zero, and the regular values are dense.

Mathlib proves the corresponding result for an endomorphism of one normed space in addHaar_image_eq_zero_of_det_fderivWithin_eq_zero. We transport the codomain across a continuous linear equivalence and use uniqueness of additive Haar measure to return to the original codomain. This is the first, equal-dimensional slice of finite-dimensional Sard required by Lane F0 of the analytic Heegaard Floer roadmap. The general Morse--Sard theorem additionally needs the higher-regularity argument when the dimensions differ.

Main results

• TauCeti.addHaar_image_eq_zero_of_not_surjective_fderivWithin: a map between equal-dimensional spaces sends a set of nonsurjective derivative points to a null set.
• Differentiable.addHaar_image_criticalPoints_eq_zero: the critical values of a globally differentiable map between equal-dimensional spaces form a null set.
• Differentiable.dense_compl_image_criticalPoints: the regular values of such a map are dense.

The measure-theoretic input follows Sébastien Gouëzel's Mathlib formalization of the change of variables theorem, itself based on Fremlin, Measure Theory, volume 2.

theorem TauCeti.addHaar_image_eq_zero_of_not_surjective_fderivWithin {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set E} {f : E → F} {f' : E → E →L[ℝ] F} (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] (hdim : Module.finrank ℝ E = Module.finrank ℝ F) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hcrit : ∀ x ∈ s, ¬Function.Surjective ⇑(f' x)) : ν (f '' s) = 0

Sard's lemma in equal dimensions. Let E and F be finite-dimensional real normed spaces of equal dimension. If f is differentiable along s with derivative f', and f' is nowhere surjective on s, then f '' s has additive Haar measure zero in F.

Unlike the endomorphism version in Mathlib, the domain and codomain need not be the same normed space and may carry unrelated norms and Haar measure normalizations.

theorem Differentiable.addHaar_image_criticalPoints_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {f : E → F} (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] (hf : Differentiable ℝ f) (hdim : Module.finrank ℝ E = Module.finrank ℝ F) : ν (f '' {x : E | ¬Function.Surjective ⇑(fderiv ℝ f x)}) = 0

The critical values of a differentiable map between equal-dimensional finite-dimensional real normed spaces have additive Haar measure zero. A point is critical here exactly when the Fréchet derivative is not surjective.

theorem Differentiable.dense_compl_image_criticalPoints {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {f : E → F} (hf : Differentiable ℝ f) (hdim : Module.finrank ℝ E = Module.finrank ℝ F) : Dense (f '' {x : E | ¬Function.Surjective ⇑(fderiv ℝ f x)})ᶜ

The regular values of a differentiable map between equal-dimensional finite-dimensional real normed spaces are dense. Here the regular values are expressed as the complement of the image of the points where the Fréchet derivative is not surjective.