instHasSummableGeomSeries

Mathlib.Analysis.SpecificLimits.Normed

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

English

If r ∈ ℝ satisfies |r| < 1, then the geometric series ∑_{n≥0} r^n is summable and equals 1/(1 − r).

Русский

Если r ∈ ℝ и |r| < 1, то геометрическая серия ∑_{n≥0} r^n сходится и равна 1/(1 − r).

LaTeX

$$$|r| < 1 \Rightarrow \sum_{n=0}^{\infty} r^{n} = (1 - r)^{-1}$$$

Lean4

instance : HasSummableGeomSeries K :=
  ⟨fun _ h ↦ (hasSum_geometric_of_norm_lt_one h).summable⟩

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

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

Разделы

Аффилиация

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