tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'

English

If ∑‖f‖ and ∑‖g‖ converge, then (∑ f)(∑ g) equals the antidiagonal sum ∑_{n} ∑_{kl ∈ antidiagonal n} f(k) g(l).

Русский

Если сходятся ∑‖f‖ и ∑‖g‖, то произведение сумм равно антидиагональной сумме.

LaTeX

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

Lean4

theorem tsum_mul_tsum_eq_tsum_sum_range_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, ∑ k ∈ range (n + 1), f k * g (n - k) :=
  by
  simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' hf h'f hg h'g

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