hasSum_geometric_two

Mathlib.Analysis.SpecificLimits.Basic

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

English

HasSum for the series with ratio 1/2 equals 2.

Русский

Сумма геометрического ряда с коэффициентом 1/2 равна 2.

LaTeX

$$$HasSum (n \\mapsto (1/2)^n) 2$$$

Lean4

theorem hasSum_geometric_two : HasSum (fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n) 2 := by
  convert hasSum_geometric_of_lt_one _ _ <;> norm_num

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

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

Разделы

Аффилиация

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