mul_norm — Mathlib

English

If ∑‖f‖ and ∑‖g‖ converge for f:ι→R and g:ι'→R, then ∑‖f(i)g(j)‖ over i,j converges.

Русский

Пусть сходятся суммы по нормам ∑‖f‖ и ∑‖g‖; тогда ∑‖f(i)g(j)‖ по всем парам (i,j) сходится.

LaTeX

$$$\\sum_{(i,j)\\in \\iota \\times \\iota'} \\|f(i) g(j)\\| < \\infty.$$$

Lean4

theorem mul_norm {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‖ :=
  .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun x => norm_mul_le (f x.1) (g x.2))
    (hf.mul_of_nonneg hg (fun x => norm_nonneg <| f x) fun x => norm_nonneg <| g x :)

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