summable_of_isBigO_nat — Mathlib

English

Let E be a normed additive group; if hg: Summable g for g: ℕ → ℝ and h: f =O[atTop] g for f: ℕ → E, then f is summable.

Русский

Пусть E — нормированная аддитивная группа; если ∑ g(n) сходится для g: ℕ → ℝ и f: ℕ → E удовлетворяет f =O[atTop] g, то ∑ ∥f(n)∥ сходится.

LaTeX

$$$ \\text{Summable } g \\wedge f =O[atTop] g \\Rightarrow \\text{Summable } f $$$

Lean4

theorem summable_of_isBigO_nat {E} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ}
    (hg : Summable g) (h : f =O[atTop] g) : Summable f :=
  summable_of_isBigO hg <| Nat.cofinite_eq_atTop.symm ▸ h

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