summable_sum_mul_range_of_summable_norm'

English

If ∑‖f‖ and ∑‖g‖ converge, then the range-convolution ∑_{k∈range(n+1)} f(k) g(n-k) is summable in n with respect to the norm.

Русский

Если сходятся суммы норм функций f,g, то конволюционная сумма по диапазону ∑_{k∈range(n+1)} f(k) g(n-k) по норме суммируема в n.

LaTeX

$$$\\sum_{n} \\left\\|\\sum_{k=0}^n f(k) g(n-k)\\right\\| < \\infty.$$$

Lean4

theorem summable_sum_mul_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) : Summable fun 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 summable_sum_mul_antidiagonal_of_summable_norm' hf h'f hg h'g

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