tendsto_arithGeom_atTop_of_one_lt

English

Let a>1 and suppose b/(1−a) < u0. Then the sequence arithGeom(a,b,u0) tends to infinity as n→∞.

Русский

Пусть a>1 и пусть b/(1−a) < u0. Тогда последовательность arithGeom(a,b,u0) расходится к бесконечности при n→∞.

LaTeX

$$$ (1

Lean4

theorem tendsto_arithGeom_atTop_of_one_lt [Archimedean R] (ha : 1 < a) (h0 : b / (1 - a) < u₀) :
    Tendsto (arithGeom a b u₀) atTop atTop := by
  rw [arithGeom_eq' ha.ne']
  refine tendsto_atTop_add_const_right _ _ ?_
  refine Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_
  exact tendsto_pow_atTop_atTop_of_one_lt ha

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