edist_le_of_edist_le_geometric_of_tendsto₀

English

The sum ∑' m ℕ of 2^{(-1 - m)} equals 1.

Русский

Сумма ∑' m≥0 2^{(-1 - m)} равна 1.

LaTeX

$$$$\sum_{m=0}^{\infty} 2^{(-1 - m)} = 1.$$$$

Lean4

/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, then the distance from
`f 0` to the limit of `f` is bounded above by `C / (1 - r)`. -/
theorem edist_le_of_edist_le_geometric_of_tendsto₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) : edist (f 0) a ≤ C / (1 - r) :=
  by simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0

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