feat: port Topology.Instances.ENNReal (#2734)

API changes:

* Add `HasSum.sum_range_add`, `sum_add_tsum_nat_add'`, and `tsum_eq_zero_add'`. We had these (or stronger) results for topological groups. These versions works for monoids.
* Rename `tendsto_atTop_csupr` to `tendsto_atTop_csupᵢ`, `tendsto_atBot_csupr` to `tendsto_atBot_csupᵢ`, `tendsto_atBot_cinfi` to `tendsto_atBot_cinfᵢ`, and `tendsto_atTop_cinfi` to `tendsto_atTop_cinfᵢ`.
* Add a shortcut instance for `T5Space ENNReal`.
* Add `ENNReal.nhdsWithin_Ioi_one_neBot`, `ENNReal.nhdsWithin_Ioi_nat_neBot`, `ENNReal.nhdsWithin_Ioi_ofNat_nebot`, and `ENNReal.nhdsWithin_Iio_neBot`.
* Add `ENNReal.hasBasis_nhds_of_ne_top` and `ENNReal.hasBasis_nhds_of_ne_top'`.
* Add `ENNReal.binfᵢ_le_nhds` and `ENNReal.tendsto_nhds_of_Icc`.
* Use `Real.nnabs` instead of `nnnorm` to avoid dependency on `analysis.normed.group.basic` (forward-port of leanprover-community/mathlib3#18562).
* Add `ENNReal.tsum_eq_limsup_sum_nat`.
* Add `ENNReal.tsum_comp_le_tsum_of_injective`, `ENNReal.tsum_le_tsum_comp_of_surjective`, use them to golf some proofs.
* Add `ENNReal.tsum_bunionᵢ_le_tsum`, `ENNReal.tsum_unionᵢ_le_tsum`. We had versions of these lemmas for finite collections. The proofs for infinite collections are simpler.

Most of these changes were done to fix some long proofs: it was easier for me (@urkud) to add supporting lemmas and golf the proof than to fix the original code.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Yury Kudryashov <urkud@urkud.name>

Author: j-loreaux

Mathlib.lean

@@ -1373,6 +1373,7 @@ import Mathlib.Topology.GDelta
 import Mathlib.Topology.Hom.Open
 import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Inseparable
+import Mathlib.Topology.Instances.ENNReal
 import Mathlib.Topology.Instances.Int
 import Mathlib.Topology.Instances.NNReal
 import Mathlib.Topology.Instances.Nat

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -946,7 +946,6 @@ We show the formula `(∑ i in range k, f i) + (∑' i, f (i + k)) = (∑' i, f
 `sum_add_tsum_nat_add`, as well as several results relating sums on `ℕ` and `ℤ`.
 -/
 
-
 section Nat
 
 theorem hasSum_nat_add_iff {f : ℕ → α} (k : ℕ) {a : α} :
@@ -967,16 +966,31 @@ theorem hasSum_nat_add_iff' {f : ℕ → α} (k : ℕ) {a : α} :
   simp [hasSum_nat_add_iff]
 #align has_sum_nat_add_iff' hasSum_nat_add_iff'
 
+theorem HasSum.sum_range_add [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M}
+    {k : ℕ} {a : M} (h : HasSum (fun n ↦ f (n + k)) a) : HasSum f ((∑ i in range k, f i) + a) := by
+  refine ((range k).hasSum f).add_compl ?_
+  rwa [← (notMemRangeEquiv k).symm.hasSum_iff]
+
+theorem sum_add_tsum_nat_add' [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M]
+    {f : ℕ → M} {k : ℕ} (h : Summable (fun n => f (n + k))) :
+    ((∑ i in range k, f i) + ∑' i, f (i + k)) = ∑' i, f i :=
+  h.hasSum.sum_range_add.tsum_eq.symm
+
 theorem sum_add_tsum_nat_add [T2Space α] {f : ℕ → α} (k : ℕ) (h : Summable f) :
-    ((∑ i in range k, f i) + ∑' i, f (i + k)) = ∑' i, f i := by
-  simpa only [add_comm] using
-    ((hasSum_nat_add_iff k).1 ((summable_nat_add_iff k).2 h).hasSum).unique h.hasSum
+    ((∑ i in range k, f i) + ∑' i, f (i + k)) = ∑' i, f i :=
+  sum_add_tsum_nat_add' <| (summable_nat_add_iff k).2 h
 #align sum_add_tsum_nat_add sum_add_tsum_nat_add
 
-theorem tsum_eq_zero_add [T2Space α] {f : ℕ → α} (hf : Summable f) :
+theorem tsum_eq_zero_add' [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M]
+    {f : ℕ → M} (hf : Summable (fun n => f (n + 1))) :
     (∑' b, f b) = f 0 + ∑' b, f (b + 1) := by
-  simpa only [sum_range_one] using (sum_add_tsum_nat_add 1 hf).symm
+  simpa only [sum_range_one] using (sum_add_tsum_nat_add' hf).symm
+
+theorem tsum_eq_zero_add [T2Space α] {f : ℕ → α} (hf : Summable f) :
+    (∑' b, f b) = f 0 + ∑' b, f (b + 1) :=
+  tsum_eq_zero_add' <| (summable_nat_add_iff 1).2 hf
 #align tsum_eq_zero_add tsum_eq_zero_add
+
 /-- For `f : ℕ → α`, then `∑' k, f (k + i)` tends to zero. This does not require a summability
 assumption on `f`, as otherwise all sums are zero. -/
 theorem tendsto_sum_nat_add [T2Space α] (f : ℕ → α) :

Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean

@@ -122,46 +122,46 @@ theorem tendsto_atTop_isGLB (h_anti : Antitone f) (ha : IsGLB (Set.range f) a) :
 
 end IsGLB
 
-section Csupr
+section Csupᵢ
 
 variable [ConditionallyCompleteLattice α] [SupConvergenceClass α] {f : ι → α} {a : α}
 
-theorem tendsto_atTop_csupr (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
+theorem tendsto_atTop_csupᵢ (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
     Tendsto f atTop (𝓝 (⨆ i, f i)) := by
   cases isEmpty_or_nonempty ι
   exacts[tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_csupᵢ hbdd)]
-#align tendsto_at_top_csupr tendsto_atTop_csupr
+#align tendsto_at_top_csupr tendsto_atTop_csupᵢ
 
-theorem tendsto_atBot_csupr (h_anti : Antitone f) (hbdd : BddAbove <| range f) :
-    Tendsto f atBot (𝓝 (⨆ i, f i)) := by convert tendsto_atTop_csupr h_anti.dual hbdd.dual
-#align tendsto_at_bot_csupr tendsto_atBot_csupr
+theorem tendsto_atBot_csupᵢ (h_anti : Antitone f) (hbdd : BddAbove <| range f) :
+    Tendsto f atBot (𝓝 (⨆ i, f i)) := by convert tendsto_atTop_csupᵢ h_anti.dual hbdd.dual
+#align tendsto_at_bot_csupr tendsto_atBot_csupᵢ
 
-end Csupr
+end Csupᵢ
 
-section Cinfi
+section Cinfᵢ
 
 variable [ConditionallyCompleteLattice α] [InfConvergenceClass α] {f : ι → α} {a : α}
 
-theorem tendsto_atBot_cinfi (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
-    Tendsto f atBot (𝓝 (⨅ i, f i)) := by convert tendsto_atTop_csupr h_mono.dual hbdd.dual
-#align tendsto_at_bot_cinfi tendsto_atBot_cinfi
+theorem tendsto_atBot_cinfᵢ (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
+    Tendsto f atBot (𝓝 (⨅ i, f i)) := by convert tendsto_atTop_csupᵢ h_mono.dual hbdd.dual
+#align tendsto_at_bot_cinfi tendsto_atBot_cinfᵢ
 
-theorem tendsto_atTop_cinfi (h_anti : Antitone f) (hbdd : BddBelow <| range f) :
-    Tendsto f atTop (𝓝 (⨅ i, f i)) := by convert tendsto_atBot_csupr h_anti.dual hbdd.dual
-#align tendsto_at_top_cinfi tendsto_atTop_cinfi
+theorem tendsto_atTop_cinfᵢ (h_anti : Antitone f) (hbdd : BddBelow <| range f) :
+    Tendsto f atTop (𝓝 (⨅ i, f i)) := by convert tendsto_atBot_csupᵢ h_anti.dual hbdd.dual
+#align tendsto_at_top_cinfi tendsto_atTop_cinfᵢ
 
-end Cinfi
+end Cinfᵢ
 
 section supᵢ
 
 variable [CompleteLattice α] [SupConvergenceClass α] {f : ι → α} {a : α}
 
 theorem tendsto_atTop_supᵢ (h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i)) :=
-  tendsto_atTop_csupr h_mono (OrderTop.bddAbove _)
+  tendsto_atTop_csupᵢ h_mono (OrderTop.bddAbove _)
 #align tendsto_at_top_supr tendsto_atTop_supᵢ
 
 theorem tendsto_atBot_supᵢ (h_anti : Antitone f) : Tendsto f atBot (𝓝 (⨆ i, f i)) :=
-  tendsto_atBot_csupr h_anti (OrderTop.bddAbove _)
+  tendsto_atBot_csupᵢ h_anti (OrderTop.bddAbove _)
 #align tendsto_at_bot_supr tendsto_atBot_supᵢ
 
 end supᵢ
@@ -171,11 +171,11 @@ section infᵢ
 variable [CompleteLattice α] [InfConvergenceClass α] {f : ι → α} {a : α}
 
 theorem tendsto_atBot_infᵢ (h_mono : Monotone f) : Tendsto f atBot (𝓝 (⨅ i, f i)) :=
-  tendsto_atBot_cinfi h_mono (OrderBot.bddBelow _)
+  tendsto_atBot_cinfᵢ h_mono (OrderBot.bddBelow _)
 #align tendsto_at_bot_infi tendsto_atBot_infᵢ
 
 theorem tendsto_atTop_infᵢ (h_anti : Antitone f) : Tendsto f atTop (𝓝 (⨅ i, f i)) :=
-  tendsto_atTop_cinfi h_anti (OrderBot.bddBelow _)
+  tendsto_atTop_cinfᵢ h_anti (OrderBot.bddBelow _)
 #align tendsto_at_top_infi tendsto_atTop_infᵢ
 
 end infᵢ
@@ -225,7 +225,7 @@ instance Pi.Inf_convergence_class' {ι : Type _} [Preorder α] [TopologicalSpace
 theorem tendsto_of_monotone {ι α : Type _} [Preorder ι] [TopologicalSpace α]
     [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Monotone f) :
     Tendsto f atTop atTop ∨ ∃ l, Tendsto f atTop (𝓝 l) :=
-  if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_csupr h_mono H⟩
+  if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_csupᵢ h_mono H⟩
   else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H
 #align tendsto_of_monotone tendsto_of_monotone