summable_of_isBigO' — Mathlib

English

If g is summable and f =O'(cofinite) g, then f is summable as well.

Русский

Если g суммируема и f =O'(cofinite) g, то f тоже суммируема.

LaTeX

$$$Summable g \\\\Rightarrow IsBigO'[cofinite] f g \\\\Rightarrow Summable f$$$

Lean4

theorem summable_of_isBigO' {ι E F : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F]
    [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F} (hg : Summable g) (h : f =O[cofinite] g) :
    Summable f :=
  summable_of_isBigO hg.norm h.norm_right

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