One of a family of theorems that smooth mappings have relatively few critical points. The usual form is, if f is a C1 mapping of smooth manifolds X to Y, the image under f of the set of critical points of f has Lebesgue measure zero in Y. You can find this form in most books on manifolds, for example Calculus on manifolds by Michael Spivak.

A more precise form of this theorem is due to Herbert Federer:

Suppose f: U → Y is a map of class Ck, from an open set U ⊂ Rm into any normed space Y. Let B ⊂ U be the set of points x ∈ U where the derivative Df(x) has rank ≤ n, where n < m is fixed. Then the image f(B) has s-dimensional Hausdorff measure zero, where s = n + (m - n)/k.

Thus, for a C1 map, the best you can do is the classical Sard's theorem where s = m (Hm is not exactly the Lebesgue measure of the classical theorem, but close enough). With more smoothness you get lower dimensions, down to a minimum of n. The bound given for s is sharp: Federer constructed examples of maps with Ht(B) > 0 for any t < n + (m-n)/k.

The proof of this sharp form of Sard's theorem is quite hard; it depends on rather technical methods of geometric measure theory. See Geometric measure theory by Herbert Federer, section 3.4.3.

If the domain of f is instead a Banach space, there is a form called the Morse-Sard theorem which states that f(B) is of first Baire category in Y. This is much coarser, but it's the best you can do in infinite dimensions.

This theorem is an example of a big rock, because it is frequently applied in very "geometric" contexts in differential topology and differential geometry, where people may not be very concerned with the hard analytic details that come into the proof. In differential topology all you want to know is that maps with no critical points in the "wrong places" are dense; see transversality for more information.

Log in or registerto write something here or to contact authors.