[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x => ∑' (y : ι'), f (x, y).fst * g (x, y).snd
[PROOFSTEP]
simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ kl in antidiagonal n, f kl.fst * g kl.snd‖
[PROOFSTEP]
have :=
  summable_sum_mul_antidiagonal_of_summable_mul
    (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
⊢ Summable fun n => ‖∑ kl in antidiagonal n, f kl.fst * g kl.snd‖
[PROOFSTEP]
refine' summable_of_nonneg_of_le (fun _ => norm_nonneg _) _ this
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
⊢ ∀ (b : ℕ), ‖∑ kl in antidiagonal b, f kl.fst * g kl.snd‖ ≤ ∑ kl in antidiagonal b, ‖f kl.fst‖ * ‖g kl.snd‖
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
n : ℕ
⊢ ‖∑ kl in antidiagonal n, f kl.fst * g kl.snd‖ ≤ ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
[PROOFSTEP]
calc
  ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl in antidiagonal n, ‖f kl.1 * g kl.2‖ := norm_sum_le _ _
  _ ≤ ∑ kl in antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
n : ℕ
⊢ ∑ kl in antidiagonal n, ‖f kl.fst * g kl.snd‖ ≤ ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
[PROOFSTEP]
gcongr
[GOAL]
case h
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl in antidiagonal n, ‖f kl.fst‖ * ‖g kl.snd‖
n : ℕ
i✝ : ℕ × ℕ
a✝ : i✝ ∈ antidiagonal n
⊢ ‖f i✝.fst * g i✝.snd‖ ≤ ‖f i✝.fst‖ * ‖g i✝.snd‖
[PROOFSTEP]
apply norm_mul_le
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
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)‖
[PROOFSTEP]
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
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‖
[PROOFSTEP]
exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
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)
[PROOFSTEP]
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
R : Type u_1
ι : Type u_2
ι' : Type u_3
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
[PROOFSTEP]
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg
