summable_geometric_two_encode

Mathlib.Analysis.SpecificLimits.Basic

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

← MathLib Explorer

English

For any a ∈ ℝ, the series ∑ (a/2)/2^n has sum a.

Русский

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

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{R}, \\\\ HasSum (\\\\lambda n, a/2 / 2^n) a$$$

Lean4

theorem summable_geometric_two_encode {ι : Type*} [Encodable ι] :
    Summable fun i : ι ↦ (1 / 2 : ℝ) ^ Encodable.encode i :=
  summable_geometric_two.comp_injective Encodable.encode_injective

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

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

Разделы

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

Аффилиация

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