chore: remove redundant measurable space structure on WithLp (#31190)

The `MeasurableSpace` structure over `WithLp` was introduced globally in [#26249](#26249), so the particular instances that were introduced for [NumberField.mixedEmbedding.euclidean.mixedSpace](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.html#NumberField.mixedEmbedding.euclidean.mixedSpace) and `EuclideanSpace` are no longer needed.

The measurable space structure on `WithLp` is not imported in the file where [EuclideanSpace.measurableEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Haar/OfBasis.html#EuclideanSpace.measurableEquiv) is defined, so if I want to deprecate `EuclideanSpace.measurableEquiv` I either have to add a useless import, or deprecate the instances in the file instead of removing them. Thus I did not deprecate it and just removed it.

Author: EtienneC30

Mathlib/Algebra/Module/ZLattice/Covolume.lean

@@ -168,7 +168,7 @@ theorem covolume_div_covolume_eq_relIndex' {E : Type*} [NormedAddCommGroup E]
   let f := (EuclideanSpace.equiv _ ℝ).symm.trans
     (stdOrthonormalBasis ℝ E).repr.toContinuousLinearEquiv.symm
   have hf : MeasurePreserving f := (stdOrthonormalBasis ℝ E).measurePreserving_repr_symm.comp
-    (EuclideanSpace.volume_preserving_measurableEquiv _).symm
+    (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm
   rw [← covolume_comap L₁ volume volume hf, ← covolume_comap L₂ volume volume hf,
     covolume_div_covolume_eq_relIndex _ _ (fun _ h' ↦ h h'), ZLattice.comap_toAddSubgroup,
     ZLattice.comap_toAddSubgroup, Nat.cast_inj, LinearEquiv.toAddMonoidHom_commutes,
@@ -199,7 +199,7 @@ theorem volume_image_eq_volume_div_covolume' {E : Type*} [NormedAddCommGroup E]
     ((stdOrthonormalBasis ℝ E).reindex e).repr.toContinuousLinearEquiv.symm
   have hf : MeasurePreserving f :=
     ((stdOrthonormalBasis ℝ E).reindex e).measurePreserving_repr_symm.comp
-      (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
+      (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι).symm
   rw [← hf.measure_preimage hs, ← (covolume_comap L volume volume hf),
     ← volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap)
     (b.ofZLatticeComap ℝ L f.toLinearEquiv), Basis.ofZLatticeBasis_comap,

Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

@@ -257,14 +257,13 @@ theorem integrable_cexp_neg_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re
 theorem integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace
     {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) :
     Integrable (fun (v : EuclideanSpace ℝ ι) ↦ cexp (-b * ‖v‖ ^ 2 + c * ⟪w, v⟫)) := by
-  have := EuclideanSpace.volume_preserving_measurableEquiv ι
+  have := EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι
   rw [← MeasurePreserving.integrable_comp_emb this.symm (MeasurableEquiv.measurableEmbedding _)]
   simp only [neg_mul, Function.comp_def]
   convert integrable_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 3 with v
-  simp only [EuclideanSpace.measurableEquiv, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
-    EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, PiLp.inner_apply,
-    RCLike.inner_apply, conj_trivial, ofReal_sum, ofReal_mul, Finset.mul_sum, neg_mul,
-    Finset.sum_neg_distrib, mul_assoc]
+  simp only [MeasurableEquiv.symm_symm, MeasurableEquiv.toLp_apply, EuclideanSpace.norm_eq,
+    PiLp.toLp_apply, norm_eq_abs, sq_abs, PiLp.inner_apply, RCLike.inner_apply, conj_trivial,
+    ofReal_sum, ofReal_mul, Finset.mul_sum, neg_mul, Finset.sum_neg_distrib, mul_assoc]
   norm_cast
   rw [sq_sqrt]
   · simp [Finset.mul_sum, mul_comm]
@@ -303,17 +302,17 @@ theorem integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
     {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) :
     ∫ v : EuclideanSpace ℝ ι, cexp (-b * ‖v‖ ^ 2 + c * ⟪w, v⟫) =
       (π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp (c ^ 2 * ‖w‖ ^ 2 / (4 * b)) := by
-  have := (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
+  have := (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι).symm
   rw [← this.integral_comp (MeasurableEquiv.measurableEmbedding _)]
   simp only [neg_mul]
   convert integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y
-  · simp only [EuclideanSpace.coe_measurableEquiv_symm, EuclideanSpace.norm_eq, PiLp.toLp_apply,
-      Real.norm_eq_abs, sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]
+  · simp only [MeasurableEquiv.symm_symm, MeasurableEquiv.toLp_apply, EuclideanSpace.norm_eq,
+    PiLp.toLp_apply, norm_eq_abs, sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]
     norm_cast
     left
     rw [sq_sqrt]
     exact Finset.sum_nonneg (fun i _hi ↦ by positivity)
-  · simp [PiLp.inner_apply, EuclideanSpace.measurableEquiv, Finset.mul_sum, mul_assoc]
+  · simp [PiLp.inner_apply, Finset.mul_sum, mul_assoc]
     simp_rw [mul_comm]
   · simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]
     congr

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.InnerProductSpace.Orientation
 import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 
 /-!
 # Volume forms and measures on inner product spaces
@@ -16,7 +17,7 @@ measure `1` to the parallelepiped spanned by any orthonormal basis, and that it
 the canonical `volume` from the `MeasureSpace` instance.
 -/
 
-open Module MeasureTheory MeasureTheory.Measure Set
+open Module MeasureTheory MeasureTheory.Measure Set WithLp
 
 variable {ι E F : Type*}
 
@@ -113,32 +114,56 @@ theorem OrthonormalBasis.measurePreserving_repr_symm (b : OrthonormalBasis ι 
 
 section PiLp
 
-variable (ι : Type*) [Fintype ι]
+variable (ι : Type*)
+
+/-- `WithLp.equiv` as a `MeasurableEquiv`. -/
+@[deprecated MeasurableEquiv.toLp (since := "2025-11-02")]
+protected def EuclideanSpace.measurableEquiv : EuclideanSpace ℝ ι ≃ᵐ (ι → ℝ) :=
+  (MeasurableEquiv.toLp 2 (ι → ℝ)).symm
+
+set_option linter.deprecated false in
+@[deprecated MeasurableEquiv.coe_toLp (since := "2025-11-02")]
+theorem EuclideanSpace.measurableEquiv_toEquiv :
+    (EuclideanSpace.measurableEquiv ι).toEquiv = WithLp.equiv 2 (ι → ℝ) := rfl
+
+set_option linter.deprecated false in
+@[deprecated MeasurableEquiv.coe_toLp (since := "2025-11-02")]
+theorem EuclideanSpace.coe_measurableEquiv :
+    ⇑(EuclideanSpace.measurableEquiv ι) = ofLp := rfl
+
+set_option linter.deprecated false in
+@[deprecated MeasurableEquiv.coe_toLp_symm (since := "2025-11-02")]
+theorem EuclideanSpace.coe_measurableEquiv_symm :
+    ⇑(EuclideanSpace.measurableEquiv ι).symm = toLp 2 := rfl
+
+variable [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
+theorem EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp :
+    MeasurePreserving (MeasurableEquiv.toLp 2 (ι → ℝ)).symm := by
+  suffices volume = map (MeasurableEquiv.toLp 2 (ι → ℝ)) volume by
+    convert ((MeasurableEquiv.toLp 2 (ι → ℝ)).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]
+    MeasurableEquiv.coe_toLp, ← 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_ofLp : MeasurePreserving (@WithLp.ofLp 2 (ι → ℝ)) :=
-  EuclideanSpace.volume_preserving_measurableEquiv ι
+@[deprecated (since := "2025-07-26")] alias EuclideanSpace.volume_preserving_measurableEquiv :=
+  EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp
+
+/-- A copy of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`
+for the canonical spelling of the equivalence. -/
+theorem PiLp.volume_preserving_ofLp : MeasurePreserving (@ofLp 2 (ι → ℝ)) :=
+  EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι
 
-/-- The reverse direction of `PiLp.volume_preserving_measurableEquiv`, since
+/-- The reverse direction of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, since
 `MeasurePreserving.symm` only works for `MeasurableEquiv`s. -/
-theorem PiLp.volume_preserving_toLp : MeasurePreserving (@WithLp.toLp 2 (ι → ℝ)) :=
-  (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
+theorem PiLp.volume_preserving_toLp : MeasurePreserving (@toLp 2 (ι → ℝ)) :=
+  (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι).symm
 
 lemma volume_euclideanSpace_eq_dirac [IsEmpty ι] :
     (volume : Measure (EuclideanSpace ℝ ι)) = Measure.dirac 0 := by
-  rw [← ((EuclideanSpace.volume_preserving_measurableEquiv ι).symm).map_eq,
-    volume_pi_eq_dirac 0, map_dirac (MeasurableEquiv.measurable _),
-    EuclideanSpace.coe_measurableEquiv_symm, WithLp.toLp_zero]
+  rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0,
+    map_dirac (measurable_toLp 2 _), toLp_zero]
 
 end PiLp
 

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

@@ -313,32 +313,3 @@ instance [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ
 /- This instance should not be necessary, but Lean has difficulties to find it in product
 situations if we do not declare it explicitly. -/
 instance Real.measureSpace : MeasureSpace ℝ := by infer_instance
-
-/-! # Miscellaneous instances for `EuclideanSpace`
-
-In combination with `measureSpaceOfInnerProductSpace`, these put a `MeasureSpace` structure
-on `EuclideanSpace`. -/
-
-
-namespace EuclideanSpace
-
-variable (ι)
-
--- TODO: do we want these instances for `PiLp` too?
-instance : MeasurableSpace (EuclideanSpace ℝ ι) := MeasurableSpace.pi
-
-instance [Finite ι] : BorelSpace (EuclideanSpace ℝ ι) := Pi.borelSpace
-
-/-- `WithLp.equiv` as a `MeasurableEquiv`. -/
-@[simps toEquiv]
-protected def measurableEquiv : EuclideanSpace ℝ ι ≃ᵐ (ι → ℝ) where
-  toEquiv := WithLp.equiv _ _
-  measurable_toFun := measurable_id
-  measurable_invFun := measurable_id
-
-theorem coe_measurableEquiv : ⇑(EuclideanSpace.measurableEquiv ι) = WithLp.ofLp := rfl
-
-theorem coe_measurableEquiv_symm :
-    ⇑(EuclideanSpace.measurableEquiv ι).symm = WithLp.toLp _ := rfl
-
-end EuclideanSpace

Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

@@ -325,11 +325,11 @@ theorem volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
   · suffices volume (Metric.ball (0 : EuclideanSpace ℝ ι) 1) =
         .ofReal (√π ^ card ι / Gamma (card ι / 2 + 1)) by
       rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
-    rw [← ((volume_preserving_measurableEquiv _).symm).measure_preimage
+    rw [← ((volume_preserving_symm_measurableEquiv_toLp _).symm).measure_preimage
       measurableSet_ball.nullMeasurableSet]
     simp only [Set.preimage, ball_zero_eq _ zero_le_one, one_pow, Set.mem_setOf_eq]
     convert volume_sum_rpow_lt_one ι one_le_two using 4
-    · simp [sq_abs, EuclideanSpace.measurableEquiv]
+    · simp [sq_abs]
     · rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
         two_ne_zero, one_mul]
 

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -809,10 +809,6 @@ instance : Ring (euclidean.mixedSpace K) :=
   have : Ring (EuclideanSpace ℂ {w : InfinitePlace K // IsComplex w}) := Pi.ring
   inferInstanceAs (Ring (_ × _))
 
-instance : MeasurableSpace (euclidean.mixedSpace K) := borel _
-
-instance : BorelSpace (euclidean.mixedSpace K) := ⟨rfl⟩
-
 variable [NumberField K]
 
 open Classical in

Mathlib/Probability/Moments/CovarianceBilin.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Etienne Marion
 -/
 import Mathlib.Analysis.InnerProductSpace.Positive
+import Mathlib.Analysis.Normed.Lp.MeasurableSpace
 import Mathlib.MeasureTheory.SpecificCodomains.WithLp
 import Mathlib.Probability.Moments.CovarianceBilinDual