tsum_geometric_two_encode_le_two — Mathlib

English

For any encodable index set, the sum ∑' i (1/2)^{encode i} is at most 2.

Русский

Для любого кодируемого множества индексов сумма ∑' i (1/2)^{encode i} не превосходит 2.

LaTeX

$$$$\sum_{i} (\tfrac{1}{2})^{\mathrm{encode}(i)} \le 2.$$$$

Lean4

theorem tsum_geometric_two_encode_le_two {ι : Type*} [Encodable ι] : ∑' i : ι, (2⁻¹ : ℝ≥0∞) ^ encode i ≤ 2 :=
  (ENNReal.tsum_comp_le_tsum_of_injective encode_injective _).trans_eq ENNReal.tsum_geometric_two

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