cauchySeq_of_le_geometric — Mathlib

English

If 0 < m and f: ℕ→ℕ with i ≤ f(i), then ∑ 1/m^{f(i)} converges.

Русский

Пусть 0 < m и f: ℕ→ℕ так что i ≤ f(i). Тогда сумма ∑ 1/m^{f(i)} сходится.

LaTeX

$$$$\sum_{i=0}^{\infty} \frac{1}{m^{f(i)}} < ∞, \quad m>1.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence.
Note that this lemma does not assume `0 ≤ C` or `0 ≤ r`. -/
theorem cauchySeq_of_le_geometric : CauchySeq f :=
  cauchySeq_of_dist_le_of_summable _ hu ⟨_, aux_hasSum_of_le_geometric hr hu⟩

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