tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'

English

If ∑‖f‖, ∑‖g‖ converge, then the sum over the antidiagonal of f and g equals the product of their sums in the normed setting.

Русский

Если сходятся суммы норм функций f и g, то сумма по антидиагонали эквивалентна произведению сумм.

LaTeX

$$$\\sum_{n} \\sum_{kl \\in \\mathrm{antidiagonal}(n)} f(k)g(l) = \\left(\\sum_n f(n)\\right)\\left(\\sum_n g(n)\\right).$$$

Lean4

theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)
    (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
  h'f.tsum_mul_tsum_eq_tsum_sum_antidiagonal h'g (summable_mul_of_summable_norm' hf h'f hg h'g)

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