English
If f and g are such that the product family f(x.fst) · g(x.snd) is summable, then the sum over antidiagonal blocks is summable.
Русский
Если произведение семейств f и g по антидиагоналям суммируемо, то сумма по блокам антидиагонали суммируема.
LaTeX
$$$ \text{Summable } (f: A \to \alpha) \rightarrow \text{Summable } (g: A \to \alpha) \rightarrow \text{Summable } (x: A \times A \mapsto f x.1 * g x.2) \Rightarrow \text{Summable } (n \mapsto \sum_{kl \in \operatorname{antidiagonal} n} f kl.1 * g kl.2)$$$
Lean4
theorem summable_sum_mul_antidiagonal_of_summable_mul (h : Summable fun x : A × A ↦ f x.1 * g x.2) :
Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
by
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
exact h.sigma' fun n ↦ (hasSum_fintype _).summable
