English
If ∑‖f‖ and ∑‖g‖ converge, then ∑ f(i)g(j) over i,j is summable; the equality of sums holds in terms of products of sums.
Русский
Если обе суммы по нормам сходятся, то сумма по произведению i,j сходится и равна произведению сумм.
LaTeX
$$$\\left(\\sum_i f(i)\\right)\\left(\\sum_j g(j)\\right) = \\sum_{(i,j)} f(i)g(j).$$$
Lean4
/-- Product of two infinite sums indexed by arbitrary types.
See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable, and
`tsum_mul_tsum_of_summable_norm'` when the space is not complete. -/
theorem tsum_mul_tsum_of_summable_norm [CompleteSpace R] {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖)
(hg : Summable fun x => ‖g x‖) : ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2 :=
hf.of_norm.tsum_mul_tsum hg.of_norm (summable_mul_of_summable_norm hf hg)
