feat: ofLp and toLp of a sum (#31353)

Introduce an `AddEquiv` version of `WithLp.equiv` and use it to prove that `(∑ i ∈ s, f i).ofLp = ∑ i ∈ s, (f i).ofLp` and `toLp p (∑ i ∈ s, f i) = ∑ i ∈ s, toLp p (f i)`.

Author: EtienneC30

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -270,9 +270,8 @@ theorem mem_adjoint_iff (g : Submodule 𝕜 (E × F)) (x : F × E) :
     x ∈ g.adjoint ↔
     ∀ a b, (a, b) ∈ g → inner 𝕜 b x.fst - inner 𝕜 a x.snd = 0 := by
   simp only [Submodule.adjoint, mem_map, mem_orthogonal, LinearEquiv.trans_apply,
-    LinearEquiv.skewSwap_symm_apply, WithLp.linearEquiv_symm_apply, Prod.exists,
-    WithLp.prod_inner_apply, WithLp.ofLp_fst, WithLp.ofLp_snd, forall_exists_index, and_imp,
-    WithLp.linearEquiv_apply]
+    LinearEquiv.skewSwap_symm_apply, coe_symm_linearEquiv, Prod.exists, prod_inner_apply, ofLp_fst,
+    ofLp_snd, forall_exists_index, and_imp, coe_linearEquiv]
   constructor
   · rintro ⟨y, h1, h2⟩ a b hab
     rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -373,8 +373,8 @@ instance instFunLike : FunLike (OrthonormalBasis ι 𝕜 E) ι E where
         have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
         rw [this, Pi.single_smul]
         replace h := congr_fun h i
-        simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe,
-          LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply, EuclideanSpace.toLp_single,
+        simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
+          coe_symm_linearEquiv, EuclideanSpace.toLp_single,
           LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
         rw [h]
 

Mathlib/Analysis/InnerProductSpace/ProdL2.lean

@@ -63,7 +63,7 @@ def prod (v : OrthonormalBasis ι₁ 𝕜 E) (w : OrthonormalBasis ι₂ 𝕜 F)
     · simp
     · 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,
+        OrthonormalBasis.coe_toBasis, LinearMap.coe_inr, WithLp.coe_symm_linearEquiv,
         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]

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -812,7 +812,7 @@ protected def _root_.LinearIsometryEquiv.piLpCongrRight (e : ∀ i, α i ≃ₗ
       ≪≫ₗ (LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv)
       ≪≫ₗ (WithLp.linearEquiv _ _ _).symm
   norm_map' := (WithLp.linearEquiv p 𝕜 _).symm.surjective.forall.2 fun x => by
-    simp only [LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply, WithLp.linearEquiv_apply]
+    simp only [coe_symm_linearEquiv, LinearEquiv.trans_apply, coe_linearEquiv]
     obtain rfl | hp := p.dichotomy
     · simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply,
         LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]
@@ -1012,23 +1012,33 @@ lemma norm_toLp_one {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) [One β] :
     ‖toLp p (1 : ι → β)‖ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖(1 : β)‖ :=
   (norm_toLp_const hp (1 : β)).trans rfl
 
-variable (𝕜 p)
+end Fintype
+
+section
+
+variable [Semiring 𝕜] [∀ i, SeminormedAddCommGroup (β i)] [∀ i, Module 𝕜 (β i)]
 
 /-- `WithLp.linearEquiv` as a continuous linear equivalence. -/
-@[simps! -fullyApplied apply symm_apply]
+@[simps! apply symm_apply]
 def continuousLinearEquiv : PiLp p β ≃L[𝕜] ∀ i, β i where
   toLinearEquiv := WithLp.linearEquiv _ _ _
   continuous_toFun := continuous_ofLp _ _
   continuous_invFun := continuous_toLp p _
 
+lemma coe_continuousLinearEquiv :
+    ⇑(PiLp.continuousLinearEquiv p 𝕜 β) = ofLp := rfl
+
+lemma coe_symm_continuousLinearEquiv :
+    ⇑(PiLp.continuousLinearEquiv p 𝕜 β).symm = toLp p := rfl
+
 variable {𝕜} in
 /-- The projection on the `i`-th coordinate of `PiLp p β`, as a continuous linear map. -/
 @[simps!]
 def proj (i : ι) : PiLp p β →L[𝕜] β i where
   __ := projₗ p β i
   cont := PiLp.continuous_apply ..
 
-end Fintype
+end
 
 section Basis
 
@@ -1042,7 +1052,7 @@ def basisFun : Basis ι 𝕜 (PiLp p fun _ : ι => 𝕜) :=
 @[simp]
 theorem basisFun_apply [DecidableEq ι] (i) :
     basisFun p 𝕜 ι i = toLp p (Pi.single i 1) := by
-  simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.linearEquiv_symm_apply]
+  simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv]
 
 @[simp]
 theorem basisFun_repr (x : PiLp p fun _ : ι => 𝕜) (i : ι) : (basisFun p 𝕜 ι).repr x i = x i :=

Mathlib/Analysis/Normed/Lp/WithLp.lean

@@ -219,14 +219,63 @@ end equiv
 
 variable (K V)
 
+/-- `WithLp.equiv` as a group isomorphism. -/
+@[simps apply symm_apply]
+protected def addEquiv [AddCommGroup V] : WithLp p V ≃+ V where
+  toFun := ofLp
+  invFun := toLp p
+  map_add' := ofLp_add p
+
+lemma coe_addEquiv [AddCommGroup V] : ⇑(WithLp.addEquiv p V) = ofLp := rfl
+
+lemma coe_symm_addEquiv [AddCommGroup V] : ⇑(WithLp.addEquiv p V).symm = toLp p := rfl
+
+@[simp]
+lemma ofLp_sum [AddCommGroup V] {ι : Type*} (s : Finset ι) (f : ι → WithLp p V) :
+    (∑ i ∈ s, f i).ofLp = ∑ i ∈ s, (f i).ofLp :=
+  map_sum (WithLp.addEquiv _ _) _ _
+
+@[simp]
+lemma toLp_sum [AddCommGroup V] {ι : Type*} (s : Finset ι) (f : ι → V) :
+    toLp p (∑ i ∈ s, f i) = ∑ i ∈ s, toLp p (f i) :=
+  map_sum (WithLp.addEquiv _ _).symm _ _
+
+@[simp]
+lemma ofLp_listSum [AddCommGroup V] (l : List (WithLp p V)) :
+    l.sum.ofLp = (l.map ofLp).sum :=
+  map_list_sum (WithLp.addEquiv _ _) _
+
+@[simp]
+lemma toLp_listSum [AddCommGroup V] (l : List V) :
+    toLp p l.sum = (l.map (toLp p)).sum :=
+  map_list_sum (WithLp.addEquiv _ _).symm _
+
+@[simp]
+lemma ofLp_multisetSum [AddCommGroup V] (s : Multiset (WithLp p V)) :
+    s.sum.ofLp = (s.map ofLp).sum :=
+  map_multiset_sum (WithLp.addEquiv _ _) _
+
+@[simp]
+lemma toLp_multisetSum [AddCommGroup V] (s : Multiset V) :
+    toLp p s.sum = (s.map (toLp p)).sum :=
+  map_multiset_sum (WithLp.addEquiv _ _).symm _
+
 /-- `WithLp.equiv` as a linear equivalence. -/
-@[simps -fullyApplied apply symm_apply]
+@[simps apply symm_apply]
 protected def linearEquiv [Semiring K] [AddCommGroup V] [Module K V] : WithLp p V ≃ₗ[K] V where
-  toFun := WithLp.ofLp
-  invFun := WithLp.toLp p
-  map_add' _ _ := rfl
+  __ := WithLp.addEquiv p V
   map_smul' _ _ := rfl
 
+lemma coe_linearEquiv [Semiring K] [AddCommGroup V] [Module K V] :
+    ⇑(WithLp.linearEquiv p K V) = ofLp := rfl
+
+lemma coe_symm_linearEquiv [Semiring K] [AddCommGroup V] [Module K V] :
+    ⇑(WithLp.linearEquiv p K V).symm = toLp p := rfl
+
+@[simp]
+lemma toAddEquiv_linearEquiv [Semiring K] [AddCommGroup V] [Module K V] :
+    (WithLp.linearEquiv p K V).toAddEquiv = WithLp.addEquiv p V := rfl
+
 instance instModuleFinite
     [Semiring K] [AddCommGroup V] [Module K V] [Module.Finite K V] :
     Module.Finite K (WithLp p V) :=

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -148,7 +148,7 @@ theorem EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp :
   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,
-    MeasurableEquiv.coe_toLp, ← PiLp.continuousLinearEquiv_symm_apply 2 ℝ, Basis.map_addHaar]
+    MeasurableEquiv.coe_toLp, ← PiLp.coe_symm_continuousLinearEquiv 2 ℝ, Basis.map_addHaar]
   exact (EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm
 
 @[deprecated (since := "2025-07-26")] alias EuclideanSpace.volume_preserving_measurableEquiv :=