summable_of_isEquivalent_nat — Mathlib

English

Let E be a normed additive group with a real vector space structure, and f,g : N → E. If g is summable and f ~[atTop] g, then f is summable.

Русский

Пусть E — нормированная абелева группа с реаловым стеком пространства. Пусть f,g : N → E. Если g суммируема и f эквивалентна g на бесконечности, то и f суммируема.

LaTeX

$$$ \\operatorname{Summable}(g) \\land f ~_{\\mathrm{atTop}} g \\Rightarrow \\operatorname{Summable}(f) $$$

Lean4

theorem summable_of_isEquivalent_nat {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {f : ℕ → E} {g : ℕ → E} (hg : Summable g) (h : f ~[atTop] g) : Summable f :=
  hg.trans_sub (summable_of_isBigO_nat' hg h.isLittleO.isBigO)

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