English
Let f, g: β → R with g ≥ 0 and g ≤ f. If ∑ f converges (is summable), then ∑ g converges as well.
Русский
Пусть f, g: β → ℝ такие, что g ≥ 0 и g ≤ f для всех индексов. Если ∑ f наиболее сходится, то и ∑ g сходится.
LaTeX
$$$\left( \forall b,\ 0 \le g(b) \right) \land \left( \forall b,\ g(b) \le f(b) \right) \land \text{Summable}(f) \implies \text{Summable}(g).$$$
Lean4
/-- Comparison test of convergence of series of non-negative real numbers. -/
theorem of_nonneg_of_le {f g : β → ℝ} (hg : ∀ b, 0 ≤ g b) (hgf : ∀ b, g b ≤ f b) (hf : Summable f) : Summable g :=
by
lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)
lift g to β → ℝ≥0 using hg
rw [NNReal.summable_coe] at hf ⊢
exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf
