Sard's theorem for maps between manifolds of arbitrary dimensions

Let f : M → N be a map between real manifolds modelled on finite-dimensional spaces E and E', of dimensions m and n, with M Lindelöf (for instance second countable). This file proves that the critical values of f, the images of the points where mfderiv I J f is not surjective, form a null set of N: their image in every chart of N is null for every Haar measure on E' (TauCeti.IsNullSet). No measure on N itself is chosen. The regularity needed depends on the dimensions.

• If m < n, every point is critical and the whole image of a differentiable map is null; here M and N may have boundary or corners.
• In general, a C^k map with k > m - n and k ≥ 1 suffices, in particular a smooth map. This is the sharp regularity of Sard's theorem: Whitney's example shows that a C¹ function on the plane can have critical values of positive measure.

Each statement only asks for the regularity at the points of a given set s of critical points, so it applies to maps that are only defined, or only regular, on an open subset of M. Except in the first case, M is boundaryless, in the sense that its model fills E.

The proofs read f in pairs of extended charts and apply the corresponding theorem for maps between normed spaces (TauCeti.addHaar_image_criticalPoints_eq_zero and DifferentiableOn.addHaar_image_eq_zero_of_finrank_lt_finrank). A countable family of charts covers M (TauCeti.isNullSet_image_of_forall_addHaar_image_extChartAt), and since nullity is tested in every chart of N, no comparison of target charts is needed. The equal-dimensional case, which needs only first derivatives and allows boundary in the source, is TauCeti.isNullSet_image_of_not_isRegularPoint.

Main results

• TauCeti.isNullSet_image_of_finrank_lt_finrank: the image of a differentiable map from a manifold of smaller dimension is null.
• TauCeti.isNullSet_image_of_not_isRegularPoint_of_contMDiffAt: Sard's theorem at the sharp regularity k > m - n, k ≥ 1, for arbitrary dimensions.
• ContMDiff.isNullSet_image_criticalPoints and ContMDiff.dense_isRegularValue: the critical values of such a map are null, and its regular values are dense.

References

• A. Sard, The measure of the critical values of differentiable maps, Bull. Amer. Math. Soc. 48 (1942), 883–890.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Theorem 6.10 and its proof (passage from coordinates to manifolds).

theorem TauCeti.isNullSet_image_of_finrank_lt_finrank {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {s : Set M} [IsManifold I 1 M] [IsManifold J 1 N] (hdim : Module.finrank ℝ E < Module.finrank ℝ E') (hf : ∀ x ∈ s, MDiffAt f x) : IsNullSet J (f '' s)

Sard's theorem when the source has smaller dimension. If the model of M has smaller dimension than the model of N and f is differentiable at every point of s, then f '' s is null in N. Both manifolds may have boundary or corners.

theorem MDifferentiable.isNullSet_range_of_finrank_lt_finrank {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} [IsManifold I 1 M] [IsManifold J 1 N] (hf : MDiff f) (hdim : Module.finrank ℝ E < Module.finrank ℝ E') : TauCeti.IsNullSet J (Set.range f)

The range of a differentiable map from a Lindelöf manifold to a manifold of larger dimension is null.

theorem TauCeti.isNullSet_image_of_not_isRegularPoint_of_contMDiffAt {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {s : Set M} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ E' + 1) ≤ n) (hf : ∀ x ∈ s, ContMDiffAt I J n f x) (hs : ∀ x ∈ s, ¬IsRegularPoint I J f x) : IsNullSet J (f '' s)

Sard's theorem. Let M be a boundaryless Lindelöf manifold modelled on a space of dimension m and N a manifold modelled on a space of dimension n. If f is C^k at every point of s with k > m - n and k ≥ 1, and no point of s is regular, then f '' s is null in N. This is the sharp regularity of Sard's theorem.

theorem ContMDiff.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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] (hf : ContMDiff I J n f) (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ E' + 1) ≤ n) : TauCeti.IsNullSet J (f '' {x : M | ¬TauCeti.IsRegularPoint I J f x})

Sard's theorem. The critical values of a C^k map from a boundaryless Lindelöf manifold of dimension m to a manifold of dimension n form a null set when k > m - n and k ≥ 1, in particular when the map is smooth.

theorem ContMDiff.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] [LindelofSpace 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] {f : M → N} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] (hf : ContMDiff I J n f) (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ E' + 1) ≤ n) : Dense {y : N | TauCeti.IsRegularValue I J f y}

The regular values of a C^k map from a boundaryless Lindelöf manifold of dimension m to a manifold of dimension n are dense when k > m - n and k ≥ 1, in particular when the map is smooth.