English
If f: ι → ℝ and g: ι' → ℝ are summable, then the double sequence (f(i)g(j)) on ι×ι' is summable and its total sum equals (∑ f)(∑ g).
Русский
Пусть f и g суммируемы; тогда двоичная последовательность f(i)g(j) по i∈ι, j∈ι' суммируема и её сумма равна произведению сумм ∑ f · ∑ g.
LaTeX
$$$\\sum_{(i,j)\\in \\iota \\times \\iota'} f(i)g(j) = \\left(\\sum_{i} f(i)\\right)\\left(\\sum_{j} g(j)\\right).$$$
Lean4
theorem mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ} (hf : Summable f) (hg : Summable g) (hf' : 0 ≤ f) (hg' : 0 ≤ g) :
Summable fun x : ι × ι' => f x.1 * g x.2 :=
(summable_prod_of_nonneg fun _ ↦ mul_nonneg (hf' _) (hg' _)).2
⟨fun x ↦ hg.mul_left (f x), by simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)⟩
