exists_le_hasSum_of_le — Mathlib

English

If g ≤ f pointwise and HasSum f r, then there exists p ≤ r with HasSum g p.

Русский

Если g ≤ f по каждой точке и HasSum f r, тогда существует p ≤ r с HasSum g p.

LaTeX

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

Lean4

/-- Comparison test of convergence of `ℝ≥0`-valued series. -/
theorem exists_le_hasSum_of_le {f g : β → ℝ≥0} {r : ℝ≥0} (hgf : ∀ b, g b ≤ f b) (hfr : HasSum f r) :
    ∃ p ≤ r, HasSum g p :=
  have : (∑' b, (g b : ℝ≥0∞)) ≤ r :=
    by
    refine hasSum_le (fun b => ?_) ENNReal.summable.hasSum (ENNReal.hasSum_coe.2 hfr)
    exact ENNReal.coe_le_coe.2 (hgf _)
  let ⟨p, Eq, hpr⟩ := ENNReal.le_coe_iff.1 this
  ⟨p, hpr, ENNReal.hasSum_coe.1 <| Eq ▸ ENNReal.summable.hasSum⟩

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