chore: move summable lemmas (#12503)

We move some lemmas out of `Topology/Instances/ENNReal` into `Topology/Algebra/InfiniteSum/Real`. Also use this to address a porting TODO.

This was originally part of #12446 



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Manuel Candales. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
-import Mathlib.Topology.Instances.ENNReal
+import Mathlib.Topology.Algebra.InfiniteSum.Real
 import Mathlib.Data.Nat.Squarefree
 
 #align_import wiedijk_100_theorems.sum_of_prime_reciprocals_diverges from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"

Mathlib/Analysis/Normed/Field/InfiniteSum.lean

@@ -5,7 +5,7 @@ Authors: Anatole Dedecker
 -/
 import Mathlib.Analysis.Normed.Field.Basic
 import Mathlib.Analysis.Normed.Group.InfiniteSum
-import Mathlib.Topology.Instances.ENNReal
+import Mathlib.Topology.Algebra.InfiniteSum.Real
 
 #align_import analysis.normed.field.infinite_sum from "leanprover-community/mathlib"@"008205aa645b3f194c1da47025c5f110c8406eab"
 
@@ -67,7 +67,6 @@ In order to avoid `Nat` subtraction, we also provide
 where the `n`-th term is a sum over all pairs `(k, l)` such that `k+l=n`, which corresponds to the
 `Finset` `Finset.antidiagonal n`. -/
 
-
 section Nat
 
 open Finset.Nat

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -6,8 +6,8 @@ Authors: Sébastien Gouëzel, Johannes Hölzl, Yury G. Kudryashov, Patrick Masso
 import Mathlib.Algebra.GeomSum
 import Mathlib.Order.Filter.Archimedean
 import Mathlib.Order.Iterate
-import Mathlib.Topology.Instances.ENNReal
 import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.InfiniteSum.Real
 
 #align_import analysis.specific_limits.basic from "leanprover-community/mathlib"@"57ac39bd365c2f80589a700f9fbb664d3a1a30c2"
 

Mathlib/Topology/Algebra/InfiniteSum/Real.lean

@@ -6,63 +6,30 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Topology.Algebra.InfiniteSum.Order
 import Mathlib.Topology.Instances.Real
+import Mathlib.Topology.Instances.ENNReal
 
 #align_import topology.algebra.infinite_sum.real from "leanprover-community/mathlib"@"9a59dcb7a2d06bf55da57b9030169219980660cd"
 
 /-!
 # Infinite sum in the reals
 
-This file provides lemmas about Cauchy sequences in terms of infinite sums.
+This file provides lemmas about Cauchy sequences in terms of infinite sums and infinite sums valued
+in the reals.
 -/
 
 open Filter Finset BigOperators NNReal Topology
 
-variable {α : Type*}
-
-/-- If the extended distance between consecutive points of a sequence is estimated
-by a summable series of `NNReal`s, then the original sequence is a Cauchy sequence. -/
-theorem cauchySeq_of_edist_le_of_summable [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ≥0)
-    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : Summable d) : CauchySeq f := by
-  refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_
-  -- Actually we need partial sums of `d` to be a Cauchy sequence
-  replace hd : CauchySeq fun n : ℕ ↦ ∑ x in range n, d x :=
-    let ⟨_, H⟩ := hd
-    H.tendsto_sum_nat.cauchySeq
-  -- Now we take the same `N` as in one of the definitions of a Cauchy sequence
-  refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_
-  specialize hN n hn
-  -- We simplify the known inequality
-  rw [dist_nndist, NNReal.nndist_eq, ← sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
-    NNReal.coe_lt_coe, max_lt_iff] at hN
-  rw [edist_comm]
-  -- Then use `hf` to simplify the goal to the same form
-  refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_
-  exact mod_cast hN.1
-#align cauchy_seq_of_edist_le_of_summable cauchySeq_of_edist_le_of_summable
-
-variable [PseudoMetricSpace α] {f : ℕ → α} {a : α}
+variable {α β : Type*} [PseudoMetricSpace α] {f : ℕ → α} {a : α}
 
 /-- If the distance between consecutive points of a sequence is estimated by a summable series,
 then the original sequence is a Cauchy sequence. -/
 theorem cauchySeq_of_dist_le_of_summable (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
     (hd : Summable d) : CauchySeq f := by
-  -- Porting note (#11215): TODO: with `Topology.Instances.NNReal` we can use this:
-  -- lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)
-  -- refine cauchySeq_of_edist_le_of_summable d ?_ ?_
-  -- · exact_mod_cast hf
-  -- · exact_mod_cast hd
-  refine' Metric.cauchySeq_iff'.2 fun ε εpos ↦ _
-  replace hd : CauchySeq fun n : ℕ ↦ ∑ x in range n, d x :=
-    let ⟨_, H⟩ := hd
-    H.tendsto_sum_nat.cauchySeq
-  refine' (Metric.cauchySeq_iff'.1 hd ε εpos).imp fun N hN n hn ↦ _
-  have hsum := hN n hn
-  rw [Real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum
-  calc
-    dist (f n) (f N) = dist (f N) (f n) := dist_comm _ _
-    _ ≤ ∑ x in Ico N n, d x := dist_le_Ico_sum_of_dist_le hn fun _ _ ↦ hf _
-    _ ≤ |∑ x in Ico N n, d x| := le_abs_self _
-    _ < ε := hsum
+  lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)
+  apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)
+  · exact_mod_cast hf
+  · exact_mod_cast hd
+
 #align cauchy_seq_of_dist_le_of_summable cauchySeq_of_dist_le_of_summable
 
 theorem cauchySeq_of_summable_dist (h : Summable fun n ↦ dist (f n) (f n.succ)) : CauchySeq f :=
@@ -94,3 +61,54 @@ theorem dist_le_tsum_dist_of_tendsto₀ (h : Summable fun n ↦ dist (f n) (f n.
     (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ ∑' n, dist (f n) (f n.succ) := by
   simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0
 #align dist_le_tsum_dist_of_tendsto₀ dist_le_tsum_dist_of_tendsto₀
+
+section summable
+
+theorem not_summable_iff_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
+    ¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i in Finset.range n, f i) atTop atTop := by
+  lift f to ℕ → ℝ≥0 using hf
+  exact mod_cast NNReal.not_summable_iff_tendsto_nat_atTop
+#align not_summable_iff_tendsto_nat_at_top_of_nonneg not_summable_iff_tendsto_nat_atTop_of_nonneg
+
+theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
+    Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i in Finset.range n, f i) atTop atTop := by
+  rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]
+#align summable_iff_not_tendsto_nat_at_top_of_nonneg summable_iff_not_tendsto_nat_atTop_of_nonneg
+
+theorem summable_sigma_of_nonneg {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
+    Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩ := by
+  lift f to (Σx, β x) → ℝ≥0 using hf
+  exact mod_cast NNReal.summable_sigma
+#align summable_sigma_of_nonneg summable_sigma_of_nonneg
+
+theorem summable_prod_of_nonneg {f : (α × β) → ℝ} (hf : 0 ≤ f) :
+    Summable f ↔ (∀ x, Summable fun y ↦ f (x, y)) ∧ Summable fun x ↦ ∑' y, f (x, y) :=
+  (Equiv.sigmaEquivProd _ _).summable_iff.symm.trans <| summable_sigma_of_nonneg fun _ ↦ hf _
+
+theorem summable_of_sum_le {ι : Type*} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f)
+    (h : ∀ u : Finset ι, ∑ x in u, f x ≤ c) : Summable f :=
+  ⟨⨆ u : Finset ι, ∑ x in u, f x,
+    tendsto_atTop_ciSup (Finset.sum_mono_set_of_nonneg hf) ⟨c, fun _ ⟨u, hu⟩ => hu ▸ h u⟩⟩
+#align summable_of_sum_le summable_of_sum_le
+
+theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
+    (h : ∀ n, ∑ i in Finset.range n, f i ≤ c) : Summable f := by
+  refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
+  rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
+  exact lt_irrefl _ (hn.trans_le (h n))
+#align summable_of_sum_range_le summable_of_sum_range_le
+
+theorem Real.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
+    (h : ∀ n, ∑ i in Finset.range n, f i ≤ c) : ∑' n, f n ≤ c :=
+  _root_.tsum_le_of_sum_range_le (summable_of_sum_range_le hf h) h
+#align real.tsum_le_of_sum_range_le Real.tsum_le_of_sum_range_le
+
+/-- If a sequence `f` with non-negative terms is dominated by a sequence `g` with summable
+series and at least one term of `f` is strictly smaller than the corresponding term in `g`,
+then the series of `f` is strictly smaller than the series of `g`. -/
+theorem tsum_lt_tsum_of_nonneg {i : ℕ} {f g : ℕ → ℝ} (h0 : ∀ b : ℕ, 0 ≤ f b)
+    (h : ∀ b : ℕ, f b ≤ g b) (hi : f i < g i) (hg : Summable g) : ∑' n, f n < ∑' n, g n :=
+  tsum_lt_tsum h hi (.of_nonneg_of_le h0 h hg) hg
+#align tsum_lt_tsum_of_nonneg tsum_lt_tsum_of_nonneg
+
+end summable

Mathlib/Topology/Instances/ENNReal.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Topology.Order.MonotoneContinuity
-import Mathlib.Topology.Algebra.InfiniteSum.Real
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
 import Mathlib.Topology.Instances.NNReal
 import Mathlib.Topology.EMetricSpace.Lipschitz
@@ -1352,53 +1351,6 @@ theorem ENNReal.ofReal_tsum_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤
   simp_rw [ENNReal.ofReal, ENNReal.tsum_coe_eq (NNReal.hasSum_real_toNNReal_of_nonneg hf_nonneg hf)]
 #align ennreal.of_real_tsum_of_nonneg ENNReal.ofReal_tsum_of_nonneg
 
-theorem not_summable_iff_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
-    ¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i in Finset.range n, f i) atTop atTop := by
-  lift f to ℕ → ℝ≥0 using hf
-  exact mod_cast NNReal.not_summable_iff_tendsto_nat_atTop
-#align not_summable_iff_tendsto_nat_at_top_of_nonneg not_summable_iff_tendsto_nat_atTop_of_nonneg
-
-theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
-    Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i in Finset.range n, f i) atTop atTop := by
-  rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]
-#align summable_iff_not_tendsto_nat_at_top_of_nonneg summable_iff_not_tendsto_nat_atTop_of_nonneg
-
-theorem summable_sigma_of_nonneg {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
-    Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩ := by
-  lift f to (Σx, β x) → ℝ≥0 using hf
-  exact mod_cast NNReal.summable_sigma
-#align summable_sigma_of_nonneg summable_sigma_of_nonneg
-
-theorem summable_prod_of_nonneg {f : (α × β) → ℝ} (hf : 0 ≤ f) :
-    Summable f ↔ (∀ x, Summable fun y ↦ f (x, y)) ∧ Summable fun x ↦ ∑' y, f (x, y) :=
-  (Equiv.sigmaEquivProd _ _).summable_iff.symm.trans <| summable_sigma_of_nonneg fun _ ↦ hf _
-
-theorem summable_of_sum_le {ι : Type*} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f)
-    (h : ∀ u : Finset ι, ∑ x in u, f x ≤ c) : Summable f :=
-  ⟨⨆ u : Finset ι, ∑ x in u, f x,
-    tendsto_atTop_ciSup (Finset.sum_mono_set_of_nonneg hf) ⟨c, fun _ ⟨u, hu⟩ => hu ▸ h u⟩⟩
-#align summable_of_sum_le summable_of_sum_le
-
-theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
-    (h : ∀ n, ∑ i in Finset.range n, f i ≤ c) : Summable f := by
-  refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
-  rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
-  exact lt_irrefl _ (hn.trans_le (h n))
-#align summable_of_sum_range_le summable_of_sum_range_le
-
-theorem Real.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
-    (h : ∀ n, ∑ i in Finset.range n, f i ≤ c) : ∑' n, f n ≤ c :=
-  _root_.tsum_le_of_sum_range_le (summable_of_sum_range_le hf h) h
-#align real.tsum_le_of_sum_range_le Real.tsum_le_of_sum_range_le
-
-/-- If a sequence `f` with non-negative terms is dominated by a sequence `g` with summable
-series and at least one term of `f` is strictly smaller than the corresponding term in `g`,
-then the series of `f` is strictly smaller than the series of `g`. -/
-theorem tsum_lt_tsum_of_nonneg {i : ℕ} {f g : ℕ → ℝ} (h0 : ∀ b : ℕ, 0 ≤ f b)
-    (h : ∀ b : ℕ, f b ≤ g b) (hi : f i < g i) (hg : Summable g) : ∑' n, f n < ∑' n, g n :=
-  tsum_lt_tsum h hi (.of_nonneg_of_le h0 h hg) hg
-#align tsum_lt_tsum_of_nonneg tsum_lt_tsum_of_nonneg
-
 section
 
 variable [EMetricSpace β]
@@ -1497,6 +1449,27 @@ theorem Filter.Tendsto.edist {f g : β → α} {x : Filter β} {a b : α} (hf :
   (continuous_edist.tendsto (a, b)).comp (hf.prod_mk_nhds hg)
 #align filter.tendsto.edist Filter.Tendsto.edist
 
+/-- If the extended distance between consecutive points of a sequence is estimated
+by a summable series of `NNReal`s, then the original sequence is a Cauchy sequence. -/
+theorem cauchySeq_of_edist_le_of_summable [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ≥0)
+    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : Summable d) : CauchySeq f := by
+  refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_
+  -- Actually we need partial sums of `d` to be a Cauchy sequence.
+  replace hd : CauchySeq fun n : ℕ ↦ ∑ x in Finset.range n, d x :=
+    let ⟨_, H⟩ := hd
+    H.tendsto_sum_nat.cauchySeq
+  -- Now we take the same `N` as in one of the definitions of a Cauchy sequence.
+  refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_
+  specialize hN n hn
+  -- We simplify the known inequality.
+  rw [dist_nndist, NNReal.nndist_eq, ← Finset.sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
+    NNReal.coe_lt_coe, max_lt_iff] at hN
+  rw [edist_comm]
+  -- Then use `hf` to simplify the goal to the same form.
+  refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_
+  exact mod_cast hN.1
+#align cauchy_seq_of_edist_le_of_summable cauchySeq_of_edist_le_of_summable
+
 theorem cauchySeq_of_edist_le_of_tsum_ne_top {f : ℕ → α} (d : ℕ → ℝ≥0∞)
     (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : tsum d ≠ ∞) : CauchySeq f := by
   lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i