English
If ∑‖f‖ and ∑‖g‖ converge, then the sequence n ↦ ‖∑_{kl ∈ antidiagonal n} f(k)g(l)‖ is summable over n.
Русский
При суммируемости норм f и g последовательность n ↦ ∥∑_{kl ∈ antidiagonal n} f(k)g(l)∥ суммируема по n.
LaTeX
$$$\\sum_{n} \\left\\|\\sum_{kl \\in \\mathrm{antidiagonal}(n)} f(k)g(l)\\right\\| < \\infty.$$$
Lean4
theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)
(hg : Summable fun x => ‖g x‖) : Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ :=
by
have :=
summable_sum_mul_antidiagonal_of_summable_mul
(Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)
calc
‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ := norm_sum_le _ _
_ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le
