feat(MeasureTheory): WithLp 2 (U × V) → U × V is measure preserving

Author: wwylele

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Analysis.InnerProductSpace.Orientation
+public import Mathlib.Analysis.InnerProductSpace.ProdL2
 public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 public import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 
@@ -180,3 +181,60 @@ theorem measurePreserving (f : E ≃ₗᵢ[ℝ] F) :
   congr
 
 end LinearIsometryEquiv
+
+section Prod
+
+variable (U V : Type*)
+variable [NormedAddCommGroup U] [InnerProductSpace ℝ U] [MeasurableSpace U] [BorelSpace U]
+variable [FiniteDimensional ℝ U]
+variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
+variable [FiniteDimensional ℝ V]
+
+-- Decompose `WithLp 2 (U × V) ≃ᵐ U × V` into a series of known measure-preserving equivalences
+private noncomputable def aux :
+    WithLp 2 (U × V) ≃ᵐ U × V :=
+  ( -- WithLp 2 (U × V) ≃ₗᵢ[ℝ] WithLp 2 (WithLp 2 (Fin .. → ℝ) × WithLp 2 (Fin .. → ℝ)
+    (LinearIsometryEquiv.withLpProdCongr 2
+      (stdOrthonormalBasis ℝ U).repr
+      (stdOrthonormalBasis ℝ V).repr).trans <|
+    -- .. ≃ₗᵢ[ℝ] WithLp 2 (Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ)
+    (PiLp.sumPiLpEquivProdLpPiLp 2 (fun _ ↦ ℝ)).symm
+  ).toMeasurableEquiv.trans <|
+  -- .. ≃ᵐ Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ
+  (MeasurableEquiv.toLp 2 _).symm.trans <|
+  -- .. ≃ᵐ Fin (finrank ℝ U) → ℝ × Fin (finrank ℝ V) → ℝ
+  (MeasurableEquiv.sumPiEquivProdPi (fun _ ↦ ℝ)).trans <|
+  -- .. ≃ᵐ U × V
+  (MeasurableEquiv.prodCongr
+    ((MeasurableEquiv.toLp 2 _).trans (stdOrthonormalBasis ℝ U).repr.symm.toMeasurableEquiv)
+    ((MeasurableEquiv.toLp 2 _).trans (stdOrthonormalBasis ℝ V).repr.symm.toMeasurableEquiv))
+
+/-- The measure equivalence between `WithLp 2 (U × V)` and `U × V` is volume preserving. -/
+theorem EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod :
+    MeasurePreserving (MeasurableEquiv.toLp 2 (U × V)).symm := by
+  suffices MeasurePreserving (aux U V) by
+    convert this
+    ext uv
+    <;> simp [aux, MeasurableEquiv.coe_sumPiEquivProdPi, LinearEquiv.prodCongr_symm,
+      MeasurableEquiv.prodCongr]
+  refine (LinearIsometryEquiv.measurePreserving _).trans ?_
+  refine (volume_preserving_symm_measurableEquiv_toLp _).trans ?_
+  refine (measurePreserving_sumPiEquivProdPi _).trans ?_
+  refine MeasurePreserving.prod ?_ ?_
+  all_goals
+  · refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_
+    exact (LinearIsometryEquiv.measurePreserving _)
+
+/-- A copy of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod`
+for the canonical spelling of the equivalence. -/
+theorem Prod.volume_preserving_ofLp :
+    MeasurePreserving (WithLp.ofLp : WithLp 2 (U × V) → U × V) :=
+  EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod U V
+
+/-- The reverse direction of `Prod.volume_preserving_ofLp`, since
+`MeasurePreserving.symm` only works for `MeasurableEquiv`s. -/
+theorem Prod.volume_preserving_toLp :
+    MeasurePreserving (WithLp.toLp 2 : U × V → WithLp 2 (U × V)) :=
+  (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp_prod U V).symm
+
+end Prod