Lipschitz Images of Lebesgue Null Sets

This is an equidimensional measure-theoretic lemma.

Let $E$ be a finite-dimensional real inner-product space equipped with its measurable and Borel structures. Let $f:E\to E$, let $K\in[0,\infty)$ (NNReal), and let $s\subseteq E$. Assume:

1. $f$ is Lipschitz on $s$ with constant $K$.
2. The Lebesgue measure of $s$ is zero:

Then the image is also Lebesgue-null:

The declaration volume_image_eq_zero_of_lipschitzOnWith_readable does not require measurability of $s$ as an explicit hypothesis. It is restricted to maps from a finite-dimensional space to itself.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem volume_image_eq_zero_of_lipschitzOnWith {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {f : E → E} {K : NNReal} {s : Set E} (hf : LipschitzOnWith K f s)
    (hs : (volume : Measure E) s = 0) : (volume : Measure E) (f '' s) = 0

Module navigation

Module: Analysis/Sard/Equidimensional.

Source excerpt, lines 133–136 · Frozen source 408915f.