Boundedness of a square-root averaging recurrence
ProvedWorkbookSource.plus_57482lean-workbooksequencessource-checked
A real sequence satisfies 2xₙ=xₙ₋₁+√(3−3xₙ₋₁²). Then it is bounded: some real M satisfies |xₙ|<M for every natural index n.
Source: InternLM Lean-Workbook, record lean_workbook_plus_57482 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookSource.plus_57482 (x : ℕ → ℝ) (hx: ∀ n, 2*x n = x (n-1) + Real.sqrt (3 - 3*(x (n-1))^2)) : ∃ M, ∀ n, |x n| < M := by sorry
Source