summable_geometric_two'

Mathlib.Analysis.SpecificLimits.Basic

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

English

For any a ∈ ℝ, the sequence a/2/2^n is summable.

Русский

Для любого a ∈ ℝ последовательность a/2/2^n суммируема.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{R}, Summable (n \\\\mapsto a/2 / 2^n).$$$

Lean4

theorem summable_geometric_two' (a : ℝ) : Summable fun n : ℕ ↦ a / 2 / 2 ^ n :=
  ⟨a, hasSum_geometric_two' a⟩

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

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

Разделы

Аффилиация

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