|
The theorem of Sard
asserts that if a mapping F from a region in R7n to Rp is smooth enough,
then the set of critical values of F has measure zero in Rp. The purpose of
this paper is to give a constructive proof of this theorem. By a constructive
proof is meant one which has numerical content, as explained in E. Bishop’s
Foundations of Constructive Analysis. In particular, it is shown that in every
open ball in Rp one can compute a point which is not a critical value of
F.
The proof is based on one given by Milnor, which is a modification of a
proof of Pontryagin. These proofs, as well as all other known proofs, are
nonconstructive, and it is not obvious that they can be constructivized. One
difficulty lies in the fact that, given two real numbers a and b, one cannot, in
general, prove constructively that either α ≧ b or α < b; one can only prove,
for arbitrary 𝜖 > 0, that either a > b − 𝜖 or a < b. This fact forces, among
other things, the consideration of ‘nearly critical values’ instead of critical
values, and the derivation of a slightly more general result. Once a proper
interpretation for “nearly critical values” has been found, Milnor’s proof can
be followed, replacing various nonconstructive arguments by constructive
ones.
|
