of_norm_bounded_eventually_nat — Mathlib

English

If f is bounded by g and g is summable, then f is summable as a sequence over ℕ.

Русский

Если f(i) ограничено g(i) и ∑ g_i сходится, то ∑ f_i сходится по i∈ℕ.

LaTeX

$$$\\text{Summable } g \\land (\\forall i, \\|f(i)\\| ≤ g(i)) \\Rightarrow \\text{Summable } f$$$

Lean4

/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
real function `g` which is summable, then `f` is summable. -/
theorem of_norm_bounded_eventually_nat {f : ℕ → E} {g : ℕ → ℝ} (hg : Summable g) (h : ∀ᶠ i in atTop, ‖f i‖ ≤ g i) :
    Summable f :=
  .of_norm_bounded_eventually hg <| Nat.cofinite_eq_atTop ▸ h

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