feat(topology/algebra/infinite_sum): add lemmas about continuous linear maps (#5243)

Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Author: dupuisf

src/analysis/normed_space/operator_norm.lean

@@ -815,6 +815,10 @@ protected lemma continuous_linear_map.summable {f : ι → M} (φ : M →L[R] M
 
 alias continuous_linear_map.summable ← summable.mapL
 
+protected lemma continuous_linear_map.map_tsum [t2_space M₂] {f : ι → M}
+  (φ : M →L[R] M₂) (hf : summable f) : φ (∑' z, f z) = ∑' z, φ (f z) :=
+(hf.has_sum.mapL φ).tsum_eq.symm
+
 /-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
 protected lemma continuous_linear_equiv.has_sum {f : ι → M} (e : M ≃L[R] M₂) {y : M₂} :
   has_sum (λ (b:ι), e (f b)) y ↔ has_sum f (e.symm y) :=
@@ -825,6 +829,21 @@ protected lemma continuous_linear_equiv.summable {f : ι → M} (e : M ≃L[R] M
   summable (λ b:ι, e (f b)) ↔ summable f :=
 ⟨λ hf, (e.has_sum.1 hf.has_sum).summable, (e : M →L[R] M₂).summable⟩
 
+lemma continuous_linear_equiv.tsum_eq_iff [t2_space M] [t2_space M₂] {f : ι → M}
+  (e : M ≃L[R] M₂) {y : M₂} : (∑' z, e (f z)) = y ↔ (∑' z, f z) = e.symm y :=
+begin
+  by_cases hf : summable f,
+  { exact ⟨λ h, (e.has_sum.mp ((e.summable.mpr hf).has_sum_iff.mpr h)).tsum_eq,
+      λ h, (e.has_sum.mpr (hf.has_sum_iff.mpr h)).tsum_eq⟩ },
+  { have hf' : ¬summable (λ z, e (f z)) := λ h, hf (e.summable.mp h),
+    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf'],
+    exact ⟨by { rintro rfl, simp }, λ H, by simpa using (congr_arg (λ z, e z) H)⟩ }
+end
+
+protected lemma continuous_linear_equiv.map_tsum [t2_space M] [t2_space M₂] {f : ι → M}
+  (e : M ≃L[R] M₂) : e (∑' z, f z) = ∑' z, e (f z) :=
+by { refine symm (e.tsum_eq_iff.mpr _), rw e.symm_apply_apply _ }
+
 end has_sum
 
 namespace continuous_linear_equiv

src/topology/algebra/infinite_sum.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 import algebra.big_operators.intervals
 import topology.instances.real
+import topology.algebra.module
 import data.indicator_function
 import data.equiv.encodable.lattice
 import order.filter.at_top_bot
@@ -604,6 +605,24 @@ end tsum
 
 end topological_semiring
 
+section topological_semimodule
+variables {R : Type*}
+[semiring R] [topological_space R]
+[topological_space α] [add_comm_monoid α]
+[semimodule R α] [topological_semimodule R α]
+{f : β → α}
+
+lemma has_sum.smul {a : α} {r : R} (hf : has_sum f a) : has_sum (λ z, r • f z) (r • a) :=
+hf.map (const_smul_hom α r) (continuous_const.smul continuous_id)
+
+lemma summable.smul {r : R} (hf : summable f) : summable (λ z, r • f z) :=
+hf.has_sum.smul.summable
+
+lemma tsum_smul [t2_space α] {r : R} (hf : summable f) : (∑' z, r • f z) = r • (∑' z, f z) :=
+hf.has_sum.smul.tsum_eq
+
+end topological_semimodule
+
 section division_ring
 
 variables [division_ring α] [topological_space α] [topological_semiring α]