tsum_geometric_two'

Mathlib.Analysis.SpecificLimits.Basic

URI: https://scilib.ai/kg/mathlib#tsum_geometric_two'

English

For any a ∈ ℝ, the sum of a/2/2^n equals a.

Русский

Для любого a ∈ ℝ сумма a/2/2^n равна a.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{R}, \\\\sum' n, a/2 / 2^n = a.$$$

Lean4

theorem tsum_geometric_two' (a : ℝ) : ∑' n : ℕ, a / 2 / 2 ^ n = a :=
  (hasSum_geometric_two' a).tsum_eq

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

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

Разделы

Аффилиация

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