Convergence of a quadratic square-root approximation
ProvedWorkbookCorrected.plus_26448corrected-formalizationlean-workbooksequencessource-checked
For c ∈ [0,1], let f₀ = 0 and fₙ₊₁ = fₙ + (c−fₙ²)/2 for every natural number n. Then fₙ converges to √c.
Formalization Note: Restores the complete epsilon/eventual quantifiers required for convergence in the natural source; the original formalization instead required arbitrary accuracy at a single index.
Source: InternLM Lean-Workbook, record lean_workbook_plus_26448 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_26448 (c : ℝ) (hc : c ∈ Set.Icc 0 1) (f : ℕ → ℝ)
(h0 : f 0 = 0) (h : ∀ n : ℕ, f (n+1)=f n+(c-(f n)^2)/2) :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |f n-Real.sqrt c| < ε := by sorrySource