Commit 2026-03-10 05:41 9d092b11

View on Github →

feat(Geometry/Euclidean): the Euclidean volume measure (#34697) This PR starts a series to set up volume measure for Euclidean geometry, so it can be used in formalizing problems involving area and volume. This PR only introduce the basic definition and properties. Some future PR will also include

Integral along an affine subspace to calculate the volume of an object
Define volume of a simplex using the base * height / n formula (not assuming measurability)
Show that the defined volume matches the measure of the interior (see the draft #34826 for the target lemma)
More specialized formula for the area of triangles.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Volume/Measure.lean

added theorem AffineSubspace.euclideanHausdorffMeasure_coe_image

added theorem EuclideanGeometry.euclideanHausdorffMeasure_eq

added theorem EuclideanGeometry.measurePreserving_vaddConst

added theorem EuclideanSpace.euclideanHausdorffMeasure_eq_volume

added theorem InnerProductSpace.euclideanHausdorffMeasure_eq_volume

added theorem Isometry.euclideanHausdorffMeasure_image

added theorem Isometry.euclideanHausdorffMeasure_preimage

added theorem Isometry.map_euclideanHausdorffMeasure

added theorem IsometryEquiv.measurePreserving_euclideanHausdorffMeasure

added def MeasureTheory.Measure.euclideanHausdorffMeasure

added theorem MeasureTheory.Measure.euclideanHausdorffMeasure_def

added theorem MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean