summable_sum_mul_range_of_summable_mul

English

If h is summable for the bilinear form f(i) · g(j), then the sequence n ↦ ∑_{k ∈ range(n+1)} f(k) · g(n-k) is summable.

Русский

Если сумма по диапазону конволюции определена для f и g, то ряд по диапазонам 0..n суммируем.

LaTeX

$$$ \text{Summable } f \rightarrow \text{Summable } g \rightarrow \text{Summable } (x: \mathbb{N} \times \mathbb{N} \mapsto f x.1 * g x.2) \rightarrow \text{Summable } (n \mapsto \sum_{k \in \operatorname{range}(n+1)} f k * g (n - k))$$$

Lean4

theorem summable_sum_mul_range_of_summable_mul (h : Summable fun x : ℕ × ℕ ↦ f x.1 * g x.2) :
    Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k) :=
  by
  simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
  exact summable_sum_mul_antidiagonal_of_summable_mul h

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