Volume measure for Euclidean geometry

In this file we introduce a d-dimensional measure for n-dimensional Euclidean affine space, namely MeasureTheory.Measure.euclideanHausdorffMeasure d with notation μHE[d]. This is the suitable measure to describe area and volume in an environment of arbitrary dimension. It is characterized by the following properties:

• Coincides with Lebesgue measure when d = n.
• Preserved through isometry, and specifically through affine subspace inclusion.

Internally, this is defined as the MeasureTheory.Measure.hausdorffMeasure scaled by a factor. The factor is defined nonconstructively as the MeasureTheory.Measure.addHaarScalarFactor between the Hausdorff measure and the Lebesgue measure on a model Euclidean space.

TODO: show the scaling factor equals to the ratio between the volume of d-dimensional Metric.ball with Euclidean metric and with sup metric.

Main definitions

• MeasureTheory.Measure.euclideanHausdorffMeasure: the Euclidean Hausdorff measure.

Main statements

• EuclideanGeometry.measurePreserving_vaddConst: μHE[d] on an affine space matches volume on the associated inner product space.
• AffineSubspace.euclideanHausdorffMeasure_coe_image: μHE[d] is preserved through subspace inclusion.

Tags

Hausdorff measure, measure, metric measure, volume, area

instance instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast (d : ℕ) : (MeasureTheory.Measure.hausdorffMeasure ↑d).IsAddHaarMeasure

noncomputable def MeasureTheory.Measure.euclideanHausdorffMeasure {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (d : ℕ) : Measure X

Euclidean Hausdorff measure μHE[d], defined as μH[d] scaled to agree with Lebesgue measure on a d-dimensional Euclidean space. While this is defined on any (e)metric space, it is intended to be used for affine space associated with an inner product space, where it agrees with the volume measure on the inner product space.

Equations

• MeasureTheory.Measure.euclideanHausdorffMeasure d = MeasureTheory.volume.addHaarScalarFactor (MeasureTheory.Measure.hausdorffMeasure ↑d) • MeasureTheory.Measure.hausdorffMeasure ↑d

def MeasureTheory.«termμHE[_]» : Lean.ParserDescr

Euclidean Hausdorff measure μHE[d], defined as μH[d] scaled to agree with Lebesgue measure on a d-dimensional Euclidean space. While this is defined on any (e)metric space, it is intended to be used for affine space associated with an inner product space, where it agrees with the volume measure on the inner product space.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_def {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (d : ℕ) : euclideanHausdorffMeasure d = volume.addHaarScalarFactor (hausdorffMeasure ↑d) • hausdorffMeasure ↑d

@[simp]

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_zero {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] : euclideanHausdorffMeasure 0 = hausdorffMeasure 0

μHE[0] and μH[0] are equal.

theorem MeasureTheory.Measure.addHaarScalarFactor_volume_hausdorffMeasure_ne_zero (d : ℕ) : volume.addHaarScalarFactor (hausdorffMeasure ↑d) ≠ 0

The scalar that defines μHE[d] is non-zero.

instance MeasureTheory.isAddHaarMeasure_euclideanHausdorffMeasure {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).IsAddHaarMeasure

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_zero_or_top {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d₁ d₂ : ℕ} (h : d₁ < d₂) (s : Set X) : (euclideanHausdorffMeasure d₂) s = 0 ∨ (euclideanHausdorffMeasure d₁) s = ⊤

If d₁ < d₂, then for any set s we have either μHE[d₂] s = 0, or μHE[d₁] s = ∞.

μHE[d] is preserved through isometry

theorem IsometryEquiv.measurePreserving_euclideanHausdorffMeasure {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (e : X ≃ᵢ Y) (d : ℕ) : MeasureTheory.MeasurePreserving (⇑e) (MeasureTheory.Measure.euclideanHausdorffMeasure d) (MeasureTheory.Measure.euclideanHausdorffMeasure d)

theorem Isometry.euclideanHausdorffMeasure_image {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {d : ℕ} (hf : Isometry f) (s : Set X) : (MeasureTheory.Measure.euclideanHausdorffMeasure d) (f '' s) = (MeasureTheory.Measure.euclideanHausdorffMeasure d) s

theorem Isometry.euclideanHausdorffMeasure_preimage {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {d : ℕ} (hf : Isometry f) (s : Set Y) : (MeasureTheory.Measure.euclideanHausdorffMeasure d) (f ⁻¹' s) = (MeasureTheory.Measure.euclideanHausdorffMeasure d) (s ∩ Set.range f)

theorem Isometry.map_euclideanHausdorffMeasure {X : Type u_1} {Y : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [EMetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {d : ℕ} (hf : Isometry f) : MeasureTheory.Measure.map f (MeasureTheory.Measure.euclideanHausdorffMeasure d) = (MeasureTheory.Measure.euclideanHausdorffMeasure d).restrict (Set.range f)

Applying scalers to μHE[d]

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀ {𝕜 : Type u_3} {E : Type u_4} [NormedAddCommGroup E] [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [MeasurableSpace E] [BorelSpace E] (d : ℕ) {r : 𝕜} (hr : r ≠ 0) (s : Set E) : (euclideanHausdorffMeasure d) (r • s) = ‖r‖₊ ^ d • (euclideanHausdorffMeasure d) s

theorem MeasureTheory.euclideanHausdorffMeasure_homothety_image {𝕜 : Type u_3} {V : Type u_4} {P : Type u_5} [NormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [MeasurableSpace P] [MetricSpace P] [NormedAddTorsor V P] [BorelSpace P] (d : ℕ) (x : P) {c : 𝕜} (hc : c ≠ 0) (s : Set P) : (Measure.euclideanHausdorffMeasure d) (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • (Measure.euclideanHausdorffMeasure d) s

theorem MeasureTheory.euclideanHausdorffMeasure_homothety_preimage {𝕜 : Type u_3} {V : Type u_4} {P : Type u_5} [NormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [MeasurableSpace P] [MetricSpace P] [NormedAddTorsor V P] [BorelSpace P] (d : ℕ) (x : P) {c : 𝕜} (hc : c ≠ 0) (s : Set P) : (Measure.euclideanHausdorffMeasure d) (⇑(AffineMap.homothety x c) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • (Measure.euclideanHausdorffMeasure d) s

μHE[d] agree with the volume measure on inner product spaces

theorem EuclideanSpace.euclideanHausdorffMeasure_eq_volume (d : ℕ) : MeasureTheory.Measure.euclideanHausdorffMeasure d = MeasureTheory.volume

theorem InnerProductSpace.euclideanHausdorffMeasure_eq_volume {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] : MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V) = MeasureTheory.volume

μHE[d] on an affine space matches the volume measure on the associated inner product space.

theorem EuclideanGeometry.euclideanHausdorffMeasure_eq {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (p : P) : MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V) = MeasureTheory.Measure.map (⇑(IsometryEquiv.vaddConst p)) MeasureTheory.volume

theorem EuclideanGeometry.measurePreserving_vaddConst {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (p : P) : MeasureTheory.MeasurePreserving (⇑(IsometryEquiv.vaddConst p)) MeasureTheory.volume (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V))

μHE[d] is preserved through subspace inclusion

theorem AffineSubspace.euclideanHausdorffMeasure_coe_image {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (d : ℕ) (s : AffineSubspace ℝ P) (t : Set ↥s) : (MeasureTheory.Measure.euclideanHausdorffMeasure d) (Subtype.val '' t) = (MeasureTheory.Measure.euclideanHausdorffMeasure d) t

μHE[d] is translation invariant

instance instVAddInvariantMeasureEuclideanHausdorffMeasureOfIsIsometricVAdd {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {α : Type u_5} [AddGroup α] [AddAction α X] [IsIsometricVAdd α X] (d : ℕ) : MeasureTheory.VAddInvariantMeasure α X (MeasureTheory.Measure.euclideanHausdorffMeasure d)

instance instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [AddGroup X] [IsIsometricVAdd X X] (d : ℕ) : (MeasureTheory.Measure.euclideanHausdorffMeasure d).IsAddLeftInvariant

instance instIsAddRightInvariantEuclideanHausdorffMeasureOfIsIsometricVAddAddOpposite {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [AddGroup X] [IsIsometricVAdd Xᵃᵒᵖ X] (d : ℕ) : (MeasureTheory.Measure.euclideanHausdorffMeasure d).IsAddRightInvariant

Integration formula for μHE[d]

noncomputable def Submodule.measurableEquivProd {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (s : Submodule ℝ V) (p : P) : P ≃ᵐ ↥s × ↥sᗮ

A measurable equivalence between an affine space and its orthogonal decomposition by a base point and a direction. We show that this is measure preserving between μHE[finrank ℝ V] and volume at Submodule.measurePreserving_measurableEquivProd.

This is similar to Submodule.orthogonalDecomposition as a MeasurableEquiv, but as the right-hand side is not with L²-norm, this is not an isometry.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Submodule.measurableEquivProd_apply {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (s : Submodule ℝ V) (p q : P) : (s.measurableEquivProd p) q = (s.orthogonalProjection (q -ᵥ p), sᗮ.orthogonalProjection (q -ᵥ p))

@[simp]

theorem Submodule.measurableEquivProd_symm_apply {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (s : Submodule ℝ V) (p : P) (q : ↥s × ↥sᗮ) : (s.measurableEquivProd p).symm q = (↑q.1 + ↑q.2) +ᵥ p

theorem Submodule.measurePreserving_measurableEquivProd {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (s : Submodule ℝ V) (p : P) : MeasureTheory.MeasurePreserving (⇑(s.measurableEquivProd p)) (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) MeasureTheory.volume

theorem AffineSubspace.euclideanHausdorffMeasure_eq_lintegral {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) [hs : Nonempty ↥s] {t : Set P} (ht : MeasurableSet t) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) t = ∫⁻ (x : ↥s), (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ ↥s.directionᗮ)) (t ∩ ↑(mk' (↑x) s.directionᗮ)) ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ ↥s.direction)

The $n$-dimensional volume of an object in an $n$-dimensional space is equal to the integral of the volume of $(n-d)$-dimensional cross-section along an orthogonal $d$-dimensional subspace. This is an analogue to MeasureTheory.Measure.prod_apply.

theorem EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P] (p : P) {v : V} (hv : v ≠ 0) {t : Set P} (ht : MeasurableSet t) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) t = ‖v‖ₑ * ∫⁻ (x : ℝ), (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V - 1)) (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

The $n$-dimensional volume of an object in an $n$-dimensional space is equal to the integral of the volume of $(n-1)$-dimensional orthogonal cross-section along a line defined by a direction vector. This is a special case of AffineSubspace.euclideanHausdorffMeasure_eq_lintegral with a one-dimensional subspace.