English
The Cauchy product formula for sums indexed by antidiagonal: provided f and g are summable and hfg is summable, then (∑ f) (∑ g) equals ∑ n ∑ kl ∈ antidiagonal n f kl.1 · g kl.2.
Русский
Формула произведения по антидиагонали: если f и g суммируемы, а hfg суммируема, то (∑ f) (∑ g) равно ∑ n ∑ kl ∈ антидиагональ n f(k) g(l).
LaTeX
$$$ \text{Summable } f \rightarrow \text{Summable } g \rightarrow \text{Summable } (x: A \times A \mapsto f x.1 * g x.2) \rightarrow ((\sum' n, f n) * (\sum' n, g n)) = \sum' n, \sum_{kl \in \operatorname{antidiagonal} n} f kl.1 * g kl.2$$$
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_of_summable_norm` if `f` and `g` are absolutely
summable. -/
protected theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal (hf : Summable f) (hg : Summable g)
(hfg : Summable fun x : A × A ↦ f x.1 * g x.2) :
((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
by
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
rw [hf.tsum_mul_tsum hg hfg, ← sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]
exact (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg).tsum_sigma' (fun n ↦ (hasSum_fintype _).summable)
