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

sard_theorem — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Sard's theorem** (Morse 1939 / Sard 1942), Knill's rank-
deficient form. The image of the rank-deficient locus of a smooth
map `f : ℝᵐ → ℝⁿ` has Lebesgue measure zero. -/
theorem sard {m n : ℕ} (f : E m → E n) (_hf : ContDiff ℝ ∞ f) :
    volume (criticalValues f) = 0 := by
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: sard
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.