Prove2Me

lean_workbook_plus_6877

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let un=xnxn+1 u_n=x_nx_{n+1}\nWe have u0=ab u_0=ab and un=12(1+un−1) u_n=\frac 12(1+u_{n-1}) and so un=1+ab−12n u_n=1+\frac{ab-1}{2^n}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6877  (a b : ℝ)
  (n : ℕ)
  (u : ℕ → ℝ)
  (h₀ : u 0 = a * b)
  (h₁ : ∀ n, u (n + 1) = (1 + u n) / 2) :
  u n = 1 + (a * b - 1) / 2 ^ n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph