Validated numerics

Remarks

Example: the interval Newton test. Let $f(x) = x^2 - 2$ and $X = [1.4, 1.5]$; with midpoint $m = 1.45$ and the enclosure $[2.8, 3.0]$ of $f'$ on $X$, the interval Newton step is $N(X) = m - f(m)/[2.8, 3.0] = 1.45 - 0.1025/[2.8, 3.0] \subseteq [1.4133, 1.4159]$. Since $N(X) \subseteq X$ and $0 \notin [2.8, 3.0]$, the interval Newton theorem shows that $f$ has exactly one zero in $X$, and it lies in $N(X)$. Done with outward rounding, this proves $1.4133 \le \sqrt{2} \le 1.4159$. Non-example: running Newton's method in floating point until two iterates agree to $15$ digits gives an excellent approximation, but no guarantee, so it is not a validated computation.