hasSum_sum_range_mul_of_summable_norm

English

If ∑‖f‖ and ∑‖g‖ converge, then the sum over range of the convolution equals the product of sums; this is witnessed by HasSum of the appropriate convolution.

Русский

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

LaTeX

$$$\\text{HasSum}\\Big(\\lambda n. \\sum_{k\\in\\mathrm{range}(n+1)} f(k)g(n-k)\\Big)\\Big( \\sum_n f(n) \\Big)\\Big( \\sum_n g(n) \\Big).$$$

Lean4

theorem hasSum_sum_range_mul_of_summable_norm [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)
    (hg : Summable fun x => ‖g x‖) : HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n) :=
  by
  convert (summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum
  exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm hf hg

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