English
If ∑‖f‖ and ∑‖g‖ converge (norm), then (∑ f)(∑ g) equals ∑_{n} ∑_{k∈range(n+1)} f(k) g(n-k).
Русский
При сходящихся по норме суммах (∑ f)(∑ g) равно ∑_n ∑_{k∈range(n+1)} f(k) g(n-k).
LaTeX
$$$\\left(\\sum_n f(n)\\right)\\left(\\sum_n g(n)\\right) = \\sum_{n} \\sum_{k \\in \\mathrm{range}(n+1)} f(k) g(n-k).$$$
Lean4
/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
expressed by summing on `Finset.range`.
See also `tsum_mul_tsum_eq_tsum_sum_range` if `f` and `g` are
not* absolutely summable, and `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'` when the
space is not complete. -/
theorem tsum_mul_tsum_eq_tsum_sum_range_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, ∑ k ∈ range (n + 1), f k * g (n - k) :=
by
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg
