Sard's theorem for maps between manifolds of equal dimension

Let f : M → N be a differentiable map between real manifolds modelled on finite-dimensional spaces of the same dimension, where M is Lindelöf (for instance σ-compact or second countable). The image of the set of non-regular points of f is a null set of N, read through charts against Haar measure on the model, and consequently the regular values of f are dense in N. The manifolds may have boundary or corners.

The proof reads f in pairs of extended charts and applies the flat equal-dimensional Sard lemma TauCeti.addHaar_image_eq_zero_of_not_surjective_fderivWithin, which only needs derivatives within the model range range I. Countably many charts cover M by the Lindelöf property (TauCeti.isNullSet_image_of_forall_addHaar_image_extChartAt). For models of different dimensions, see TauCeti.Geometry.Manifold.Sard.Basic. Only first derivatives enter: in equal dimensions no higher regularity is needed.

Main results

• TauCeti.isNullSet_image_of_not_isRegularPoint: the image of any set of non-regular points at which f is differentiable is null.
• TauCeti.isNullSet_image_criticalPoints: the critical values of a differentiable map form a null set.
• TauCeti.dense_isRegularValue: the regular values of a differentiable map are dense.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Theorem 6.10.

theorem TauCeti.isNullSet_image_of_not_isRegularPoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {f : M → N} {s : Set M} [LindelofSpace M] [MeasurableSpace E'] [BorelSpace E'] (hdim : Module.finrank ℝ E = Module.finrank ℝ E') (hf : ∀ x ∈ s, MDiffAt f x) (hs : ∀ x ∈ s, ¬IsRegularPoint I J f x) : IsNullSet J (f '' s)

Sard's theorem in equal dimensions, for a set of non-regular points. Let M and N be real manifolds whose finite-dimensional models have the same dimension, with M Lindelöf. If f is differentiable at every point of s and no point of s is regular, then f '' s is null in N.

theorem TauCeti.isNullSet_image_criticalPoints {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {f : M → N} [LindelofSpace M] [MeasurableSpace E'] [BorelSpace E'] (hdim : Module.finrank ℝ E = Module.finrank ℝ E') (hf : MDiff f) : IsNullSet J (f '' {x : M | ¬IsRegularPoint I J f x})

Sard's theorem in equal dimensions. The critical values of a differentiable map from a Lindelöf manifold to a manifold whose finite-dimensional model has the same dimension form a null set.

theorem TauCeti.dense_isRegularValue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {f : M → N} [LindelofSpace M] (hdim : Module.finrank ℝ E = Module.finrank ℝ E') (hf : MDiff f) : Dense {y : N | IsRegularValue I J f y}

The regular values of a differentiable map from a Lindelöf manifold to a manifold whose finite-dimensional model has the same dimension are dense.