feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#…

…2171)

* more material on infinite sums

* minor fixes

* cleanup

* yury's comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/analysis/normed_space/banach.lean

@@ -145,13 +145,13 @@ begin
          ... = (1 / 2) ^ n * (C * ∥y∥) : by ring },
   have sNu : summable (λn, ∥u n∥),
   { refine summable_of_nonneg_of_le (λn, norm_nonneg _) ule _,
-    exact summable_mul_right _ (summable_geometric (by norm_num) (by norm_num)) },
+    exact summable.mul_right _ (summable_geometric (by norm_num) (by norm_num)) },
   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∥)) :
-      tsum_le_tsum ule sNu (summable_mul_right _ summable_geometric_two)
+      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]
@@ -164,7 +164,7 @@ begin
     { rw [sum_range_succ, f.map_add, IH, nat.iterate_succ'],
       simp [u, h, sub_eq_add_neg, add_comm, add_left_comm] } },
   have : tendsto (λn, (range n).sum u) at_top (𝓝 x) :=
-    tendsto_sum_nat_of_has_sum (has_sum_tsum su),
+    su.has_sum.tendsto_sum_nat,
   have L₁ : tendsto (λn, f((range n).sum u)) at_top (𝓝 (f x)) :=
     (f.continuous.tendsto _).comp this,
   simp only [fsumeq] at L₁,

src/analysis/normed_space/basic.lean

@@ -229,8 +229,11 @@ nnreal.coe_le_coe.2 $ dist_norm_norm_le g h
 lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (nnnorm x : ennreal) :=
 ennreal.of_real_eq_coe_nnreal _
 
+lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (nnnorm (x - y) : ennreal) :=
+by rw [edist_dist, dist_eq_norm, of_real_norm_eq_coe_nnnorm]
+
 lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (nnnorm x : ennreal) :=
-by { rw [edist_dist, dist_eq_norm, _root_.sub_zero, of_real_norm_eq_coe_nnnorm] }
+by rw [edist_eq_coe_nnnorm_sub, _root_.sub_zero]
 
 lemma nndist_add_add_le (g₁ g₂ h₁ h₂ : α) :
   nndist (g₁ + g₂) (h₁ + h₂) ≤ nndist g₁ h₁ + nndist g₂ h₂ :=
@@ -806,12 +809,13 @@ end restrict_scalars
 section summable
 open_locale classical
 open finset filter
-variables [normed_group α] [complete_space α]
+variables [normed_group α]
 
-lemma summable_iff_vanishing_norm {f : ι → α} :
-  summable f ↔ ∀ε > 0, ∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε :=
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → α} :
+  cauchy_seq (λ s : finset ι, s.sum f) ↔ ∀ε > 0, ∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε :=
 begin
-  simp only [summable_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
+  simp only [cauchy_seq_finset_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
   split,
   { assume h ε hε, refine h {x | ∥x∥ < ε} ε hε _, rw [ball_0_eq ε] },
   { assume h s ε hε hs,
@@ -821,24 +825,60 @@ begin
     exact ht u hu }
 end
 
-lemma summable_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
-  summable f :=
-summable_iff_vanishing_norm.2 $ assume ε hε,
-  let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hf ε hε in
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma summable_iff_vanishing_norm [complete_space α] {f : ι → α} :
+  summable f ↔ ∀ε > 0, ∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε :=
+by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm]
+
+lemma cauchy_seq_finset_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hg : summable g)
+  (h : ∀i, ∥f i∥ ≤ g i) : cauchy_seq (λ s : finset ι, s.sum f) :=
+cauchy_seq_finset_iff_vanishing_norm.2 $ assume ε hε,
+  let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hg ε hε in
   ⟨s, assume t ht,
     have ∥t.sum g∥ < ε := hs t ht,
     have nn : 0 ≤ t.sum g := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
     lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
       by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
 
+lemma cauchy_seq_finset_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) :
+  cauchy_seq (λ s : finset ι, s.sum f) :=
+cauchy_seq_finset_of_norm_bounded _ hf (assume i, le_refl _)
+
+/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
+its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
+with sum `a`. -/
+lemma has_sum_of_subseq_of_summable {f : ι → α} (hf : summable (λa, ∥f a∥))
+  {s : β → finset ι} {p : filter β} (hp : p ≠ ⊥)
+  (hs : tendsto s p at_top) {a : α} (ha : tendsto (λ b, (s b).sum f) p (𝓝 a)) :
+  has_sum f a :=
+tendsto_nhds_of_cauchy_seq_of_subseq (cauchy_seq_finset_of_summable_norm hf) hp hs ha
+
+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)∥) :=
+      (continuous_norm.tendsto _).comp h.has_sum,
+    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₂ (univ_mem_sets' (assume s, norm_sum_le _ _)) },
+  { rw tsum_eq_zero_of_not_summable h,
+    simp [tsum_nonneg] }
+end
+
+variable [complete_space α]
+
+lemma summable_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hg : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
+  summable f :=
+by { rw summable_iff_cauchy_seq_finset, exact cauchy_seq_finset_of_norm_bounded g hg h }
+
+lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → nnreal) (hg : summable g)
+  (h : ∀i, nnnorm (f i) ≤ g i) : summable f :=
+summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
+
 lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
 summable_of_norm_bounded _ hf (assume i, le_refl _)
 
-lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
-have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (𝓝 ∥(∑ i, f i)∥) :=
-  (continuous_norm.tendsto _).comp (has_sum_tsum $ summable_of_summable_norm hf),
-have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (𝓝 (∑ i, ∥f i∥)) :=
-  has_sum_tsum hf,
-le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_sum_le _ _
+lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λa, nnnorm (f a))) : summable f :=
+summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
 
 end summable

src/analysis/specific_limits.lean

@@ -183,6 +183,13 @@ tendsto_inv_at_top_zero.comp (tendsto_coe_nat_real_at_top_iff.2 tendsto_id)
 lemma tendsto_const_div_at_top_nhds_0_nat (C : ℝ) : tendsto (λ n : ℕ, C / n) at_top (𝓝 0) :=
 by simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_at_top_nhds_0_nat
 
+lemma nnreal.tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : nnreal)⁻¹) at_top (𝓝 0) :=
+by { rw ← nnreal.tendsto_coe, convert tendsto_inverse_at_top_nhds_0_nat, simp }
+
+lemma nnreal.tendsto_const_div_at_top_nhds_0_nat (C : nnreal) :
+  tendsto (λ n : ℕ, C / n) at_top (𝓝 0) :=
+by simpa using tendsto_const_nhds.mul nnreal.tendsto_inverse_at_top_nhds_0_nat
+
 lemma tendsto_one_div_add_at_top_nhds_0_nat :
   tendsto (λ n : ℕ, 1 / ((n : ℝ) + 1)) at_top (𝓝 0) :=
 suffices tendsto (λ n : ℕ, 1 / (↑(n + 1) : ℝ)) at_top (𝓝 0), by simpa,
@@ -216,7 +223,7 @@ tsum_eq_has_sum has_sum_geometric_two
 
 lemma has_sum_geometric_two' (a : ℝ) : has_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=
 begin
-  convert has_sum_mul_left (a / 2) (has_sum_geometric
+  convert has_sum.mul_left (a / 2) (has_sum_geometric
     (le_of_lt one_half_pos) one_half_lt_one),
   { funext n, simp, refl, },
   { norm_num, rw div_mul_cancel, norm_num }
@@ -268,7 +275,7 @@ begin
   have hf : has_sum f ε := has_sum_geometric_two' _,
   have f0 : ∀ n, 0 < f n := λ n, div_pos (half_pos hε) (pow_pos two_pos _),
   refine ⟨f ∘ encodable.encode, λ i, f0 _, _⟩,
-  rcases summable_comp_of_summable_of_injective f (summable_spec hf) (@encodable.encode_injective ι _)
+  rcases hf.summable.summable_comp_of_injective (@encodable.encode_injective ι _)
     with ⟨c, hg⟩,
   refine ⟨c, hg, has_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
   { assume i _, exact le_of_lt (f0 _) },
@@ -287,7 +294,7 @@ then `f` is a Cauchy sequence.-/
 lemma cauchy_seq_of_edist_le_geometric : cauchy_seq f :=
 begin
   refine cauchy_seq_of_edist_le_of_tsum_ne_top _ hu _,
-  rw [ennreal.mul_tsum, ennreal.tsum_geometric],
+  rw [ennreal.tsum_mul_left, ennreal.tsum_geometric],
   refine ennreal.mul_ne_top hC (ennreal.inv_ne_top.2 _),
   exact ne_of_gt (ennreal.zero_lt_sub_iff_lt.2 hr)
 end
@@ -300,7 +307,7 @@ lemma edist_le_of_edist_le_geometric_of_tendsto {a : α} (ha : tendsto f at_top
   edist (f n) a ≤ (C * r^n) / (1 - r) :=
 begin
   convert edist_le_tsum_of_edist_le_of_tendsto _ hu ha _,
-  simp only [pow_add, ennreal.mul_tsum, ennreal.tsum_geometric, ennreal.div_def, mul_assoc]
+  simp only [pow_add, ennreal.tsum_mul_left, ennreal.tsum_geometric, ennreal.div_def, mul_assoc]
 end
 
 /-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, then the distance from
@@ -363,13 +370,13 @@ begin
   { simp [has_sum_zero] },
   { have rnonneg: r ≥ 0, from nonneg_of_mul_nonneg_left
       (by simpa only [pow_one] using le_trans dist_nonneg (hu 1)) Cpos,
-    refine has_sum_mul_left C _,
+    refine has_sum.mul_left C _,
     by simpa using has_sum_geometric rnonneg hr }
 end
 
 variables (r C)
 
-/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence.
+/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence.
 Note that this lemma does not assume `0 ≤ C` or `0 ≤ r`. -/
 lemma cauchy_seq_of_le_geometric : cauchy_seq f :=
 cauchy_seq_of_dist_le_of_summable _ hu ⟨_, aux_has_sum_of_le_geometric hr hu⟩
@@ -390,7 +397,7 @@ begin
   convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n,
   simp only [pow_add, mul_left_comm C, mul_div_right_comm],
   rw [mul_comm],
-  exact (eq.symm $ tsum_eq_has_sum $ has_sum_mul_left _ this)
+  exact (eq.symm $ tsum_eq_has_sum $ this.mul_left _)
 end
 
 omit hr hu
@@ -417,11 +424,44 @@ begin
   convert dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n,
   simp only [add_comm n, pow_add, (div_div_eq_div_mul _ _ _).symm],
   symmetry,
-  exact tsum_eq_has_sum (has_sum_mul_right _ $ has_sum_geometric_two' C)
+  exact tsum_eq_has_sum (has_sum.mul_right _ $ has_sum_geometric_two' C)
 end
 
 end le_geometric
 
+section summable_le_geometric
+
+variables [normed_group α] {r C : ℝ} {f : ℕ → α}
+
+lemma dist_partial_sum_le_of_le_geometric (hf : ∀n, ∥f n∥ ≤ C * r^n) (n : ℕ) :
+  dist ((finset.range n).sum f) ((finset.range (n+1)).sum f) ≤ C * r ^ n :=
+begin
+  rw [sum_range_succ, dist_eq_norm, ← norm_neg],
+  convert hf n,
+  abel
+end
+
+/-- If `∥f n∥ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` form a
+Cauchy sequence. This lemma does not assume `0 ≤ r` or `0 ≤ C`. -/
+lemma cauchy_seq_finset_of_geometric_bound (hr : r < 1) (hf : ∀n, ∥f n∥ ≤ C * r^n) :
+  cauchy_seq (λ s : finset (ℕ), s.sum f) :=
+cauchy_seq_finset_of_norm_bounded _
+  (aux_has_sum_of_le_geometric hr (dist_partial_sum_le_of_le_geometric hf)).summable hf
+
+/-- If `∥f n∥ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` are within
+distance `C * r ^ n / (1 - r)` of the sum of the series. This lemma does not assume `0 ≤ r` or
+`0 ≤ C`. -/
+lemma norm_sub_le_of_geometric_bound_of_has_sum (hr : r < 1) (hf : ∀n, ∥f n∥ ≤ C * r^n)
+  {a : α} (ha : has_sum f a) (n : ℕ) :
+  ∥(finset.range n).sum f - a∥ ≤ (C * r ^ n) / (1 - r) :=
+begin
+  rw ← dist_eq_norm,
+  apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf),
+  exact ha.tendsto_sum_nat
+end
+
+end summable_le_geometric
+
 namespace nnreal
 
 theorem exists_pos_sum_of_encodable {ε : nnreal} (hε : 0 < ε) (ι) [encodable ι] :

src/data/option/basic.lean

@@ -172,4 +172,10 @@ by cases a; refl
 @[simp] lemma lift_or_get_some_some {f} {a b : α} :
   lift_or_get f (some a) (some b) = f a b := rfl
 
+/-- given an element of `a : option α`, a default element `b : β` and a function `α → β`, apply this
+function to `a` if it comes from `α`, and return `b` otherwise. -/
+def cases_on' : option α → β → (α → β) → β
+| none     n s := n
+| (some a) n s := s a
+
 end option

src/data/real/cardinality.lean

@@ -36,7 +36,7 @@ by { ext n, cases h : f (n + 1); simp [h, _root_.pow_succ] }
 lemma summable_cantor_function (f : ℕ → bool) (h1 : 0 ≤ c) (h2 : c < 1) :
   summable (cantor_function_aux c f) :=
 begin
-  apply summable_of_summable_of_sub _ _ (summable_geometric h1 h2),
+  apply (summable_geometric h1 h2).summable_of_eq_zero_or_self,
   intro n, cases h : f n; simp [h]
 end
 

src/measure_theory/outer_measure.lean

@@ -234,7 +234,7 @@ instance : has_scalar ennreal (outer_measure α) :=
   measure_of := λs, a * m s,
   empty := by simp,
   mono := λ s t h, canonically_ordered_semiring.mul_le_mul (le_refl _) (m.mono' h),
-  Union_nat := λ s, by rw ennreal.mul_tsum; exact
+  Union_nat := λ s, by rw ennreal.tsum_mul_left; exact
     canonically_ordered_semiring.mul_le_mul (le_refl _) (m.Union_nat _) }⟩
 
 @[simp] theorem smul_apply (a : ennreal) (m : outer_measure α) (s : set α) :

src/measure_theory/probability_mass_function.lean

@@ -22,7 +22,7 @@ instance : has_coe_to_fun (pmf α) := ⟨λp, α → nnreal, λp a, p.1 a⟩
 
 lemma has_sum_coe_one (p : pmf α) : has_sum p 1 := p.2
 
-lemma summable_coe (p : pmf α) : summable p := summable_spec p.has_sum_coe_one
+lemma summable_coe (p : pmf α) : summable p := (p.has_sum_coe_one).summable
 
 @[simp] lemma tsum_coe (p : pmf α) : (∑a, p a) = 1 := tsum_eq_has_sum p.has_sum_coe_one
 
@@ -49,8 +49,8 @@ def bind (p : pmf α) (f : α → pmf β) : pmf β :=
   begin
     apply ennreal.has_sum_coe.1,
     simp only [ennreal.coe_tsum (bind.summable p f _)],
-    rw [has_sum_iff_of_summable ennreal.summable, ennreal.tsum_comm],
-    simp [ennreal.mul_tsum, (ennreal.coe_tsum (f _).summable_coe).symm,
+    rw [ennreal.summable.has_sum_iff, ennreal.tsum_comm],
+    simp [ennreal.tsum_mul_left, (ennreal.coe_tsum (f _).summable_coe).symm,
       (ennreal.coe_tsum p.summable_coe).symm]
   end⟩
 
@@ -74,7 +74,8 @@ by ext b; simp [this]
   (p.bind f).bind g = p.bind (λa, (f a).bind g) :=
 begin
   ext b,
-  simp only [ennreal.coe_eq_coe.symm, coe_bind_apply, ennreal.mul_tsum.symm, ennreal.tsum_mul.symm],
+  simp only [ennreal.coe_eq_coe.symm, coe_bind_apply, ennreal.tsum_mul_left.symm,
+             ennreal.tsum_mul_right.symm],
   rw [ennreal.tsum_comm],
   simp [mul_assoc, mul_left_comm, mul_comm]
 end
@@ -83,7 +84,8 @@ lemma bind_comm (p : pmf α) (q : pmf β) (f : α → β → pmf γ) :
   p.bind (λa, q.bind (f a)) = q.bind (λb, p.bind (λa, f a b)) :=
 begin
   ext b,
-  simp only [ennreal.coe_eq_coe.symm, coe_bind_apply, ennreal.mul_tsum.symm, ennreal.tsum_mul.symm],
+  simp only [ennreal.coe_eq_coe.symm, coe_bind_apply, ennreal.tsum_mul_left.symm,
+             ennreal.tsum_mul_right.symm],
   rw [ennreal.tsum_comm],
   simp [mul_assoc, mul_left_comm, mul_comm]
 end

src/order/liminf_limsup.lean

@@ -426,5 +426,3 @@ end
 end conditionally_complete_linear_order
 
 end filter
-
-#lint