chore(topology/algebra/infinite_sum): refactor tsum_mul_left/right (#…

…5533)

* move old lemmas to `summable` namespace;
* add new `tsum_mul_left` and `tsum_mul_right` that work in a `division_ring` without a `summable` assumption.

src/analysis/analytic/basic.lean

@@ -638,9 +638,6 @@ begin
     (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ) :
       begin
         rw tsum_mul_right,
-        convert p.change_origin_summable_aux3 k h,
-        ext ⟨_, _, _⟩,
-        refl
       end
   ... = tsum (A ∘ change_origin_summable_aux_j k) :
     begin

src/analysis/normed_space/banach.lean

@@ -151,10 +151,9 @@ begin
     ∥x∥ ≤ (∑'n, ∥u n∥) : norm_tsum_le_tsum_norm sNu
     ... ≤ (∑'n, (1/2)^n * (C * ∥y∥)) :
       tsum_le_tsum ule sNu (summable.mul_right _ summable_geometric_two)
-    ... = (∑'n, (1/2)^n) * (C * ∥y∥) : by { rw tsum_mul_right, exact summable_geometric_two }
-    ... = 2 * (C * ∥y∥) : by rw tsum_geometric_two
-    ... = 2 * C * ∥y∥ + 0 : by rw [add_zero, mul_assoc]
-    ... ≤ 2 * C * ∥y∥ + ∥y∥ : add_le_add (le_refl _) (norm_nonneg _)
+    ... = (∑'n, (1/2)^n) * (C * ∥y∥) : tsum_mul_right
+    ... = 2 * C * ∥y∥ : by rw [tsum_geometric_two, mul_assoc]
+    ... ≤ 2 * C * ∥y∥ + ∥y∥ : le_add_of_nonneg_right (norm_nonneg y)
     ... = (2 * C + 1) * ∥y∥ : by ring,
   have fsumeq : ∀n:ℕ, f (∑ i in finset.range n, u i) = y - (h^[n]) y,
   { assume n,
@@ -172,10 +171,8 @@ begin
     rw tendsto_iff_norm_tendsto_zero,
     simp only [sub_zero],
     refine squeeze_zero (λ_, norm_nonneg _) hnle _,
-    have : 0 = 0 * ∥y∥, by rw zero_mul,
-    rw this,
-    refine tendsto.mul _ tendsto_const_nhds,
-    exact tendsto_pow_at_top_nhds_0_of_lt_1 (by norm_num) (by norm_num) },
+    rw [← zero_mul ∥y∥],
+    refine (tendsto_pow_at_top_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds; norm_num },
   have feq : f x = y - 0 := tendsto_nhds_unique L₁ L₂,
   rw sub_zero at feq,
   exact ⟨x, feq, x_ineq⟩

src/data/real/cardinality.lean

@@ -86,7 +86,7 @@ lemma cantor_function_succ (f : ℕ → bool) (h1 : 0 ≤ c) (h2 : c < 1) :
   cantor_function c f = cond (f 0) 1 0 + c * cantor_function c (λ n, f (n+1)) :=
 begin
   rw [cantor_function, tsum_eq_zero_add (summable_cantor_function f h1 h2)],
-  rw [cantor_function_aux_succ, tsum_mul_left _ (summable_cantor_function _ h1 h2)], refl
+  rw [cantor_function_aux_succ, tsum_mul_left], refl
 end
 
 /-- `cantor_function c` is strictly increasing with if `0 < c < 1/2`, if we endow `ℕ → bool` with a

src/topology/algebra/infinite_sum.lean

@@ -611,10 +611,10 @@ lemma summable.mul_right (a) (hf : summable f) : summable (λb, f b * a) :=
 section tsum
 variables [t2_space α]
 
-lemma tsum_mul_left (a) (hf : summable f) : (∑'b, a * f b) = a * (∑'b, f b) :=
+lemma summable.tsum_mul_left (a) (hf : summable f) : (∑'b, a * f b) = a * (∑'b, f b) :=
 (hf.has_sum.mul_left _).tsum_eq
 
-lemma tsum_mul_right (a) (hf : summable f) : (∑'b, f b * a) = (∑'b, f b) * a :=
+lemma summable.tsum_mul_right (a) (hf : summable f) : (∑'b, f b * a) = (∑'b, f b) * a :=
 (hf.has_sum.mul_right _).tsum_eq
 
 end tsum
@@ -656,6 +656,18 @@ lemma summable_mul_left_iff (h : a ≠ 0) : summable f ↔ summable (λb, a * f
 lemma summable_mul_right_iff (h : a ≠ 0) : summable f ↔ summable (λb, f b * a) :=
 ⟨λ H, H.mul_right _, λ H, by simpa only [mul_inv_cancel_right' h] using H.mul_right a⁻¹⟩
 
+lemma tsum_mul_left [t2_space α] : (∑' x, a * f x) = a * ∑' x, f x :=
+if hf : summable f then hf.tsum_mul_left a
+else if ha : a = 0 then by simp [ha]
+else by rw [tsum_eq_zero_of_not_summable hf,
+  tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).2 hf), mul_zero]
+
+lemma tsum_mul_right [t2_space α] : (∑' x, f x * a) = (∑' x, f x) * a :=
+if hf : summable f then hf.tsum_mul_right a
+else if ha : a = 0 then by simp [ha]
+else by rw [tsum_eq_zero_of_not_summable hf,
+  tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).2 hf), zero_mul]
+
 end division_ring
 
 section order_topology
@@ -713,17 +725,23 @@ le_has_sum (summable.has_sum hf) b hb
 lemma tsum_le_tsum (h : ∀b, f b ≤ g b) (hf : summable f) (hg : summable g) : (∑'b, f b) ≤ (∑'b, g b) :=
 has_sum_le h hf.has_sum hg.has_sum
 
+lemma has_sum.nonneg (h : ∀ b, 0 ≤ g b) (ha : has_sum g a) : 0 ≤ a :=
+has_sum_le h has_sum_zero ha
+
+lemma has_sum.nonpos (h : ∀ b, g b ≤ 0) (ha : has_sum g a) : a ≤ 0 :=
+has_sum_le h ha has_sum_zero
+
 lemma tsum_nonneg (h : ∀ b, 0 ≤ g b) : 0 ≤ (∑'b, g b) :=
 begin
   by_cases hg : summable g,
-  { simpa using tsum_le_tsum h summable_zero hg },
+  { exact hg.has_sum.nonneg h },
   { simp [tsum_eq_zero_of_not_summable hg] }
 end
 
 lemma tsum_nonpos (h : ∀ b, f b ≤ 0) : (∑'b, f b) ≤ 0 :=
 begin
   by_cases hf : summable f,
-  { simpa using tsum_le_tsum h hf summable_zero},
+  { exact hf.has_sum.nonpos h },
   { simp [tsum_eq_zero_of_not_summable hf] }
 end
 

src/topology/instances/nnreal.lean

@@ -87,6 +87,12 @@ if hf : summable f
 then (eq.symm $ (has_sum_coe.2 $ hf.has_sum).tsum_eq)
 else by simp [tsum, hf, mt summable_coe.1 hf]
 
+lemma tsum_mul_left (a : ℝ≥0) (f : α → ℝ≥0) : (∑' x, a * f x) = a * ∑' x, f x :=
+nnreal.eq $ by simp only [coe_tsum, nnreal.coe_mul, tsum_mul_left]
+
+lemma tsum_mul_right (f : α → ℝ≥0) (a : ℝ≥0) : (∑' x, f x * a) = (∑' x, f x) * a :=
+nnreal.eq $ by simp only [coe_tsum, nnreal.coe_mul, tsum_mul_right]
+
 lemma summable_comp_injective {β : Type*} {f : α → ℝ≥0} (hf : summable f)
   {i : β → α} (hi : function.injective i) :
   summable (f ∘ i) :=