20241022-modulated-real-sequences.tex

\documentclass[12pt,a4paper]{article}  % -*- coding: utf-8 -*-
\usepackage[a4paper,margin=1.5cm]{geometry}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{times}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
%
\usepackage{mathrsfs}
%\usepackage{bm}
%\usepackage{stmaryrd}
\usepackage{wasysym}
\usepackage{url}
\usepackage{graphicx}
\usepackage[usenames,dvipsnames]{xcolor}
%\usepackage{tikz}
%\usetikzlibrary{matrix,arrows,decorations.markings}
%\usepackage{hyperref}
%
%
%
\theoremstyle{definition}
\newtheorem{comcnt}{Anything}
\newcommand\thingy{%
\refstepcounter{comcnt}\medbreak\noindent\textparagraph\textbf{\thecomcnt.} }
\newtheorem{prop}[comcnt]{Proposition}
%
%
%
\newcommand{\apart}{\mathrel{\#}}
%
%
%
\begin{document}
\pretolerance=8000
\tolerance=50000

\thingy We work in a constructive math setting in the absence of any
form of Choice (except Unique Choice; e.g., a topos with a natural
numbers object, or in $\mathsf{IZF}$).  We denote by $\mathbb{R}$ the
set of Dedekind reals, which we simply call “real numbers” or “reals”.

\thingy We use the following definitions:

\begin{itemize}
\item An \textbf{unmodulated}\footnote{To avoid the confusion arising
from both meanings of the word “Cauchy sequence” (some people assume a
modulus, others do not), it seems wiser to systematically prefix the
word “Cauchy” by either “modulated” or “unmodulated”.  Of course,
“unmodulated” really means “not assumed to be modulated”, but this is
too much of a mouthful.}\textbf{\ Cauchy sequence} of real numbers is
  a sequence $(x_n)$ such that
\[
\forall n\in\mathbb{N}.\penalty0\,
\exists m\in\mathbb{N}.\penalty0\,
\forall i,j\geq m.\penalty0\,|x_i-x_j|\leq 2^{-n}
\]
Such a sequence has a (unique) limit: in other words, there is a
unique $y$ satisfying $\forall n\in\mathbb{N}.\penalty0\, \exists
m\in\mathbb{N}.\penalty0\, \forall i\geq m.\penalty0\,|x_i-y|\leq
2^{-n}$, and conversely, this condition implies that $(x_n)$ is
unmodulated Cauchy (as follows easily from the fact that $|x_i-x_j|
\leq |x_i-y| + |y-x_j|$).  For extra emphasis, we can say that $(x_n)$
\textbf{converges unmodulatedly} to $y$ when it is unmodulated Cauchy
and has $y$ as limit.
\item An \textbf{unmodulated Cauchy real} is a real number which is
  the limit of an unmodulated Cauchy sequence of \emph{rationals}
  (i.e., there is a sequence of rationals which converges
  unmodulatedly to said real).
\item A \textbf{modulated Cauchy sequence} of real numbers is a
  sequence $(x_n)$ such that
\[
\exists \mu\colon \mathbb{N}\to\mathbb{N}.\penalty0\,
\forall n\in\mathbb{N}.\penalty0\,
\forall i,j\geq \mu(n).\penalty0\,|x_i-x_j|\leq 2^{-n}
\]
(Of course this is stronger than an unmodulated Cauchy sequence since
we are now requiring a choice $\mu(n)$ of the $m$ for a given $n$.)
We call such a $\mu\colon \mathbb{N}\to\mathbb{N}$ a
\textbf{modulus}\footnote{That is, a modulus of Cauchyness, but since
a modulus of Cauchyness also works as a modulus of convergence and a
modulus of convergence provides a modulus of Cauchyness after a mere
shift, the distinction between the two can be ignored.} for the
sequence.  Note that its limit $y$ automatically satisfies $\exists
\mu\colon \mathbb{N}\to\mathbb{N}.\penalty0\, \forall
n\in\mathbb{N}.\penalty0\, \forall i\geq \mu(n).\penalty0\,|x_i-y|\leq
2^{-n}$ (indeed, this holds for the very same $\mu$ as in the
displayed formula), and conversely, this condition implies that
$(x_n)$ is modulated Cauchy (as follows again easily from the fact
that $|x_i-x_j| \leq |x_i-y| + |y-x_j|$).  We shall say that $(x_n)$
\textbf{converges modulatedly} to $y$ when it is modulated Cauchy and
has $y$ as limit.
\item An \textbf{modulated Cauchy real} is a real number which is the
  limit of a modulated Cauchy sequence of \emph{rationals} (i.e.,
  there is a sequence of rationals which converges modulatedly to said
  real).
\end{itemize}

Of course, in the absence of a modicum of Choice (say, Countable
Choice, or even just Countable Choice for $\mathbb{N}$) or in
classical logic, every Cauchy sequence is modulated (construct $\mu$
by choosing an $m$ for each $n$, or, in classical logic, say, by
taking the smallest one which works), and, in fact, all Dedekind reals
are modulated Cauchy reals, so all these distinctions vanish.

\thingy\label{modulus-explicitation} Our use of $2^{-n}$ in the above
definitions is, of course, irrelevant, and $\frac{1}{n}$ (assuming
$n\geq 1$) could be used as well, or, indeed, we could use
$\varepsilon$ ranging over the positive rationals.

In the case of a modulated Cauchy sequence, we can replace $\mu(n)$ by
$\max(\mu(0),\ldots,\mu(n))$ to ensure that $\mu$ is order-preserving
(weakly increasing) and then $x_n$ by $x_{\mu(n)}$ to ensure that we
have simply
\[
\forall n\in\mathbb{N}.\penalty0\,
\forall i,j\geq n.\penalty0\,|x_i-x_j|\leq 2^{-n}
\]
which is sometimes more convenient.  This might be called an
\textbf{explicitly modulated Cauchy sequence} or something of the
sort, and of course its limit $y$ automatically satisfies $\forall
n\in\mathbb{N}.\penalty0\, \forall i\geq n.\penalty0\,|x_i-y|\leq
2^{-n}$.  By what has just been said, every modulated Cauchy real is
the limit of an explicitly modulated Cauchy sequence of rationals, so
we do not need to introduce a notion of “explicitly modulated Cauchy
real”.

\thingy Of course, every real number has a sequence of \emph{reals}
that converges modulatedly to it: namely the constant sequence.  This
is why when defining the terms “unmodulated Cauchy real” and
“modulated Cauchy real”, we refer specifically to sequences of
\emph{rationals}.

Perhaps surprisingly, it turns out that the notion of modulatedness of
a sequence of rationals is a property associated to the limit, as the
following proposition shows, which is taken from Lubarsky \& Richman,
“Signed-Bit Representations of Real Numbers”, \textit{J. Log. Anal.}
\textbf{1} (2009), paper 10 (theorem 2.2):

\begin{prop}\label{sequence-tending-to-modulated-real}
If $x$ is a modulated Cauchy real and $(s_n)$ a sequence of rationals
that converges (unmodulatedly!) to $x$, then, in fact, $(s_n)$ is
modulated Cauchy (and thus, converges modulatedly to $x$).
\end{prop}
\begin{proof}
By assumption, there exists a modulated Cauchy sequence $(r_n)$
converging to $x$.  As explained in ¶\ref{modulus-explicitation}, we
can assume w.l.o.g. that $\forall n\in\mathbb{N}.\penalty0\, \forall
i\geq n.\penalty0\,|r_i-x|\leq 2^{-n}$.  We are also assuming that
$(s_n)$ converges (unmodulatedly) to $x$, and we wish to show that, in
fact, it is modulated Cauchy.

Let $n\in\mathbb{N}$.  Since $s_n$ converges to $x$, there is $m\geq
n+3$ such that $|s_i-x| \leq 2^{-(n+3)}$ if $i\geq m$; furthermore, by
the assumption on $(r_n)$, we also have $|r_i-x| \leq 2^{-(n+3)}$ if
$i\geq m$, which implies $|s_i-r_i| \leq 2^{-(n+2)}$.  Define $\nu(n)$
to be the smallest $m\geq n+3$ such that $i\geq m$ implies $|s_i-r_i|
\leq 2^{-(n+2)}$: this is well-defined because (a) we have just
pointed out that such a $m$ exists, and (b) the condition $|s_i-r_i|
\leq 2^{-(n+2)}$ is decidable (recall that any inhabited and decidable
subset of $\mathbb{N}$ has a smallest element).

Now if $i,j\geq\nu(n)$ then $|s_i-r_i| \leq 2^{-(n+2)}$ and $|s_j-r_j|
\leq 2^{-(n+2)}$, but also $|r_i-r_j| \leq 2^{-(n+3)}$, and this
implies $|s_i-s_j| \leq 2^{-n}$.  So we have shown that $(s_n)$ is
modulated Cauchy (with modulus $\nu$).
\end{proof}

Note how in the above proof it is crucial that we are dealing with
rationals: one certainly cannot assert that if two sequences of real
numbers have the same limit and one is modulated Cauchy then the other
one also is.  The assumption that the $r_i$ and $s_i$ are rationals
has been used in the proof to conclude that $|s_i-r_i| \leq 2^{-N}$ is
decidable.

\bigskip

We now fully state and prove a pair of propositions left as exercises
to the reader in Lubarsky, “On the Cauchy Completeness of the
Constructive Cauchy Reals”, \textit{Electron. Notes
  Theor. Comput. Sci.}, \textbf{167} (2007), 225–254.

The first is easy, and does not care about the elements of the
sequences being rationals:

\begin{prop}
(A) Let $(x_{i,k})_{(i,k)\in\mathbb{N}^2}$ be a double sequence of
  reals, and let $\mu\colon \mathbb{N}^2\to\mathbb{N}$.  We assume
  that
\begin{itemize}\setlength\itemsep{0pt}
\item for each $i\in\mathbb{N}$, the sequence
  $(x_{i,k})_{k\in\mathbb{N}}$ is modulated Cauchy with $n\mapsto
  \mu(i,n)$ as modulus, and, if we call $y_i$ its limit,
\item the sequence $(y_i)$ is unmodulated Cauchy.
\end{itemize}
\emph{Then} the limit $z$ of the $y_i$ is, in fact, the limit of a
sequence $(x_{\alpha(i),\beta(i)})_{i\in\mathbb{N}}$ extracted from
$(x_{i,k})$.  In particular, if $x_{i,k} = r_{i,k}$ are actually
rationals (so the $y_i$ are modulated Cauchy reals), then $z$ is an
unmodulated Cauchy real.

(B) \emph{Furthermore}, if we also assume that the sequence $(y_i)$ is
modulated Cauchy, then the extracted sequence
$(x_{\alpha(i),\beta(i)})$ can also be found to be modulated Cauchy.
In particular, under this assumption, if $x_{i,k} = r_{i,k}$ are
actually rationals, then $z$ is a modulated Cauchy real.
\end{prop}

(In short: (A) “an unmodulated sequence of Cauchy-and-modulus pairs
gives an unmodulated Cauchy extracted sequence” and (B) “a modulated
sequence of Cauchy-and-modulus pairs gives a modulated Cauchy
extracted sequence”.)

\begin{proof}
First, similarly to ¶\ref{modulus-explicitation}, by redefining
$\mu(i,k)$ as $\max(\mu(i,0),\ldots,\mu(i,k+1))$ and then $x_{i,k}$ as
$x_{i,\mu(i,k)}$, we can arrange w.l.o.g. that $\forall
i\in\mathbb{N}.\penalty0\, \forall n\in\mathbb{N}.\penalty0\, \forall
k\geq n.\penalty0\,|x_{i,k}-y_i|\leq 2^{-(n+1)}$.

We then define the extracted sequence to be simply $t_i = x_{i,i}$.

In case (A): if $n\in\mathbb{N}$, then there is $m\in\mathbb{N}$,
which we can take to be $\geq n$, such that $|y_i-z| \leq 2^{-(n+1)}$
if $i\geq m$.  But now $|x_{i,i}-z| \leq |x_{i,i}-y_i| + |y_i-z| \leq
2^{-(n+1)} + 2^{-(n+1)} \leq 2^{-n}$, that is $|t_i-z| \leq 2^{-n}$
for $i\geq m$.  So indeed $(t_i)$ has limit $z$.

In case (B): now we are given a modulus $\nu$ for the sequence
$(y_i)$.  The argument of the previous paragraph applied with $m =
\nu(n+1)$ shows that $|t_i-z| \leq 2^{-n}$ for $i\geq \nu(n+1)$, so
indeed $(t_i)$ converges modulatedly to $z$.
\end{proof}

The second proposition is, as Lubarsky puts it in \textit{loc. cit.},
“a bit tricky”, and really shouldn't have been left to the reader.
The fact that we are dealing with rationals is, this time, crucial, as
like in prop. \ref{sequence-tending-to-modulated-real} we will use the
decidability of rational inequalities:

\begin{prop}
Let $(r_{i,k})_{(i,k)\in\mathbb{N}^2}$ be a double sequence of
rationals.  We assume that
\begin{itemize}\setlength\itemsep{0pt}
\item for each $i\in\mathbb{N}$, the sequence
  $(r_{i,k})_{k\in\mathbb{N}}$ is unmodulated Cauchy, and, if we call
  $y_i$ its limit,
\item the sequence (of unmodulated Cauchy reals) $(y_i)$ is modulated
  Cauchy.
\end{itemize}
\emph{Then} the limit $z$ of the $y_i$ is, in fact, the limit of a
sequence $(r_{\alpha(i),\beta(i)})_{i\in\mathbb{N}}$ extracted from
$(r_{i,k})$, and in particular, it is an unmodulated Cauchy real.
\end{prop}

(In short: “a modulated sequence of unmodulated Cauchy sequences of
rationals converges to an unmodulated Cauchy real”.)

\begin{proof}
First, similarly to ¶\ref{modulus-explicitation}, by redefining
$\mu(n)$ as $\max(\mu(0),\ldots,\mu(n+1))$ and then $r_{n,k}$
(resp. $y_n$) as $r_{\mu(n),k}$ (resp. $y_{\mu(n)}$), we can arrange
w.l.o.g. that $\forall n\in\mathbb{N}.\penalty0\, \forall i,j\geq
n.\penalty0\,|y_i-y_j|\leq 2^{-(n+1)}$.

We now wish to extract from the $r_{i,k}$ a sequence $(s_i)$ of
rationals tending (unmodulatedly) to $z$.  To this effect, we first
construct $\rho\colon \mathbb{N}\to\mathbb{N}$ as follows.

Let $n\in\mathbb{N}$.  Since the $(r_{i,k})_k$ converge to $y_i$ for
all $0\leq i\leq n$, there is $\ell$ such that $k\geq\ell$ implies
$|r_{i,k}-y_i| \leq 2^{-(n+2)}$ for all $0\leq i\leq n$; furthermore,
by the assumption on $(y_i)$, we also have $|y_i-y_j| \leq 2^{-(i+1)}$
if $0\leq i\leq j\leq n$ so $|r_{i,k}-r_{j,k}| \leq |r_{i,k}-y_i| +
|y_i-y_j| + |r_{j,k}-y_j| \leq 2^{-(n+2)} + 2^{-(i+1)} + 2^{-(n+2)}
\leq 2^{-i}$ when $0\leq i\leq j\leq n$ and $k\geq\ell$.  Define
$\rho(n)$ to be the smallest $\ell\geq n$ such that $k\geq\ell$
implies $|r_{i,k}-r_{j,k}| \leq 2^{-i}$ for all $0\leq i\leq j\leq n$
(the fact that “the smallest $\ell$” is meaningful here is as in the
proof of proposition \ref{sequence-tending-to-modulated-real}: (a) we
have just seen that such an $\ell$ exists, and (b) the condition that
$|r_{i,k}-r_{j,k}| \leq 2^{-i}$ for all $0\leq i\leq j\leq n$ is
decidable).

Note that $\rho$ is order-preserving (or that we can make it so) and
$\rho(n)\geq n$, and its definition means that $|r_{i,k}-r_{j,k}| \leq
2^{-\min(i,j)}$ for all $i,j$ and $k \geq \max(\rho(i),\rho(j))$.

Now we put $s_i = r_{i,\rho(i)}$.  We wish to show that $s_i$ tends
to $z$.  Let $n\in\mathbb{N}$.  We have $|y_{n+1}-z| \leq 2^{-(n+2)}$.
Now, since $(r_{n+1,k})_k$ converge to $y_{n+1}$, there is $\ell$,
which we can take to be $\geq n+1$ such that if $k\geq\ell$ then
$|r_{n+1,k}-y_{n+1}| \leq 2^{-(n+2)}$: in particular, if $j\geq\ell$
(which implies $\rho(j) \geq \rho(\ell) \geq \ell$) then we have
$|r_{n+1,\rho(j)}-y_{n+1}| \leq 2^{-(n+2)}$.  But the previous
paragraph implies that, if $j\geq n+1$ then
$|r_{n+1,\rho(j)}-r_{j,\rho(j)}| \leq 2^{-(n+1)}$.  We now get
$|r_{j,\rho(j)}-z| \leq |r_{n+1,\rho(j)}-r_{j,\rho(j)}| +
|r_{n+1,\rho(j)}-y_{n+1}| + |y_{n+1}-z| \leq 2^{-(n+1)} + 2^{-(n+2)} +
2^{-(n+2)} \leq 2^{-n}$, which proves $|s_j-z| \leq 2^{-n}$ for
$j\geq\ell$.  So indeed $(s_i)$ has limit $z$.
\end{proof}

\end{document}