Eilenberg's inequality

Let f : X → Y be K-Lipschitz on a set A of an extended metric space, where Y is a real normed space of finite dimension m carrying an additive Haar measure μ. For every real t, Eilenberg's inequality (the coarea inequality) bounds the Hausdorff measures of the fibers of f on average:

∫* μH[t] (A ∩ f ⁻¹' {y}) dμ(y) ≤ μ (ball 0 1) * K ^ m * μH[m + t] A.

No measurability of A, of the fibers, or of the fiber-measure function is assumed. The integral on the left is an upper integral: we produce a measurable majorant of y ↦ μH[t] (A ∩ f ⁻¹' {y}) with integral bounded by the right-hand side. Consequently, if μH[m + t] A = 0 then almost every fiber is μH[t]-null, and if μH[m + t] A < ∞ then almost every fiber has finite μH[t] measure. These are the exceptional-set statements used in the proof of the coarea formula, where X is n-dimensional, t = n - m, and μ is Lebesgue measure. We also give them for the Euclidean-normalized Hausdorff measures μHE[k].

The constant is not sharp: it comes from enclosing a set of diameter d in a ball of radius d, whereas the isodiametric inequality would give the optimal constant.

The argument

Cover A by sets c i of diameter at most δ whose (m + t)-dimensional Hausdorff sum is close to μH[m + t] A. For every y, the sets c i ∩ A ∩ f ⁻¹' {y} cover the fiber over y, so its δ-approximate t-dimensional Hausdorff content is at most ∑ i, ediam (c i ∩ A) ^ t * 1[y ∈ closure (f '' (c i ∩ A))]. The closure of f '' (c i ∩ A) has diameter at most K * ediam (c i ∩ A), hence measure at most μ (ball 0 1) * (K * ediam (c i ∩ A)) ^ m, so the integral of this majorant is at most μ (ball 0 1) * K ^ m * ∑ i, ediam (c i) ^ (m + t). Letting δ → 0, Fatou's lemma bounds the integral of the lower limit of the majorants.

For t < 0 the inequality is degenerate: μH[t] is infinite on every nonempty set, and either μH[m + t] A = ∞ or μH[m] A = 0. In the second case the majorant for t = 0 has integral zero and is positive on the image of A, so ∞ times it is a majorant with integral zero.

Main declarations

• LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le: Eilenberg's inequality with a measurable majorant of the fiber measures.
• LipschitzOnWith.lintegral_hausdorffMeasure_inter_preimage_le: the integral form.
• LipschitzOnWith.ae_hausdorffMeasure_inter_preimage_eq_zero and LipschitzOnWith.ae_hausdorffMeasure_inter_preimage_lt_top: almost every fiber is null, respectively of finite measure, under the corresponding hypothesis on A.
• LipschitzOnWith.ae_euclideanHausdorffMeasure_inter_preimage_eq_zero and LipschitzOnWith.ae_euclideanHausdorffMeasure_inter_preimage_lt_top: the same for μHE.

References

• H. Federer, Geometric Measure Theory, 2.10.25.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §3.4.1 (the coarea formula, preliminaries).

theorem LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → Y} {A : Set X} {t : ℝ} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) : ∃ (G : Y → ENNReal), Measurable G ∧ (∀ (y : Y), (MeasureTheory.Measure.hausdorffMeasure t) (A ∩ f ⁻¹' {y}) ≤ G y) ∧ ∫⁻ (y : Y), G y ∂μ ≤ μ (Metric.ball 0 1) * ↑K ^ Module.finrank ℝ Y * (MeasureTheory.Measure.hausdorffMeasure (↑(Module.finrank ℝ Y) + t)) A

Eilenberg's inequality, in its strong form. If f is K-Lipschitz on a set A with values in an m-dimensional real normed space with additive Haar measure μ, and t is real, then the fiber measures y ↦ μH[t] (A ∩ f ⁻¹' {y}) have a measurable majorant whose integral is at most μ (ball 0 1) * K ^ m * μH[m + t] A. In other words, the upper integral of the fiber measures obeys this bound. Neither A nor the fibers need be measurable.

theorem LipschitzOnWith.lintegral_hausdorffMeasure_inter_preimage_le {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → Y} {A : Set X} {t : ℝ} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) : ∫⁻ (y : Y), (MeasureTheory.Measure.hausdorffMeasure t) (A ∩ f ⁻¹' {y}) ∂μ ≤ μ (Metric.ball 0 1) * ↑K ^ Module.finrank ℝ Y * (MeasureTheory.Measure.hausdorffMeasure (↑(Module.finrank ℝ Y) + t)) A

Eilenberg's inequality, integral form: for f K-Lipschitz on A with values in an m-dimensional real normed space with additive Haar measure μ, and t real, ∫⁻ y, μH[t] (A ∩ f ⁻¹' {y}) ∂μ ≤ μ (ball 0 1) * K ^ m * μH[m + t] A.

The fiber-measure function y ↦ μH[t] (A ∩ f ⁻¹' {y}) need not be measurable, and for a non-measurable integrand ∫⁻ is the lower Lebesgue integral (the supremum of the integrals of the measurable functions below it). So this bounds the lower integral of the fiber measures. The upper-integral form is LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le: a measurable G dominating the fiber measures with ∫⁻ y, G y ∂μ ≤ μ (ball 0 1) * K ^ m * μH[m + t] A.

theorem LipschitzOnWith.ae_hausdorffMeasure_inter_preimage_eq_zero {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → Y} {A : Set X} {t : ℝ} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) (hA : (MeasureTheory.Measure.hausdorffMeasure (↑(Module.finrank ℝ Y) + t)) A = 0) : ∀ᵐ (y : Y) ∂μ, (MeasureTheory.Measure.hausdorffMeasure t) (A ∩ f ⁻¹' {y}) = 0

If f is Lipschitz on A with values in an m-dimensional real normed space and μH[m + t] A = 0, then for almost every y the fiber A ∩ f ⁻¹' {y} is μH[t]-null.

theorem LipschitzOnWith.ae_hausdorffMeasure_inter_preimage_lt_top {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → Y} {A : Set X} {t : ℝ} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) (hA : (MeasureTheory.Measure.hausdorffMeasure (↑(Module.finrank ℝ Y) + t)) A ≠ ⊤) : ∀ᵐ (y : Y) ∂μ, (MeasureTheory.Measure.hausdorffMeasure t) (A ∩ f ⁻¹' {y}) < ⊤

If f is Lipschitz on A with values in an m-dimensional real normed space and μH[m + t] A < ∞, then for almost every y the fiber A ∩ f ⁻¹' {y} has finite μH[t] measure.

theorem LipschitzOnWith.ae_euclideanHausdorffMeasure_inter_preimage_eq_zero {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → Y} {A : Set X} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) {k : ℕ} (hA : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ Y + k)) A = 0) : ∀ᵐ (y : Y) ∂μ, (MeasureTheory.Measure.euclideanHausdorffMeasure k) (A ∩ f ⁻¹' {y}) = 0

If f is Lipschitz on A with values in an m-dimensional real normed space and μHE[m + k] A = 0, then for almost every y the fiber A ∩ f ⁻¹' {y} is μHE[k]-null.

theorem LipschitzOnWith.ae_euclideanHausdorffMeasure_inter_preimage_lt_top {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal} {f : X → Y} {A : Set X} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) {k : ℕ} (hA : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ Y + k)) A ≠ ⊤) : ∀ᵐ (y : Y) ∂μ, (MeasureTheory.Measure.euclideanHausdorffMeasure k) (A ∩ f ⁻¹' {y}) < ⊤

If f is Lipschitz on A with values in an m-dimensional real normed space and μHE[m + k] A < ∞, then for almost every y the fiber A ∩ f ⁻¹' {y} has finite μHE[k] measure.