hasSum_sum_range_mul_of_summable_norm'

English

If ∑‖f‖ and ∑‖g‖ converge, then the norm of the antidiagonal sum ∑ kl ∈ antidiagonal n f(k)g(l) is summable in n.

Русский

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

LaTeX

$$$\\sum_{n} \\left\\|\\sum_{kl \\in \\mathrm{antidiagonal}(n)} f(k)g(l)\\right\\| < \\infty.$$$

Lean4

theorem hasSum_sum_range_mul_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) :
    HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n) :=
  by
  convert (summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum
  exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' hf h'f hg h'g

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