Sard's regular-value corollary

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

Notes

For a smooth f : ℝᵐ → ℝ, almost every c ∈ ℝ is a regular value (every point of f⁻¹(c) has nonzero derivative). The measure-theoretic heart of the regular-value form of Sard's theorem; the main critical-set-null Sard theorem is a separate lean-eval problem (§125 main). Trusted helper IsRegularValue (non-hole). Mathlib has the equal-dimension Jacobian lemma and Hausdorff-dimension corollaries but not the general critical-values-null statement. Candidate from §125 of the Knill survey (additional 1).

Formal statement

/-- **Regular value corollary (Sard).** For a smooth `f : ℝᵐ → ℝ`, almost every
`c ∈ ℝ` is a regular value. -/
theorem regular_value_ae {m : ℕ} (f : EuclideanSpace ℝ (Fin m) → ℝ)
    (hf : ContDiff ℝ ∞ f) :
    ∀ᵐ c ∂(volume : Measure ℝ), IsRegularValue f c := by
  sorry

Informal solution sketch

Apply Sard's theorem with target dimension n = 1: the set of critical values of f (images of points where df = 0) has Lebesgue measure zero. A value c is regular iff it is not a critical value, so the regular values are the complement of a null set, i.e. almost every c is regular. Reduces to the main Sard theorem (critical set null) specialized to real-valued f.

Source

A. Sard, The measure of the critical values of differentiable maps, Bull. AMS 48 (1942); A. P. Morse (1939). Knill, Some fundamental theorems in mathematics, §125.

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: regular_value_ae
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.