summable_norm_sum_mul_range_of_summable_norm

English

If ∑‖f‖ and ∑‖g‖ converge, then the sequence n ↦ ∥∑_{k∈range(n+1)} f(k) g(n-k)∥ is summable over n.

Русский

Если ∑‖f‖ и ∑‖g‖ сходятся, тогда последовательность n ↦ ∥∑_{k∈range(n+1)} f(k) g(n-k)∥ суммируема по n.

LaTeX

$$$\\sum_{n} \\left\\|\\sum_{k\\in\\mathrm{range}(n+1)} f(k)g(n-k)\\right\\| < \\infty.$$$

Lean4

theorem summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)
    (hg : Summable fun x => ‖g x‖) : 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_norm_sum_mul_antidiagonal_of_summable_norm hf hg

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