summable_of_sum_range_norm_le — Mathlib

English

If a sequence f: Nat → E has the property that the partial sums of ||f i|| are bounded by c, then f is summable.

Русский

Если частичные суммы ||f i|| ограничены константой, то f суммируема.

LaTeX

$$$\\forall n, \\sum_{i=0}^{n-1} \\|f(i)\\| \\le c \\\\Rightarrow \\ Summable f$$$

Lean4

theorem summable_of_sum_range_norm_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {c : ℝ} {f : ℕ → E} (h : ∀ n, ∑ i ∈ Finset.range n, ‖f i‖ ≤ c) : Summable f :=
  summable_norm_iff.mp <| summable_of_sum_range_le (fun _ ↦ norm_nonneg _) h

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