edist_le_of_edist_le_geometric_of_tendsto

English

If edist(f_n, f(n+1)) ≤ C r^n with r<1 then edist(f_0, a) ≤ C/(1−r) for limit a of f.

Русский

Если edist(f_n, f_{n+1}) ≤ C r^n при r<1, то edist(f_0, a) ≤ C/(1−r) для предела a функции f.

LaTeX

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

Lean4

/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, then the distance from
`f n` to the limit of `f` is bounded above by `C * r^n / (1 - r)`. -/
theorem edist_le_of_edist_le_geometric_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    edist (f n) a ≤ C * r ^ n / (1 - r) :=
  by
  convert edist_le_tsum_of_edist_le_of_tendsto _ hu ha _
  simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]

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