Sard's theorem

DefinitionCritical points of a map to Euclidean space#✓fully proved

Let \(M\) be a Hausdorff, second-countable smooth manifold without boundary modelled on a finite-dimensional real normed space, and let \(f : M \to \mathbb{R}^n\) be a map. The critical set of \(f\) is the set of points \(x \in M\) at which the manifold derivative of \(f\) at \(x\), a linear map \(T_xM \to \mathbb{R}^n\), is not surjective.

The derivative is taken to be \(0\) at points where \(f\) is not differentiable.

def criticalSet (f : M → EuclideanSpace ℝ (Fin n)) : Set M :=
  {x | ¬ Function.Surjective (mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) f x)}
Used by 2
Used byCritical values of a map to Euclidean space · Sard's theorem for maps into Euclidean space

DefinitionCritical values of a map to Euclidean space#✓fully proved

Let \(M\) be a Hausdorff, second-countable smooth manifold without boundary modelled on a finite-dimensional real normed space, and let \(f : M \to \mathbb{R}^n\) be a map. The set of critical values of \(f\) is the image under \(f\) of its critical set, the set of points \(x \in M\) at which the manifold derivative of \(f\) at \(x\) is not surjective.

def criticalValues (f : M → EuclideanSpace ℝ (Fin n)) : Set (EuclideanSpace ℝ (Fin n)) :=
  f '' criticalSet (I := I) (M := M) (n := n) f
Uses 1 · Used by 2
Statement usesCritical points of a map to Euclidean space
Used bySard's theorem for maps into Euclidean space · Approximation by maps having zero as a regular value

TheoremSard's theorem on open subsets of finite-dimensional spaces#✓fully proved

Let \(E\) and \(F\) be finite-dimensional real normed spaces, let \(\mu\) be an additive Haar measure on \(F\) with its Borel \(\sigma\)-algebra, let \(U \subseteq E\) be open, and let \(g : E \to F\) be \(C^\infty\) on \(U\). Then the image under \(g\) of the set of points \(x \in U\) at which the derivative of \(g\) is not surjective has \(\mu\)-measure zero.

theorem sard_euclidean_open
    (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (F : Type v) [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
    [MeasurableSpace F] [BorelSpace F]
    (μ : Measure F) [μ.IsAddHaarMeasure]
    (U : Set E) (hU : IsOpen U) (g : E → F) (hg : ContDiffOn ℝ ∞ g U) :
    μ (g '' {x | x ∈ U ∧ ¬ Function.Surjective (fderiv ℝ g x)}) = 0
Uses 1 · Used by 2
Proof usesSets with locally null image have null image
Used byExistence of Morse functions · Parametric Sard theorem for real analytic families

TheoremSard's theorem for maps into Euclidean space#✓fully proved

Let \(M\) be a Hausdorff, second-countable smooth manifold without boundary modelled on a finite-dimensional real normed space, and let \(f : M \to \mathbb{R}^n\) be a \(C^\infty\) map. Then the set of critical values of \(f\), the image under \(f\) of the points of \(M\) at which the manifold derivative of \(f\) is not surjective, has Lebesgue measure zero.

theorem sard_theorem
    (f : M → EuclideanSpace ℝ (Fin n))
    (hf : ContMDiff I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) (⊤ : ℕ∞) f) :
    volume (criticalValues (I := I) (M := M) (n := n) f) = 0
Sources
  • A. Sard, Bull. Amer. Math. Soc. 48 (1942) 883–890 measure of critical values; J. Lee, Introduction to Smooth Manifolds, 2nd ed.; Guillemin-Pollack, Differential Topology; Lean states finite-dimensional manifold to EuclideanSpace ℝ (Fin n) specialization.
Uses 3 · Used by 1
Statement usesCritical values of a map to Euclidean space
Proof usesCritical points of a map to Euclidean space · Sets with locally null image have null image
Used byApproximation by maps having zero as a regular value

DefinitionBad parameter set#✓fully proved

Let \(F \colon \mathbb{R}^p \times \mathbb{R}^m \to \mathbb{R}^n\) be a map and \(y \in \mathbb{R}^n\). For \(a \in \mathbb{R}^p\) write \(F_a = F(a, \cdot)\) for the slice \(\mathbb{R}^m \to \mathbb{R}^n\). The bad parameter set of \(F\) at \(y\) is the set of \(a \in \mathbb{R}^p\) for which there is \(x \in \mathbb{R}^m\) with \(F(a, x) = y\) and the derivative of \(F_a\) at \(x\) not surjective, that is, the set of \(a\) for which \(y\) is not a regular value of \(F_a\).

The derivative of a map at a point where it is not differentiable is taken to be zero.

def badParameterSet {p m n : ℕ}
    (F : EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n))
    (y : EuclideanSpace ℝ (Fin n)) : Set (EuclideanSpace ℝ (Fin p)) :=
  { a | ∃ x : EuclideanSpace ℝ (Fin m), F (a, x) = y ∧
      ¬ Function.Surjective (fderiv ℝ (fun x : EuclideanSpace ℝ (Fin m) => F (a, x)) x) }
Used by 1
Used byParametric Sard theorem for real analytic families

TheoremParametric Sard theorem for real analytic families#✓fully proved

Let \(p, m, n\) be natural numbers, let \(F \colon \mathbb{R}^p \times \mathbb{R}^m \to \mathbb{R}^n\) be a real analytic (\(C^\omega\)) map and let \(y \in \mathbb{R}^n\). Suppose that the derivative of \(F\) is surjective at every point \((a, x)\) with \(F(a, x) = y\). Then the bad parameter set of \(F\) at \(y\), the set of \(a \in \mathbb{R}^p\) for which some \(x \in \mathbb{R}^m\) has \(F(a, x) = y\) and the derivative of the slice \(F(a, \cdot) \colon \mathbb{R}^m \to \mathbb{R}^n\) at \(x\) is not surjective, has Lebesgue measure zero.

theorem parametricSard
    {p m n : ℕ}
    (F : EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n))
    (y : EuclideanSpace ℝ (Fin n))
    (hF : ContDiff ℝ ⊤ F)
    (hreg : ∀ a x, F (a, x) = y → Function.Surjective (fderiv ℝ F (a, x))) :
    volume (badParameterSet (F := F) (y := y)) = 0
Sources
  • R. Abraham, Bull. Amer. Math. Soc. 69 (1963), 470–475, DOI 10.1090/S0002-9904-1963-10969-6 parametric transversality; V. Guillemin and A. Pollack, Differential Topology; J. Lee, Intro to Smooth Manifolds, 2nd ed.; Lean states Euclidean finite-dimensional measure-zero form with fderiv ℝ F surjective hypothesis.
Uses 3
Statement usesBad parameter set
Proof usesSard's theorem on open subsets of finite-dimensional spaces · Sets with locally null image have null image
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.