Accuracy after thirty Newton iterations for the square root of 2002
ProvedWorkbookSource.plus_20651lean-workbooksequencessource-checked
Let x₀ = 1000 and xₙ₊₁ = (xₙ + 2002/xₙ)/2 for every natural number n. Then x₃₀ < √2002 + 10⁻⁶.
Source: InternLM Lean-Workbook, record lean_workbook_plus_20651 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookSource.plus_20651 (x : ℕ → ℝ) (x0 : x 0 = 1000) (h : ∀ n, x (n + 1) = 1 / 2 * (x n + 2002 / x n)) : x 30 < 1 / (10^6) + Real.sqrt 2002 := by sorry
Source