summable_of_isBigO — Mathlib

English

Let f: ι → E and g: ι → ℝ with hg summable. If f =O[cofinite] g, then f is summable (i.e., ∑ ∥f∥ converges).

Русский

Пусть f: ι → E и g: ι → ℝ, причём ∑ |g_i| сходится. Если f =O[cofinite] g, то ∑ ∥f_i∥ сходится.

LaTeX

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

Lean4

theorem summable_of_isBigO {ι E} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ} (hg : Summable g)
    (h : f =O[cofinite] g) : Summable f :=
  let ⟨_, hC⟩ := h.isBigOWith
  .of_norm_bounded_eventually (hg.abs.mul_left _) hC.bound

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