edist_le_of_edist_le_geometric_two_of_tendsto

English

If edist distances are bounded by a geometric progression, then edist(f_n, a) tends to 0 at rate.

Русский

Если edist ограничена геометрической прогрессией, edist(f_n, a) стремится к 0 с темпом геометрического прогресса.

LaTeX

$$$$edist(f_n, a) \to 0\quad (n\to\infty).$$$$

Lean4

/-- If `edist (f n) (f (n+1))` is bounded by `C * 2^-n`, then the distance from
`f n` to the limit of `f` is bounded above by `2 * C * 2^-n`. -/
theorem edist_le_of_edist_le_geometric_two_of_tendsto (n : ℕ) : edist (f n) a ≤ 2 * C / 2 ^ n :=
  by
  simp only [div_eq_mul_inv, ENNReal.inv_pow] at *
  rw [mul_assoc, mul_comm]
  convert edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1
  rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]

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