feat(*): a few more tests for summable, docstrings (#4325)

### Important new theorems:

* `summable_geometric_iff_norm_lt_1`: a geometric series in a normed field is summable iff the norm of the common ratio is less than 1;
* `summable.tendsto_cofinite_zero`: divergence test: if `f` is a `summable` function, then `f x` tends to zero along `cofinite`;

### API change

* rename `cauchy_seq_of_tendsto_nhds` to `filter.tendsto.cauchy_seq` to enable dot syntax.

src/analysis/specific_limits.lean

@@ -258,6 +258,18 @@ summable_geometric_of_norm_lt_1 h
 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
+one. -/
+@[simp] lemma summable_geometric_iff_norm_lt_1 : summable (λ n : ℕ, ξ ^ n) ↔ ∥ξ∥ < 1 :=
+begin
+  refine ⟨λ h, _, summable_geometric_of_norm_lt_1⟩,
+  obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
+    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists,
+  simp only [normed_field.norm_pow, dist_zero_right] at hk,
+  rw [← one_pow k] at hk,
+  exact lt_of_pow_lt_pow _ zero_le_one hk
+end
+
 end geometric
 
 /-!

src/order/filter/cofinite.lean

@@ -22,10 +22,10 @@ Define filters for other cardinalities of the complement.
 open set
 open_locale classical
 
-namespace filter
-
 variables {α : Type*}
 
+namespace filter
+
 /-- The cofinite filter is the filter of subsets whose complements are finite. -/
 def cofinite : filter α :=
 { sets             := {s | finite sᶜ},
@@ -49,7 +49,16 @@ end filter
 
 open filter
 
-lemma set.infinite_iff_frequently_cofinite {α : Type*} {s : set α} :
+lemma set.finite.compl_mem_cofinite {s : set α} (hs : s.finite) : sᶜ ∈ (@cofinite α) :=
+mem_cofinite.2 $ (compl_compl s).symm ▸ hs
+
+lemma set.finite.eventually_cofinite_nmem {s : set α} (hs : s.finite) : ∀ᶠ x in cofinite, x ∉ s :=
+hs.compl_mem_cofinite
+
+lemma finset.eventually_cofinite_nmem (s : finset α) : ∀ᶠ x in cofinite, x ∉ s :=
+s.finite_to_set.eventually_cofinite_nmem
+
+lemma set.infinite_iff_frequently_cofinite {s : set α} :
   set.infinite s ↔ (∃ᶠ x in cofinite, x ∈ s) :=
 frequently_cofinite_iff_infinite.symm
 

src/topology/algebra/infinite_sum.lean

@@ -707,13 +707,12 @@ end canonically_ordered
 section uniform_group
 
 variables [add_comm_group α] [uniform_space α]
-variables {f g : β → α} {a a₁ a₂ : α}
 
-lemma summable_iff_cauchy_seq_finset [complete_space α] :
+lemma summable_iff_cauchy_seq_finset [complete_space α] {f : β → α} :
   summable f ↔ cauchy_seq (λ (s : finset β), ∑ b in s, f b) :=
 cauchy_map_iff_exists_tendsto.symm
 
-variable [uniform_add_group α]
+variables [uniform_add_group α] {f g : β → α} {a a₁ a₂ : α}
 
 lemma cauchy_seq_finset_iff_vanishing :
   cauchy_seq (λ (s : finset β), ∑ b in s, f b)
@@ -809,6 +808,33 @@ tsum_comm' h h.prod_factor h.prod_symm.prod_factor
 
 end uniform_group
 
+section topological_group
+
+variables {G : Type*} [topological_space G] [add_comm_group G] [topological_add_group G]
+  {f : α → G}
+
+lemma summable.vanishing (hf : summable f) ⦃e : set G⦄ (he : e ∈ 𝓝 (0 : G)) :
+  ∃ s : finset α, ∀ t, disjoint t s → ∑ k in t, f k ∈ e :=
+begin
+  letI : uniform_space G := topological_add_group.to_uniform_space G,
+  letI : uniform_add_group G := topological_add_group_is_uniform,
+  rcases hf with ⟨y, hy⟩,
+  exact cauchy_seq_finset_iff_vanishing.1 hy.cauchy_seq e he
+end
+
+/-- Series divergence test: if `f` is a convergent series, then `f x` tends to zero along
+`cofinite`. -/
+lemma summable.tendsto_cofinite_zero (hf : summable f) : tendsto f cofinite (𝓝 0) :=
+begin
+  intros e he,
+  rw [filter.mem_map],
+  rcases hf.vanishing he with ⟨s, hs⟩,
+  refine s.eventually_cofinite_nmem.mono (λ x hx, _),
+  by simpa using hs {x} (singleton_disjoint.2 hx)
+end
+
+end topological_group
+
 section cauchy_seq
 open finset.Ico filter
 
@@ -820,7 +846,7 @@ begin
   refine emetric.cauchy_seq_iff_nnreal.2 (λ ε εpos, _),
   -- Actually we need partial sums of `d` to be a Cauchy sequence
   replace hd : cauchy_seq (λ (n : ℕ), ∑ x in range n, d x) :=
-    let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ H.tendsto_sum_nat,
+    let ⟨_, H⟩ := hd in H.tendsto_sum_nat.cauchy_seq,
   -- Now we take the same `N` as in one of the definitions of a Cauchy sequence
   refine (metric.cauchy_seq_iff'.1 hd ε (nnreal.coe_pos.2 εpos)).imp (λ N hN n hn, _),
   have hsum := hN n hn,
@@ -842,7 +868,7 @@ lemma cauchy_seq_of_dist_le_of_summable [metric_space α] {f : ℕ → α} (d :
 begin
   refine metric.cauchy_seq_iff'.2 (λε εpos, _),
   replace hd : cauchy_seq (λ (n : ℕ), ∑ x in range n, d x) :=
-    let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ H.tendsto_sum_nat,
+    let ⟨_, H⟩ := hd in H.tendsto_sum_nat.cauchy_seq,
   refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _),
   have hsum := hN n hn,
   rw [real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum,

src/topology/instances/ennreal.lean

@@ -526,6 +526,13 @@ tsum_le_tsum h ennreal.summable ennreal.summable
 protected lemma sum_le_tsum {f : α → ennreal} (s : finset α) : ∑ x in s, f x ≤ ∑' x, f x :=
 sum_le_tsum s (λ x hx, zero_le _) ennreal.summable
 
+protected lemma tsum_eq_supr_nat' {f : ℕ → ennreal} {N : ℕ → ℕ} (hN : tendsto N at_top at_top) :
+  (∑'i:ℕ, f i) = (⨆i:ℕ, ∑ a in finset.range (N i), f a) :=
+ennreal.tsum_eq_supr_sum' _ $ λ t,
+  let ⟨n, hn⟩    := t.exists_nat_subset_range,
+      ⟨k, _, hk⟩ := exists_le_of_tendsto_at_top hN 0 n in
+  ⟨k, finset.subset.trans hn (finset.range_mono hk)⟩
+
 protected lemma tsum_eq_supr_nat {f : ℕ → ennreal} :
   (∑'i:ℕ, f i) = (⨆i:ℕ, ∑ a in finset.range i, f a) :=
 ennreal.tsum_eq_supr_sum' _ finset.exists_nat_subset_range
@@ -594,7 +601,10 @@ end ennreal
 
 namespace nnreal
 
-lemma exists_le_has_sum_of_le {f g : β → nnreal} {r : nnreal}
+open_locale nnreal
+
+/-- Comparison test of convergence of `ℝ≥0`-valued series. -/
+lemma exists_le_has_sum_of_le {f g : β → ℝ≥0} {r : ℝ≥0}
   (hgf : ∀b, g b ≤ f b) (hfr : has_sum f r) : ∃p≤r, has_sum g p :=
 have (∑'b, (g b : ennreal)) ≤ r,
 begin
@@ -604,25 +614,28 @@ end,
 let ⟨p, eq, hpr⟩ := ennreal.le_coe_iff.1 this in
 ⟨p, hpr, ennreal.has_sum_coe.1 $ eq ▸ ennreal.summable.has_sum⟩
 
-lemma summable_of_le {f g : β → nnreal} (hgf : ∀b, g b ≤ f b) : summable f → summable g
+/-- Comparison test of convergence of `ℝ≥0`-valued series. -/
+lemma summable_of_le {f g : β → ℝ≥0} (hgf : ∀b, g b ≤ f b) : summable f → summable g
 | ⟨r, hfr⟩ := let ⟨p, _, hp⟩ := exists_le_has_sum_of_le hgf hfr in hp.summable
 
-lemma has_sum_iff_tendsto_nat {f : ℕ → nnreal} (r : nnreal) :
+/-- A series of non-negative real numbers converges to `r` in the sense of `has_sum` if and only if
+the sequence of partial sum converges to `r`. -/
+lemma has_sum_iff_tendsto_nat {f : ℕ → ℝ≥0} (r : ℝ≥0) :
   has_sum f r ↔ tendsto (λn:ℕ, ∑ i in finset.range n, f i) at_top (𝓝 r) :=
 begin
   rw [← ennreal.has_sum_coe, ennreal.has_sum_iff_tendsto_nat],
   simp only [ennreal.coe_finset_sum.symm],
   exact ennreal.tendsto_coe
 end
 
-lemma tsum_comp_le_tsum_of_inj {β : Type*} {f : α → nnreal} (hf : summable f)
-  {i : β → α} (hi : function.injective i) : tsum (f ∘ i) ≤ tsum f :=
+lemma tsum_comp_le_tsum_of_inj {β : Type*} {f : α → ℝ≥0} (hf : summable f)
+  {i : β → α} (hi : function.injective i) : (∑' x, f (i x)) ≤ ∑' x, f x :=
 tsum_le_tsum_of_inj i hi (λ c hc, zero_le _) (λ b, le_refl _) (summable_comp_injective hf hi) hf
 
 open finset
 
 /-- If `f : ℕ → ℝ≥0` and `∑' f` exists, then `∑' k, f (k + i)` tends to zero. -/
-lemma tendsto_sum_nat_add (f : ℕ → nnreal) (hf : summable f) :
+lemma tendsto_sum_nat_add (f : ℕ → ℝ≥0) (hf : summable f) :
   tendsto (λ i, ∑' k, f (k + i)) at_top (𝓝 0) :=
 begin
   have h₀ : (λ i, (∑' i, f i) - ∑ j in range i, f j) = λ i, ∑' (k : ℕ), f (k + i),
@@ -659,6 +672,7 @@ begin
   { rw nnreal.coe_tsum, congr }
 end
 
+/-- Comparison test of convergence of series of non-negative real numbers. -/
 lemma summable_of_nonneg_of_le {f g : β → ℝ}
   (hg : ∀b, 0 ≤ g b) (hgf : ∀b, g b ≤ f b) (hf : summable f) : summable g :=
 let f' (b : β) : nnreal := ⟨f b, le_trans (hg b) (hgf b)⟩ in
@@ -668,6 +682,8 @@ have summable g', from
   nnreal.summable_of_le (assume b, (@nnreal.coe_le_coe (g' b) (f' b)).2 $ hgf b) this,
 show summable (λb, g' b : β → ℝ), from nnreal.summable_coe.2 this
 
+/-- A series of non-negative real numbers converges to `r` in the sense of `has_sum` if and only if
+the sequence of partial sum converges to `r`. -/
 lemma has_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀i, 0 ≤ f i) (r : ℝ) :
   has_sum f r ↔ tendsto (λn:ℕ, ∑ i in finset.range n, f i) at_top (𝓝 r) :=
 ⟨has_sum.tendsto_sum_nat,

src/topology/sequences.lean

@@ -303,7 +303,7 @@ begin
   intros x x_in φ,
   intros hφ huφ,
   obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V,
-    from (cauchy_seq_of_tendsto_nhds _ huφ).mem_entourage V_in,
+    from huφ.cauchy_seq.mem_entourage V_in,
   specialize hN N (N+1) (le_refl N) (nat.le_succ N),
   specialize hu (φ $ N+1) (φ N) (hφ $ lt_add_one N),
   exact hu hN,

src/topology/uniform_space/cauchy.lean

@@ -70,6 +70,11 @@ lemma cauchy_nhds {a : α} : cauchy (𝓝 a) :=
 lemma cauchy_pure {a : α} : cauchy (pure a) :=
 cauchy_nhds.mono (pure_le_nhds a)
 
+lemma filter.tendsto.cauchy_map {l : filter β} [ne_bot l] {f : β → α} {a : α}
+  (h : tendsto f l (𝓝 a)) :
+  cauchy (map f l) :=
+cauchy_nhds.mono h
+
 /-- The common part of the proofs of `le_nhds_of_cauchy_adhp` and
 `sequentially_complete.le_nhds_of_seq_tendsto_nhds`: if for any entourage `s`
 one can choose a set `t ∈ f` of diameter `s` such that it contains a point `y`
@@ -144,10 +149,10 @@ begin
   exact H (i, j) ⟨le_of_max_le_left  hi, le_of_max_le_right hj⟩,
 end
 
-lemma cauchy_seq_of_tendsto_nhds [semilattice_sup β] [nonempty β] (f : β → α) {x}
+lemma filter.tendsto.cauchy_seq [semilattice_sup β] [nonempty β] {f : β → α} {x}
   (hx : tendsto f at_top (𝓝 x)) :
   cauchy_seq f :=
-cauchy_nhds.mono hx
+hx.cauchy_map
 
 lemma cauchy_seq_iff_tendsto [nonempty β] [semilattice_sup β] {u : β → α} :
   cauchy_seq u ↔ tendsto (prod.map u u) at_top (𝓤 α) :=