More Measure Theory in $\mathsf{WWKL}_0$

In this section we show that a good theory of measurable functions and measurable sets can be developed within $\mathsf{WWKL}_0$.

We first consider pointwise values of measurable functions. Our approach is due to Yu [21,24].

Let X be a compact separable metric space and let $\mu:C(X)\to\mathbb{R}$be a positive Borel probability measure on X. Recall that $L_1(X,\mu)$ is defined within $\mathsf{RCA}_0$ as the completion of C(X)under the L₁-norm. In what sense or to what extent can we prove that a point of the Banach space $L_1(X,\mu)$ gives rise to a function $f:X\to\mathbb{R}\,$?

In order to answer this question, recall that $f\in L_1(X,\mu)$ is given by a sequence $f_n\in C(X)$, $n\in\mathbb{N}$, which converges to fin the L₁-norm; more precisely

$$\Vert f_n-f_{n+1}\Vert _1 \,\leq\, \frac1{2^n}$$

for all $n\in\mathbb{N}$. We now observe that it is provable in $\mathsf{WWKL}_0$ that the sequence of continuous functions f_n, $n\in\mathbb{N}$, converges pointwise almost everywhere. This is established by the following proposition:

Proposition 4.1 (Yu [21])   Provably in $\mathsf{WWKL}_0$ we have a sequence of closed sets

$$C^f_0 \subseteq C^f_1 \subseteq \dots \subseteq C^f_n \subseteq\dots\,,\,\, n\in\mathbb{N}$$

such that

$$\mu(X\setminus C^f_n) \,\,\leq\,\, \frac1{2^n}$$

for all n, and

$$\vert f_m(x)-f_{m'}(x)\vert\,\,\leq\,\, \frac1{2^k}$$

for all $x\in C^f_n$ and all m, m', k such that $m,m'\geq n+2k+2$.

Proof. Put

$$C^f_n\,\,=\,\,\left\{\,x\,\,\Big\vert\,\,\forall k\sum_{i=n+... ...f_i(x)-f_{i+1}(x)\vert\,\, \leq\,\,\frac1{2^k}\,\right\} \,\,.$$

Then for $x\in C^f_n$ and $m'\geq m\geq n+2k+2$ we have

$$\begin{eqnarray*}\vert f_m(x)-f_{m'}(x)\vert & \leq & \sum_{i=m}^{m'-1}\vert f_i... ...fty\vert f_i(x)-f_{i+1}(x)\vert \\ & \leq & \frac1{2^k} \,\,. \end{eqnarray*}$$

Moreover C^f_n is a closed set. It remains to show that $\mu(X\setminus C^f_n)\leq1/2^n$. To see this, note that $C^f_n=\bigcap_{k=0}^\infty C^f_{nk}$ where

$$C^f_{nk}\,\,=\,\,\left\{\,x\,\,\Big\vert\,\,\sum_{i=n+2k+2}^\... ...t f_i(x)-f_{i+1}(x)\vert\,\,\leq\,\,\frac1{2^k}\,\right\} \,\,.$$

We need a lemma:

Lemma 4.2   The following is provable in $\mathsf{RCA}_0$. For $f\in C(X)$ and $\epsilon>0$, we have $\mu(\{x\mid f(x)>\epsilon\}) \,\leq\,\Vert f\Vert _1/\epsilon$.

Proof. Put $U=\{x\mid f(x)>\epsilon\}$. Note that U is an open set. If $g\in C(X)$, $0\leq g\leq1$, g=0 on $X\setminus U$, then we have $\epsilon g\leq\vert f\vert$, hence $\epsilon\mu(g)=\mu(\epsilon g)\leq\mu(\vert f\vert)=\Vert f\Vert _1$, hence $\mu(g)\leq\Vert f\Vert _1/\epsilon$. Thus $\mu(U)\leq\Vert f\Vert _1/\epsilon$ and the lemma is proved.

Using this lemma we have

$$\begin{eqnarray*}\mu(X\setminus C^f_{nk}) &=& \mu\left(\left\{x\,\Big\vert\,\su... ...m_{i=n+2k+2}^\infty\frac1{2^i} \\ &=& \frac1{2^{n+k+1}} \,\,, \end{eqnarray*}$$

hence by countable additivity

$$\begin{eqnarray*}\mu(X\setminus C^f_n) &\leq& \sum_{k=0}^\infty\,\mu(X\setminus ... ...sum_{k=0}^\infty\,\frac1{2^{n+k+1}} \,\,=\,\, \frac1{2^n} \,\,. \end{eqnarray*}$$

This completes the proof of Proposition 4.1.

Remark 4.3 (Yu [21])   In accordance with Proposition 4.1, for

$$f\,\,=\,\,\left\langle f_n\right\rangle_{n\in\mathbb{N} }\,\,\in\,\, L_1(X,\mu)$$

and $x\in\bigcup_{n=0}^\infty C^f_n$, we define $f(x)=\lim_{n\to\infty}f_n(x)$. Thus we see that f(x) is defined on an $F_\sigma$ set of measure 1. Moreover, if f=g in $L_1(X,\mu)$, i.e. if $\Vert f-g\Vert _1=0$, then f(x)=g(x) for all x in an $F_\sigma$ set of measure 1. These facts are provable in $\mathsf{WWKL}_0$.

We now turn to a discussion of measurable sets within $\mathsf{WWKL}_0$. We sketch two approaches to this topic. Our first approach is to identify measurable sets with their characteristic functions in $L_1(X,\mu)$, according to the following definition.

Definition 4.4   This definition is made within $\mathsf{WWKL}_0$. We say that $f\in L_1(X,\mu)$ is a measurable characteristic function if there exists a sequence of closed sets

$$C_0\subseteq C_1\subseteq\dots\subseteq C_n\subseteq\dots\,,\quad n\in\mathbb{N}\,,$$

such that $\mu(X\setminus C_n)\leq1/2^n$ for all n, and $f(x)\in\{0,1\}$ for all $x\in\bigcup_{n=0}^\infty C_n$. Here f(x) is as defined in Remark 4.3.

Our second approach is more direct, but in its present form it applies only to certain specific situations. For concreteness we consider only Lebesgue measure $\mu_L$ on the unit interval [0,1]. Our discussion can easily be extended to Lebesgue measure on the n-cube [0,1]ⁿ, the ``fair coin'' measure on the Cantor space $2^\mathbb{N}$, etc.

Definition 4.5   The following definition is made within $\mathsf{RCA}_0$. Let S be the Boolean algebra of finite unions of intervals in [0,1] with rational endpoints. For E₁, $E_2\in S$ we define the distance

$$d(E_1,E_2)\,\,=\,\,\mu_L((E_1\setminus E_2)\cup(E_2\setminus E_1)) \,\,,$$

the Lebesgue measure of the symmetric difference of E₁ and E₂. Thus d is a pseudometric on S, and we define $\widehat{S}$ to be the compact separable metric space which is the completion of S under d. A point $E\in\widehat{S}$ is called a Lebesgue measurable set in [0,1].

We shall show that these two approaches to measurable sets (Definitions 4.4 and 4.5) are equivalent in $\mathsf{WWKL}_0$.

Begin by defining an isometry $\chi:S\to L_1([0,1],\mu_L)$ as follows. For $0\leq a<b\leq1$ define

$$\chi([a,b])\,\,=\,\,\left\langle f_n\right\rangle_{n\in\mathbb{N} }\,\,\in\,\,L_1([0,1],\mu_L)$$

where f_n(0)=f_n(a)=f_n(b)=f_n(1)=0 and

$$f_n\!\left(a+\frac{b-a}{2^{n+1}}\right) \,=\, f_n\!\left(b-\frac{b-a}{2^{n+1}}\right) \,=\, 1$$

and $f_n\in C([0,1])$ is piecewise linear otherwise. Thus $\chi([a,b])$ is a measurable characteristic function corresponding to the interval [a,b]. For $0\leq a_1<b_1<\dots<a_k<b_k\leq1$ define

$$\chi([a_1,b_1]\cup\dots\cup[a_k,b_k]) \,\,=\,\, \chi([a_1,b_1])+\dots+\chi([a_k,b_k]) \,.$$

It is straightforward to prove in $\mathsf{RCA}_0$ that $\chi$ extends to an isometry

$$\widehat{\chi}:\widehat{S}\to L_1([0,1],\mu_L) \,\,.$$

Proposition 4.6   The following is provable in $\mathsf{WWKL}_0$. If $E\in\widehat{S}$ is a Lebesgue measurable set, then $\widehat{\chi}(E)$ is a measurable characteristic function in $L_1([0,1],\mu_L)$. Conversely, given a measurable characteristic function $f\in L_1([0,1],\mu_L)$, we can find $E\in\widehat{S}$ such that $\widehat{\chi}(E)=f$ in $L_1([0,1],\mu_L)$.

Proof. It is straightforward to prove in $\mathsf{RCA}_0$ that for all $E\in\widehat{S}$, $\widehat{\chi}(E)$ is a measurable characteristic function.

For the converse, let f be a measurable characteristic function. By Definition 4.4 we have that $f(x)\in\{0,1\}$ for all $x\in\bigcup_{n=0}^\infty C_n$. By Proposition 4.1 we have |f(x)-f_3n+3(x)|<1/2ⁿ for all $x\in C^f_n$. Put $U_n=\{x\mid\vert f_{3n+3}(x)-1\vert<1/2^n\}$ and $V_n=\{x\mid\vert f_{3n+3}(x)\vert<1/2^n\}$. Then for $n\geq1$, U_n and V_n are disjoint open sets. Moreover $C_n\cap C^f_n\subseteq U_n\cup V_n$, hence $\mu_L(U_n\cup V_n)\geq1-1/2^{n-1}$. By countable additivity (Theorem 3.3) we can effectively find $E_n,F_n\in S$ such that $E_n\subseteq U_n$ and $F_n\subseteq V_n$ and $\mu_L(E_n\cup F_n)\geq1-1/2^{n-2}$. Put $E=\left\langle E_{n+5}\right\rangle_{n\in\mathbb{N} }$. It is straightforward to show that E belongs to $\widehat{S}$ and that $\widehat{\chi}(E)=f$ in $L_1([0,1],\mu_L)$. This completes the proof.

Remark 4.7   We have presented two notions of Lebesgue measurable set and shown that they are equivalent in $\mathsf{WWKL}_0$. Our first notion (Definition 4.4) has the advantage of generality in that it applies to any measure on a compact separable metric space. Our second notion (Definition 4.5) is advantageous in other ways, namely it is more straightforward and works well in $\mathsf{RCA}_0$. It would be desirable to find a single definition which combines all of these advantages.