feat(Geometry/Euclidean): the Euclidean volume measure

[wwylele]

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 feat(Geometry/Euclidean): volume of a simplex #34826 for the target lemma)
• More specialized formula for the area of triangles.

---

Zulip thread: #Is there code for X? > Measure on affine space

[github-actions]

PR summary ab89ddb3be

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Euclidean.Volume.Measure (new file)	2392

---

Declarations diff

+ AffineSubspace.euclideanHausdorffMeasure_coe_image
+ EuclideanGeometry.euclideanHausdorffMeasure_eq
+ EuclideanGeometry.measurePreserving_vaddConst
+ EuclideanSpace.euclideanHausdorffMeasure_eq_volume
+ InnerProductSpace.euclideanHausdorffMeasure_eq_volume
+ Isometry.euclideanHausdorffMeasure_image
+ Isometry.euclideanHausdorffMeasure_preimage
+ Isometry.map_euclideanHausdorffMeasure
+ IsometryEquiv.measurePreserving_euclideanHausdorffMeasure
+ MeasureTheory.Measure.euclideanHausdorffMeasure
+ MeasureTheory.Measure.euclideanHausdorffMeasure_def
+ MeasureTheory.Measure.euclideanHausdorffMeasure_smul₀
+ instance (d : ℕ) : (μH[d] : Measure (EuclideanSpace ℝ (Fin d))).IsAddHaarMeasure := by

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[Copilot]

Pull request overview

This PR introduces the Euclidean volume measure for Euclidean geometry, enabling formalization of problems involving area and volume. The measure is defined as a scaled Hausdorff measure that coincides with Lebesgue measure in appropriate dimensions and is preserved through isometries and affine subspace inclusions.

Changes:

• Introduces euclideanHausdorffMeasure (notation μHE[d]) as a d-dimensional measure for n-dimensional Euclidean affine spaces
• Proves preservation properties through isometries and equivalence with volume measures on inner product spaces
• Establishes the measure's behavior on affine subspaces

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File	Description
Mathlib/Geometry/Euclidean/Volume/Measure.lean	New file defining the Euclidean Hausdorff measure with proofs of its key properties
Mathlib.lean	Adds public import for the new measure module

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[wwylele]

About @mathlib-triage, I think @jsm28 said they'd like someone familiar with measure theory to review this instead.

@eric-wieser Got a chance for another review?