hasSum_geometric_two' — Mathlib

English

For any real a with 0 < a/2, the series sum of a/2 · (1/2)^n converges to a.

Русский

Для любого вещественного a с 0 < a/2 сумма ряда a/2 · (1/2)^n равна a.

LaTeX

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

Lean4

theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun n : ℕ ↦ a / 2 / 2 ^ n) a :=
  by
  convert HasSum.mul_left (a / 2) (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1
  · funext n
    simp only [one_div, inv_pow]
    rfl
  · norm_num

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