lean_workbook_plus_26452

Proved

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

Let the series ${x_n}$ be given by: $x_1 = a$ where $a > 0$ , $x_{n+1} = \frac{(x_n)^2 + 2}{3}, n \geq 1$ . Show that if a is such that $x_2 > x_1$ , then the series is strictly growing. And if a is such that $x_2 < x_1$ , the series is strictly decreasing.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26452 (a : ℝ) (x : ℕ → ℝ) (hx: x 1 = a) (hn: ∀ n:ℕ, x (n+1) = (x n)^2 + 2 / 3) : (x 2 > x 1 → ∀ n:ℕ, x (n+1) > x n) ∧ (x 2 < x 1 → ∀ n:ℕ, x (n+1) < x n)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph