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

μ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

μ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