Theorem 5.3, p. 320 — from ‖x₀ − x*‖ ≤ μ/(2M), Newton's method is well defined and ‖x_{k+1} − x*‖ ≤ (M/μ)‖x_k − x*‖²

Let $f:\mathbb R^n\to\mathbb R$ be a $C^2$ function whose Hessian is $M$-Lipschitz in operator norm, $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ for all $x,y$, with $M>0$. Let $x^*$ be a local minimum of $f$ with strictly positive Hessian, $\nabla^2 f(x^*)\succeq\mu I_n$ for some $\mu>0$. Suppose the starting point $x_0$ satisfies

Then Newton's method started at $x_0$ is well defined: there is exactly one sequence $(x_k)_{k\ge0}$ with first term $x_0$ satisfying $\nabla^2 f(x_k)(x_k-x_{k+1})=\nabla f(x_k)$ for all $k$, and along it every Hessian $\nabla^2 f(x_k)$ is invertible, so that $x_{k+1}=x_k-[\nabla^2 f(x_k)]^{-1}\nabla f(x_k)$. Moreover the iterates converge to $x^*$ at a quadratic rate:

This is the classical local quadratic convergence of Newton's method: close enough to a nondegenerate local minimum, the number of correct digits roughly doubles at every step. It is the starting point of the interior point methods of §5.3, which keep Newton's method inside such a region of fast convergence.

Formalization Note $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); the gradient and Hessian are explicit maps tied to $f$ (definition item), and the Hessian condition at $x^*$ is the quadratic-form inequality $\langle\nabla^2 f(x^*)v,v\rangle\ge\mu\|v\|^2$. "Well-defined" is formalized as unique existence of a Newton run from $x_0$ together with invertibility (bijectivity) of every Hessian along every such run; the quadratic rate and the convergence are asserted for every Newton run from $x_0$. $M>0$ is a disclosed implicit hypothesis (the radius $\mu/(2M)$ divides by $M$; with $M=0$ Lean's $\mu/0=0$ would force $x_0=x^*$). Convexity of $f$ is not assumed, as on the page.