tsum_mul_tsum_of_summable_norm' — Mathlib

English

If ∑‖f‖ and ∑‖g‖ converge, then ∑ ‖f(i)g(j)‖ over i,j converges to ∑‖f(i)‖ ∑‖g(j)‖.

Русский

Если ∑‖f‖ и ∑‖g‖ сходятся, то ∑ ‖f(i)g(j)‖ сходится к произведению сумм норм.

LaTeX

$$$\\sum_{(i,j)} \\|f(i)g(j)\\| = \\left(\\sum_i \\|f(i)\\|\\right) \\left(\\sum_j \\|g(j)\\|\\right).$$$

Lean4

theorem tsum_mul_tsum_of_summable_norm' {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2 :=
  h'f.tsum_mul_tsum h'g (summable_mul_of_summable_norm' hf h'f hg h'g)

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