English
Cauchy product over naturals: if f,g are summable and hfg summable, then (∑ f_n) (∑ g_n) equals ∑_{n} ∑_{k ∈ range(n+1)} f_k · g(n-k).
Русский
Кошиевское произведение по нат. индексам: сумма произведений равна двойной сумме по диапазонам.
LaTeX
$$$ \text{Summable } f \rightarrow \text{Summable } g \rightarrow \text{Summable } (x: \mathbb{N} \times \mathbb{N} \mapsto f x.1 * g x.2) \rightarrow \left( \left( \sum' n, f n \right) * \left( \sum' n, g n \right) \right) = \sum' n, \sum_{k \in \operatorname{range}(n+1)} f k * g (n - k)\!$$$
Lean4
/-- The **Cauchy product formula** for the product of two infinites sums indexed by `ℕ`, expressed
by summing on `Finset.range`.
See also `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm` if `f` and `g` are absolutely summable.
-/
protected theorem tsum_mul_tsum_eq_tsum_sum_range (hf : Summable f) (hg : Summable g)
(hfg : Summable fun x : ℕ × ℕ ↦ f x.1 * g x.2) :
((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k) :=
by
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
exact hf.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg hfg
