R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
have :=
  summable_sum_mul_antidiagonal_of_summable_mul
    (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
refine' summable_of_nonneg_of_le (fun _ => norm_nonneg _) _ this
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
intro n
no goals
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
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
case h
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
gcongr
no goals
case h
R : Type u_1
ι : Type ?u.5264
ι' : Type ?u.5267
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‖
apply norm_mul_le