English
On a countable index set there exists a positive summable ε' with sum less than ε.
Русский
На счётном индексе существует положительная сходящаяся сумма, меньшая чем ε.
LaTeX
$$$$\exists ε' : ι \to \mathbb{R}_{>0}, \ HasSum ε' (ε) \land ε < ε.$$$$
Lean4
/-- A series whose terms are bounded by the terms of a converging geometric series converges. -/
theorem summable_one_div_pow_of_le {m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi : ∀ i, i ≤ f i) :
Summable fun i ↦ 1 / m ^ f i :=
by
refine
.of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
(summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
rw [div_pow, one_pow]
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a)) <;> exact pow_pos (zero_lt_one.trans hm) _
