summable_mul_of_summable_norm — Mathlib

English

If ∑‖f‖ and ∑‖g‖ converge with indices ℕ, then ∑‖f(n)g(m)‖ over n,m converges to the double sum of norms.

Русский

Если ∑‖f‖ и ∑‖g‖ сходятся, то ∑‖f(n)g(m)‖ по парам (n,m) сходится к двойной сумме норм.

LaTeX

$$$\\left(\\sum_{n} f(n)\\right)\\left(\\sum_{m} g(m)\\right) = \\sum_{(n,m)\\in \\mathbb{N}\\times\\mathbb{N}} f(n)g(m).$$$

Lean4

theorem summable_mul_of_summable_norm [CompleteSpace R] {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖)
    (hg : Summable fun x => ‖g x‖) : Summable fun x : ι × ι' => f x.1 * g x.2 :=
  (hf.mul_norm hg).of_norm

Похожие утверждения