mul_neg_geom_series — Mathlib

English

Sum_{i≥0} x^i = (1 - x)^{-1} for |x|<1.

Русский

Сумма по i≥0 x^i равна (1 - x)^{-1} при |x|<1.

LaTeX

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

Lean4

theorem mul_neg_geom_series (x : R) (h : ‖x‖ < 1) : (1 - x) * ∑' i : ℕ, x ^ i = 1 :=
  by
  have := (summable_geometric_of_norm_lt_one h).hasSum.mul_left (1 - x)
  refine tendsto_nhds_unique this.tendsto_sum_nat ?_
  have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
    simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)
  convert ← this
  rw [← mul_neg_geom_sum, Finset.mul_sum]

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