feat: Add OrthonormalBasis.measurePreserving_measurableEquiv (#8427)

Let `F` be a finite-dimensional inner product space. Then any orthonormal basis of `F` defines a measurable equivalence between `F` and the euclidean space of the same dimension that is volume preserving.

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -78,6 +78,25 @@ theorem OrthonormalBasis.addHaar_eq_volume {ι F : Type*} [Fintype ι] [NormedAd
   rw [Basis.addHaar_eq_iff]
   exact b.volume_parallelepiped
 
+/-- An orthonormal basis of a finite-dimensional inner product space defines a measurable
+equivalence between the space and the Euclidean space of the same dimension. -/
+noncomputable def OrthonormalBasis.measurableEquiv (b : OrthonormalBasis ι ℝ F) :
+    F ≃ᵐ EuclideanSpace ℝ ι := b.repr.toHomeomorph.toMeasurableEquiv
+
+/-- The measurable equivalence defined by an orthonormal basis is volume preserving. -/
+theorem OrthonormalBasis.measurePreserving_measurableEquiv (b : OrthonormalBasis ι ℝ F) :
+    MeasurePreserving b.measurableEquiv volume volume := by
+  convert (b.measurableEquiv.symm.measurable.measurePreserving _).symm
+  rw [← (EuclideanSpace.basisFun ι ℝ).addHaar_eq_volume]
+  erw [MeasurableEquiv.coe_toEquiv_symm, Basis.map_addHaar _ b.repr.symm.toContinuousLinearEquiv]
+  exact b.addHaar_eq_volume.symm
+
+theorem OrthonormalBasis.measurePreserving_repr (b : OrthonormalBasis ι ℝ F) :
+    MeasurePreserving b.repr volume volume := b.measurePreserving_measurableEquiv
+
+theorem OrthonormalBasis.measurePreserving_repr_symm (b : OrthonormalBasis ι ℝ F) :
+    MeasurePreserving b.repr.symm volume volume := b.measurePreserving_measurableEquiv.symm
+
 section PiLp
 
 variable (ι : Type*) [Fintype ι]