Nested interval theorem (source code)

= Nested interval theorem

If $I_1\supseteq I_2\supseteq\cdots$ are nonempty <closed intervals> with finite endpoints, then at least one <real number> belongs to every member. If their lengths tend to zero, exactly one <real number> belongs to every member. The result turns an unlimited sequence of consistent enclosures into an existence guarantee.

Write $I_n=[a_n,b_n]$. Nesting makes the left endpoints <nondecreasing> and the right endpoints <nonincreasing>. Their bounds give finite <supremum> and <infimum>, with
$$
\bigcap_{n=1}^{\infty}I_n=
\left[\sup_{n\geq1}a_n,\ \inf_{n\geq1}b_n\right].
$$
Indeed, every $b_n$ is an <upper bound> for all the $a_j$, so the <least-upper-bound property> gives $\sup_j a_j\leq b_n$ for every $n$. This proves the displayed interval is nonempty. If $b_n-a_n\to0$, its two endpoints must coincide. This is the connection to the <completeness of the real numbers> discussed in https://homepage.univie.ac.at/christian.schmeiser/einfanalysis.pdf[Günther Hörmann and David Langer, Einführung in die Analysis, §§3.15–3.16: nested intervals and order completeness].

\Image[/nested-intervals-intersection-cases.png]
{title=Nested enclosures can converge to one point, retain a whole interval, or have no common point when endpoints are excluded}

The distinction between existence and uniqueness is useful in computation. If an unknown point $x_*$ lies in every $[a_n,b_n]$, the <midpoint> $m_n=(a_n+b_n)/2$ satisfies
$$
|m_n-x_*|\leq\frac{b_n-a_n}{2}.
$$
Thus the enclosure itself certifies an <absolute error> without knowing the answer. The <bisection error bound> is the special case where each update halves the width.

Closedness and a finite initial enclosure matter. The <open intervals> $(0,1/n)$ have no common point, while the closed but unbounded intervals $[n,\infty)$ also have empty intersection. A picture of a few intervals cannot certify the intersection of an infinite family; the hypotheses of the <nested interval theorem> do that work.