The intermediate strata in Sard's theorem

This file supplies the local dimension-reduction step for the intermediate strata in the Morse--Sard proof. Suppose the ith iterated derivative of a smooth map vanishes at a, but the derivative of order i + 1 does not. A scalar component of the ith derivative then has a nonzero differential at a. Its zero set is a regular hypersurface containing every nearby point where the ith derivative vanishes.

TauCeti.exists_parametrization_iteratedFDeriv_eq_zero makes this reduction explicit. It gives a C^r parametrization θ from the kernel of a nonzero scalar functional, whose dimension is one less than that of the source. Locally, the zero set of the ith derivative is contained in the image under θ of any prescribed neighbourhood of the origin, and θ itself lies in a regular scalar level set containing that zero set. This is the induction-on-source-dimension input for proving that the images of the intermediate strata Σ_i \ Σ_{i+1} are null.

The scalar component is obtained by Hahn--Banach from a nonzero value of the derivative of iteratedFDeriv ℝ i f. The parametrization is Mathlib's implicit function for that scalar component. This is the second stratification step following the flat-stratum estimate in TauCeti.Analysis.Calculus.Sard.FlatStratum.

Main result

• TauCeti.exists_parametrization_iteratedFDeriv_eq_zero: near a point of Σ_i \ Σ_{i+1}, the set Σ_i is contained in the image of a C^r map from a codimension-one space.

References

The reduction is the intermediate-stratum step in the proof of Sard's theorem given in J. Milnor, Topology from the Differentiable Viewpoint, Section 3, and M. Hirsch, Differential Topology, Chapter 3.

theorem TauCeti.exists_parametrization_iteratedFDeriv_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {a : E} {i r : ℕ} (hf : ContDiffAt ℝ (↑(r + i)) f a) (hr : r ≠ 0) (hi : iteratedFDeriv ℝ i f a = 0) (hnext : iteratedFDeriv ℝ (i + 1) f a ≠ 0) : ∃ (g : E → ℝ) (g' : E →L[ℝ] ℝ) (θ : ↥(↑g').ker → E), ContDiffAt ℝ (↑r) g a ∧ HasFDerivAt g g' a ∧ (↑g').range = ⊤ ∧ (∀ (x : E), iteratedFDeriv ℝ i f x = 0 → g x = 0) ∧ θ 0 = a ∧ ContDiffAt ℝ (↑r) θ 0 ∧ (∀ᶠ (z : ↥(↑g').ker) in nhds 0, g (θ z) = 0) ∧ (∀ V ∈ nhds 0, ∀ᶠ (x : E) in nhds a, iteratedFDeriv ℝ i f x = 0 → x ∈ θ '' V) ∧ Module.finrank ℝ ↥(↑g').ker + 1 = Module.finrank ℝ E

Local hypersurface reduction for an intermediate Sard stratum. Suppose f is C^{r+i} at a, with r > 0, its ith iterated derivative vanishes at a, and its (i+1)st derivative does not. Then there are a scalar component g of the ith derivative, its nonzero derivative g', and a C^r parametrization θ from ker g' such that:

• every zero of iteratedFDeriv ℝ i f is a zero of g;
• locally at a, every zero of iteratedFDeriv ℝ i f lies in the image under θ of any prescribed neighbourhood of the origin;
• locally at the origin, θ lies in the regular level set g = 0; and
• ker g' has dimension one less than E.

In particular, the intermediate stratum where all derivatives through order i vanish but the next does not is locally carried by a smooth map from a strictly lower-dimensional source.