[Merged by Bors] - feat: Prove that the measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving

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,29 @@ protected theorem repr_reindex (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι')
 
 end OrthonormalBasis
 
+namespace EuclideanSpace
+
+variable (𝕜 ι)
+
+/-- The basis `Pi.basisFun` bundled as an orthormal basis of `EuclideanSpace 𝕜 ι`. -/
+noncomputable def basisFun :
+    OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι) := ⟨LinearIsometryEquiv.refl _ _⟩
+
+theorem basisFun_repr (x : EuclideanSpace 𝕜 ι) (i : ι) :
+    (basisFun ι 𝕜).repr x i = x i := rfl
+
+theorem basisFun_toBasis :
+    (basisFun ι 𝕜).toBasis =
+      (Pi.basisFun 𝕜 ι).map (EuclideanSpace.equiv ι 𝕜).toLinearEquiv.symm := rfl
+
+instance _root_.OrthonormalBasis.instInhabited :
+    Inhabited (OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)) := ⟨basisFun ι 𝕜⟩
+#align orthonormal_basis.inhabited OrthonormalBasis.instInhabited
+
+end EuclideanSpace
+
+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 +690,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 -/

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -67,3 +67,28 @@ 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 EuclideanSpace
+
+open EuclideanSpace
+
+/-- The measure equivalence between `EuclideanSpace ℝ ι` and `ι → ℝ` is volume preserving. -/
+theorem EuclideanSpace.volume_preserving_measurableEquiv (ι : Type*) [Fintype ι] :
+    MeasurePreserving (EuclideanSpace.measurableEquiv ι) := by
+  classical
+  convert ((EuclideanSpace.measurableEquiv ι).symm.measurable.measurePreserving _).symm
+  rw [eq_comm, ← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def,
+    coe_continuousLinearEquiv_symm, Basis.map_addHaar, Basis.addHaar_eq_iff,
+    ContinuousLinearEquiv.symm_toLinearEquiv, ← EuclideanSpace.basisFun_toBasis ι ℝ]
+  exact OrthonormalBasis.volume_parallelepiped (EuclideanSpace.basisFun _ _)
+
+end EuclideanSpace

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

@@ -293,4 +293,13 @@ 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
+
+theorem coe_continuousLinearEquiv :
+    ⇑(EuclideanSpace.measurableEquiv ι) = (EuclideanSpace.equiv ι ℝ) := rfl
+
+theorem coe_continuousLinearEquiv_symm :
+    ⇑(EuclideanSpace.measurableEquiv ι).symm = (EuclideanSpace.equiv ι ℝ).symm := rfl
+
 end EuclideanSpace