The Sard--Smale theorem #
A Fredholm map between Banach spaces is one whose Fréchet derivative is a Fredholm operator at every point. Sard's theorem fails outright in infinite dimensions -- there is no Haar measure to be null for, and the critical values of a smooth map on a Hilbert space can be everything -- but Smale observed that a Fredholm map is finite-dimensional in the only direction that matters, and that the finite-dimensional theorem therefore survives with "measure zero" replaced by "meagre":
Sard--Smale. The critical values of a sufficiently smooth Fredholm map on an open subset of a separable Banach space are meagre, so its regular values are residual, and in particular dense.
This file proves that, in the local form
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints first and then in the
global forms TauCeti.isMeagre_image_criticalPoints_of_isFredholm and
TauCeti.dense_compl_image_criticalPoints_of_isFredholm. The local form needs no separability;
the global ones assume the domain second countable, since their proof covers it by countably many
of the local neighbourhoods.
The proof #
The two halves of the local statement are proved from the two halves of the substrate already in place over the linear Fredholm theory.
Empty interior comes from the Lyapunov--Schmidt normal form of
TauCeti.Analysis.Fredholm.NormalForm. In the normal-form chart Φ at a point a, the map
reads y ↦ y.1 + q y where the obstruction q takes values in the finite-dimensional
complement pkg.decCodom.X₀ of the range; the first coordinate is therefore free, and the
derivative at Φ.symm y is surjective exactly when the derivative of the slice
z ↦ q (y.1, z) is, a map between the two finite-dimensional spaces pkg.decDom.X₀ = ker and
pkg.decCodom.X₀ = coker. Finite-dimensional Morse--Sard
(TauCeti.interior_image_criticalPoints_eq_empty) applies to each slice, so the image of the
critical set meets every fibre of the product pkg.decCodom.X₁ × pkg.decCodom.X₀ in a set with
empty interior. A set whose fibres over the second factor all have empty interior has empty
interior, because an interior point would supply a whole box; this is where the infinite
dimension of the first factor is harmless.
Closedness comes from Smale's local properness lemma in TauCeti.Analysis.Fredholm.Proper: on a
small closed ball N the preimage of a compact set is compact, and the critical locus is
relatively closed there -- again read off the slice, whose target is finite dimensional, where
TauCeti.isOpen_setOf_surjective applies. A convergent sequence of critical values then has its
sources in a compact set, and a subsequential limit produces the missing critical point. Without
this half only density, not residuality, would follow, since a countable union of sets with empty
interior need not be meagre.
The global statement follows by covering: a second-countable domain is Lindelöf, so countably many
of these balls suffice, and a countable union of closed nowhere dense sets is meagre. Density of
the regular values is then the Baire category theorem. The CompleteSpace F assumption supplies
both the Baire instance and the local properness used above to prove closedness.
The regularity threshold is inherited unchanged from the finite-dimensional theorem: C^k with
k ≥ (dim ker)² + 1, rather than Smale's sharp k > index, because the underlying
TauCeti.addHaar_image_criticalPoints_eq_zero is proved with the cruder bound.
Main results #
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints: the local form -- inside any neighbourhood of a point with Fredholm derivative there is a neighbourhood whose critical values are closed and nowhere dense.TauCeti.isMeagre_image_criticalPoints_of_isFredholm: the Sard--Smale theorem.TauCeti.dense_compl_image_criticalPoints_of_isFredholm: the regular values of a Fredholm map are dense, the form transversality arguments consume.
References #
- S. Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965), 861--866.
- D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.
Sard--Smale, locally. Near a point where a sufficiently smooth map has Fredholm
derivative there is a neighbourhood on which the critical values form a closed nowhere dense set.
The neighbourhood can be taken inside any prescribed neighbourhood U of the point, so the
conclusion can be confined to a region on which f is known to be the map of interest.
Completeness of the target enters through Smale's local properness lemma, which supplies the compactness used to prove that the local critical-value image is closed.
The regularity threshold (dim ker)² + 1 is the one inherited from the finite-dimensional
Morse--Sard theorem TauCeti.interior_image_criticalPoints_eq_empty, which the fibrewise step
applies to the obstruction slice, a map out of ker (fderiv ℝ f a).
The Sard--Smale theorem. The critical values of a sufficiently smooth Fredholm map on an open subset of a separable Banach space form a meagre set.
Sard's theorem itself is false in infinite dimensions, and "measure zero" has no meaning there; what survives is that the Fredholm condition confines the failure of regularity to a finite-dimensional direction, in which the finite-dimensional theorem applies fibrewise.
The regularity threshold is the pointwise one of
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints: at each point C^k with
k ≥ (dim ker)² + 1. In particular n = ∞ needs no side condition.
Sard--Smale, in the form transversality arguments consume: the regular values of a
sufficiently smooth Fredholm map are dense, being the complement of a meagre set in a Baire
space. The regularity threshold is that of
TauCeti.isMeagre_image_criticalPoints_of_isFredholm.