summable_of_le — Mathlib

English

Same as above but in NNReal context: if g ≤ f and HasSum f r, then there exists p ≤ r with HasSum g p.

Русский

Аналогично в NNReal: если g ≤ f и HasSum f r, то существует p ≤ r с HasSum g p.

LaTeX

$$$\\forall b, g(b) \\le f(b) \\Rightarrow HasSum f r \\Rightarrow \\exists p \\le r, HasSum g p$$$

Lean4

/-- Comparison test of convergence of `ℝ≥0`-valued series. -/
theorem summable_of_le {f g : β → ℝ≥0} (hgf : ∀ b, g b ≤ f b) : Summable f → Summable g
  | ⟨_r, hfr⟩ =>
    let ⟨_p, _, hp⟩ := exists_le_hasSum_of_le hgf hfr
    hp.summable

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