Moreira's version of Sard's theorem

Source: doi:10.5565/PUBLMAT_45101_06 Authors: Yury G. Kudryashov Status: verified Main declarations: dimH_image_le_sardMoreiraBound_of_finrank_le Tags: analysis, measure-theory, sard-theorem, hausdorff-measure MSC: 28A78, 58C25

Mathematical overview

Moreira's strengthening of Sard's theorem on the Hausdorff dimension of the critical-value set of a sufficiently differentiable map.

Main results

• hausdorffMeasure_sardMoreiraBound_image_null_of_finrank_le — Hausdorff measure vanishing for the image of a set whose derivative rank is bounded by p.
• dimH_image_le_sardMoreiraBound_of_finrank_le — the corresponding Hausdorff-dimension bound for critical-value images.
• ContDiffMoreiraHolderAt — the pointwise C^{k+α} predicate (function is C^k at a point and the k-th derivative is locally Hölder of exponent α).
• WithRPowDist — metric-space wrapper giving dist x y ^ α as the metric, used to apply Vitali covering arguments to product spaces with mixed scaling.