tendsto_div_one_add_pow_nhds_zero

English

The geometric sum times (1 - x) equals 1: (sum x^i) (1 - x) = 1.

Русский

Геометрическая сумма, умноженная на (1 - x), равна единице: (Σ x^i)(1 - x) = 1.

LaTeX

$$$\\\\left(\\\\sum_{i=0}^{\\\\infty} x^i\\\\right)(1 - x) = 1 \\\\text{ for } |x| < 1$$$

Lean4

/-- `v (1 / (1 + a ^n))` tends to `0` whenever `v : AbsoluteValue R S` for fields `R` and `S`,
provided `1 < v a`. -/
theorem tendsto_div_one_add_pow_nhds_zero {v : AbsoluteValue R S} {a : R} (ha : 1 < v a) :
    Filter.Tendsto (fun (n : ℕ) ↦ v (1 / (1 + a ^ n))) Filter.atTop (𝓝 0) :=
  by
  simp_rw [div_eq_mul_inv, one_mul, map_inv₀, fun n ↦ add_comm 1 (a ^ n)]
  refine (tendsto_atTop_mono (fun n ↦ v.le_add _ _) ?_).inv_tendsto_atTop
  simpa using
    (tendsto_atTop_add_right_of_le _ _ (tendsto_pow_atTop_atTop_of_one_lt ha) (fun _ ↦ le_rfl)).congr fun n ↦
      (sub_eq_add_neg (v a ^ n) 1).symm

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