geom_series_eq_inverse

Mathlib.Analysis.SpecificLimits.Normed

URI: https://scilib.ai/kg/mathlib#geom_series_eq_inverse

← MathLib Explorer

English

For ||x|| < 1, the geometric series sums to (1 - x)^{-1}.

Русский

Для ||x|| < 1 геометрическая сумма равна (1 - x)^{-1}.

LaTeX

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

Lean4

theorem geom_series_eq_inverse (x : R) (h : ‖x‖ < 1) : ∑' i, x ^ i = Ring.inverse (1 - x) :=
  by
  change (Units.oneSub x h)⁻¹ = Ring.inverse (1 - x)
  rw [← Ring.inverse_unit]
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru