11.2.2 Dedekind reals are Cauchy complete

Recall that $x:\mathbb{N}\to\mathbb{Q}$ is a Cauchy sequence when it satisfies

\mathchoice{\prod_{(\epsilon:\mathbb{Q}_{+})}\,}{\mathchoice{{\textstyle\prod_% {(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}\mathchoice{\sum_{(n:\mathbb{N})}\,}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{% \sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}\mathchoice{\prod_{(m,k\geq n)}\,}{\mathchoice{{\textstyle\prod_{(m,k% \geq n)}}}{\prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}}{% \mathchoice{{\textstyle\prod_{(m,k\geq n)}}}{\prod_{(m,k\geq n)}}{\prod_{(m,k% \geq n)}}{\prod_{(m,k\geq n)}}}{\mathchoice{{\textstyle\prod_{(m,k\geq n)}}}{% \prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}{\prod_{(m,k\geq n)}}}|x_{m}-x_{k}|<\epsilon.

(11.2.1)

Note that we did not truncate the inner existential because we actually want to compute rates of convergence—an approximation without an error estimate carries little useful information. By \autorefthm:ttac, (11.2.1) yields a function $M:\mathbb{Q}_{+}\to\mathbb{N}$ , called the modulus of convergence, such that $m,k\geq M(\epsilon)$ implies $|x_{m}-x_{k}|<\epsilon$ . From this we get $|x_{M(\delta/2)}-x_{M(\epsilon/2)}|<\delta+\epsilon$ for all $\epsilon:\mathbb{Q}_{+}$ . In fact, the map $(\epsilon\mapsto x_{M(\epsilon/2)}):\mathbb{Q}_{+}\to\mathbb{Q}$ carries the same information about the limit as the original Cauchy condition (11.2.1). We shall work with these approximation functions rather than with Cauchy sequences.

Definition 11.2.2.

A Cauchy approximation is a map $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{d}}$ which satisfies

\forall(\delta,\epsilon:\mathbb{Q}_{+}).\,|x_{\delta}-x_{\epsilon}|<\delta+\epsilon.

(11.2.2)

The limit of a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{d}}$ is a number $\ell:\mathbb{R}_{\mathsf{d}}$ such that

\forall(\epsilon,\theta:\mathbb{Q}_{+}).\,|x_{\epsilon}-\ell|<\epsilon+\theta.

Theorem 11.2.4.

Every Cauchy approximation in $\mathbb{R}_{\mathsf{d}}$ has a limit.

Proof.

Note that we are showing existence, not mere existence, of the limit. Given a Cauchy approximation $x:\mathbb{Q}_{+}\to\mathbb{R}_{\mathsf{d}}$ , define

	$\displaystyle L_{y}(q)$	$\displaystyle:\!\!\equiv\exists(\epsilon,\theta:\mathbb{Q}_{+}).\,L_{x_{% \epsilon}}(q+\epsilon+\theta),$
	$\displaystyle U_{y}(q)$	$\displaystyle:\!\!\equiv\exists(\epsilon,\theta:\mathbb{Q}_{+}).\,U_{x_{% \epsilon}}(q-\epsilon-\theta).$

It is clear that $L_{y}$ and $U_{y}$ are inhabited, rounded, and disjoint. To establish locatedness, consider any $q,r:\mathbb{Q}$ such that $q<r$ . There is $\epsilon:\mathbb{Q}_{+}$ such that $5\epsilon<r-q$ . Since $q+2\epsilon<r-2\epsilon$ merely $L_{x_{\epsilon}}(q+2\epsilon)$ or $U_{x_{\epsilon}}(r-2\epsilon)$ . In the first case we have $L_{y}(q)$ and in the second $U_{y}(r)$ .

To show that $y$ is the limit of $x$ , consider any $\epsilon,\theta:\mathbb{Q}_{+}$ . Because $\mathbb{Q}$ is dense in $\mathbb{R}_{\mathsf{d}}$ there merely exist $q,r:\mathbb{Q}$ such that

x_{\epsilon}-\epsilon-\theta/2<q<x_{\epsilon}-\epsilon-\theta/4<x_{\epsilon}<% \\ x_{\epsilon}+\epsilon+\theta/4<r<x_{\epsilon}+\epsilon+\theta/2,

and thus $q<y<r$ . Now either $y<x_{\epsilon}+\theta/2$ or $x_{\epsilon}-\theta/2<y$ . In the first case we have

x_{\epsilon}-\epsilon-\theta/2<q<y<x_{\epsilon}+\theta/2,

and in the second

x_{\epsilon}-\theta/2<y<r<x_{\epsilon}+\epsilon+\theta/2.

In either case it follows that $|y-x_{\epsilon}|<\epsilon+\theta$ . ∎

For sake of completeness we record the classic formulation as well.

Corollary 11.2.5.

Suppose $x:\mathbb{N}\to\mathbb{R}_{\mathsf{d}}$ satisfies the Cauchy condition (11.2.1). Then there exists $y:\mathbb{R}_{\mathsf{d}}$ such that

\mathchoice{\prod_{(\epsilon:\mathbb{Q}_{+})}\,}{\mathchoice{{\textstyle\prod_% {(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(% \epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\mathchoice{{% \textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:\mathbb{Q}_{+})% }}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}}{% \mathchoice{{\textstyle\prod_{(\epsilon:\mathbb{Q}_{+})}}}{\prod_{(\epsilon:% \mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{Q}_{+})}}{\prod_{(\epsilon:\mathbb{% Q}_{+})}}}\mathchoice{\sum_{(n:\mathbb{N})}\,}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{% \sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\sum_{(n% :\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb% {N})}}}\mathchoice{\prod_{(m\geq n)}\,}{\mathchoice{{\textstyle\prod_{(m\geq n% )}}}{\prod_{(m\geq n)}}{\prod_{(m\geq n)}}{\prod_{(m\geq n)}}}{\mathchoice{{% \textstyle\prod_{(m\geq n)}}}{\prod_{(m\geq n)}}{\prod_{(m\geq n)}}{\prod_{(m% \geq n)}}}{\mathchoice{{\textstyle\prod_{(m\geq n)}}}{\prod_{(m\geq n)}}{\prod% _{(m\geq n)}}{\prod_{(m\geq n)}}}|x_{m}-y|<\epsilon.

Proof.

By \autorefthm:ttac there is $M:\mathbb{Q}_{+}\to\mathbb{N}$ such that $\bar{x}(\epsilon):\!\!\equiv x_{M(\epsilon/2)}$ is a Cauchy approximation. Let $y$ be its limit, which exists by \autorefRD-cauchy-complete. Given any $\epsilon:\mathbb{Q}_{+}$ , let $n:\!\!\equiv M(\epsilon/4)$ and observe that, for any $m\geq n$ ,

|x_{m}-y|\leq|x_{m}-x_{n}|+|x_{n}-y|=|x_{m}-x_{n}|+|\bar{x}(\epsilon/2)-y|<% \epsilon/4+\epsilon/2+\epsilon/4=\epsilon.\qed

Title	11.2.2 Dedekind reals are Cauchy complete
\metatable