of_norm_bounded — Mathlib

English

If the norm of f is bounded by a summable g, then f is summable.

Русский

Если ||f_i|| ≤ g_i и ∑ g_i сходится, то ∑ f_i сходится.

LaTeX

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

Lean4

/-- The direct comparison test for series:  if the norm of `f` is bounded by a real function `g`
which is summable, then `f` is summable. -/
theorem of_norm_bounded [CompleteSpace E] {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) :
    Summable f := by
  rw [summable_iff_cauchySeq_finset]
  exact cauchySeq_finset_of_norm_bounded hg h

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