hasSum_geom_series_inverse

Mathlib.Analysis.SpecificLimits.Normed

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

← MathLib Explorer

English

For ||x|| < 1, HasSum of x^n equals (1 - x)^{-1}.

Русский

Для ||x|| < 1 сумма HasSum ряда x^n равна (1 - x)^{-1}.

LaTeX

$$$HasSum(\\\\mapsto x^n) = (1 - x)^{-1} \\\\text{ if } \\\\|x\\\\| < 1$$$

Lean4

theorem hasSum_geom_series_inverse (x : R) (h : ‖x‖ < 1) : HasSum (fun i ↦ x ^ i) (Ring.inverse (1 - x)) :=
  by
  convert (summable_geometric_of_norm_lt_one h).hasSum
  exact (geom_series_eq_inverse x h).symm

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

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

Разделы

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

Аффилиация

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