ι : Type ?u.34737
κ : Type ?u.34740
R : Type ?u.34743
α : 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 : ℕ), ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
ι : Type ?u.34737
κ : Type ?u.34740
R : Type ?u.34743
α : 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 : ℕ), ∑ k in range (n + 1), f k * g (n - k)
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
no goals
ι : Type ?u.34737
κ : Type ?u.34740
R : Type ?u.34743
α : 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 : ℕ), ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal hf hg hfg