feat: Prove that the measure equivalence between EuclideanSpace ℝ ι a…

…nd ι → ℝ is volume preserving (#7037) We prove that the two `MeasureSpace` structures on $\mathbb{R}^\iota$, the one coming from its identification with `ι→ ℝ` and the one coming from `EuclideanSpace ℝ ι`, agree in the sense that the measure equivalence between the two corresponding volumes is measure preserving. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Sep 22, 2023 · 83fe8e7 · 83fe8e7
1 parent b1c3ef6
commit 83fe8e7
Show file tree

Hide file tree

Showing 3 changed files with 63 additions and 4 deletions.
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -334,10 +334,6 @@ variable {ι 𝕜 E}
 
 namespace OrthonormalBasis
 
-instance instInhabited : Inhabited (OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)) :=
-  ⟨ofRepr (LinearIsometryEquiv.refl 𝕜 (EuclideanSpace 𝕜 ι))⟩
-#align orthonormal_basis.inhabited OrthonormalBasis.instInhabited
-
 theorem repr_injective :
     Injective (repr : OrthonormalBasis ι 𝕜 E → E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) := fun f g h => by
   cases f
@@ -612,6 +608,31 @@ protected theorem repr_reindex (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι')
 
 end OrthonormalBasis
 
+namespace EuclideanSpace
+
+variable (𝕜 ι)
+
+/-- The basis `Pi.basisFun`, bundled as an orthornormal basis of `EuclideanSpace 𝕜 ι`. -/
+noncomputable def basisFun : OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι) :=
+  ⟨LinearIsometryEquiv.refl _ _⟩
+
+@[simp]
+theorem basisFun_apply [DecidableEq ι] (i : ι) : basisFun ι 𝕜 i = EuclideanSpace.single i 1 :=
+  PiLp.basisFun_apply _ _ _ _
+
+@[simp]
+theorem basisFun_repr (x : EuclideanSpace 𝕜 ι) (i : ι) : (basisFun ι 𝕜).repr x i = x i := rfl
+
+theorem basisFun_toBasis : (basisFun ι 𝕜).toBasis = PiLp.basisFun _ 𝕜 ι := rfl
+
+end EuclideanSpace
+
+instance OrthonormalBasis.instInhabited : Inhabited (OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)) :=
+  ⟨EuclideanSpace.basisFun ι 𝕜⟩
+#align orthonormal_basis.inhabited OrthonormalBasis.instInhabited
+
+section Complex
+
 /-- `![1, I]` is an orthonormal basis for `ℂ` considered as a real inner product space. -/
 def Complex.orthonormalBasisOneI : OrthonormalBasis (Fin 2) ℝ ℂ :=
   Complex.basisOneI.toOrthonormalBasis
@@ -671,6 +692,8 @@ theorem Complex.isometryOfOrthonormal_apply (v : OrthonormalBasis (Fin 2) ℝ F)
   simp [← v.sum_repr_symm]
 #align complex.isometry_of_orthonormal_apply Complex.isometryOfOrthonormal_apply
 
+end Complex
+
 open FiniteDimensional
 
 /-! ### Matrix representation of an orthonormal basis with respect to another -/

diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
@@ -67,3 +67,36 @@ theorem OrthonormalBasis.volume_parallelepiped (b : OrthonormalBasis ι ℝ F) :
   rw [← o.measure_eq_volume]
   exact o.measure_orthonormalBasis b
 #align orthonormal_basis.volume_parallelepiped OrthonormalBasis.volume_parallelepiped
+
+/-- The Haar measure defined by any orthonormal basis of a finite-dimensional inner product space
+is equal to its volume measure. -/
+theorem OrthonormalBasis.addHaar_eq_volume {ι F : Type*} [Fintype ι] [NormedAddCommGroup F]
+    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
+    (b : OrthonormalBasis ι ℝ F) :
+    b.toBasis.addHaar = volume := by
+  rw [Basis.addHaar_eq_iff]
+  exact b.volume_parallelepiped
+
+section PiLp
+variable (ι : Type*) [Fintype ι]
+
+/-- The measure equivalence between `EuclideanSpace ℝ ι` and `ι → ℝ` is volume preserving. -/
+theorem EuclideanSpace.volume_preserving_measurableEquiv :
+    MeasurePreserving (EuclideanSpace.measurableEquiv ι) := by
+  suffices volume = map (EuclideanSpace.measurableEquiv ι).symm volume by
+    convert ((EuclideanSpace.measurableEquiv ι).symm.measurable.measurePreserving _).symm
+  rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def,
+    coe_measurableEquiv_symm, ← PiLp.continuousLinearEquiv_symm_apply 2 ℝ, Basis.map_addHaar]
+  exact (EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm
+
+/-- A copy of `EuclideanSpace.volume_preserving_measurableEquiv` for the canonical spelling of the
+equivalence. -/
+theorem PiLp.volume_preserving_equiv : MeasurePreserving (WithLp.equiv 2 (ι → ℝ)) :=
+  EuclideanSpace.volume_preserving_measurableEquiv ι
+
+/-- The reverse direction of `PiLp.volume_preserving_measurableEquiv`, since
+`MeasurePreserving.symm` only works for `MeasurableEquiv`s. -/
+theorem PiLp.volume_preserving_equiv_symm : MeasurePreserving (WithLp.equiv 2 (ι → ℝ)).symm :=
+  (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
+
+end PiLp
diff --git a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
@@ -294,4 +294,7 @@ protected def measurableEquiv : EuclideanSpace ℝ ι ≃ᵐ (ι → ℝ) where
 theorem coe_measurableEquiv : ⇑(EuclideanSpace.measurableEquiv ι) = WithLp.equiv 2 _ := rfl
 #align euclidean_space.coe_measurable_equiv EuclideanSpace.coe_measurableEquiv
 
+theorem coe_measurableEquiv_symm :
+    ⇑(EuclideanSpace.measurableEquiv ι).symm = (WithLp.equiv 2 _).symm := rfl
+
 end EuclideanSpace