R : Type u_1
ι : Type ?u.12044
ι' : Type ?u.12047
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ ij in antidiagonal n, f ij.fst * g ij.snd
R : Type u_1
ι : Type ?u.12044
ι' : Type ?u.12047
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ k in range (n + 1), f k * g (n - k)
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
no goals
R : Type u_1
ι : Type ?u.12044
ι' : Type ?u.12047
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ ij in antidiagonal n, f ij.fst * g ij.snd
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg