A second-order reciprocal average stays between one and two
ProvedWorkbookCorrected.plus_66762corrected-formalizationlean-workbooksequencessource-checked
Let a₁=a₂=1 and aₙ₊₂=(aₙ₊₁+2/aₙ)/2 for every integer n≥1. Then 1≤aₙ≤2 for every integer n≥1.
Formalization Note: Uses the source’s original positive indices.
Source: InternLM Lean-Workbook, record lean_workbook_plus_66762 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_66762 (a : ℕ → ℝ) (h1 : a 1 = 1) (h2 : a 2 = 1) (h : ∀ n : ℕ, 1 ≤ n → a (n+2)=(a (n+1)+2/a n)/2) : ∀ n : ℕ, 1 ≤ n → 1 ≤ a n ∧ a n ≤ 2 := by sorry
Source