chore: turn WithLp into a structure (#27270)

Turn `WithLp` into a one field structure, as was suggested many times on Zulip and discussed here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/526234806.
Here is what this PR does:
- The instances on `WithLp p α` which were defeq to those on `α` (algebraic instances, topology, uniformity, bornology) are now pulled back from `α` along `WithLp.equiv p α`. A few declarations are added to ease the process, such as versions of `WithLp.equiv` as a homeomorphism or a uniform isomorphism.
- The `MeasurableSpace` structure was pushed forward from `α`. We now make it pulled back because it is much more convenient to prove that this preserves the `BorelSpace` instance.
- It introduces some definitions to equip `α × β` with the Lp distance, and similarly for `Π i, α i`. This is then used to define relevant instances on type synonyms, such as for matrix norms.
- The PR fixes all the defeq abuses (which break obviously).

Author: EtienneC30

Archive/Hairer.lean

@@ -23,7 +23,7 @@ This is a test of the state of the library suggested by Martin Hairer.
 
 noncomputable section
 
-open Metric Set MeasureTheory
+open Metric Set MeasureTheory PiLp
 open MvPolynomial hiding support
 open Function hiding eval
 open scoped ContDiff
@@ -73,7 +73,8 @@ lemma hasCompactSupport [ProperSpace E] (f : ContDiffSupportedOn 𝕜 E F n (clo
 theorem integrable_eval_mul (p : MvPolynomial ι ℝ)
     (f : ContDiffSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1)) :
     Integrable fun (x : EuclideanSpace ℝ ι) ↦ eval x p * f x :=
-  p.continuous_eval.mul (ContDiffSupportedOn.contDiff f).continuous
+  (p.continuous_eval.comp (continuous_ofLp 2 _)).mul
+    (ContDiffSupportedOn.contDiff f).continuous
     |>.integrable_of_hasCompactSupport (hasCompactSupport f).mul_left
 
 end ContDiffSupportedOn
@@ -97,7 +98,8 @@ lemma inj_L : Injective (L ι) :=
   (injective_iff_map_eq_zero _).mpr fun p hp ↦ by
     have H : ∀ᵐ x : EuclideanSpace ℝ ι, x ∈ ball 0 1 → eval x p = 0 :=
       isOpen_ball.ae_eq_zero_of_integral_contDiff_smul_eq_zero
-        (continuous_eval p |>.locallyIntegrable.locallyIntegrableOn _)
+        (p.continuous_eval.comp (continuous_ofLp 2 _)
+          |>.locallyIntegrable.locallyIntegrableOn _)
         fun g hg _h2g g_supp ↦ by
           simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
     simp_rw [MvPolynomial.funext_iff, map_zero]
@@ -106,7 +108,8 @@ lemma inj_L : Injective (L ι) :=
       (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial
       (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial
     rw [← ae_restrict_iff'₀ measurableSet_ball.nullMeasurableSet] at H
-    apply Measure.eqOn_of_ae_eq H p.continuous_eval.continuousOn continuousOn_const
+    apply Measure.eqOn_of_ae_eq H
+      (p.continuous_eval.comp (continuous_ofLp 2 _)).continuousOn continuousOn_const
     rw [isOpen_ball.interior_eq]
     apply subset_closure
 

Mathlib/Algebra/Module/ZLattice/Covolume.lean

@@ -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_symm_measurableEquiv_toLp ι).symm
+      (PiLp.volume_preserving_toLp ι)
   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/CStarAlgebra/Matrix.lean

@@ -210,7 +210,7 @@ lemma l2_opNorm_mul (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) :
     |>.opNorm_comp_le <| (toEuclideanLin (n := l) (m := n) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) B
   convert this
   ext1 x
-  exact congr($(Matrix.toLin'_mul A B) x)
+  exact congr(toLp 2 ($(Matrix.toLin'_mul A B) x))
 
 lemma l2_opNNNorm_mul (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊ :=
   l2_opNorm_mul A B

Mathlib/Analysis/Calculus/FDeriv/WithLp.lean

@@ -59,7 +59,7 @@ theorem hasStrictFDerivAt_ofLp (f : PiLp p E) :
   .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm
 
 @[deprecated hasStrictFDerivAt_ofLp (since := "2025-05-07")]
-theorem hasStrictFDerivAt_equiv (f : ∀ i, E i) :
+theorem hasStrictFDerivAt_equiv (f : PiLp p E) :
     HasStrictFDerivAt (WithLp.equiv p _)
       (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
   hasStrictFDerivAt_ofLp _ f

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -53,7 +53,7 @@ Unbounded operators, closed operators
 
 noncomputable section
 
-open RCLike LinearPMap
+open RCLike LinearPMap WithLp
 
 open scoped ComplexConjugate
 
@@ -272,12 +272,12 @@ theorem mem_adjoint_iff (g : Submodule 𝕜 (E × F)) (x : F × E) :
   constructor
   · rintro ⟨y, h1, h2⟩ a b hab
     rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
-    specialize h1 (b, -a) a b hab rfl
+    specialize h1 (toLp 2 (b, -a)) a b hab rfl
     dsimp at h1
     simp only [inner_neg_left, ← sub_eq_add_neg] at h1
     exact h1
   · intro h
-    refine ⟨x, ?_, rfl⟩
+    refine ⟨toLp 2 x, ?_, rfl⟩
     intro u a b hab hu
     simp [← hu, ← sub_eq_add_neg, h a b hab]
 

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -183,7 +183,8 @@ variable [Fintype ι]
 @[simp]
 theorem finrank_euclideanSpace :
     Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι := by
-  simp [WithLp]
+  convert (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).finrank_eq
+  simp
 
 theorem finrank_euclideanSpace_fin {n : ℕ} :
     Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n := by simp
@@ -202,11 +203,12 @@ def DirectSum.IsInternal.isometryL2OfOrthogonalFamily [DecidableEq ι] {V : ι 
     E ≃ₗᵢ[𝕜] PiLp 2 fun i => V i := by
   let e₁ := DirectSum.linearEquivFunOnFintype 𝕜 ι fun i => V i
   let e₂ := LinearEquiv.ofBijective (DirectSum.coeLinearMap V) hV
-  refine LinearEquiv.isometryOfInner (e₂.symm.trans e₁) ?_
+  refine LinearEquiv.isometryOfInner ((e₂.symm.trans e₁).trans
+    (WithLp.linearEquiv 2 𝕜 (Π i, V i)).symm) ?_
   suffices ∀ (v w : PiLp 2 fun i => V i), ⟪v, w⟫ = ⟪e₂ (e₁.symm v), e₂ (e₁.symm w)⟫ by
     intro v₀ w₀
-    convert this (e₁ (e₂.symm v₀)) (e₁ (e₂.symm w₀)) <;>
-      simp only [LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply]
+    simp only [LinearEquiv.trans_apply, linearEquiv_symm_apply]
+    convert this (toLp 2 (e₁ (e₂.symm v₀))) (toLp 2 (e₁ (e₂.symm w₀))) <;> simp
   intro v w
   trans ⟪∑ i, (V i).subtypeₗᵢ (v i), ∑ i, (V i).subtypeₗᵢ (w i)⟫
   · simp only [sum_inner, hV'.inner_right_fintype, PiLp.inner_apply]
@@ -263,7 +265,7 @@ theorem EuclideanSpace.single_apply (i : ι) (a : 𝕜) (j : ι) :
 
 @[simp]
 theorem EuclideanSpace.single_eq_zero_iff {i : ι} {a : 𝕜} :
-    EuclideanSpace.single i a = 0 ↔ a = 0 := Pi.single_eq_zero_iff
+    EuclideanSpace.single i a = 0 ↔ a = 0 := (toLp_eq_zero 2).trans Pi.single_eq_zero_iff
 
 variable [Fintype ι]
 
@@ -430,14 +432,14 @@ lemma inner_eq_ite [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i j : ι)
 
 /-- The `Basis ι 𝕜 E` underlying the `OrthonormalBasis` -/
 protected def toBasis (b : OrthonormalBasis ι 𝕜 E) : Basis ι 𝕜 E :=
-  Basis.ofEquivFun b.repr.toLinearEquiv
+  Basis.ofEquivFun (b.repr.toLinearEquiv.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)))
 
 @[simp]
 protected theorem coe_toBasis (b : OrthonormalBasis ι 𝕜 E) : (⇑b.toBasis : ι → E) = ⇑b := rfl
 
 @[simp]
 protected theorem coe_toBasis_repr (b : OrthonormalBasis ι 𝕜 E) :
-    b.toBasis.equivFun = b.repr.toLinearEquiv :=
+    b.toBasis.equivFun = b.repr.toLinearEquiv.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)) :=
   Basis.equivFun_ofEquivFun _
 
 @[simp]
@@ -446,6 +448,7 @@ protected theorem coe_toBasis_repr_apply (b : OrthonormalBasis ι 𝕜 E) (x : E
   rw [← Basis.equivFun_apply, OrthonormalBasis.coe_toBasis_repr]
   -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
   erw [LinearIsometryEquiv.coe_toLinearEquiv]
+  rfl
 
 protected theorem sum_repr (b : OrthonormalBasis ι 𝕜 E) (x : E) : ∑ i, b.repr x i • b i = x := by
   simp_rw [← b.coe_toBasis_repr_apply, ← b.coe_toBasis]
@@ -536,11 +539,11 @@ protected theorem toBasis_map {G : Type*} [NormedAddCommGroup G] [InnerProductSp
 def _root_.Module.Basis.toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
     OrthonormalBasis ι 𝕜 E :=
   OrthonormalBasis.ofRepr <|
-    LinearEquiv.isometryOfInner v.equivFun
+    LinearEquiv.isometryOfInner (v.equivFun.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm)
       (by
         intro x y
-        let p : EuclideanSpace 𝕜 ι := v.equivFun x
-        let q : EuclideanSpace 𝕜 ι := v.equivFun y
+        let p : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun x)
+        let q : EuclideanSpace 𝕜 ι := toLp 2 (v.equivFun y)
         have key : ⟪p, q⟫ = ⟪∑ i, p i • v i, ∑ i, q i • v i⟫ := by
           simp [inner_sum, inner_smul_right, hv.inner_left_fintype, PiLp.inner_apply]
         convert key
@@ -549,19 +552,23 @@ def _root_.Module.Basis.toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonorm
 
 @[simp]
 theorem _root_.Module.Basis.coe_toOrthonormalBasis_repr (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
-    ((v.toOrthonormalBasis hv).repr : E → EuclideanSpace 𝕜 ι) = v.equivFun :=
+    ((v.toOrthonormalBasis hv).repr : E → EuclideanSpace 𝕜 ι) =
+    v.equivFun.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm :=
   rfl
 
 @[simp]
-theorem _root_.Module.Basis.coe_toOrthonormalBasis_repr_symm (v : Basis ι 𝕜 E)
-    (hv : Orthonormal 𝕜 v) :
-    ((v.toOrthonormalBasis hv).repr.symm : EuclideanSpace 𝕜 ι → E) = v.equivFun.symm :=
+theorem _root_.Module.Basis.coe_toOrthonormalBasis_repr_symm
+    (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
+    ((v.toOrthonormalBasis hv).repr.symm : EuclideanSpace 𝕜 ι → E) =
+    (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).trans v.equivFun.symm :=
   rfl
 
 @[simp]
 theorem _root_.Module.Basis.toBasis_toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
     (v.toOrthonormalBasis hv).toBasis = v := by
-  simp [Basis.toOrthonormalBasis, OrthonormalBasis.toBasis]
+  simp only [OrthonormalBasis.toBasis, Basis.toOrthonormalBasis,
+    LinearEquiv.isometryOfInner_toLinearEquiv]
+  exact v.ofEquivFun_equivFun
 
 @[simp]
 theorem _root_.Module.Basis.coe_toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
@@ -636,7 +643,7 @@ theorem _root_.Pi.orthonormalBasis_repr {η : Type*} [Fintype η] {ι : η → T
     [∀ i, Fintype (ι i)] {𝕜 : Type*} [RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)]
     [∀ i, InnerProductSpace 𝕜 (E i)] (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) (x : (i : η) → E i)
     (j : (i : η) × (ι i)) :
-    (Pi.orthonormalBasis B).repr x j = (B j.fst).repr (x j.fst) j.snd := rfl
+    (Pi.orthonormalBasis B).repr (toLp 2 x) j = (B j.fst).repr (x j.fst) j.snd := rfl
 
 variable {v : ι → E}
 
@@ -776,11 +783,10 @@ lemma equiv_symm : (b.equiv b' e).symm = b'.equiv b e.symm := by
 @[simp]
 lemma equiv_apply_basis (i : ι) : b.equiv b' e (b i) = b' (e i) := by
   classical
-  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self,
-    LinearIsometryEquiv.piLpCongrLeft_apply]
+  simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]
   refine DFunLike.congr rfl ?_
   ext j
-  simp [Equiv.symm_apply_eq]
+  simp [Pi.single_apply, Equiv.symm_apply_eq]
 
 @[simp]
 lemma equiv_self_rfl : b.equiv b (.refl ι) = .refl 𝕜 E := by

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -196,9 +196,10 @@ open ComplexOrder in
 @[simp] theorem posSemidef_toMatrix_iff {ι : Type*} [Fintype ι] [DecidableEq ι]
     {A : E →ₗ[𝕜] E} (b : OrthonormalBasis ι 𝕜 E) :
     (A.toMatrix b.toBasis b.toBasis).PosSemidef ↔ A.IsPositive := by
-  rw [← Matrix.isPositive_toEuclideanLin_iff, (by exact Matrix.toLin'_toMatrix' _ :
-    (A.toMatrix b.toBasis b.toBasis).toEuclideanLin =
-      b.repr.toLinearMap ∘ₗ A ∘ₗ b.repr.symm.toLinearMap), isPositive_linearIsometryEquiv_conj_iff]
+  rw [← Matrix.isPositive_toEuclideanLin_iff]
+  convert isPositive_linearIsometryEquiv_conj_iff b.repr
+  ext
+  simp [LinearMap.toMatrix]
 
 /-- A symmetric projection is positive. -/
 @[aesop 10% apply, grind →]

Mathlib/Analysis/InnerProductSpace/ProdL2.lean

@@ -60,15 +60,15 @@ def prod (v : OrthonormalBasis ι₁ 𝕜 E) (w : OrthonormalBasis ι₂ 𝕜 F)
     · unfold Pairwise
       simp only [ne_eq, Basis.map_apply, Basis.prod_apply, LinearMap.coe_inl,
         OrthonormalBasis.coe_toBasis, LinearMap.coe_inr, WithLp.linearEquiv_symm_apply,
-        WithLp.prod_inner_apply, WithLp.ofLp_toLp, Sum.forall, Sum.elim_inl,
-        Function.comp_apply, inner_zero_right, add_zero, Sum.elim_inr, zero_add, Sum.inl.injEq,
-        reduceCtorEq, not_false_eq_true, inner_zero_left, imp_self, implies_true, and_true,
-        Sum.inr.injEq, true_and]
+        WithLp.prod_inner_apply, Sum.forall, Sum.elim_inl, Function.comp_apply, inner_zero_right,
+        add_zero, Sum.elim_inr, zero_add, Sum.inl.injEq, reduceCtorEq, not_false_eq_true,
+        inner_zero_left, imp_self, implies_true, and_true, Sum.inr.injEq, true_and]
       exact ⟨v.orthonormal.2, w.orthonormal.2⟩)
 
 @[simp] theorem prod_apply (v : OrthonormalBasis ι₁ 𝕜 E) (w : OrthonormalBasis ι₂ 𝕜 F) :
     ∀ i : ι₁ ⊕ ι₂, v.prod w i =
-      Sum.elim ((LinearMap.inl 𝕜 E F) ∘ v) ((LinearMap.inr 𝕜 E F) ∘ w) i := by
+      Sum.elim ((WithLp.toLp 2) ∘ (LinearMap.inl 𝕜 E F) ∘ v)
+        ((WithLp.toLp 2) ∘ (LinearMap.inr 𝕜 E F) ∘ w) i := by
   rw [Sum.forall]
   unfold OrthonormalBasis.prod
   aesop

Mathlib/Analysis/InnerProductSpace/Spectrum.lean

@@ -62,7 +62,7 @@ local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
 
 open scoped ComplexConjugate
 
-open Module.End
+open Module.End WithLp
 
 namespace LinearMap
 
@@ -180,12 +180,12 @@ theorem diagonalization_apply_self_apply (hT : T.IsSymmetric) (v : E) (μ : Eige
     hT.diagonalization (T v) μ = (μ : 𝕜) • hT.diagonalization v μ := by
   suffices
     ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
-      T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => (μ : 𝕜) • w μ by
+      T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ => (μ : 𝕜) • w μ) by
     simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
       congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
   intro w
   have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2
-  simp only [hwT, diagonalization_symm_apply, map_sum, Submodule.coe_smul_of_tower]
+  simp only [diagonalization_symm_apply, map_sum, hwT, SetLike.val_smul]
 
 end Version1
 
@@ -274,15 +274,15 @@ theorem eigenvectorBasis_apply_self_apply (hT : T.IsSymmetric) (hn : Module.finr
   suffices
     ∀ w : EuclideanSpace 𝕜 (Fin n),
       T ((hT.eigenvectorBasis hn).repr.symm w) =
-        (hT.eigenvectorBasis hn).repr.symm fun i => hT.eigenvalues hn i * w i by
+        (hT.eigenvectorBasis hn).repr.symm (toLp 2 fun i ↦ hT.eigenvalues hn i * w i) by
     simpa [OrthonormalBasis.sum_repr_symm] using
       congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i)
         (this ((hT.eigenvectorBasis hn).repr v))
   intro w
   simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, map_smul, apply_eigenvectorBasis]
   apply Fintype.sum_congr
   intro a
-  rw [smul_smul, mul_comm]
+  rw [smul_smul, mul_comm, ofLp_toLp]
 
 end Version2