English
For summable f,g, the product of sums equals the sum over the antidiagonal of products: (∑ f)(∑ g) = ∑_{n} ∑_{kl ∈ antidiagonal n} f(k)g(l).
Русский
Для суммируемых f,g произведение сумм равно сумме по антидиагонали от произведений: (∑ f)(∑ g) = ∑_n ∑_{kl ∈ antidiagonal n} f(k)g(l).
LaTeX
$$$\\left(\\sum_n f(n)\\right)\\left(\\sum_n g(n)\\right) = \\sum_{n} \\sum_{kl \\in \\mathrm{antidiagonal}(n)} f(k)g(l).$$$
Lean4
/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
expressed by summing on `Finset.antidiagonal`.
See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
*not* absolutely summable, and `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'`
when the space is not complete. -/
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
(hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
hf.of_norm.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg.of_norm (summable_mul_of_summable_norm hf hg)
