From 0660a48dfd6c5b85b567251a28b395e4dac4a7a1 Mon Sep 17 00:00:00 2001
From: dtumad <dtumad@gmail.com>
Date: Thu, 1 Jun 2023 23:01:27 -0500
Subject: [PATCH 1/2] feat(topology/algebra/infinite_sum): Lemmas for sums over

---
 src/topology/algebra/infinite_sum/basic.lean | 25 +++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/topology/algebra/infinite_sum/basic.lean b/src/topology/algebra/infinite_sum/basic.lean
index 9d0486d2144d3..e3541fcc25a70 100644
--- a/src/topology/algebra/infinite_sum/basic.lean
+++ b/src/topology/algebra/infinite_sum/basic.lean
@@ -565,7 +565,7 @@ lemma tsum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (
 
 /-- Version of `tsum_eq_add_tsum_ite` for `add_comm_monoid` rather than `add_comm_group`.
 Requires a different convergence assumption involving `function.update`. -/
-lemma tsum_eq_add_tsum_ite' {f : β → α} (b : β) (hf : summable (f.update b 0)) :
+lemma tsum_eq_add_tsum_ite' [decidable_eq β] {f : β → α} (b : β) (hf : summable (f.update b 0)) :
   ∑' x, f x = f b + ∑' x, ite (x = b) 0 (f x) :=
 calc ∑' x, f x = ∑' x, ((ite (x = b) (f x) 0) + (f.update b 0 x)) :
     tsum_congr (λ n, by split_ifs; simp [function.update_apply, h])
@@ -576,6 +576,18 @@ calc ∑' x, f x = ∑' x, ((ite (x = b) (f x) 0) + (f.update b 0 x)) :
   ... = f b + ∑' x, ite (x = b) 0 (f x) :
     by simp only [function.update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite]
 
+/-- Version of `tsum_option_eq_none_add_tsum` for `add_comm_monoid` rather than `add_comm_group`.
+Requires a different convergence assumption involving `function.update`. -/
+lemma tsum_option_eq_none_add_tsum' {f : option β → α} (hf : summable (f.update none 0)) :
+  ∑' x : option β, f x = f none + ∑' x : β, f (some x) :=
+begin
+  refine (tsum_eq_add_tsum_ite' none hf).trans (congr_arg ((+) (f none)) _),
+  calc ∑' x, ite (x = none) 0 (f x) = ∑' x, (set.range option.some).indicator f x :
+      tsum_congr (λ x, by cases x; simp)
+    ... = ∑' x : (set.range option.some), f ↑x : (tsum_subtype _ _).symm
+    ... = ∑' x, f (option.some x) : tsum_range f (option.some_injective β)
+end
+
 variables [add_comm_monoid δ] [topological_space δ] [t3_space δ] [has_continuous_add δ]
 
 lemma tsum_sigma' {γ : β → Type*} {f : (Σb:β, γ b) → δ} (h₁ : ∀b, summable (λc, f ⟨b, c⟩))
@@ -806,6 +818,17 @@ begin
   exact (add_sub_cancel'_right _ _).symm,
 end
 
+/-- The sum of a function `f` on `option β` is `f none` plus the sum of `f ∘ some` on `β`. -/
+lemma tsum_option_eq_none_add_tsum {f : option β → α} (hf : summable f) :
+  ∑' x : option β, f x = f none + ∑' x : β, f (some x) :=
+begin
+  refine (tsum_eq_add_tsum_ite hf none).trans (congr_arg ((+) (f none)) _),
+  calc ∑' x, ite (x = none) 0 (f x) = ∑' x, (set.range option.some).indicator f x :
+      tsum_congr (λ x, by cases x; simp)
+    ... = ∑' x : (set.range option.some), f ↑x : (tsum_subtype _ _).symm
+    ... = ∑' x, f (option.some x) : tsum_range f (option.some_injective β)
+end
+
 end tsum
 
 /-!

From c0afc9a0d507dcdbffb2fa7fd4124890b3724d76 Mon Sep 17 00:00:00 2001
From: dtumad <dtumad@gmail.com>
Date: Mon, 5 Jun 2023 19:11:25 -0500
Subject: [PATCH 2/2] lemmas in terms of has_sum

---
 src/topology/algebra/infinite_sum/basic.lean | 48 ++++++++++----------
 1 file changed, 25 insertions(+), 23 deletions(-)

diff --git a/src/topology/algebra/infinite_sum/basic.lean b/src/topology/algebra/infinite_sum/basic.lean
index e3541fcc25a70..f976373d1e78b 100644
--- a/src/topology/algebra/infinite_sum/basic.lean
+++ b/src/topology/algebra/infinite_sum/basic.lean
@@ -164,6 +164,11 @@ begin
   exact if_neg hb'
 end
 
+lemma has_sum_singleton (f : β → α) (b : β) : has_sum (f ∘ coe : ({b} : set β) → α) (f b) :=
+suffices has_sum ((f ∘ coe : ({b} : set β) → α)) (∑ b' : ({b} : set β), f ↑b'),
+  by simpa only [univ_unique, sum_singleton] using this,
+has_sum_sum_of_ne_finset_zero (λ x h, (h (finset.mem_univ x)).elim)
+
 lemma has_sum_pi_single [decidable_eq β] (b : β) (a : α) :
   has_sum (pi.single b a) a :=
 show has_sum (λ x, pi.single b a x) a, by simpa only [pi.single_apply] using has_sum_ite_eq b a
@@ -313,6 +318,16 @@ lemma has_sum.compl_add {s : set β} (ha : has_sum (f ∘ coe : sᶜ → α) a)
   has_sum f (a + b) :=
 ha.add_is_compl is_compl_compl.symm hb
 
+lemma has_sum.sum_t {f : β ⊕ γ → α} {a_inl a_inr : α} (h_inl : has_sum (f ∘ sum.inl) a_inl)
+  (h_inr : has_sum (f ∘ sum.inr) a_inr) : has_sum f (a_inl + a_inr) :=
+has_sum.add_is_compl (set.is_compl_range_inl_range_inr)
+  (sum.inl_injective.has_sum_range_iff.2 h_inl) (sum.inr_injective.has_sum_range_iff.2 h_inr)
+
+lemma has_sum.option {f : option β → α} {a_some : α} (hf : has_sum (f ∘ option.some) a_some) :
+  has_sum f (f none + a_some) :=
+has_sum.add_is_compl (set.is_compl_range_some_none β).symm (has_sum_singleton f none)
+  ((option.some_injective β).has_sum_range_iff.2 hf)
+
 lemma has_sum.even_add_odd {f : ℕ → α} (he : has_sum (λ k, f (2 * k)) a)
   (ho : has_sum (λ k, f (2 * k + 1)) b) :
   has_sum f (a + b) :=
@@ -576,18 +591,6 @@ calc ∑' x, f x = ∑' x, ((ite (x = b) (f x) 0) + (f.update b 0 x)) :
   ... = f b + ∑' x, ite (x = b) 0 (f x) :
     by simp only [function.update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite]
 
-/-- Version of `tsum_option_eq_none_add_tsum` for `add_comm_monoid` rather than `add_comm_group`.
-Requires a different convergence assumption involving `function.update`. -/
-lemma tsum_option_eq_none_add_tsum' {f : option β → α} (hf : summable (f.update none 0)) :
-  ∑' x : option β, f x = f none + ∑' x : β, f (some x) :=
-begin
-  refine (tsum_eq_add_tsum_ite' none hf).trans (congr_arg ((+) (f none)) _),
-  calc ∑' x, ite (x = none) 0 (f x) = ∑' x, (set.range option.some).indicator f x :
-      tsum_congr (λ x, by cases x; simp)
-    ... = ∑' x : (set.range option.some), f ↑x : (tsum_subtype _ _).symm
-    ... = ∑' x, f (option.some x) : tsum_range f (option.some_injective β)
-end
-
 variables [add_comm_monoid δ] [topological_space δ] [t3_space δ] [has_continuous_add δ]
 
 lemma tsum_sigma' {γ : β → Type*} {f : (Σb:β, γ b) → δ} (h₁ : ∀b, summable (λc, f ⟨b, c⟩))
@@ -685,6 +688,16 @@ lemma tsum_add_tsum_compl {s : set β} (hs : summable (f ∘ coe : s → α))
   (∑' x : s, f x) + (∑' x : sᶜ, f x) = ∑' x, f x :=
 (hs.has_sum.add_compl hsc.has_sum).tsum_eq.symm
 
+/-- Split a sum over `option β` into `f none` plus the sum of `f ∘ some` on `β`. -/
+lemma tsum_option {f : option β → α} (hf : summable (f ∘ option.some)) :
+  ∑' x : option β, f x = f none + ∑' x : β, f (some x) :=
+hf.has_sum.option.tsum_eq
+
+/-- Split a sum over `β ⊕ γ` into the sum of `f ∘ inl` over `β` and `f ∘ inr` over `γ`. -/
+lemma tsum_sum_t {f : β ⊕ γ → α} (hf : summable (f ∘ sum.inl)) (hf' : summable (f ∘ sum.inr)) :
+  ∑' x : β ⊕ γ, f x = (∑' x : β, f (sum.inl x)) + (∑' x : γ, f (sum.inr x)) :=
+(hf.has_sum.sum_t hf'.has_sum).tsum_eq
+
 lemma tsum_union_disjoint {s t : set β} (hd : disjoint s t)
   (hs : summable (f ∘ coe : s → α)) (ht : summable (f ∘ coe : t → α)) :
   (∑' x : s ∪ t, f x) = (∑' x : s, f x) + (∑' x : t, f x) :=
@@ -818,17 +831,6 @@ begin
   exact (add_sub_cancel'_right _ _).symm,
 end
 
-/-- The sum of a function `f` on `option β` is `f none` plus the sum of `f ∘ some` on `β`. -/
-lemma tsum_option_eq_none_add_tsum {f : option β → α} (hf : summable f) :
-  ∑' x : option β, f x = f none + ∑' x : β, f (some x) :=
-begin
-  refine (tsum_eq_add_tsum_ite hf none).trans (congr_arg ((+) (f none)) _),
-  calc ∑' x, ite (x = none) 0 (f x) = ∑' x, (set.range option.some).indicator f x :
-      tsum_congr (λ x, by cases x; simp)
-    ... = ∑' x : (set.range option.some), f ↑x : (tsum_subtype _ _).symm
-    ... = ∑' x, f (option.some x) : tsum_range f (option.some_injective β)
-end
-
 end tsum
 
 /-!