cauchySeq_of_edist_le_geometric — Mathlib

English

If edist(f_n, f(n+1)) ≤ C r^n, then for any a = lim f, edist(f_n, a) ≤ (C r^n)/(1−r).

Русский

Если edist(f_n, f_{n+1}) ≤ C r^n, то для предела a последовательности имеет место: edist(f_n, a) ≤ (C r^n)/(1−r).

LaTeX

$$$$edist(f_n, a) \le \frac{C r^n}{1 - r}.$$$$

Lean4

/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, `C ≠ ∞`, `r < 1`,
then `f` is a Cauchy sequence. -/
theorem cauchySeq_of_edist_le_geometric : CauchySeq f :=
  by
  refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_
  rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
  have := (tsub_pos_iff_lt.2 hr).ne'
  finiteness

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