Sard's lemma on the flat stratum #
This file proves the case of finite-dimensional Sard's theorem carried by the higher derivatives:
if f is C^{k+1} and every iterated derivative of order 1 ≤ i ≤ k vanishes on a set s, then
f '' s is null as soon as finrank ℝ E < (k + 1) * finrank ℝ F. In Morse's proof of the
Morse--Sard theorem this is the estimate for the innermost stratum Σ_k of the critical set, the
one place where regularity beyond C¹ is genuinely needed; the two slices already available,
TauCeti.addHaar_image_eq_zero_of_not_surjective_fderivWithin (equal dimensions, C¹) and
Differentiable.addHaar_image_eq_zero_of_finrank_lt_finrank (smaller source,
differentiable), neither says anything when the source dimension exceeds the target dimension.
The argument is the classical one, but the covering estimate is replaced by Hausdorff dimension.
Iterating the mean value inequality down the tower of derivatives turns the vanishing hypothesis
into the Taylor-type bound ‖f y - f x‖ ≤ M * ‖y - x‖ ^ (k + 1), valid for x in the stratum and
y in a convex set on which ‖D^{k+1} f‖ ≤ M. On the stratum this bound is a Hölder condition
with exponent k + 1, so Mathlib's dimH_image_le_of_locally_holder_on divides the Hausdorff
dimension of the source by k + 1, and measure_zero_of_dimH_lt finishes.
When [Nontrivial F], a point of the stratum with 1 ≤ k has vanishing first derivative, so the
stratum consists of critical points and this is a statement about critical values; see
TauCeti.not_surjective_fderiv_of_iteratedFDeriv_one_eq_zero.
This is Lane F0 of the analytic Heegaard Floer roadmap, where finite-dimensional Sard is the prerequisite for Sard--Smale and hence for every transversality argument downstream.
Main results #
TauCeti.norm_sub_le_pow_of_iteratedFDeriv_eq_zero: the Taylor-type estimate obtained from the vanishing of the derivatives of order1 ≤ i ≤ kat a point.TauCeti.holderOnWith_of_iteratedFDeriv_eq_zero: a map is Hölder of exponentk + 1on any set of such points inside a convex set with bounded(k+1)-st derivative.TauCeti.dimH_image_le_of_iteratedFDeriv_eq_zero: such a set has its Hausdorff dimension divided byk + 1underf.TauCeti.addHaar_image_eq_zero_of_iteratedFDeriv_eq_zero: the resulting nullity statement, andTauCeti.ContDiff.addHaar_image_flatStratum_eq_zeroits global form on the whole stratum.TauCeti.ContDiff.dense_compl_image_flatStratum: the complement of the image of the stratum is dense.
References #
The proof is the first step of Morse's argument as presented in J. Milnor, Topology from the
Differentiable Viewpoint, §3, and in M. Hirsch, Differential Topology, Chapter 3.
The Hausdorff-dimension proof architecture is adapted from the sibling module
TauCeti/Analysis/Calculus/Sard/LowDimension.lean.
The Taylor-type estimate on the flat stratum. If f is C^{k+1} on a convex set s whose
(k+1)-st derivative is bounded by M, and if all iterated derivatives of order 1 ≤ i ≤ k
vanish at x ∈ s, then f moves points of s by at most M * ‖y - x‖ ^ (k + 1).
No factorials appear because the bound is obtained by applying the mean value inequality k + 1
times rather than by integrating a Taylor remainder.
The flat stratum is a Hölder set of exponent k + 1. On a set A of points at which all
iterated derivatives of order 1 ≤ i ≤ k vanish, sitting inside a convex set V on which f is
C^{k+1} with ‖D^{k+1} f‖ ≤ C, the map f is Hölder continuous with exponent k + 1.
This is where the vanishing of the derivatives is converted into a statement about how much f
can spread out a set, which is what controls Hausdorff dimension.
Sard's lemma on the flat stratum, in Hausdorff dimension. A C^{k+1} map divides the
Hausdorff dimension of a set of points at which all iterated derivatives of order 1 ≤ i ≤ k
vanish by k + 1.
The Hölder bound of TauCeti.holderOnWith_of_iteratedFDeriv_eq_zero only holds near a given point,
where the (k+1)-st derivative is bounded, so the countably stable local form
dimH_image_le_of_locally_holder_on is what applies.
Sard's lemma on the flat stratum. Let f be C^{k+1} on an open set U of a
finite-dimensional real normed space, and let s ⊆ U be a set at each point of which every
iterated derivative of order 1 ≤ i ≤ k vanishes. If finrank ℝ E < (k + 1) * finrank ℝ F, then
f '' s has additive Haar measure zero.
This is the slice of finite-dimensional Sard that higher regularity buys: for a fixed pair of
dimensions with positive-dimensional target, the hypothesis holds as soon as k is large enough.
Sard's lemma on the flat stratum, global form: the image of the whole set of points at
which all iterated derivatives of order 1 ≤ i ≤ k vanish is null, provided
finrank ℝ E < (k + 1) * finrank ℝ F.
The complement of the image of the flat stratum of a C^{k+1} map is dense, provided
finrank ℝ E < (k + 1) * finrank ℝ F.
A point at which the first derivative vanishes is a critical point, as long as the target is
nontrivial. In particular the flat stratum of f for 1 ≤ k consists of critical points, so
TauCeti.addHaar_image_eq_zero_of_iteratedFDeriv_eq_zero is a statement about critical values.