geom_series_mul_neg — Mathlib

English

The geometric sum times (1 - x) equals 1.

Русский

Геометрическая сумма умноженная на (1 - x) даёт 1.

LaTeX

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

Lean4

theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * (1 - x) = 1 :=
  by
  have := (summable_geometric_of_norm_lt_one h).hasSum.mul_right (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 [← geom_sum_mul_neg, Finset.sum_mul]

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