English
If f and g are summable and their pointwise products are summable, then the product of their sums equals the double sum over the product pairs.
Русский
Если f и g сходятся суммой и их попарные произведения суммируемы, то произведение сумм равно двойной сумме по парам произведений.
LaTeX
$$$ \text{Summable } f \rightarrow \text{Summable } g \rightarrow \text{Summable } (\lambda x: ι \times κ, f x.1 * g x.2) \rightarrow (\sum' x, f x) * (\sum' y, g y) = \sum' z: ι \times κ, f z.1 * g z.2$$$
Lean4
/-- Product of two infinites sums indexed by arbitrary types.
See also `tsum_mul_tsum_of_summable_norm` if `f` and `g` are absolutely summable. -/
protected theorem tsum_mul_tsum (hf : Summable f) (hg : Summable g) (hfg : Summable fun x : ι × κ ↦ f x.1 * g x.2) :
((∑' x, f x) * ∑' y, g y) = ∑' z : ι × κ, f z.1 * g z.2 :=
hf.hasSum.mul_eq hg.hasSum hfg.hasSum
