refactor(tsum): use ∑' instead of ∑ as notation (#2571)

As discussed in: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/big.20ops/near/195821357

This is the result of
```
git grep -l '∑' | grep -v "mean_ineq" | xargs sed -i "s/∑/∑'/g"
```
after manually cleaning some occurences of `∑` in TeX strings. Probably `∑` has now also been changed in a lot of comments and docstrings, but my reasoning is that if the string "tsum" occurs in the file, then it doesn't do harm to write `∑'` instead of `∑` in the comments as well.

src/algebra/geom_sum.lean

@@ -13,7 +13,7 @@ variable {α : Type u}
 
 open finset
 
-/-- Sum of the finite geometric series $∑_{i=0}^{n-1} x^i$. -/
+/-- Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i$. -/
 def geom_series [semiring α] (x : α) (n : ℕ) :=
 (range n).sum (λ i, x ^ i)
 
@@ -27,7 +27,7 @@ theorem geom_series_def [semiring α] (x : α) (n : ℕ) :
   geom_series x 1 = 1 :=
 by { rw [geom_series_def, sum_range_one, pow_zero] }
 
-/-- Sum of the finite geometric series $∑_{i=0}^{n-1} x^i y^{n-1-i}$. -/
+/-- Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i y^{n-1-i}$. -/
 def geom_series₂ [semiring α] (x y : α) (n : ℕ) :=
 (range n).sum (λ i, x ^ i * (y ^ (n - 1 - i)))
 
@@ -46,7 +46,7 @@ by { have : 1 - 1 - 0 = 0 := rfl,
   geom_series₂ x 1 n = geom_series x n :=
 sum_congr rfl (λ i _, by { rw [one_pow, mul_one] })
 
-/-- $x^n-y^n=(x-y)∑x^ky^{n-1-k}$ reformulated without `-` signs. -/
+/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
 protected theorem commute.geom_sum₂_mul_add [semiring α] {x y : α} (h : commute x y) (n : ℕ) :
   (geom_series₂ (x + y) y n) * x + y ^ n = (x + y) ^ n :=
 begin
@@ -76,7 +76,7 @@ begin
     rw[mul_assoc, ← mul_add y, ih] }
 end
 
-/-- $x^n-y^n=(x-y)∑x^ky^{n-1-k}$ reformulated without `-` signs. -/
+/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
 theorem geom_sum₂_mul_add [comm_semiring α] (x y : α) (n : ℕ) :
   (geom_series₂ (x + y) y n) * x + y ^ n = (x + y) ^ n :=
 (commute.all x y).geom_sum₂_mul_add n

src/analysis/analytic/basic.lean

@@ -32,12 +32,12 @@ for `n : ℕ`.
 * `p.le_radius_of_bound`, `p.bound_of_lt_radius`, `p.geometric_bound_of_lt_radius`: relating the
   value of the radius with the growth of `∥p n∥ * r^n`.
 * `p.partial_sum n x`: the sum `∑_{i = 0}^{n-1} pᵢ xⁱ`.
-* `p.sum x`: the sum `∑_{i = 0}^{∞} pᵢ xⁱ`.
+* `p.sum x`: the sum `∑'_{i = 0}^{∞} pᵢ xⁱ`.
 
 Additionally, let `f` be a function from `E` to `F`.
 
 * `has_fpower_series_on_ball f p x r`: on the ball of center `x` with radius `r`,
-  `f (x + y) = ∑_n pₙ yⁿ`.
+  `f (x + y) = ∑'_n pₙ yⁿ`.
 * `has_fpower_series_at f p x`: on some ball of center `x` with positive radius, holds
   `has_fpower_series_on_ball f p x r`.
 * `analytic_at 𝕜 f x`: there exists a power series `p` such that holds
@@ -203,15 +203,15 @@ section
 variables {f g : E → F} {p pf pg : formal_multilinear_series 𝕜 E F} {x : E} {r r' : ennreal}
 
 /-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as
-a power series on the ball of radius `r > 0` around `x` if `f (x + y) = ∑ pₙ yⁿ` for all `∥y∥ < r`. -/
+a power series on the ball of radius `r > 0` around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `∥y∥ < r`. -/
 structure has_fpower_series_on_ball
   (f : E → F) (p : formal_multilinear_series 𝕜 E F) (x : E) (r : ennreal) : Prop :=
 (r_le    : r ≤ p.radius)
 (r_pos   : 0 < r)
 (has_sum : ∀ {y}, y ∈ emetric.ball (0 : E) r → has_sum (λn:ℕ, p n (λ(i : fin n), y)) (f (x + y)))
 
 /-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as
-a power series around `x` if `f (x + y) = ∑ pₙ yⁿ` for all `y` in a neighborhood of `0`. -/
+a power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a neighborhood of `0`. -/
 def has_fpower_series_at (f : E → F) (p : formal_multilinear_series 𝕜 E F) (x : E) :=
 ∃ r, has_fpower_series_on_ball f p x r
 
@@ -513,9 +513,9 @@ begin
     by { ext b, rcases b with ⟨n, s⟩, simp [Bnnnorm, nnreal.coe_pow, coe_nnnorm] },
   rw [this, nnreal.summable_coe, ← ennreal.tsum_coe_ne_top_iff_summable],
   apply ne_of_lt,
-  calc (∑ b, ↑(Bnnnorm b))
-  = (∑ n, (∑ s, ↑(Bnnnorm ⟨n, s⟩))) : by exact ennreal.tsum_sigma' _
-  ... ≤ (∑ n, (((nnnorm (p n) * (nnnorm x + r)^n) : nnreal) : ennreal)) :
+  calc (∑' b, ↑(Bnnnorm b))
+  = (∑' n, (∑' s, ↑(Bnnnorm ⟨n, s⟩))) : by exact ennreal.tsum_sigma' _
+  ... ≤ (∑' n, (((nnnorm (p n) * (nnnorm x + r)^n) : nnreal) : ennreal)) :
     begin
       refine ennreal.tsum_le_tsum (λ n, _),
       rw [tsum_fintype, ← ennreal.coe_finset_sum, ennreal.coe_le_coe],
@@ -527,7 +527,7 @@ begin
       ... = nnnorm (p n) * (nnnorm x + r) ^ n :
       by { rw [add_comm, ← finset.mul_sum, ← fin.sum_pow_mul_eq_add_pow], congr, ext s, ring }
     end
-  ... ≤ (∑ (n : ℕ), (C * a ^ n : ennreal)) :
+  ... ≤ (∑' (n : ℕ), (C * a ^ n : ennreal)) :
     tsum_le_tsum (λ n, by exact_mod_cast hC n) ennreal.summable ennreal.summable
   ... < ⊤ :
     by simp [ennreal.mul_eq_top, ha, ennreal.tsum_mul_left, ennreal.tsum_geometric,

src/analysis/analytic/composition.lean

@@ -11,10 +11,10 @@ import combinatorics.composition
 
 in this file we prove that the composition of analytic functions is analytic.
 
-The argument is the following. Assume `g z = ∑ qₙ (z, ..., z)` and `f y = ∑ pₖ (y, ..., y)`. Then
+The argument is the following. Assume `g z = ∑' qₙ (z, ..., z)` and `f y = ∑' pₖ (y, ..., y)`. Then
 
-`g (f y) = ∑ qₙ (∑ pₖ (y, ..., y), ..., ∑ pₖ (y, ..., y))
-= ∑ qₙ (p_{i₁} (y, ..., y), ..., p_{iₙ} (y, ..., y))`.
+`g (f y) = ∑' qₙ (∑' pₖ (y, ..., y), ..., ∑' pₖ (y, ..., y))
+= ∑' qₙ (p_{i₁} (y, ..., y), ..., p_{iₙ} (y, ..., y))`.
 
 For each `n` and `i₁, ..., iₙ`, define a `i₁ + ... + iₙ` multilinear function mapping
 `(y₀, ..., y_{i₁ + ... + iₙ - 1})` to
@@ -209,7 +209,7 @@ end
 /-- Formal composition of two formal multilinear series. The `n`-th coefficient in the composition
 is defined to be the sum of `q.comp_along_composition p c` over all compositions of
 `n`. In other words, this term (as a multilinear function applied to `v_0, ..., v_{n-1}`) is
-`∑_{k} ∑_{i₁ + ... + iₖ = n} pₖ (q_{i_1} (...), ..., q_{i_k} (...))`, where one puts all variables
+`∑'_{k} ∑'_{i₁ + ... + iₖ = n} pₖ (q_{i_1} (...), ..., q_{i_k} (...))`, where one puts all variables
 `v_0, ..., v_{n-1}` in increasing order in the dots.-/
 protected def comp (q : formal_multilinear_series 𝕜 F G) (p : formal_multilinear_series 𝕜 E F) :
   formal_multilinear_series 𝕜 E G :=
@@ -296,16 +296,16 @@ begin
   refine ⟨r, r_pos, _⟩,
   rw [← ennreal.tsum_coe_ne_top_iff_summable],
   apply ne_of_lt,
-  calc (∑ (i : Σ (n : ℕ), composition n), ↑(nnnorm (q.comp_along_composition p i.2) * r ^ i.1))
-  ≤ (∑ (i : Σ (n : ℕ), composition n), (Cq : ennreal) * a ^ i.1) : ennreal.tsum_le_tsum I
-  ... = (∑ (n : ℕ), (∑ (c : composition n), (Cq : ennreal) * a ^ n)) : ennreal.tsum_sigma' _
-  ... = (∑ (n : ℕ), ↑(fintype.card (composition n)) * (Cq : ennreal) * a ^ n) :
+  calc (∑' (i : Σ (n : ℕ), composition n), ↑(nnnorm (q.comp_along_composition p i.2) * r ^ i.1))
+  ≤ (∑' (i : Σ (n : ℕ), composition n), (Cq : ennreal) * a ^ i.1) : ennreal.tsum_le_tsum I
+  ... = (∑' (n : ℕ), (∑' (c : composition n), (Cq : ennreal) * a ^ n)) : ennreal.tsum_sigma' _
+  ... = (∑' (n : ℕ), ↑(fintype.card (composition n)) * (Cq : ennreal) * a ^ n) :
     begin
       congr' 1,
       ext1 n,
       rw [tsum_fintype, finset.sum_const, add_monoid.smul_eq_mul, finset.card_univ, mul_assoc]
     end
-  ... ≤ (∑ (n : ℕ), (2 : ennreal) ^ n * (Cq : ennreal) * a ^ n) :
+  ... ≤ (∑' (n : ℕ), (2 : ennreal) ^ n * (Cq : ennreal) * a ^ n) :
     begin
       apply ennreal.tsum_le_tsum (λ n, _),
       apply ennreal.mul_le_mul (ennreal.mul_le_mul _ (le_refl _)) (le_refl _),
@@ -316,7 +316,7 @@ begin
       rw ← ennreal.coe_le_coe at this,
       exact this
     end
-  ... = (∑ (n : ℕ), (Cq : ennreal) * (2 * a) ^ n) : by { congr' 1, ext1 n, rw mul_pow, ring }
+  ... = (∑' (n : ℕ), (Cq : ennreal) * (2 * a) ^ n) : by { congr' 1, ext1 n, rw mul_pow, ring }
   ... = (Cq : ennreal) * (1 - 2 * a) ⁻¹ : by rw [ennreal.tsum_mul_left, ennreal.tsum_geometric]
   ... < ⊤ : by simp [lt_top_iff_ne_top, ennreal.mul_eq_top, two_a]
 end
@@ -333,12 +333,12 @@ apply le_radius_of_bound _ (tsum (λ (i : Σ (n : ℕ), composition n),
     (nnnorm (comp_along_composition q p i.snd) * r ^ i.fst))),
   assume n,
   calc nnnorm (formal_multilinear_series.comp q p n) * r ^ n ≤
-  ∑ (c : composition n), nnnorm (comp_along_composition q p c) * r ^ n :
+  ∑' (c : composition n), nnnorm (comp_along_composition q p c) * r ^ n :
     begin
       rw [tsum_fintype, ← finset.sum_mul],
       exact mul_le_mul_of_nonneg_right (nnnorm_sum_le _ _) bot_le
     end
-  ... ≤ ∑ (i : Σ (n : ℕ), composition n),
+  ... ≤ ∑' (i : Σ (n : ℕ), composition n),
           nnnorm (comp_along_composition q p i.snd) * r ^ i.fst :
     begin
       let f : composition n → (Σ (n : ℕ), composition n) := λ c, ⟨n, c⟩,

src/analysis/normed_space/banach.lean

@@ -149,10 +149,10 @@ begin
   have su : summable u := summable_of_summable_norm sNu,
   let x := tsum u,
   have x_ineq : ∥x∥ ≤ (2 * C + 1) * ∥y∥ := calc
-    ∥x∥ ≤ (∑n, ∥u n∥) : norm_tsum_le_tsum_norm sNu
-    ... ≤ (∑n, (1/2)^n * (C * ∥y∥)) :
+    ∥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 }
+    ... = (∑'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 _)

src/analysis/normed_space/basic.lean

@@ -860,14 +860,14 @@ lemma has_sum_of_subseq_of_summable {f : ι → α} (hf : summable (λa, ∥f a
   has_sum f a :=
 tendsto_nhds_of_cauchy_seq_of_subseq (cauchy_seq_finset_of_summable_norm hf) hp hs ha
 
-/-- If `∑ i, ∥f i∥` is summable, then `∥(∑ i, f i)∥ ≤ (∑ i, ∥f i∥)`. Note that we do not assume that
-`∑ i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
-lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
+/-- If `∑' i, ∥f i∥` is summable, then `∥(∑' i, f i)∥ ≤ (∑' i, ∥f i∥)`. Note that we do not assume that
+`∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
+lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑'i, f i)∥ ≤ (∑' i, ∥f i∥) :=
 begin
   by_cases h : summable f,
-  { have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (𝓝 ∥(∑ i, f i)∥) :=
+  { have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (𝓝 ∥(∑' i, f i)∥) :=
       (continuous_norm.tendsto _).comp h.has_sum,
-    have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (𝓝 (∑ i, ∥f i∥)) :=
+    have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (𝓝 (∑' i, ∥f i∥)) :=
       hf.has_sum,
     exact le_of_tendsto_of_tendsto' at_top_ne_bot h₁ h₂ (assume s, norm_sum_le _ _) },
   { rw tsum_eq_zero_of_not_summable h,

src/analysis/specific_limits.lean

@@ -210,7 +210,7 @@ have (λ n, (range n).sum (λ i, r ^ i)) = (λ n, geom_series r n) := rfl,
 lemma summable_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : summable (λn:ℕ, r ^ n) :=
 ⟨_, has_sum_geometric h₁ h₂⟩
 
-lemma tsum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : (∑n:ℕ, r ^ n) = (1 - r)⁻¹ :=
+lemma tsum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
 tsum_eq_has_sum (has_sum_geometric h₁ h₂)
 
 lemma has_sum_geometric_two : has_sum (λn:ℕ, ((1:ℝ)/2) ^ n) 2 :=
@@ -219,7 +219,7 @@ by convert has_sum_geometric _ _; norm_num
 lemma summable_geometric_two : summable (λn:ℕ, ((1:ℝ)/2) ^ n) :=
 ⟨_, has_sum_geometric_two⟩
 
-lemma tsum_geometric_two : (∑n:ℕ, ((1:ℝ)/2) ^ n) = 2 :=
+lemma tsum_geometric_two : (∑'n:ℕ, ((1:ℝ)/2) ^ n) = 2 :=
 tsum_eq_has_sum has_sum_geometric_two
 
 lemma has_sum_geometric_two' (a : ℝ) : has_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=
@@ -233,7 +233,7 @@ end
 lemma summable_geometric_two' (a : ℝ) : summable (λ n:ℕ, (a / 2) / 2 ^ n) :=
 ⟨a, has_sum_geometric_two' a⟩
 
-lemma tsum_geometric_two' (a : ℝ) : (∑ n:ℕ, (a / 2) / 2^n) = a :=
+lemma tsum_geometric_two' (a : ℝ) : (∑' n:ℕ, (a / 2) / 2^n) = a :=
 tsum_eq_has_sum $ has_sum_geometric_two' a
 
 lemma nnreal.has_sum_geometric {r : nnreal} (hr : r < 1) :
@@ -248,12 +248,12 @@ end
 lemma nnreal.summable_geometric {r : nnreal} (hr : r < 1) : summable (λn:ℕ, r ^ n) :=
 ⟨_, nnreal.has_sum_geometric hr⟩
 
-lemma tsum_geometric_nnreal {r : nnreal} (hr : r < 1) : (∑n:ℕ, r ^ n) = (1 - r)⁻¹ :=
+lemma tsum_geometric_nnreal {r : nnreal} (hr : r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
 tsum_eq_has_sum (nnreal.has_sum_geometric hr)
 
 /-- The series `pow r` converges to `(1-r)⁻¹`. For `r < 1` the RHS is a finite number,
 and for `1 ≤ r` the RHS equals `∞`. -/
-lemma ennreal.tsum_geometric (r : ennreal) : (∑n:ℕ, r ^ n) = (1 - r)⁻¹ :=
+lemma ennreal.tsum_geometric (r : ennreal) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
 begin
   cases lt_or_le r 1 with hr hr,
   { rcases ennreal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩,
@@ -478,7 +478,7 @@ end nnreal
 namespace ennreal
 
 theorem exists_pos_sum_of_encodable {ε : ennreal} (hε : 0 < ε) (ι) [encodable ι] :
-  ∃ ε' : ι → nnreal, (∀ i, 0 < ε' i) ∧ (∑ i, (ε' i : ennreal)) < ε :=
+  ∃ ε' : ι → nnreal, (∀ i, 0 < ε' i) ∧ (∑' i, (ε' i : ennreal)) < ε :=
 begin
   rcases dense hε with ⟨r, h0r, hrε⟩,
   rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, hx⟩,

src/data/real/cardinality.lean

@@ -41,7 +41,7 @@ begin
   intro n, cases h : f n; simp [h]
 end
 
-def cantor_function (c : ℝ) (f : ℕ → bool) : ℝ := ∑ n, cantor_function_aux c f n
+def cantor_function (c : ℝ) (f : ℕ → bool) : ℝ := ∑' n, cantor_function_aux c f n
 
 lemma cantor_function_le (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ n, f n → g n) :
   cantor_function c f ≤ cantor_function c g :=

src/measure_theory/integration.lean

@@ -1238,7 +1238,7 @@ end
 end
 
 lemma lintegral_tsum [encodable β] {f : β → α → ennreal} (hf : ∀i, measurable (f i)) :
-  (∫⁻ a, ∑ i, f i a) = (∑ i, ∫⁻ a, f i a) :=
+  (∫⁻ a, ∑' i, f i a) = (∑' i, ∫⁻ a, f i a) :=
 begin
   simp only [ennreal.tsum_eq_supr_sum],
   rw [lintegral_supr_directed],
@@ -1302,7 +1302,7 @@ if hf : measurable f then
     (by simp)
     begin
       assume s hs hd,
-      have : ∀a, (⨆ (h : a ∈ ⋃i, s i), f a) = (∑i, (⨆ (h : a ∈ s i), f a)),
+      have : ∀a, (⨆ (h : a ∈ ⋃i, s i), f a) = (∑'i, (⨆ (h : a ∈ s i), f a)),
       { assume a,
         by_cases ha : ∃j, a ∈ s j,
         { rcases ha with ⟨j, haj⟩,

src/measure_theory/lebesgue_measure.lean

@@ -93,7 +93,7 @@ outer_measure.of_function_le _ _ _
 
 lemma lebesgue_length_subadditive {a b : ℝ} {c d : ℕ → ℝ}
   (ss : Icc a b ⊆ ⋃i, Ioo (c i) (d i)) :
-  (of_real (b - a) : ennreal) ≤ ∑ i, of_real (d i - c i) :=
+  (of_real (b - a) : ennreal) ≤ ∑' i, of_real (d i - c i) :=
 begin
   suffices : ∀ (s:finset ℕ) b
     (cv : Icc a b ⊆ ⋃ i ∈ (↑s:set ℕ), Ioo (c i) (d i)),