R : Type u_1
ι : Type ?u.10189
ι' : Type ?u.10192
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ ij in antidiagonal n, f ij.fst * g ij.snd‖
R : Type u_1
ι : Type ?u.10189
ι' : Type ?u.10192
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun 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.10189
ι' : Type ?u.10192
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ ij in antidiagonal n, f ij.fst * g ij.snd‖
exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg