lean_workbook_plus_78640

Proved

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

Show that $a_{n+1} = \frac{a_n^2}{a_n^2 - a_n + 1} \le \frac{4a_n^2}{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78640 (a : ℕ → ℝ) (n : ℕ) (ha : a (n + 1) = a n ^ 2 / (a n ^ 2 - a n + 1)) : a (n + 1) ≤ 4 * a n ^ 2 / 3   :=  by sorry

Source