summable_geometric_of_norm_lt_one

Mathlib.Analysis.SpecificLimits.Normed

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

← MathLib Explorer

English

The geometric series converges to (1 - x)^{-1} when |x|<1.

Русский

Геометрическая сумма сходится к (1 - x)^{-1} при |x|<1.

LaTeX

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

Lean4

theorem summable_geometric_of_norm_lt_one {K : Type*} [NormedRing K] [HasSummableGeomSeries K] {x : K} (h : ‖x‖ < 1) :
    Summable (fun n ↦ x ^ n) :=
  HasSummableGeomSeries.summable_geometric_of_norm_lt_one x h

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

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

Разделы

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

Аффилиация

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