chore(analysis|measure_theory|topology): give tsum notation precedence 67 (#5709)

This saves us a lot of `()`
In particular, lean no longer thinks that `∑' i, f i = 37` is a tsum of propositions.

Author: jcommelin

src/algebra/big_operators/basic.lean

@@ -48,7 +48,7 @@ rfl
 
 end finset
 
-/-
+/--
 ## Operator precedence of `∏` and `∑`
 
 There is no established mathematical convention
@@ -68,6 +68,7 @@ In practice, this means that parentheses should be placed as follows:
 ```
 (Example taken from page 490 of Knuth's *Concrete Mathematics*.)
 -/
+library_note "operator precedence of big operators"
 
 localized "notation `∑` binders `, ` r:(scoped:67 f, finset.sum finset.univ f) := r"
   in big_operators

src/analysis/normed_space/banach.lean

@@ -148,8 +148,8 @@ 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∥) : tsum_mul_right
     ... = 2 * C * ∥y∥ : by rw [tsum_geometric_two, mul_assoc]

src/analysis/normed_space/basic.lean

@@ -1203,13 +1203,13 @@ 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) hs ha
 
-/-- If `∑' i, ∥f i∥` is summable, then `∥(∑' i, f i)∥ ≤ (∑' i, ∥f i∥)`. Note that we do not assume
+/-- 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∥) :=
+  ∥∑'i, f i∥ ≤ ∑' i, ∥f i∥ :=
 begin
   by_cases h : summable f,
-  { have h₁ : tendsto (λs:finset ι, ∥∑ i in s, f i∥) at_top (𝓝 ∥(∑' i, f i)∥) :=
+  { have h₁ : tendsto (λs:finset ι, ∥∑ i in s, f i∥) at_top (𝓝 ∥∑' i, f i∥) :=
       (continuous_norm.tendsto _).comp h.has_sum,
     have h₂ : tendsto (λs:finset ι, ∑ i in s, ∥f i∥) at_top (𝓝 (∑' i, ∥f i∥)) :=
       hf.has_sum,
@@ -1231,10 +1231,10 @@ lemma summable_of_norm_bounded
 by { rw summable_iff_cauchy_seq_finset, exact cauchy_seq_finset_of_norm_bounded g hg h }
 
 /-- Quantitative result associated to the direct comparison test for series:  If `∑' i, g i` is
-summable, and for all `i`, `∥f i∥ ≤ g i`, then `∥(∑' i, f i)∥ ≤ (∑' i, g i)`. Note that we do not
+summable, and for all `i`, `∥f i∥ ≤ g i`, then `∥∑' i, f i∥ ≤ ∑' i, g 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 tsum_of_norm_bounded {f : ι → α} {g : ι → ℝ} {a : ℝ} (hg : has_sum g a) (h : ∀i, ∥f i∥ ≤ g i) :
-  ∥(∑' (i:ι), f i)∥ ≤ a :=
+  ∥∑' i:ι, f i∥ ≤ a :=
 begin
   have h' : summable (λ (i : ι), ∥f i∥),
   { let f' : ι → ℝ := λ i, ∥f i∥,
@@ -1243,9 +1243,9 @@ begin
       convert h i,
       simp },
     simpa [f'] using summable_of_norm_bounded g hg.summable h'' },
-  have h1 : ∥(∑' (i:ι), f i)∥ ≤ ∑' (i:ι), ∥f i∥ := by simpa using norm_tsum_le_tsum_norm h',
+  have h1 : ∥∑' i:ι, f i∥ ≤ ∑' i:ι, ∥f i∥ := by simpa using norm_tsum_le_tsum_norm h',
   have h2 := tsum_le_tsum h h' hg.summable,
-  have h3 : a = ∑' (i:ι), g i := (has_sum.tsum_eq hg).symm,
+  have h3 : a = ∑' i:ι, g i := (has_sum.tsum_eq hg).symm,
   linarith
 end
 

src/analysis/normed_space/operator_norm.lean

@@ -847,7 +847,7 @@ protected lemma continuous_linear_equiv.summable {f : ι → M} (e : M ≃L[R] M
 ⟨λ 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 :=
+  (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,

src/analysis/normed_space/units.lean

@@ -38,7 +38,7 @@ namespace units
 from `1` is a unit.  Here we construct its `units` structure.  -/
 def one_sub (t : R) (h : ∥t∥ < 1) : units R :=
 { val := 1 - t,
-  inv := ∑' (n : ℕ), t ^ n,
+  inv := ∑' n : ℕ, t ^ n,
   val_inv := mul_neg_geom_series t h,
   inv_val := geom_series_mul_neg t h }
 
@@ -171,7 +171,7 @@ begin
   { have : (2:ℝ)⁻¹ < 1 := by cancel_denoms,
     linarith },
   simp only [inverse_one_sub t ht', norm_one, mul_one, set.mem_set_of_eq],
-  change ∥(∑' (n : ℕ), t ^ n)∥ ≤ _,
+  change ∥∑' n : ℕ, t ^ n∥ ≤ _,
   have := normed_ring.tsum_geometric_of_norm_lt_1 t ht',
   have : (1 - ∥t∥)⁻¹ ≤ 2,
   { rw ← inv_inv' (2:ℝ),

src/analysis/p_series.lean

@@ -92,7 +92,7 @@ namespace ennreal
 variable {f : ℕ → ennreal}
 
 lemma le_tsum_condensed (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) :
-  (∑' k, f k) ≤ f 0 + ∑' k : ℕ, (2 ^ k) * f (2 ^ k) :=
+  ∑' k, f k ≤ f 0 + ∑' k : ℕ, (2 ^ k) * f (2 ^ k) :=
 begin
   rw [ennreal.tsum_eq_supr_nat' (nat.tendsto_pow_at_top_at_top_of_one_lt _root_.one_lt_two)],
   refine supr_le (λ n, (finset.le_sum_condensed hf n).trans (add_le_add_left _ _)),
@@ -101,7 +101,7 @@ begin
 end
 
 lemma tsum_condensed_le (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) :
-  (∑' k : ℕ, (2 ^ k) * f (2 ^ k)) ≤ f 1 + 2 * ∑' k, f k :=
+  ∑' k : ℕ, (2 ^ k * f (2 ^ k)) ≤ f 1 + 2 * ∑' k, f k :=
 begin
   rw [ennreal.tsum_eq_supr_nat' (tendsto_at_top_mono nat.le_succ tendsto_id), two_mul, ← two_nsmul],
   refine supr_le (λ n, le_trans _ (add_le_add_left (nsmul_le_nsmul_of_le_right

src/analysis/specific_limits.lean

@@ -243,7 +243,7 @@ have (λ n, (∑ i in range n, r ^ i)) = (λ n, geom_series r n) := rfl,
 lemma summable_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : summable (λn:ℕ, r ^ n) :=
 ⟨_, has_sum_geometric_of_lt_1 h₁ h₂⟩
 
-lemma tsum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
+lemma tsum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : ∑'n:ℕ, r ^ n = (1 - r)⁻¹ :=
 (has_sum_geometric_of_lt_1 h₁ h₂).tsum_eq
 
 lemma has_sum_geometric_two : has_sum (λn:ℕ, ((1:ℝ)/2) ^ n) 2 :=
@@ -252,7 +252,7 @@ by convert has_sum_geometric_of_lt_1 _ _; 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 :=
 has_sum_geometric_two.tsum_eq
 
 lemma sum_geometric_two_le (n : ℕ) : ∑ (i : ℕ) in range n, (1 / (2 : ℝ)) ^ i ≤ 2 :=
@@ -274,7 +274,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 :=
 (has_sum_geometric_two' a).tsum_eq
 
 lemma nnreal.has_sum_geometric {r : ℝ≥0} (hr : r < 1) :
@@ -289,12 +289,12 @@ end
 lemma nnreal.summable_geometric {r : ℝ≥0} (hr : r < 1) : summable (λn:ℕ, r ^ n) :=
 ⟨_, nnreal.has_sum_geometric hr⟩
 
-lemma tsum_geometric_nnreal {r : ℝ≥0} (hr : r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
+lemma tsum_geometric_nnreal {r : ℝ≥0} (hr : r < 1) : ∑'n:ℕ, r ^ n = (1 - r)⁻¹ :=
 (nnreal.has_sum_geometric hr).tsum_eq
 
 /-- 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'⟩,
@@ -325,7 +325,7 @@ end
 lemma summable_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : summable (λn:ℕ, ξ ^ n) :=
 ⟨_, has_sum_geometric_of_norm_lt_1 h⟩
 
-lemma tsum_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : (∑'n:ℕ, ξ ^ n) = (1 - ξ)⁻¹ :=
+lemma tsum_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : ∑'n:ℕ, ξ ^ n = (1 - ξ)⁻¹ :=
 (has_sum_geometric_of_norm_lt_1 h).tsum_eq
 
 lemma has_sum_geometric_of_abs_lt_1 {r : ℝ} (h : abs r < 1) : has_sum (λn:ℕ, r ^ n) (1 - r)⁻¹ :=
@@ -334,7 +334,7 @@ has_sum_geometric_of_norm_lt_1 h
 lemma summable_geometric_of_abs_lt_1 {r : ℝ} (h : abs r < 1) : summable (λn:ℕ, r ^ n) :=
 summable_geometric_of_norm_lt_1 h
 
-lemma tsum_geometric_of_abs_lt_1 {r : ℝ} (h : abs r < 1) : (∑'n:ℕ, r ^ n) = (1 - r)⁻¹ :=
+lemma tsum_geometric_of_abs_lt_1 {r : ℝ} (h : abs r < 1) : ∑'n:ℕ, r ^ n = (1 - r)⁻¹ :=
 tsum_geometric_of_norm_lt_1 h
 
 /-- A geometric series in a normed field is summable iff the norm of the common ratio is less than
@@ -554,20 +554,20 @@ end
 /-- Bound for the sum of a geometric series in a normed ring.  This formula does not assume that the
 normed ring satisfies the axiom `∥1∥ = 1`. -/
 lemma normed_ring.tsum_geometric_of_norm_lt_1
-  (x : R) (h : ∥x∥ < 1) : ∥(∑' (n:ℕ), x ^ n)∥ ≤ ∥(1:R)∥ - 1 + (1 - ∥x∥)⁻¹ :=
+  (x : R) (h : ∥x∥ < 1) : ∥∑' n:ℕ, x ^ n∥ ≤ ∥(1:R)∥ - 1 + (1 - ∥x∥)⁻¹ :=
 begin
   rw tsum_eq_zero_add (normed_ring.summable_geometric_of_norm_lt_1 x h),
   simp only [pow_zero],
   refine le_trans (norm_add_le _ _) _,
-  have : ∥(∑' (b : ℕ), (λ n, x ^ (n + 1)) b)∥ ≤ (1 - ∥x∥)⁻¹ - 1,
+  have : ∥∑' b : ℕ, (λ n, x ^ (n + 1)) b∥ ≤ (1 - ∥x∥)⁻¹ - 1,
   { refine tsum_of_norm_bounded _ (λ b, norm_pow_le' _ (nat.succ_pos b)),
     convert (has_sum_nat_add_iff' 1).mpr (has_sum_geometric_of_lt_1 (norm_nonneg x) h),
     simp },
   linarith
 end
 
 lemma geom_series_mul_neg (x : R) (h : ∥x∥ < 1) :
-  (∑' (i:ℕ), x ^ i) * (1 - x) = 1 :=
+  (∑' i:ℕ, x ^ i) * (1 - x) = 1 :=
 begin
   have := ((normed_ring.summable_geometric_of_norm_lt_1 x h).has_sum.mul_right (1 - x)),
   refine tendsto_nhds_unique this.tendsto_sum_nat _,
@@ -579,7 +579,7 @@ begin
 end
 
 lemma mul_neg_geom_series (x : R) (h : ∥x∥ < 1) :
-  (1 - x) * (∑' (i:ℕ), x ^ i) = 1 :=
+  (1 - x) * ∑' i:ℕ, x ^ i = 1 :=
 begin
   have := (normed_ring.summable_geometric_of_norm_lt_1 x h).has_sum.mul_left (1 - x),
   refine tendsto_nhds_unique this.tendsto_sum_nat _,
@@ -624,7 +624,7 @@ end nnreal
 namespace ennreal
 
 theorem exists_pos_sum_of_encodable {ε : ennreal} (hε : 0 < ε) (ι) [encodable ι] :
-  ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ (∑' i, (ε' i : ennreal)) < ε :=
+  ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∑' i, (ε' i : ennreal) < ε :=
 begin
   rcases exists_between hε with ⟨r, h0r, hrε⟩,
   rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, hx⟩,

src/measure_theory/measure_space.lean

@@ -97,7 +97,7 @@ extension of the restricted measure. -/
 structure measure (α : Type*) [measurable_space α] extends outer_measure α :=
 (m_Union ⦃f : ℕ → set α⦄ :
   (∀ i, is_measurable (f i)) → pairwise (disjoint on f) →
-  measure_of (⋃ i, f i) = (∑' i, measure_of (f i)))
+  measure_of (⋃ i, f i) = ∑' i, measure_of (f i))
 (trimmed : to_outer_measure.trim = to_outer_measure)
 
 /-- Measure projections for a measure space.
@@ -121,7 +121,7 @@ namespace measure
 def of_measurable (m : Π (s : set α), is_measurable s → ennreal)
   (m0 : m ∅ is_measurable.empty = 0)
   (mU : ∀ {{f : ℕ → set α}} (h : ∀ i, is_measurable (f i)), pairwise (disjoint on f) →
-    m (⋃ i, f i) (is_measurable.Union h) = (∑' i, m (f i) (h i))) : measure α :=
+    m (⋃ i, f i) (is_measurable.Union h) = ∑' i, m (f i) (h i)) : measure α :=
 { m_Union := λ f hf hd,
   show induced_outer_measure m _ m0 (Union f) =
       ∑' i, induced_outer_measure m _ m0 (f i), begin
@@ -139,7 +139,7 @@ def of_measurable (m : Π (s : set α), is_measurable s → ennreal)
 lemma of_measurable_apply {m : Π (s : set α), is_measurable s → ennreal}
   {m0 : m ∅ is_measurable.empty = 0}
   {mU : ∀ {{f : ℕ → set α}} (h : ∀ i, is_measurable (f i)), pairwise (disjoint on f) →
-    m (⋃ i, f i) (is_measurable.Union h) = (∑' i, m (f i) (h i))}
+    m (⋃ i, f i) (is_measurable.Union h) = ∑' i, m (f i) (h i)}
   (s : set α) (hs : is_measurable s) : of_measurable m m0 mU s = m s hs :=
 induced_outer_measure_eq m0 mU hs
 
@@ -223,7 +223,7 @@ lemma exists_is_measurable_superset_iff_measure_eq_zero :
   (∃ t, s ⊆ t ∧ is_measurable t ∧ μ t = 0) ↔ μ s = 0 :=
 ⟨λ ⟨t, hst, _, ht⟩, measure_mono_null hst ht, exists_is_measurable_superset_of_null⟩
 
-theorem measure_Union_le [encodable β] (s : β → set α) : μ (⋃ i, s i) ≤ (∑' i, μ (s i)) :=
+theorem measure_Union_le [encodable β] (s : β → set α) : μ (⋃ i, s i) ≤ ∑' i, μ (s i) :=
 μ.to_outer_measure.Union _
 
 lemma measure_bUnion_le {s : set β} (hs : countable s) (f : β → set α) :
@@ -269,7 +269,7 @@ lemma measure_union_null_iff : μ (s₁ ∪ s₂) = 0 ↔ μ s₁ = 0 ∧ μ s
 
 lemma measure_Union [encodable β] {f : β → set α}
   (hn : pairwise (disjoint on f)) (h : ∀ i, is_measurable (f i)) :
-  μ (⋃ i, f i) = (∑' i, μ (f i)) :=
+  μ (⋃ i, f i) = ∑' i, μ (f i) :=
 begin
   rw [measure_eq_extend (is_measurable.Union h),
     extend_Union is_measurable.empty _ is_measurable.Union _ hn h],
@@ -311,7 +311,7 @@ end
 of the fibers `f ⁻¹' {y}`. -/
 lemma tsum_measure_preimage_singleton {s : set β} (hs : countable s) {f : α → β}
   (hf : ∀ y ∈ s, is_measurable (f ⁻¹' {y})) :
-  (∑' b : s, μ (f ⁻¹' {↑b})) = μ (f ⁻¹' s) :=
+  ∑' b : s, μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s) :=
 by rw [← set.bUnion_preimage_singleton, measure_bUnion hs (pairwise_on_disjoint_fiber _ _) hf]
 
 /-- If `s` is a `finset`, then the measure of its preimage can be found as the sum of measures
@@ -340,7 +340,7 @@ by { rw ← measure_bUnion_finset H h, exact measure_mono (subset_univ _) }
 
 lemma tsum_measure_le_measure_univ {s : ι → set α} (hs : ∀ i, is_measurable (s i))
   (H : pairwise (disjoint on s)) :
-  (∑' i, μ (s i)) ≤ μ (univ : set α) :=
+  ∑' i, μ (s i) ≤ μ (univ : set α) :=
 begin
   rw [ennreal.tsum_eq_supr_sum],
   exact supr_le (λ s, sum_measure_le_measure_univ (λ i hi, hs i) (λ i hi j hj hij, H i j hij))
@@ -459,7 +459,7 @@ end
 /-- One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of measurable sets such that
   ∑ μ sᵢ exists, then the limit superior of the sᵢ is a null set. -/
 lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∀ i, is_measurable (s i))
-  (hs' : (∑' i, μ (s i)) ≠ ⊤) : μ (limsup at_top s) = 0 :=
+  (hs' : ∑' i, μ (s i) ≠ ⊤) : μ (limsup at_top s) = 0 :=
 begin
   rw limsup_eq_infi_supr_of_nat',
   -- We will show that both `μ (⨅ n, ⨆ i, s (i + n))` and `0` are the limit of `μ (⊔ i, s (i + n))`
@@ -553,7 +553,7 @@ instance : has_add (measure α) :=
 ⟨λ μ₁ μ₂, {
   to_outer_measure := μ₁.to_outer_measure + μ₂.to_outer_measure,
   m_Union := λ s hs hd,
-    show μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑' i, μ₁ (s i) + μ₂ (s i),
+    show μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑' i, (μ₁ (s i) + μ₂ (s i)),
     by rw [ennreal.tsum_add, measure_Union hd hs, measure_Union hd hs],
   trimmed := by rw [outer_measure.trim_add, μ₁.trimmed, μ₂.trimmed] }⟩
 
@@ -1342,7 +1342,7 @@ ae_eq_bot.trans restrict_eq_zero
 /-- A version of the Borel-Cantelli lemma: if sᵢ is a sequence of measurable sets such that
 ∑ μ sᵢ exists, then for almost all x, x does not belong to almost all sᵢ. -/
 lemma ae_eventually_not_mem {s : ℕ → set α} (hs : ∀ i, is_measurable (s i))
-  (hs' : (∑' i, μ (s i)) ≠ ⊤) : ∀ᵐ x ∂ μ, ∀ᶠ n in at_top, x ∉ s n :=
+  (hs' : ∑' i, μ (s i) ≠ ⊤) : ∀ᵐ x ∂ μ, ∀ᶠ n in at_top, x ∉ s n :=
 begin
   refine measure_mono_null _ (measure_limsup_eq_zero hs hs'),
   rw ←set.le_eq_subset,