Consecutive-term ratio bounds for a quadratic recurrence
ProvedWorkbookCorrected.plus_47850corrected-formalizationlean-workbooksequencessource-checked
Let a₁ = 1/2 and aₙ₊₁ = aₙ−aₙ² for every integer n ≥ 1. Then 1 ≤ aₙ/aₙ₊₁ ≤ 2 for every integer n ≥ 1.
Formalization Note: Restores the source’s initial index and positive recurrence indices.
Source: InternLM Lean-Workbook, record lean_workbook_plus_47850 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_47850 (a : ℕ → ℝ) (h1 : a 1=1/2)
(h : ∀ n : ℕ, 1 ≤ n → a (n+1)=a n-(a n)^2) :
∀ n : ℕ, 1 ≤ n → 1 ≤ a n/a (n+1) ∧ a n/a (n+1) ≤ 2 := by sorrySource