tendsto_arithGeom_nhds_of_lt_one — Mathlib

English

If Archimedean R and 0 ≤ a < 1, then arithGeom(a,b,u0) tends to b/(1-a) as n → ∞.

Русский

Если R Архимедово, 0 ≤ a < 1, то arithGeom(a,b,u0) стремится к b/(1-a) при n → ∞.

LaTeX

$$0 \le a \land a < 1 \Rightarrow \lim_{n \to \infty} \mathrm{arithGeom}(a,b,u_0,n) = \frac{b}{1-a}$$

Lean4

theorem tendsto_arithGeom_nhds_of_lt_one [Archimedean R] [TopologicalSpace R] [OrderTopology R] (ha_pos : 0 ≤ a)
    (ha : a < 1) : Tendsto (arithGeom a b u₀) atTop (𝓝 (b / (1 - a))) :=
  by
  rw [arithGeom_eq' ha.ne]
  conv_rhs => rw [← zero_add (b / (1 - a))]
  refine Tendsto.add ?_ tendsto_const_nhds
  conv_rhs => rw [← zero_mul (u₀ - (b / (1 - a)))]
  exact (tendsto_pow_atTop_nhds_zero_of_lt_one ha_pos ha).mul_const _

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