tsum_mul_tsum_of_nonarchimedean — Mathlib

English

If f: ℤ → G is Multipliable with given half-terms, then the bilateral tprod equals a combination of nonnegative and negative parts divided by f(0).

Русский

Если f: ℤ → G с заданными половинами сходится, то двустороннее tprod равно сочетанию частей по неотрицательным и по отрицательным индексам делённому на f(0).

LaTeX

$$$\\displaystyle \\text{tprod}\\ f = \\dfrac{\\text{tprod}_{n\\ge0} f(n) \\cdot \\text{tprod}_{n\\ge0} f(-n)}{f(0)}$$$

Lean4

theorem tsum_mul_tsum_of_nonarchimedean [T0Space R] {f : α → R} {g : β → R} (hf : Summable f) (hg : Summable g) :
    (∑' i, f i) * (∑' i, g i) = ∑' i : α × β, f i.1 * g i.2 :=
  (hf.hasSum.mul_of_nonarchimedean hg.hasSum).tsum_eq.symm

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