feat(topology/algebra/infinite_sum): Double sum is equal to a single …

…value (#15157)

A generalized version of `tsum_eq_single` that works for a double indexed sum, when all but one summand is zero.



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

src/topology/algebra/infinite_sum.lean

@@ -452,6 +452,12 @@ lemma tsum_eq_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0)  :
   ∑'b, f b = f b :=
 (has_sum_single b hf).tsum_eq
 
+lemma tsum_tsum_eq_single (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 0)
+  (hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 0) :
+  ∑' b' c', f b' c' = f b c :=
+calc ∑' b' c', f b' c' = ∑' b', f b' c : tsum_congr $ λ b', tsum_eq_single _ (hfc b')
+... = f b c : tsum_eq_single _ hfb
+
 @[simp] lemma tsum_ite_eq (b : β) [decidable_pred (= b)] (a : α) :
   ∑' b', (if b' = b then a else 0) = a :=
 (has_sum_ite_eq b a).tsum_eq