English
Let f : N → E and g : N → F with E a normed additive group that is complete, F a finite-dimensional real normed space, and suppose g is summable and f =O atTop g. Then f is summable.
Русский
Пусть f : N → E и g : N → F, где E является полным нормированным аддитивным группой, а F — конечномерным нормированным пространством над \u211d. Пусть g суммируема, и f =O за бесконечностью от g. Тогда f суммируема.
LaTeX
$$$ \\operatorname{Summable}(g) \\land f =O_{\\mathrm{atTop}} g \\Rightarrow \\operatorname{Summable}(f) $$$
Lean4
theorem summable_of_isBigO_nat' {E F : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F]
[NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F} (hg : Summable g) (h : f =O[atTop] g) :
Summable f :=
summable_of_isBigO_nat hg.norm h.norm_right
