Sard's theorem (critical-set image has measure zero)

sard_theorem

Submitter: Kim Morrison.

Notes: For a smooth map f : ℝᵐ → ℝⁿ, the image of the rank-deficient locus {x | rank df(x) < m ∧ rank df(x) < n} has Lebesgue measure zero. This is Knill's specific phrasing — the standard textbook Sard theorem uses the larger critical set {x | rank df(x) < n} (failure of surjectivity), which is a weaker hypothesis, so textbook Sard *implies* the form proved here. The two agree when m ≥ n; for m < n a smooth immersion has every point critical under the textbook definition but no critical points under Knill's. The manifold form follows chart-by-chart from this Euclidean version. Mathlib has the equal-dimension case (`addHaar_image_eq_zero_of_det_fderivWithin_eq_zero`) when det df = 0, plus topological corollaries via Hausdorff dimension (`ContDiff.dense_compl_range_of_finrank_lt_finrank`), but no general critical-value / Sard statement. §125 of Knill's *Some Fundamental Theorems in Mathematics*.

Source: A.P. Morse, 'The behavior of a function on its critical set', Ann. of Math. (2) 40 (1939) 62–70; A. Sard, 'The measure of the critical values of differentiable maps', Bull. Amer. Math. Soc. 48 (1942) 883–890. §125 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The classical proof stratifies the critical set by rank, applies the implicit function theorem to straighten `f` locally on each stratum into a normal form, and bounds the image with Taylor estimates plus Fubini and countable covers. The standard regularity threshold is `C^k` for `k ≥ max(m − n + 1, 1)` (Whitney's threshold for the surjectivity-failure form); the smooth (`C^∞`) hypothesis used here is stronger than needed. Knill's rank-deficient form is implied by the textbook surjectivity-failure form. Mathlib has the equal-dimension Jacobian-determinant lemma (`addHaar_image_eq_zero_of_det_fderivWithin_eq_zero`) and Hausdorff-dimension topological corollaries, but not the rank-stratification / normal-form / Fubini-and-cover machinery, and not the general critical-value Sard statement.

theorem declaration uses `sorry`sard {m n : ℕ} (f : LeanEval.Geometry.SardTheoremProblem.E m → LeanEval.Geometry.SardTheoremProblem.E n) (_hf : ContDiff ℝ ∞ f) :
    volume (LeanEval.Geometry.SardTheoremProblem.criticalValues f) = 0 := bym:ℕn:ℕf:E m → E n_hf:ContDiff ℝ ∞ f⊢ volume (criticalValues f) = 0
  sorryAll goals completed! 🐙

Solved by

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 5, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jun 5, 2026