Sard's lemma when the source has smaller dimension

This file proves the lower-dimensional-source case of finite-dimensional Sard's theorem. If a differentiable map goes from a finite-dimensional real normed space to one of strictly larger dimension, then the image of every subset of the source has additive Haar measure zero. In particular, the whole range is null.

Every derivative in this dimension range is nonsurjective, so the range is exactly the set of critical values. The proof uses the Hausdorff-dimension route already developed in Mathlib: DifferentiableOn.dimH_image_le says that differentiable maps do not increase dimension, and measure_zero_of_dimH_lt turns the resulting strict dimension bound into nullity. Uniqueness of additive Haar measure transfers the statement from Hausdorff measure to any Haar normalization.

This supplies the source-dimension-smaller-than-target case of finite-dimensional Sard in Lane F0 of the analytic Heegaard Floer roadmap. Together with the equal-dimensional case, it isolates the higher-regularity Morse--Sard argument to the remaining case where the source dimension is larger.

Main declarations

• DifferentiableOn.addHaar_image_eq_zero_of_dimH_lt_finrank: a differentiable map on a set of sufficiently small Hausdorff dimension sends it to an additive-Haar-null set.
• Differentiable.addHaar_image_eq_zero_of_finrank_lt_finrank: a differentiable map into a strictly higher-dimensional space sends every subset to an additive-Haar-null set.
• Differentiable.addHaar_range_eq_zero_of_finrank_lt_finrank: the whole range of such a map is additive-Haar-null.
• TauCeti.not_surjective_fderiv_of_finrank_lt_finrank: every derivative in this dimension range is nonsurjective.
• TauCeti.setOf_not_surjective_fderiv_eq_univ_of_finrank_lt_finrank: every point belongs to the critical locus in this dimension range.
• Differentiable.addHaar_image_not_surjective_fderiv_eq_zero_of_finrank_lt_finrank: the critical values are additive-Haar-null, in the form used by Sard's theorem.

The Hausdorff-dimension argument follows the one used for the lower-dimensional Sard corollary in Mathlib's Topology.MetricSpace.HausdorffDimension.

theorem DifferentiableOn.addHaar_image_eq_zero_of_dimH_lt_finrank {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set E} {f : E → F} (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] (hf : DifferentiableOn ℝ f s) (hsF : dimH s < ↑(Module.finrank ℝ F)) : ν (f '' s) = 0

A differentiable map on a set of Hausdorff dimension strictly smaller than the dimension of the codomain sends that set to an additive-Haar-null set.

The source may be any real normed space, the codomain may carry an arbitrary finite-dimensional norm, and ν may be any normalization of additive Haar measure.

theorem Differentiable.addHaar_image_eq_zero_of_finrank_lt_finrank {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {f : E → F} (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] (hf : Differentiable ℝ f) (hEF : Module.finrank ℝ E < Module.finrank ℝ F) (t : Set E) : ν (f '' t) = 0

A differentiable map from a finite-dimensional real normed space to a strictly higher-dimensional one sends every subset of its domain to an additive-Haar-null set.

theorem Differentiable.addHaar_range_eq_zero_of_finrank_lt_finrank {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {f : E → F} (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] (hf : Differentiable ℝ f) (hEF : Module.finrank ℝ E < Module.finrank ℝ F) : ν (Set.range f) = 0

A differentiable map from a finite-dimensional real normed space to a strictly higher-dimensional one has additive-Haar-null range. This is the lower-dimensional-source case of Sard's theorem: every point of the source is critical because no derivative can be surjective.

theorem TauCeti.not_surjective_fderiv_of_finrank_lt_finrank {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hEF : Module.finrank ℝ E < Module.finrank ℝ F) (x : E) : ¬Function.Surjective ⇑(fderiv ℝ f x)

When the source has strictly smaller finite dimension than the codomain, every Fréchet derivative is nonsurjective. Thus every source point is critical, independently of the regularity of the function.

@[simp]

theorem TauCeti.setOf_not_surjective_fderiv_eq_univ_of_finrank_lt_finrank {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hEF : Module.finrank ℝ E < Module.finrank ℝ F) : {x : E | ¬Function.Surjective ⇑(fderiv ℝ f x)} = Set.univ

When the source has strictly smaller finite dimension than the codomain, the critical locus of any function is the whole source.

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

The critical values of a differentiable map from a finite-dimensional real normed space to a strictly higher-dimensional one have additive Haar measure zero. In this dimension range every point is critical, but stating the result for the critical locus gives the Sard form consumed by later regular-value arguments.