An invariant interval for a rational recurrence
ProvedWorkbookCorrected.plus_60440corrected-formalizationlean-workbooksequencessource-checked
Let 2<a≤3, x₁=a, and xₙ₊₁=xₙ²/(2(xₙ−1)) for every integer n≥1. Then xₙ≤3 for every integer n≥1.
Formalization Note: Restores the source’s missing initial equality and its positive indices.
Source: InternLM Lean-Workbook, record lean_workbook_plus_60440 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_60440 (a : ℝ) (x : ℕ → ℝ) (ha : 2 < a) (ha3 : a ≤ 3)
(h1 : x 1=a) (h : ∀ n : ℕ, 1 ≤ n → x (n+1)=x n^2/(2*(x n-1))) :
∀ n : ℕ, 1 ≤ n → x n ≤ 3 := by sorrySource