refactor: golf proof using lmarginal (#10857)

Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com)

Mathlib/Data/Matrix/Basis.lean

@@ -56,6 +56,14 @@ theorem stdBasisMatrix_add (i : m) (j : n) (a b : α) :
   split_ifs with h <;> simp [h]
 #align matrix.std_basis_matrix_add Matrix.stdBasisMatrix_add
 
+theorem mulVec_stdBasisMatrix [Fintype m] (i : n) (j : m) (c : α) (x : m → α) :
+    mulVec (stdBasisMatrix i j c) x = Function.update (0 : n → α) i (c * x j) := by
+  ext i'
+  simp [stdBasisMatrix, mulVec, dotProduct]
+  rcases eq_or_ne i i' with rfl|h
+  · simp
+  simp [h, h.symm]
+
 theorem matrix_eq_sum_std_basis [Fintype m] [Fintype n] (x : Matrix m n α) :
     x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j) := by
   ext i j; symm

Mathlib/MeasureTheory/Group/LIntegral.lean

@@ -12,7 +12,7 @@ We develop properties of integrals with a group as domain.
 This file contains properties about Lebesgue integration.
 -/
 
--- assert_not_exists NormedSpace -- this doesn't work after #6225, but will hopefully work soon
+assert_not_exists NormedSpace
 
 namespace MeasureTheory
 

Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

@@ -7,7 +7,8 @@ import Mathlib.Dynamics.Ergodic.MeasurePreserving
 import Mathlib.LinearAlgebra.Determinant
 import Mathlib.LinearAlgebra.Matrix.Diagonal
 import Mathlib.LinearAlgebra.Matrix.Transvection
-import Mathlib.MeasureTheory.Constructions.Pi
+import Mathlib.MeasureTheory.Group.LIntegral
+import Mathlib.MeasureTheory.Integral.Marginal
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 
@@ -377,44 +378,23 @@ theorem smul_map_diagonal_volume_pi [DecidableEq ι] {D : ι → ℝ} (h : det (
 /-- A transvection preserves Lebesgue measure. -/
 theorem volume_preserving_transvectionStruct [DecidableEq ι] (t : TransvectionStruct ι ℝ) :
     MeasurePreserving (toLin' t.toMatrix) := by
-  /- We separate the coordinate along which there is a shearing from the other ones, and apply
-    Fubini. Along this coordinate (and when all the other coordinates are fixed), it acts like a
+  /- We use `lmarginal` to conveniently use Fubini's theorem.
+    Along the coordinate where there is a shearing, it acts like a
     translation, and therefore preserves Lebesgue. -/
-  let p : ι → Prop := fun i => i ≠ t.i
-  let α : Type _ := { x // p x }
-  let β : Type _ := { x // ¬p x }
-  let g : (α → ℝ) → (β → ℝ) → β → ℝ := fun a b => (fun _ => t.c * a ⟨t.j, t.hij.symm⟩) + b
-  let F : (α → ℝ) × (β → ℝ) → (α → ℝ) × (β → ℝ) := fun p => (id p.1, g p.1 p.2)
-  let e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun _ : ι => ℝ) p
-  have : (toLin' t.toMatrix : (ι → ℝ) → ι → ℝ) = e.symm ∘ F ∘ e := by
-    cases t with | mk t_i t_j t_hij t_c =>
-    ext f k
-    simp only [e, g, p, LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not,
-      Algebra.id.smul_eq_mul, one_mul, dotProduct, stdBasisMatrix,
-      MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply,
-      zero_mul, LinearMap.smul_apply, Function.comp_apply,
-      MeasurableEquiv.piEquivPiSubtypeProd_apply, Matrix.TransvectionStruct.toMatrix_mk,
-      Matrix.mulVec, LinearEquiv.map_add, ite_mul, Matrix.toLin'_apply, Pi.smul_apply,
-      Subtype.coe_mk, LinearMap.add_apply, Finset.sum_congr, Matrix.toLin'_one]
-    by_cases h : t_i = k
-    · simp only [h, true_and_iff, Finset.mem_univ, if_true, eq_self_iff_true, Finset.sum_ite_eq,
-        one_apply, boole_mul, add_comm]
-    · simp only [h, Ne.symm h, add_zero, if_false, Finset.sum_const_zero, false_and_iff,
-        mul_zero]
-  rw [this]
-  have A : MeasurePreserving e := by
-    convert volume_preserving_piEquivPiSubtypeProd (fun _ : ι => ℝ) p
-  have B : MeasurePreserving F :=
-    haveI g_meas : Measurable (Function.uncurry g) := by
-      have : Measurable fun c : α → ℝ => c ⟨t.j, t.hij.symm⟩ :=
-        measurable_pi_apply ⟨t.j, t.hij.symm⟩
-      refine Measurable.add ?_ measurable_snd
-      refine measurable_pi_lambda _ fun _ => Measurable.const_mul ?_ _
-      exact this.comp measurable_fst
-    (MeasurePreserving.id _).skew_product g_meas
-      (eventually_of_forall fun a => map_add_left_eq_self
-        (Measure.pi fun _ => (stdOrthonormalBasis ℝ ℝ).toBasis.addHaar) _)
-  exact ((A.symm e).comp B).comp A
+  have ht : Measurable (toLin' t.toMatrix) :=
+    (toLin' t.toMatrix).continuous_of_finiteDimensional.measurable
+  refine ⟨ht, ?_⟩
+  refine (pi_eq fun s hs ↦ ?_).symm
+  have h2s : MeasurableSet (univ.pi s) := .pi countable_univ fun i _ ↦ hs i
+  simp_rw [← pi_pi, ← lintegral_indicator_one h2s]
+  rw [lintegral_map (measurable_one.indicator h2s) ht, volume_pi]
+  refine lintegral_eq_of_lmarginal_eq {t.i} ((measurable_one.indicator h2s).comp ht)
+    (measurable_one.indicator h2s) ?_
+  simp_rw [lmarginal_singleton]
+  ext x
+  cases t with | mk t_i t_j t_hij t_c =>
+  simp [transvection, mulVec_stdBasisMatrix, t_hij.symm, ← Function.update_add,
+    lintegral_add_right_eq_self fun xᵢ ↦ indicator (univ.pi s) 1 (Function.update x t_i xᵢ)]
 #align real.volume_preserving_transvection_struct Real.volume_preserving_transvectionStruct
 
 /-- Any invertible matrix rescales Lebesgue measure through the absolute value of its
@@ -429,8 +409,8 @@ theorem map_matrix_volume_pi_eq_smul_volume_pi [DecidableEq ι] {M : Matrix ι 
     rw [smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel hD, abs_one,
       ENNReal.ofReal_one, one_smul]
   · intro t
-    simp only [Matrix.TransvectionStruct.det, ENNReal.ofReal_one,
-      (volume_preserving_transvectionStruct _).map_eq, one_smul, _root_.inv_one, abs_one]
+    simp_rw [Matrix.TransvectionStruct.det, _root_.inv_one, abs_one, ENNReal.ofReal_one, one_smul,
+      (volume_preserving_transvectionStruct _).map_eq]
   · intro A B _ _ IHA IHB
     rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA,
       smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv]