ι : Type ?u.30248
κ : Type ?u.30251
R : Type ?u.30254
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n) = ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
ι : Type ?u.30248
κ : Type ?u.30251
R : Type ?u.30254
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
ι : Type ?u.30248
κ : Type ?u.30251
R : Type ?u.30254
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (c : (n : ℕ) × { x // x ∈ Nat.antidiagonal n }),
      f (↑Nat.sigmaAntidiagonalEquivProd c).fst * g (↑Nat.sigmaAntidiagonalEquivProd c).snd) =
    ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
ι : Type ?u.30248
κ : Type ?u.30251
R : Type ?u.30254
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n) = ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
rw [tsum_mul_tsum hf hg hfg, ← Nat.sigmaAntidiagonalEquivProd.tsum_eq (_ : ℕ × ℕ → α)]
no goals
ι : Type ?u.30248
κ : Type ?u.30251
R : Type ?u.30254
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (c : (n : ℕ) × { x // x ∈ Nat.antidiagonal n }),
      f (↑Nat.sigmaAntidiagonalEquivProd c).fst * g (↑Nat.sigmaAntidiagonalEquivProd c).snd) =
    ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
exact
  tsum_sigma' (fun n => (hasSum_fintype _).summable)
    (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg)