The outermost stratum, and the Morse--Sard theorem #
The critical values of a sufficiently smooth map between finite-dimensional real normed spaces form a set of additive Haar measure zero, and its regular values are therefore dense. A point is critical when the Fréchet derivative there fails to be surjective. The conclusion is recorded here in a measure-free form as well -- the critical values have empty interior -- for use where the target carries no measurable structure of its own.
The strata of the critical set are handled in the neighbouring files, and this one supplies the
outermost stratum, where the derivative is nonzero but not surjective, together with the assembly
of all the strata into the theorem itself. The two earlier results,
Differentiable.addHaar_image_criticalPoints_eq_zero (equal dimensions),
Differentiable.addHaar_image_not_surjective_fderiv_eq_zero_of_finrank_lt_finrank
(smaller source), need only differentiability. The theorem here needs no relation between the
two dimensions, but imposes stronger smoothness.
The argument for the outermost stratum is Milnor's. Near a point a where the derivative does not
vanish, pick v₀ with Df(a) v₀ ≠ 0 and a functional φ on the target with φ (Df(a) v₀) = 1.
Then u := φ ∘ f has a nonvanishing differential at a, so x ↦ (u x, π x) is a local
diffeomorphism onto ℝ × ker (D u a) for the projection π along v₀, and its local inverse Θ
parametrizes all the nearby level sets of u at once. Splitting the target as ℝ × ker φ too,
f becomes the map (t, z) ↦ (t, G t z) with G t z := ρ (f (Θ (t, z))), where ρ projects the
target along Df(a) v₀: it preserves the level t, so it carries each hyperplane into a
hyperplane. Whenever a point is critical for f, it is critical for the restricted map G t,
whose source has one dimension less, so the induction hypothesis makes every slice of the image of
the critical set null, and Fubini finishes. Compactness enters only to make the slicing legitimate:
an image with null slices need not be null unless it is measurable, so the
argument runs over the pieces crit f ∩ closedBall a r. These are compact because
TauCeti.isOpen_setOf_surjective makes the surjective operators an open set, so the critical
locus, its preimage under the continuous derivative, is closed on the ball, and a closed subset of
a compact ball is compact.
The induction is on the dimension of the source, and both spaces are quantified inside the
statement carried through it, since the induction step replaces each of them by a
hyperplane. The regularity finrank ℝ E * finrank ℝ E + 1 is inherited from
TauCeti.addHaar_image_eq_zero_of_fderiv_eq_zero and is a sufficient bound, not the sharp
exponent max 1 (finrank ℝ E - finrank ℝ F + 1) of the Morse--Sard theorem; no regularity is lost
in the descent, since the inverse function theorem returns a local inverse as smooth as the map.
Main results #
TauCeti.addHaar_image_criticalPoints_eq_zero: the critical values taken on a set where the map is sufficiently smooth at every point form a null set.ContDiff.addHaar_image_criticalPoints_eq_zero: the Morse--Sard theorem, its global form.ContDiff.dense_compl_image_criticalPoints: the regular values are dense, without requiring a measurable structure on the target.TauCeti.interior_image_criticalPoints_eq_empty: the measure-free restatement, that the critical values have empty interior.
Finite-dimensional Sard supplies the fibrewise step in Sard--Smale and the regular values used in transversality arguments.
References #
The stratification and the Fubini step are the proof of Sard's theorem in J. Milnor, Topology from the Differentiable Viewpoint, Section 3, and M. Hirsch, Differential Topology, Chapter 3.
The Morse--Sard theorem on a set. The values taken at the points of U where the Fréchet
derivative is not surjective form a set of additive Haar measure zero, provided the map is
sufficiently smooth at every point of U. The set need not be open, and no relation between the
two finite dimensions is required.
The Morse--Sard theorem. The critical values of a sufficiently smooth map between finite-dimensional real normed spaces, that is the values it takes at the points where its Fréchet derivative is not surjective, form a set of additive Haar measure zero. No relation between the two dimensions is required.
The Morse--Sard theorem, in the form that carries no measure-theoretic data: the critical
values taken on a set where the map is sufficiently smooth at every point have empty interior.
The measure structure used to prove it is chosen inside the proof, so the target here carries no
MeasurableSpace instance; this is the shape in which Sard is fed to the fibrewise step of the
Sard--Smale theorem, where the target is a complement subspace with no measurable structure of
its own.
The regular values of a sufficiently smooth map between finite-dimensional real normed spaces are dense. This form of the Morse--Sard theorem needs no measurable structure on the target and supplies the regular values used in transversality arguments.