summable_mul_prod_iff_summable_mul_sigma_antidiagonal

English

The family (k, l) ↦ f(k) · g(l) is summable if and only if the family indexed by antidiagonal, x ↦ f(x.2).1 · g(x.2).2, is summable.

Русский

Семейство (k, l) ↦ f(k) · g(l) суммируемо тогда и только тогда, когда семейство, индексируемое антидиагональю, x ↦ f(x.2)._1 · g(x.2)._2, суммируемо.

LaTeX

$$$ \text{Summable } (\lambda x: A \times A, f x.1 * g x.2) \iff \text{Summable } (x: \Sigma n : A, \operatorname{antidiagonal} n \to (f x.2.1 * g x.2.2))$$$

Lean4

/-- The family `(k, l) : ℕ × ℕ ↦ f k * g l` is summable if and only if the family
`(n, k, l) : Σ (n : ℕ), antidiagonal n ↦ f k * g l` is summable. -/
theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal :
    (Summable fun x : A × A ↦ f x.1 * g x.2) ↔
      Summable fun x : Σ n : A, antidiagonal n ↦ f (x.2 : A × A).1 * g (x.2 : A × A).2 :=
  Finset.sigmaAntidiagonalEquivProd.summable_iff.symm

Похожие утверждения