of_norm_bounded_eventually — Mathlib

English

If ∑ g_i converges and ∥f_i∥ ≤ g_i for all i, then ∑ f_i converges.

Русский

Если ∑ g_i сходится и ∥f_i∥ ≤ g_i для всех i, то ∑ f_i сходится.

LaTeX

$$$\\text{Summable } g \\Rightarrow (\\forall i, \\|f(i)\\| ≤ g(i) \\Rightarrow \\text{Summable } f)$$$

Lean4

/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
real function `g` which is summable, then `f` is summable. -/
theorem of_norm_bounded_eventually {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) :
    Summable f :=
  summable_iff_cauchySeq_finset.2 <| cauchySeq_finset_of_norm_bounded_eventually hg h

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