Prove2Me

Boundedness from a quadratic inequality between adjacent sequence terms

Proved
WorkbookCorrected.plus_11940

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Let (xn)n≥1(x_n)_{n\ge1} be a sequence of real numbers which satisfies the following relation: (xn+1−xn)(xn+1+xn+1)≤0(x_{n+1}-x_n)(x_{n+1}+x_n+1)\le0. Show that (xn)n≥1(x_n)_{n\ge1} is bounded

Formalization Note: The source sequence starts at n=1. This correction restricts both the relation and the boundedness conclusion to the stated positive indices, leaving an unused index0 unconstrained.

Source: InternLM Lean-Workbook, record lean_workbook_plus_11940 (Apache-2.0).

Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_11940 (x : ℕ → ℝ)
    (h : ∀ n : ℕ, 1≤n → (x (n+1)-x n)*(x (n+1)+x n+1) ≤ 0) :
    ∃ M : ℝ, ∀ n : ℕ, 1≤n → |x n| ≤ M := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_11940; Apache-2.0

View graph