Sard's regular-value corollary

regular_value_ae

Submitter: Kim Morrison.

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

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.

Informal solution: 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.

theorem declaration uses `sorry`regular_value_ae {m : ℕ} (f : EuclideanSpace ℝ (Fin m) → ℝ)
    (hf : ContDiff ℝ ∞ f) :
    ∀ᵐ c ∂(volume : Measure ℝ), LeanEval.Geometry.RegularValue.IsRegularValue f c := bym:ℕf:EuclideanSpace ℝ (Fin m) → ℝhf:ContDiff ℝ ∞ f⊢ ∀ᵐ (c : ℝ), IsRegularValue f c
  sorryAll goals completed! 🐙

Solved by

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