feat(Geometry/Euclidean): volume of a simplex and extra

Mathlib.lean

@@ -4410,7 +4410,10 @@ public import Mathlib.Geometry.Euclidean.Sphere.Ptolemy
 public import Mathlib.Geometry.Euclidean.Sphere.SecondInter
 public import Mathlib.Geometry.Euclidean.Sphere.Tangent
 public import Mathlib.Geometry.Euclidean.Triangle
+public import Mathlib.Geometry.Euclidean.Volume.Basic
+public import Mathlib.Geometry.Euclidean.Volume.Def
 public import Mathlib.Geometry.Euclidean.Volume.Measure
+public import Mathlib.Geometry.Euclidean.Volume.MeasureSimplex
 public import Mathlib.Geometry.Group.Growth.LinearLowerBound
 public import Mathlib.Geometry.Group.Growth.QuotientInter
 public import Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
@@ -4700,6 +4703,7 @@ public import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
 public import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
 public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
 public import Mathlib.LinearAlgebra.AffineSpace.Basis
 public import Mathlib.LinearAlgebra.AffineSpace.Centroid
 public import Mathlib.LinearAlgebra.AffineSpace.Ceva

Mathlib/Geometry/Euclidean/Volume/Def.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Weiyi Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Weiyi Wang
+-/
+module
+
+public import Mathlib.Geometry.Euclidean.Altitude
+
+/-!
+# Volume of a simplex
+
+This file defines the volume of a simplex as `Affine.Simplex.volume`. It is kept thin and
+all lemmas are put to `Mathlib.Geometry.Euclidean.Volume.Simplex.Measure` (for connection to volume
+measure) and `Mathlib.Geometry.Euclidean.Volume.Simplex.Basic` (for lemmas outside of measure
+theory)
+-/
+
+@[expose] public section
+
+variable {V P : Type*}
+variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
+
+/-- The volume of a `n`-dimensional simplex, internally defined using base-and-height formula
+from the 0-th vertex.
+
+See also:
+* `Affine.Simplex.volume_eq_euclideanHausdorffMeasure_real_closedInterior` for connection between
+  the defintion and the volume measure.
+* `Affine.Simplex.volume_eq` for base-and-height formula from any vertex. -/
+noncomputable
+def Affine.Simplex.volume {n : ℕ} (s : Simplex ℝ P n) : ℝ := match n with
+| 0 => 1
+| n + 1 => (↑(n + 1))⁻¹ * s.height 0 * (s.faceOpposite 0).volume

Mathlib/Geometry/Euclidean/Volume/Measure.lean

@@ -9,6 +9,7 @@ public import Mathlib.MeasureTheory.Measure.Haar.Unique
 public import Mathlib.MeasureTheory.Measure.Hausdorff
 public import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
+import Mathlib.MeasureTheory.Constructions.Polish.Basic
 
 /-!
 # Volume measure for Euclidean geometry
@@ -44,7 +45,7 @@ TODO: show the scaling factor equals to the ratio between the volume of `d`-dime
 Hausdorff measure, measure, metric measure, volume, area
 -/
 
-open MeasureTheory Measure
+open MeasureTheory Measure Module
 
 public section
 
@@ -178,7 +179,7 @@ theorem MeasureTheory.euclideanHausdorffMeasure_homothety_preimage (d : ℕ) (x
 
 end Homothety
 
-variable {V P : Type*}
+variable {V P Q : Type*}
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
 variable [FiniteDimensional ℝ V]
 variable [MetricSpace P] [MeasurableSpace P] [BorelSpace P] [NormedAddTorsor V P]
@@ -192,7 +193,7 @@ theorem EuclideanSpace.euclideanHausdorffMeasure_eq_volume (d : ℕ) :
   rw [euclideanHausdorffMeasure_def, ← isAddLeftInvariant_eq_smul]
 
 theorem InnerProductSpace.euclideanHausdorffMeasure_eq_volume :
-    (μHE[Module.finrank ℝ V] : Measure V) = volume := by
+    (μHE[finrank ℝ V] : Measure V) = volume := by
   rw [← (stdOrthonormalBasis ℝ V).measurePreserving_repr_symm.map_eq,
     ← (stdOrthonormalBasis ℝ V).repr.toIsometryEquiv
       |>.symm.measurePreserving_euclideanHausdorffMeasure _ |>.map_eq,
@@ -206,14 +207,14 @@ theorem InnerProductSpace.euclideanHausdorffMeasure_eq_volume :
 associated inner product space. If it is implemented, we can unify this lemma with the previous one.
 -/
 theorem EuclideanGeometry.euclideanHausdorffMeasure_eq (p : P) :
-    μHE[Module.finrank ℝ V] = volume.map (IsometryEquiv.vaddConst p) := by
+    μHE[finrank ℝ V] = volume.map (IsometryEquiv.vaddConst p) := by
   have h := (IsometryEquiv.vaddConst p)
-    |>.measurePreserving_euclideanHausdorffMeasure (Module.finrank ℝ V) |>.map_eq
+    |>.measurePreserving_euclideanHausdorffMeasure (finrank ℝ V) |>.map_eq
   rw [InnerProductSpace.euclideanHausdorffMeasure_eq_volume] at h
   exact h.symm
 
 theorem EuclideanGeometry.measurePreserving_vaddConst (p : P) :
-    MeasurePreserving (IsometryEquiv.vaddConst p) volume μHE[Module.finrank ℝ V] where
+    MeasurePreserving (IsometryEquiv.vaddConst p) volume μHE[finrank ℝ V] where
   measurable := (IsometryEquiv.vaddConst p).toHomeomorph.measurable
   map_eq := (euclideanHausdorffMeasure_eq p).symm
 
@@ -244,3 +245,128 @@ instance [AddGroup X] [IsIsometricVAdd Xᵃᵒᵖ X] (d : ℕ) :
     (μHE[d] : Measure X).IsAddRightInvariant := by
   rw [euclideanHausdorffMeasure_def]
   infer_instance
+
+/-!
+### Integration formula for `μHE[d]`
+-/
+
+set_option backward.isDefEq.respectTransparency false in
+/-- 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.
+-/
+noncomputable def Submodule.measurableEquivProd (s : Submodule ℝ V) (p : P) : P ≃ᵐ s × sᗮ :=
+  (IsometryEquiv.vaddConst p).toHomeomorph.toMeasurableEquiv.symm.trans <|
+  s.orthogonalDecomposition.toHomeomorph.toMeasurableEquiv.trans <|
+  (MeasurableEquiv.toLp 2 _).symm
+
+@[simp]
+theorem Submodule.measurableEquivProd_apply (s : Submodule ℝ V) (p q : P) :
+    s.measurableEquivProd p q =
+    (s.orthogonalProjection (q -ᵥ p), sᗮ.orthogonalProjection (q -ᵥ p)) := by
+  simp [measurableEquivProd]
+
+@[simp]
+theorem Submodule.measurableEquivProd_symm_apply (s : Submodule ℝ V) (p : P) (q : s × sᗮ) :
+    (s.measurableEquivProd p).symm q = (q.1.val + q.2.val) +ᵥ p := by
+  simp [measurableEquivProd]
+
+set_option backward.isDefEq.respectTransparency false in
+theorem Submodule.measurePreserving_measurableEquivProd (s : Submodule ℝ V) (p : P) :
+    MeasurePreserving (s.measurableEquivProd p) μHE[finrank ℝ V] := by
+  refine (EuclideanGeometry.measurePreserving_vaddConst _).symm.trans ?_
+  refine (s.orthogonalDecomposition.measurePreserving).trans ?_
+  exact WithLp.volume_preserving_ofLp _ _
+
+set_option backward.isDefEq.respectTransparency false in
+/-- 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 a generalization of `MeasureTheory.Measure.prod_apply` in the affine Euclidean space. -/
+theorem AffineSubspace.euclideanHausdorffMeasure_eq_lintegral (s : AffineSubspace ℝ P)
+    [hs : Nonempty s] {t : Set P} (ht : MeasurableSet t) :
+    μHE[finrank ℝ V] t = ∫⁻ (x : s), μHE[finrank ℝ s.directionᗮ] (t ∩ mk' x.val s.directionᗮ)
+      ∂μHE[finrank ℝ s.direction] := by
+  obtain p := hs.some
+  rw [← (s.direction.measurePreserving_measurableEquivProd p.val).symm.measure_preimage_equiv,
+    volume_eq_prod, prod_apply (by simpa using ht),
+    EuclideanGeometry.euclideanHausdorffMeasure_eq p, MeasurableEmbedding.lintegral_map
+    (by simpa using (IsometryEquiv.vaddConst p).toHomeomorph.measurableEmbedding)]
+  congr
+  ext x
+  let u : Set (mk' (x +ᵥ p).val s.directionᗮ) := Subtype.val ⁻¹' (t ∩ mk' (x +ᵥ p).val s.directionᗮ)
+  have hu : MeasurableSet u :=
+    .preimage (ht.inter (closed_of_finiteDimensional _).measurableSet) measurable_subtype_coe
+  have hinter : t ∩ (mk' (x +ᵥ p).val s.directionᗮ) = Subtype.val '' u := by
+    ext x
+    simp [u]
+  have hxp: (x +ᵥ p).val ∈ mk' (x +ᵥ p).val s.directionᗮ := by simp
+  have hrank : finrank ℝ s.directionᗮ = finrank ℝ (mk' (x +ᵥ p).val s.directionᗮ).direction := by
+    rw [direction_mk']
+  rw [IsometryEquiv.vaddConst_apply, hinter, euclideanHausdorffMeasure_coe_image, hrank,
+    EuclideanGeometry.euclideanHausdorffMeasure_eq ⟨x +ᵥ p, hxp⟩,
+    map_apply (by simpa using (IsometryEquiv.vaddConst _).toHomeomorph.measurable) hu]
+  /- we have ⊢ volume (a : Set A) = volume (b : Set B). We'd like show a = b, but A and B are
+    non-defeq subspaces!
+    Lucky we have just developed euclideanHausdorffMeasure, which allows us to move the measure to
+    the global vector space. -/
+  simp_rw [← InnerProductSpace.euclideanHausdorffMeasure_eq_volume]
+  conv_lhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
+  conv_rhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
+  congrm μHE[$hrank] ?_
+  ext y
+  simp [u, vadd_vadd, add_comm]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- 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. -/
+theorem EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral (p : P) {v : V} (hv : v ≠ 0)
+    {t : Set P} (ht : MeasurableSet t) :
+    μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ (ℝ ∙ v)ᗮ]
+      (t ∩ AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ) := by
+  have hrank : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction = 1 := by
+    rw [AffineSubspace.direction_mk']
+    apply finrank_span_singleton hv
+  have hrank' : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ (ℝ ∙ v)ᗮ := by
+    rw [AffineSubspace.direction_mk']
+  let f : ℝ ≃L[ℝ] (AffineSubspace.mk' p (ℝ ∙ v)).direction :=
+    (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
+    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) ((AffineSubspace.mk' p (ℝ ∙ v)).direction) (by simp))
+  have hf : MeasurableEmbedding f := f.toHomeomorph.measurableEmbedding
+  let p' : AffineSubspace.mk' p (ℝ ∙ v) := ⟨p, by simp [AffineSubspace.mem_mk']⟩
+  let g : ℝ → AffineSubspace.mk' p (ℝ ∙ v) := IsometryEquiv.vaddConst p' ∘ f
+  have hadd : MeasurableEmbedding (IsometryEquiv.vaddConst p') :=
+    (IsometryEquiv.vaddConst p').toHomeomorph.measurableEmbedding
+  have hg : MeasurableEmbedding g := hadd.comp hf
+  have hm : (μHE[finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction] :
+      Measure (AffineSubspace.mk' p (ℝ ∙ v))) = ‖v‖ₑ • (volume : Measure ℝ).map g := by
+    unfold g
+    rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
+      ← Measure.map_smul]
+    congr
+    let v' : (AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, by simp⟩
+    suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']
+    exact volume_eq_of_finrank_eq_one hrank (by simpa [v'] using hv)
+  have hx (x : ℝ) : x • v +ᵥ p = g x := by rfl
+  simp_rw [(AffineSubspace.mk' p (ℝ ∙ v)).euclideanHausdorffMeasure_eq_lintegral ht, hx, hm,
+    lintegral_smul_measure, hg.lintegral_map, smul_eq_mul, hrank', AffineSubspace.direction_mk']
+
+/-
+
+
+variable [MetricSpace Q] [MeasurableSpace Q] [BorelSpace Q] [NormedAddTorsor V Q]
+
+
+
+theorem EuclideanGeometry.map_affineMap_euclideanHausdorffMeasure [FiniteDimensional ℝ V]
+    {f : P →ᵃ[ℝ] Q} (hf : f.linear.det ≠ 0) :
+    (μHE[finrank ℝ V] : Measure P).map f =
+    ENNReal.ofReal |f.linear.det⁻¹| • (μHE[finrank ℝ V] : Measure Q) := by
+
+  sorry
+
+-/