Bounds, strict increase, and limit of a logistic recurrence
ProvedWorkbookCorrected.plus_30199corrected-formalizationlean-workbooksequencessource-checked
Let 0 < x₁ < 1 and xₙ₊₁ = xₙ(2−xₙ) for every integer n ≥ 1. Every term lies in (0,1), the sequence is strictly increasing, and it converges to 1.
Formalization Note: Restores the omitted upper bound on the initial value and the positive indexing, and includes all three conclusions requested in the source.
Source: InternLM Lean-Workbook, record lean_workbook_plus_30199 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_30199 (x : ℕ → ℝ) (hx : 0 < x 1 ∧ x 1 < 1)
(h : ∀ n : ℕ, 1 ≤ n → x (n+1)=x n*(2-x n)) :
(∀ n : ℕ, 1 ≤ n → 0 < x n ∧ x n < 1) ∧
(∀ n : ℕ, 1 ≤ n → x n < x (n+1)) ∧
(∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |x n-1| < ε) := by sorrySource