feat: the volume in a MeasureSpace over an empty index is the Dirac m…

…ass (#8799)
leanprover-community · Dec 24, 2023 · 640097f · 640097f
1 parent 86393c8
commit 640097f
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -421,6 +421,11 @@ theorem pi_of_empty {α : Type*} [Fintype α] [IsEmpty α] {β : α → Type*}
   exact isEmptyElim (α := α)
 #align measure_theory.measure.pi_of_empty MeasureTheory.Measure.pi_of_empty
 
+lemma volume_pi_eq_dirac {ι : Type*} [Fintype ι] [IsEmpty ι]
+    {α : ι → Type*} [∀ i, MeasureSpace (α i)] (x : ∀ a, α a := isEmptyElim) :
+    (volume : Measure (∀ i, α i)) = Measure.dirac x :=
+  Measure.pi_of_empty _ _
+
 @[simp]
 theorem pi_empty_univ {α : Type*} [Fintype α] [IsEmpty α] {β : α → Type*}
     {m : ∀ α, MeasurableSpace (β α)} (μ : ∀ a : α, Measure (β a)) :

diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
@@ -120,4 +120,12 @@ theorem PiLp.volume_preserving_equiv : MeasurePreserving (WithLp.equiv 2 (ι →
 theorem PiLp.volume_preserving_equiv_symm : MeasurePreserving (WithLp.equiv 2 (ι → ℝ)).symm :=
   (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
 
+lemma volume_euclideanSpace_eq_dirac [IsEmpty ι] :
+    (volume : Measure (EuclideanSpace ℝ ι)) = Measure.dirac 0 := by
+  ext s hs
+  simp only [← ((EuclideanSpace.volume_preserving_measurableEquiv ι).symm).measure_preimage hs,
+    volume_pi_eq_dirac 0, MeasurableEquiv.measurableSet_preimage, hs, dirac_apply', indicator,
+    mem_preimage, Pi.one_apply]
+  rfl
+
 end PiLp