Heros_Method
Provedlimits-of-sequencesproofwikisquare-roots
Hero's method: the sequence x_{n+1} = (x_n + a/x_n)/2 converges to sqrt(a) for a > 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Heros_Method (a : ℝ) (ha : 0 < a) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hrec : ∀ n, x (n + 1) = (x n + a / x n) / 2) : Filter.Tendsto x Filter.atTop (nhds (Real.sqrt a)) := by sorry
Source