# Computable Random Variables and Conditioning

Pieter Collins
Department of Data Science and Knowledge Engineering
Maastricht University
<EMAIL_ADDRESS>
(22 December 2020)

###### Abstract

The aim of this paper is to present an elementary computable theory of random
variables, based on the approach to probability via valuations. The theory is
based on a type of lower-measurable sets, which are controlled limits of open
sets, and extends existing work in this area by providing a computable theory
of conditional random variables. The theory is based within the framework of
type-two effectivity, so has an explicit direct link with Turing computation,
and is expressed in a system of computable types and operations, so has a
clean mathematical description.

##  1 Introduction

In this paper, we present a computable theory of probability and random
variables. The theory is powerful enough to provide a theoretical foundation
for the rigorous numerical analysis of discrete-time continuous-state Markov
chains and stochastic differential equations [Col14]. We provide an exposition
of the approach to probability distributions using valuations and the
development of integrals of positive lower-semicontinuous and of bounded
continuous functions, and on the approach to random variables as limits of
almost-everywhere defined continuous partial functions.

We use the framework of _type-two effectivity (TTE)_ [Wei99], in which
computations are performed by Turing machines working on infinite sequences,
as a foundational theory of computability. We believe that this framework is
conceptually simpler for non-specialists than the alternative of using a
domain-theoretic framework. Since in TTE we work entirely in the class of
quotients of countably-based (QCB) spaces, which form a cartesian closed
category, many of the basic operations can be carried out using simple type-
theoretic constructions such as the $\lambda$-calculus.

In this paper, we deal with computability theory, rather than constructive
mathematics. In practice, this means that we allow recursive constructions,
and so accept the axiom of dependent (countable) choice, but since not all
operations are decidable, we do not accept the law of the excluded middle.
However, proofs of correctness of computable operators may use non-computable
functions and proof by contradiction.

We assume that the reader has a basic familiarity with classical probability
theory (see e.g. [Shi95, Pol02]. Much of this article is concerned with giving
computational meaning to classical concepts and arguments. The main difficulty
lies in the use of $\sigma$-algebras in classical probability, which have poor
computability properties due to the presence of countable unions and
complementation. Instead, we use only topological constructions, which can
usually be effectivised directly. We can compute lower bounds (but not upper
bounds) to the measure of open sets, and extend results to measurable sets
using completion constructions. Similarly we define types of measurable and
integral functions as completions of types of (piecewise) continuous
functions.

In Section 2, we briefly introduce the foundations of computable analysis. In
Section 3, we describe the approach to probability theory using valuations.
The main results are in Section 5, in which we give a complete theory of
random variables in separable metric spaces. We begin by constructing types of
measurable sets and measurable functions on a given base probability space
$(\Omega,P)$ using completion operators, similarly to existing approaches in
the literature. We show that the distribution of a random variable is
computable, and conversely, that for any valuation we can construct a
realisation by a random variable, similarly to results of [SS06b, HR09]. We
then show the trivial result that the product of two random variables is
computable, and the classical result [MW43, BC72] that the image of a random
variable under a continuous function is computable. We define the expectation
of a random variable, and types of integrable random variables in the standard
way. Finally, we discuss conditioning of random variables, and show how a
random variable can be computed from its conditional expectation.

### Comparison with other approaches

An early fairly complete constructive theory of measure theory based on the
Daniell integral was developed in [BC72] was presented in [BB85] and [Cha74].
The theory is developed using abstract _integration spaces_ , which are
triples $(X,L,I)$ where $X$ is a space, $L$ a subset of test functions
$X\rightarrow\mathbb{R}$ and $I:L\rightarrow\mathbb{R}$ satifying properties
of an integral. The integral is extended from test functions to integrable
functions by taking limits. Measurable functions are those which can be
uniformly approximated by integrable functions on large-measure sets. It is
shown that the image of a measurable function under a continuous function is
measurable, and analogue of our Theorem 49. Measurable sets are defined via
_complemented sets_ , which are pairs of sets $(A_{1},A_{0})$ such that
$A_{0}\cap A_{1}=\emptyset$, and are measurable if $A_{0}\cup A_{1}$ is a full
set. Abstract measure spaces are defined in terms of measurable sets, and
shown to be equivalent to integration spaces.

A standard approach to a constructive theory of probability measures, as
developed in [JP89, Eda95a, SS06a, Esc09], is through _valuations_ , which are
essentially measures restricted to open sets. Explicit representations of
valuations within the framework of type-two effectivity were given in [Sch07].
Valuations satisfy the _modularity_ property
$\nu(U_{1})+\nu(U_{2})=\nu(U_{1}\cup U_{2})+\nu(U_{1}\cap U_{2})$, and
(monotonic) continuity $\nu(U_{\infty})=\lim_{n\to\infty}\nu(U_{n})$ whenever
$U_{n}$ is an increasing sequence of open sets with
$U_{\infty}=\bigcup_{n\in\mathbb{N}}U_{n}$. Relationships between valuations
and Borel measures were given in [Eda95a] and extended in [AM02] and [GL05].

The most straightforward approach to integration is the _Choquet_ or
_horizontal_ integral, a lower integral introduced within the framework of
domain theory in [Tix95]; see also [Kön97, Law04]. The lower integral on
valuations in the form we use was given in [Vic08]. The monadic properties of
the lower integral on valuations, which has type
$(\mathbb{X}\rightarrow\mathbb{R}^{+}_{<})\rightarrow\mathbb{R}^{+}_{<}$ were
noted by [Vic11]. A similar monadic approach to probability measures was used
in [Esc09] to develop a language EPCL for nondeterministic and probabilistic
computation. Here, the type of probability measures on the Cantor space
$\Omega=\\{0,1\\}^{\omega}$ was identified with the type of integrals
$(\Omega\rightarrow\mathbb{I})\rightarrow\mathbb{I}$ where $\mathbb{I}=[0,1]$
is the unit interval.

An alternative to the use of valuations is that of [CP02]. The exposition is
given in terms of general _boolean rings_ , but in the language of sets, a
measure $\mu$ is given satisfying the modularity condition, and extended by
the completion under the metric $d(S_{1},S_{2})=\mu(S_{1}\triangle S_{2})$
where $S_{1}\triangle S_{2}=(S_{1}\setminus S_{2})\cup(S_{2}\setminus S_{1})$.
In [WD05, WD06] a concept of _computable measure space_ with a concrete
representation was given using a ring of subsets $R$ generating the Borel
$\sigma$-algebra. Disadvantages of this approach are that the elements of $R$
must have a computable measure, introducing an undesirable dependency between
the measure and the “basic” sets which is not present in the approach using
valuations.

In the approach presented here, we start with the use of valuations, since
these are intrinsic given a base type $\mathbb{X}$. For a fixed valuation, we
can extend to a class of _lower-measurable sets_ , and also give a definition
of measurable set using a completion on complemented open sets (equivalently,
on topologically regular sets). We do not use integration spaces, since we
feel that the concept of measure is more fundamental than that of integral.

In the approach of [Spi06], integrable functions are defined as limits of
simple functions with respect to the measurable sets of [CP02]. Measurable
function are defined as limits of effectively-converging Cauchy sequences with
respect to the pseudometric $d_{h}(f,g):=\int|f-g|\wedge h$ for positive
integrable $h$ and integrable $f,g$. This work was generalised to Riesz spaces
in [CS09].

Random variables over discrete domains were defined in [Mis07], based on work
of [Var02], and extended to continuous domains in [GLV11]. A continuous random
variable in $\mathbb{X}$ was defined as a pair $(\nu,f)$ where $\nu$ is a
continuous valuation on $\Omega=\\{0,1\\}^{\omega}$, and $f$ is a continuous
map from $\mathrm{supp}(\nu)$ to $\mathbb{X}$, where $\mathrm{supp}(\nu)$ is
the smallest closed set $A$ such that $\nu(A)=1$. A difficulty with this
construction is that different random variables require different valuations
on the bases space $\Omega$, which makes computation of joint distributions
problematic.

In this paper, we define measurable functions as those for which the preimage
of an open set is a lower-measurable set and satisfy the natural properties.
This mimics the standard property that the preimage of an open set under a
measurable function is (Borel) measurable. Since measurable functions are in
general uncomputable, we do not even attempt to define the “image of a point”.

A similar approach to [Spi06] is also possible, defining random variables
(measurable functions) directly by completion with respect to the Fan metric
$d(X,Y)=\sup\\!\big{\\{}\varepsilon\in\mathbb{Q}^{+}\mid\
P\big{(}\\{\omega\in\Omega\mid
d(X(\omega),Y(\omega))>\varepsilon\\}\big{)}>\varepsilon\big{\\}}.$ The
resulting theory is essentially equivalent to that of [BC72], but developed in
reverse. The resulting representation is equivalent to that using lower-
measurable sets.

In [SS06b], an alternative representation of valuations and measures on
$\mathbb{X}$ was developed by defining a valuation $\pi$ on (a subset of) the
sequence space $\\{0,1\\}^{\omega}$, and pushing-forward by the representation
$\delta$ of $\mathbb{X}$, yielding $\nu(U)=\pi(\delta^{-1}(U))$. This
representation of valuations is similar the valuation induced by our random
variables, except that our random variables are obtained by taking limits, so
we need to prove separately that the valuation induced by a random variable is
computable.

It was further shown [SS06b] and that the alternative representations of
valuations always exist on sufficiently nice spaces, which can be seen as a
realisation result for valuations, where the representation $\delta$ of the
space $\mathbb{X}$ is a random variable. In [HR09], a theory of probability
was developed for the study of algorithmic randomness, and a similar
representation result for valuations was given, here allowing both the base-
space measure $\pi$ and point-representation $\delta$ to be given. In this
paper, we also show that valuations have concrete realisations by random
variables, but our result constructs random variables relative to to uniform
probability measure on the base space $\\{0,1\\}^{\omega}$, and a Cauchy
sequence of (continuous) functions rather than a single function on a
$G_{\delta}$-set.

The problem of finding conditional expectation, which classically uses the
Radon-Nikodym derivative, was shown to be uncomputable by [HRW11]. This means
that computably, there is a difference between a random variable, and a
“conditional random variable”. Here we show that given a conditional random
variable $Y|\mathcal{X}$, and an $\mathcal{X}$-measurable random variable $X$,
we can effectively compute $Y$. This result is important for stochastic
processes, in which we typically can compute the distribution of $X_{t+1}$
given $X_{t}=x_{t}$.

##  2 Computable Analysis

In the theory of type-two effectivity, computations are performed by Turing
machines acting on _sequences_ over some alphabet $\Sigma$. A computation
performed by a machine $\mathcal{M}$ is _valid_ on an input
$p\in\Sigma^{\omega}$ if the computation does not halt, and writes infinitely
many symbols to the output tape. A type-two Turing machine therefore performs
a computation of a partial function
$\eta:\Sigma^{\omega}\rightharpoonup\Sigma^{\omega}$; we may also consider
multi-tape machines computing
$\eta:(\Sigma^{\omega})^{n}\rightharpoonup(\Sigma^{\omega})^{m}$. It is
straightforward to show that any machine-computable function
$\Sigma^{\omega}\rightharpoonup\Sigma^{\omega}$ is continuous on its domain.

In order to relate Turing computation to functions on mathematical objects, we
use _representations_ of the underlying sets, which are partial surjective
functions $\delta:\Sigma^{\omega}\rightharpoonup\mathbb{X}$. An operation
$\mathbb{X}\rightarrow\mathbb{Y}$ is
$(\delta_{\mathbb{X}};\delta_{\mathbb{Y}})$-computable if there is a machine-
computable function $\eta:\Sigma^{\omega}\rightharpoonup\Sigma^{\omega}$ with
$\mathrm{dom}(\eta)\supset\mathrm{dom}(\delta_{\mathbb{X}})$ such that
$\delta_{\mathbb{Y}}\circ\eta=f\circ\delta_{\mathbb{X}}$ on
$\mathrm{dom}(\delta_{\mathbb{X}})$. Representations are equivalent if they
induce the same computable functions. A _computable type_ is a pair
$(\mathbb{X},[\delta])$ where $\mathbb{X}$ is a space and $[\delta]$ is an
equivalence class of representations of $\mathbb{X}$.

If $X$ is a topological space, we say that a representation $\delta$ of $X$ is
an _admissible quotient representation_ if (i) whenever
$f:\mathbb{X}\rightarrow\mathbb{Y}$ is such that $f\circ\delta$ is continuous,
then $f$ is continuous, and (ii) whenever
$\phi:\Sigma^{\omega}\rightharpoonup\mathbb{X}$ is continuous, there exists
continuous $\eta:\Sigma^{\omega}\rightharpoonup\Sigma^{\omega}$ such that
$\phi=\delta\circ\eta$. Any space with a quotient representation is a quotient
of a subset of the countably-based space $\Sigma^{\omega}$, and is a
_sequential space_. (A topological space is a _sequential space_ if any subset
$W$ for which $x_{n}\to x_{\infty}$ with $x_{\infty}\in W$ implies $x_{n}\in
W$ for all sufficiently large $n$, is an open set.)

A function $f:\mathbb{X}\rightarrow\mathbb{Y}$ is _computable_ if there is a
machine-computable function
$\eta:\Sigma^{\omega}\rightharpoonup\Sigma^{\omega}$ with
$\mathrm{dom}(\eta)\supset\mathrm{dom}(\delta_{\mathbb{X}})$ such that
$\delta_{\mathbb{Y}}\circ\eta=f\circ\delta_{\mathbb{X}}$ on
$\mathrm{dom}(\delta_{\mathbb{X}})$. A multivalued function
$F:\mathbb{X}\rightrightarrows\mathbb{Y}$ is _computably selectable_ if there
is a machine-computable function
$\eta:\Sigma^{\omega}\rightharpoonup\Sigma^{\omega}$ with
$\mathrm{dom}(\eta)\supset\mathrm{dom}(\delta_{\mathbb{X}})$ such that
$\delta_{\mathbb{Y}}\circ\eta\in F\circ\delta_{\mathbb{X}}$ on
$\mathrm{dom}(\delta_{\mathbb{X}})$; note that different names of
$x\in\mathbb{X}$ may give rise to different values of $y\in\mathbb{Y}$.

The category of computable types with (sequentially) continuous functions is
Cartesian closed, and the computable functions yield a Cartesian closed
subcategory. For any types $\mathbb{X}$, $\mathbb{Y}$ there exist a canonical
product type $\mathbb{X}\times\mathbb{Y}$ with computable projections
$\pi_{\mathbb{X}}:\mathbb{X}\times\mathbb{Y}\rightarrow\mathbb{X}$ and
$\pi_{\mathbb{Y}}:\mathbb{X}\times\mathbb{Y}\rightarrow\mathbb{Y}$, and a
canonical exponential type $\mathbb{Y}^{\mathbb{X}}$ such that evaluation
$\epsilon:\mathbb{Y}^{\mathbb{X}}\times\mathbb{X}\rightarrow\mathbb{Y}:(f,x)\mapsto
f(x)$ is computable. Since objects of the exponential type are continuous
function from $\mathbb{X}$ to $\mathbb{Y}$, we also denote
$\mathbb{Y}^{\mathbb{X}}$ by $\mathbb{X}\rightarrow\mathbb{Y}$ or
$\mathcal{C}(\mathbb{X};\mathbb{Y})$; in particular, whenever we write
$f:\mathbb{X}\rightarrow\mathbb{Y}$, we imply that $f$ is continuous. There is
a canonical equivalence between
$(\mathbb{X}\times\mathbb{Y})\rightarrow\mathbb{Z}$ and
$\mathbb{X}\rightarrow(\mathbb{Y}\rightarrow\mathbb{Z})$ given by
$\tilde{f}(x):\mathbb{Y}\rightarrow\mathbb{Z}:\tilde{f}(x)(y)=f(x,y)$.

There are canonical types representing basic building blocks of mathematics,
including the natural number type $\mathbb{N}$ and the real number type
$\mathbb{R}$. We use a three-valued logical type with elements
$\\{{\sf{F}},{\sf{T}},\bot\\}$ representing _false_ , _true_ , and
_indeterminate_ or _unknowable_ , and its subtypes the _Boolean_ type
$\mathbb{B}$ with elements $\\{{\sf{F}},{\sf{T}}\\}$ and the _Sierpinski_ type
$\mathbb{S}$ with elements $\\{{\sf{T}},\bot\\}$. Given any type $\mathbb{X}$,
we can identify the type $\mathcal{O}(\mathbb{X})$ of open subsets $U$ of
$\mathbb{X}$ with $\mathbb{X}\rightarrow\mathbb{S}$ via the characteristic
function $\chi_{U}$. Further, standard operations on these types, such as
arithmetic on real numbers, are computable.

A sequence $(x_{n})$ is an _effective Cauchy sequence_ if
$d(x_{m},x_{n})<\epsilon_{\max(m,n)}$ where $(\epsilon_{n})_{n\in\mathbb{N}}$
is a known computable sequence with $\lim_{n\to\infty}\epsilon_{n}=0$, and a
_strong Cauchy sequency_ if $\epsilon_{n}=2^{-n}$. The limit of an effective
Cauchy sequence of real number is computable.

We shall also need the type $\mathbb{H}\equiv\mathbb{R}^{+,\infty}_{<}$ of
positive real numbers with infinity under the lower topology. The topology on
the lower halfline $\mathbb{H}$ is the toplogy of lower convergence, with open
sets $(a,\infty]$ for $a\in\mathbb{R}^{+}$ and $\mathbb{H}$ itself. A
representation of $\mathbb{H}$ then encodes an increasing sequence of positive
rationals with the desired limit. We note that the operators $+$ and $\times$
are computable on $\mathbb{H}$, where we define $0\times\infty=\infty\times
0=0$, as is countable supremum
$\sup:\mathbb{H}^{\omega}\rightarrow\mathbb{H}$,
$(x_{0},x_{1},x_{2},\ldots)\mapsto\sup\\{x_{0},x_{1},x_{2},\ldots\\}$.
Further, $\mathrm{abs}:\mathbb{R}\rightarrow\mathbb{H}$ is computable, as is
the embedding $\mathbb{S}\hookrightarrow\mathbb{H}$ taking ${\sf{T}}\mapsto 1$
and $\bot\mapsto 0$. We let $\mathbb{I}_{<}$ be the unit interval $[0,1]$,
again with the topology of lower convergence with open sets $(a,1]$ for
$a\in[0,1)$ and $\mathbb{I}$ itself, and $\mathbb{I}_{>}$ the interval with
the topology of upper convergence.

A _computable metric space_ is a pair $(\mathbb{X},d)$ where $\mathbb{X}$ is a
computable type, and $d:\mathbb{X}\times\mathbb{X}\rightarrow\mathbb{R}^{+}$
is a computable metric, such that the extension of $d$ to
$\mathbb{X}\times\mathcal{A}(\mathbb{X})$ (where $\mathcal{A}(\mathbb{X})$ is
the type of closet subsets of $\mathbb{X}$) defined by
$d(x,A)=\inf\\{d(x,y)\mid y\in A\\}$ is computable as a function into
$\mathbb{R}^{+,\infty}_{<}$. This implies that given an open set $U$ we can
compute $\epsilon>0$ such that $B_{\epsilon}(x)\subset U$, which captures the
relationship between the metric and the open sets. The effective metric spaces
of [Wei99] are a concrete class of computable metric space.

A type $\mathbb{X}$ is _effectively separable_ if there is a computable
function $\xi:\mathbb{N}\rightarrow\mathbb{X}$ such that $\mathrm{rng}(\xi)$
is dense in $\mathbb{X}$.

Throughout this paper we shall use the term “compute” to indicate that a
formula or procedure can be effectively carried out in the framework of type-
two effectivity. Other definitions and equations may not be possible to verify
constructively, but hold from axiomatic considerations.

##  3 Valuations

The main difficulty with classical measure theory is that Borel sets and Borel
measures have very poor computability properties. Although a computable theory
of Borel sets was given in [Bra05], the measure of a Borel set is in general
not computable in $\mathbb{R}$. However, we can consider an approach to
measure theory in which we may only compute the measure of _open_ sets. Since
open sets are precisely those which can be approximated from inside, we expect
to be able to compute lower bounds for the measure of an open set, but not
upper bounds. The above considerations suggest an approach which has become
standard in computable measure theory, namely that using _valuations_ [JP89,
Eda95a, SS06a, Esc09].

######  Definition 1 (Valuation).

The type of _valuations_ on $\mathbb{X}$ is the subtype
$\mathcal{O}(\mathbb{X})\rightarrow\mathbb{H}$ consisting of elements $\nu$
satisfying $\nu(\emptyset)=0$ and the _modularity_ condition
$\nu(U)+\nu(V)=\nu(U\cup V)+\nu(U\cap V)$ for all
$U,V\in\mathcal{O}(\mathbb{X})$.

Note that since our valuations are elements of
$\mathcal{O}(\mathbb{X})\rightarrow\mathbb{H}$, any $\nu$ satisfies the
_monotonicity_ condition $\nu(U)\leq\nu(V)$ whenever $U\subset V$, and the
_continuity_ condition
$\nu\bigl{(}\bigcup_{n=0}^{\infty}U_{n}\bigr{)}=\lim_{n\to\infty}\nu(U_{n})$
whenever $U_{n}$ is an increasing sequence of open sets.

A valuation $\nu$ on $\mathbb{X}$ is _finite_ if $\nu(\mathbb{X})$ is finite,
_effectively finite_ if $\nu(\mathbb{X})$ is a computable real number, and
_locally finite_ if $\nu(U)<\infty$ for any $U$ which is a subset of a compact
set.

An effectively finite valuation computably induces an upper-valuation on
closed sets $\bar{\nu}:\mathcal{A}(\mathbb{X})\rightarrow\mathbb{R}^{+}_{>}$
by $\bar{\nu}(A)=\nu(\mathbb{X})-\nu(\mathbb{X}\setminus A)$. For any finite
valuation, $\nu(U)\leq\bar{\nu}(A)$ whenever $U\subset A$. We say a set $S$ is
_$\nu$ -regular_ if $\bar{\nu}(\partial S)=0$. An open set $U$ is
$\nu$-regular if, and only if, $\nu(U)=\bar{\nu}(\overline{U})$.

The following result shows that the measure of a sequence of small sets
approaches zero. Recall that a space $\mathbb{X}$ is _regular_ if for any
point $x$ and open set $U$, there exists an open set $V$ and a closed set $A$
such that $x\in V\subset A\subset U$.

######  Lemma 2.

Let $\mathbb{X}$ be a separable regular space, and $\nu$ a finite valuation on
$\mathbb{X}$. If $U_{n}$ is any sequence of open sets such that
$U_{n+1}\subset U_{n}$ and $\bigcap_{n=0}^{\infty}U_{n}=\emptyset$, then
$\nu(U_{n})\to 0$ as $n\to\infty$.

A link with classical measure theorey is provided by a number of results that
show that valuations can be extended to measures on the Borel
$\sigma$-algebra.

######  Theorem 3.

Borel measures and continuous valuations are in one-to-one correspondance:

  1. 1.

on a countably-based locally-compact Hausdorff space [Eda95b, Corollary 5.3],
or

  2. 2.

on a locally compact sober space [AM02].

For a purely constructive approach valuations themselves are main objects of
study, and we only (directly) consider the measure of open and closed sets.

Just as for classical measure theory, we say (open) sets $U_{1},U_{2}$ are
_independent_ if $\nu(U_{1}\cap U_{2})=\nu(U_{1})\nu(U_{2})$.

######  Definition 4 (Conditioning).

Given a sub-topology $\mathcal{V}$ on $\mathbb{X}$ and a valuation $\nu$ on
$\mathbb{X}$, a _conditional valuation_ is a function
$\nu(\cdot|\cdot):\mathcal{O}(\mathbb{X})\times\mathcal{V}\rightarrow\mathbb{H}$
such that $\nu(U\cap V)=\nu(U|V)\nu(V)$ for all $U\in\mathcal{O}(\mathbb{X})$
and $V\in\mathcal{V}$.

Clearly, $\nu(U\cap V)$ can be computed given $\nu(U|V)$ and $\nu(V)$. The
conditional valuation $\nu(\cdot|V)$ is uniquely defined if $\nu(V)\neq 0$.
However, since $\nu(U\cap V):\mathbb{R}^{+}_{<}$ but
$1/\nu(V):\mathbb{R}^{+,\infty}_{>}$, the conditional valuation $\nu(\cdot|V)$
cannot be _computed_ , even when $\nu(V)>0$, unless we are also given a set
$A\in\mathcal{A}(\mathbb{X})$ such that $V\subset A$ and $\bar{\nu}(A\setminus
V)=0$, in which case we have $\nu(U|V)=\nu(U\cap V)/\bar{\nu}(A)$.

We can define a notion of integration for positive lower-semicontinuous
functions by the _Choquet_ or _horizontal_ integral; see [Tix95, Law04,
Vic08].

######  Definition 5 (Lower integral).

Given a valuation
$\nu:(\mathbb{X}\rightarrow\mathbb{S})\rightarrow\mathbb{H}$, define the lower
integral $(\mathbb{X}\rightarrow\mathbb{H})\rightarrow\mathbb{H}$ by

$\textstyle\int_{\mathbb{X}}\psi\,d\nu=\sup\bigl{\\{}{\textstyle\sum_{m=1}^{n}}(p_{m}-p_{m-1})\,\nu(\psi^{-1}(p_{m},\infty])\\\
\mid(p_{0},\ldots,p_{n})\in\mathbb{Q}^{*}\wedge
0=p_{0}<p_{1}<\cdots<p_{n}\bigr{\\}}$ (1)

which is equivalent to the real integral

$\textstyle\int_{\mathbb{X}}\\!\psi\,d\nu=\int_{0}^{\infty}\nu\bigl{(}\psi^{-1}(x,\infty]\bigr{)}dx.$
(2)

Note that we could use any dense set of computable positive real numbers, such
as the dyadic rationals $\mathbb{Q}_{2}$, instead of the rationals in (1).
Since each sum is computable, and the supremum of countably many elements of
$\mathbb{H}$ is computable, the lower integral is computable.

It is fairly straightforward to show that the integral is linear,

$\textstyle\int_{\mathbb{X}}(a_{1}\psi_{1}+a_{2}\psi_{2})\,d\nu=a_{1}\int_{\mathbb{X}}\psi_{1}\,d\nu+a_{2}\int_{\mathbb{X}}\psi_{2}\,d\nu$
(3)

for all $a_{1},a_{2}\in\mathbb{H}$ and
$\psi_{1},\psi_{2}:\mathbb{X}\rightarrow\mathbb{H}$.

If $\raisebox{1.89444pt}{$\chi$}_{U}$ is the characteristic function of a set
$U$, then
$\textstyle\int_{\mathbb{X}}\raisebox{1.89444pt}{$\chi$}_{U}\,d\nu=\nu(U),$
and it follows that if
$\phi=\sum_{i=1}^{n}a_{i}\,\raisebox{1.89444pt}{$\chi$}_{U_{i}}$ is a step
function, then
$\textstyle\int_{\mathbb{X}}\phi\,d\nu=\sum_{i=1}^{n}a_{i}\,\nu(U_{i}).$

Given a (lower-semi)continuous linear functional
$\mu:(\mathbb{X}\rightarrow\mathbb{H})\rightarrow\mathbb{H}$, we can define a
function $\mathcal{O}(\mathbb{X})\rightarrow\mathbb{H}$ by
$U\mapsto\mu(\raisebox{1.89444pt}{$\chi$}_{U})$ for
$U\in\mathcal{O}(\mathbb{X})$. By linearity,

$\textstyle\mu(\raisebox{1.89444pt}{$\chi$}_{U})+\mu(\raisebox{1.89444pt}{$\chi$}_{V})=\mu(\raisebox{1.89444pt}{$\chi$}_{U\cap
V})+\mu(\raisebox{1.89444pt}{$\chi$}_{U\cup V}).$

Hence $\mu$ induces a valuation on $\mathbb{X}$. We therefore obtain a
computable equivalence between the type of valuations and the type of positive
linear lower-semicontinuous functionals:

######  Theorem 6.

The type of valuations
$(\mathbb{X}\rightarrow\mathbb{S})\rightarrow\mathbb{H}$ is computably
equivalent to the type of continuous linear functionals
$(\mathbb{X}\rightarrow\mathbb{H})\rightarrow\mathbb{H}$.

Types of the form $(\mathbb{X}\rightarrow\mathbb{T})\rightarrow\mathbb{T}$ for
a fixed type $\mathbb{T}$ form a _monad_ [Str72] over $\mathbb{X}$, and are
particularly easy to work with.

In [Eda95a, Section 4], a notion of integral
$\mathcal{C}_{\mathrm{bd}}(\mathbb{X};\mathbb{R})\rightarrow\mathbb{R}$ on
continuous bounded functions was introduced based on the approximation by
measures supported on finite sets of points. Our lower integral on positive
lower-semicontinuous functions can be extended to bounded functions as
follows:

######  Definition 7 (Bounded integration).

A continuous function $f:\mathbb{X}\rightarrow\mathbb{R}$ is _effectively
bounded_ if there are (known) computable reals $a,b\in\mathbb{R}$ such that
$a<f(x)<b$ for all $x\in\mathbb{X}$.

If $\nu$ is effectively finite with $\nu(\mathbb{X})=c$, we define the
integral
$\mathcal{C}_{\mathrm{bd}}(\mathbb{X};\mathbb{R})\rightarrow\mathbb{R}$ by

$\textstyle\int_{\mathbb{X}}f(x)\,d\nu(x)=\int_{\mathbb{X}}\bigl{(}a+f(x)\bigr{)}\,d\nu(x)-a\,c=b\,c-\int_{\mathbb{X}}\bigl{(}b-f(x)\bigr{)}\,d\nu(x)$

where $a<b$ are bounds for $f$.

It is clear that the first formula for the integral of $f$ is computable in
$\mathbb{R}_{<}$ and the second in $\mathbb{R}_{>}$, and that the lower and
upper integrals agree if $f$ is continuous. If $\mathbb{X}$ is compact, then
any (semi)continuous function is effectively bounded, so the integrals always
exist.

In order to define a valuation given a positive linear functional
$\mathcal{C}_{\mathrm{cpt}}(\mathbb{X};\mathbb{R})\rightarrow\mathbb{R}$ on
compactly-supported continuous functions, we need some way of approximating
the characteristic function of an open set by continuous functions. If
$\mathbb{X}$ is _effectively regular_ , then given any open set $U$, we can
construct an increasing sequence of closed sets $A_{n}$ such that
$\bigcup_{n\to\infty}A_{n}=U$. Further, a type $\mathbb{X}$ is _effectively
quasi-normal_ if given disjoint closed sets $A_{0}$ and $A_{1}$, we can
construct a continuous function $\phi:\mathbb{X}\rightarrow[0,1]$ such that
$\phi(A_{0})=\\{0\\}$ and $\phi(A_{1})=\\{1\\}$ using an effective Uryshon
lemma; see [Sch09] for details.

We then have an effective version of the Riesz representation theorem:

######  Theorem 8.

Suppose $\mathbb{X}$ is an effectively regular and effectively quasi-normal
type. Then type of locally-finite valuations
$(\mathbb{X}\rightarrow\mathbb{S})\rightarrow\mathbb{H}$ is effectively
equivalent to the type of positive linear functionals
$\mathcal{C}_{\mathrm{cpt}}(\mathbb{X}\rightarrow\mathbb{R})\rightarrow\mathbb{R}$
on continuous functions of compact support.

We consider lower-semicontinuous functionals
$(\mathbb{X}\rightarrow\mathbb{H})\rightarrow\mathbb{H}$ to be more
appropriate as a foundation for computable measure theory than the continuous
functionals $(\mathbb{X}\rightarrow\mathbb{R})\rightarrow\mathbb{R}$, since
the equivalence given by Theorem 6 is entirely independent of any assumptions
on the type $\mathbb{X}$ whereas the equivalence of Theorem 8 requires extra
properties of $\mathbb{X}$ and places restrictions on the function space.

######  Theorem 9 (Fubini).

If $\mathbb{X}_{1}$ and $\mathbb{X}_{2}$ are countably-based spaces, then for
any $\psi:\mathbb{X}_{1}\times\mathbb{X}_{2}\rightarrow\mathbb{H}$,

$\textstyle\int_{\mathbb{X}_{1}}\int_{\mathbb{X}_{2}}\psi(x_{1},x_{2})d\nu_{2}(x_{2})d\nu_{1}(x_{1})=\int_{\mathbb{X}_{2}}\int_{\mathbb{X}_{1}}\psi(x_{1},x_{2})d\nu_{1}(x_{1})d\nu_{2}(x_{2}).$
(4)

Extending valuations to functions
$(\mathbb{X}\rightarrow\mathbb{H})\rightarrow\mathbb{H}$, we can write

$\nu_{1}(\lambda x_{1}.\nu_{2}(\lambda
x_{2}.\psi(x_{1},x_{2})))=\nu_{2}(\lambda x_{2}.\nu_{1}(\lambda
x_{1}.\psi(x_{1},x_{2}))).$

######  Definition 10 (Product valuation).

Let $\nu_{i}$ be a valuation on $\mathbb{X}_{i}$ for $i=1,2$, where each
$\mathbb{X}_{i}$ is countably-based. The _product_ of two valuations is given
by

$\displaystyle\textstyle[\nu_{1}\times\nu_{2}](U)$
$\displaystyle\textstyle:=\int_{\mathbb{X}_{1}}\int_{\mathbb{X}_{2}}\chi_{U}(x_{1},x_{2})d\nu_{2}(x_{2})d\nu_{1}(x_{1})$
(5)
$\displaystyle\textstyle\qquad=\int_{\mathbb{X}_{2}}\int_{\mathbb{X}_{1}}\chi_{U}(x_{1},x_{2})d\nu_{1}(x_{1})d\nu_{2}(x_{2}),$

where the two integrals are equal by Fubini’s theorem.

In the sequel, we shall make frequent use of the following result.

######  Proposition 11.

Let $U,V,W:\mathcal{O}(\mathbb{X})$ with $U\subset V$, and $\nu$ a valuation
on $\mathbb{X}$. Then

  1. (a)

$\nu(U)+\nu(V\cap W)\leq\nu(V)+\nu(U\cap W)$, and

  2. (b)

$\nu(U)+\nu(V\cup W)\leq\nu(V)+\nu(U\cup W)$.

The proof is straightforward.

##  4 Lower-measurable sets

In this section, we define measures of non-open sets.

The standard approach to probability theory used in classical analysis is to
define a measure over a $\sigma$-algebra of sets. The main difficulty with a
direct effectivisation of probability theory via $\sigma$-algebras is the
operation on complementation. Given an open set $U$, we can _only_ hope to
compute $\nu(U)$ in $\mathbb{R}^{+}_{<}$ (i.e. from below), and since
$\sigma$-algebras are closed under complementation, for $A=U^{\complement}$,
we compute $\nu(A)$ in $\mathbb{R}^{+}_{>}$. Then for a countable union of
nested closed sets $A_{\infty}=\bigcup_{n=0}^{\infty}A_{n}$ with
$A_{n+1}\subset A_{n}$, we need to find information about the limit
$\lim_{n\to\infty}\nu(A_{n})$ which is an increasing sequence in
$\mathbb{R}^{+}_{>}$, so we can find neither an upper- or a lower-bound.

Our solution is to consider, for a _fixed_ probability valuation $\nu$, a type
of _$\nu$ -lower-measurable sets_. These essentially extend the open sets to
the $G_{\delta}$ sets, and have a representation under which it is possible to
compute the $\nu$-measure from below. Further, they are closed under finite
intersection and countable union (so may be called a _$\sigma$ -semiring_,
though this usage is different from that of e.g. [Sch04]). However, they do
not formally define a topology on $\mathbb{X}$, since they are essentially
_equivalence-classes_ of subsets of $\mathbb{X}$ (and even this property only
holds for sufficiently nice spaces, including the Polish spaces). The
resulting theory can be seen as a construction of an outer-regular measure for
$G_{\delta}$ subsets of a space (see [vG02].

###  4.1 Definition and basic properties

We first define the type of lower-measurable sets, and prove some of its basic
properties.

######  Definition 12 (Lower-Cauchy sequence).

Let $\mathcal{V}$ be a set with a intersection (or _meet_) operation
$\cap:\mathcal{V}\times\mathcal{V}\to\mathcal{V}$ and a compatible subset (or
order) relation $\subset$ on $\mathcal{V}\times\mathcal{V}$, and let
$\nu:\mathcal{V}\to\mathbb{R}$.

A sequence $(V_{k})$ of elements of $\mathcal{V}$ is a _lower-Cauchy sequence_
if for all $\epsilon>0$, there exists $n=N(\epsilon)$, such that

$\forall m>n,\ \nu(V_{m}\cap V_{n})\geq\nu(V_{n})-\epsilon.$ (6)

The convergence is _effective_ if $N(\epsilon)$ is known, equivalently, if
there is a known sequence $(\epsilon_{k})$ with
$\lim_{k\to\infty}\epsilon_{k}=0$ such that for all $m>n$, $\nu(V_{m}\cap
V_{n})\geq\nu(V_{n})-\epsilon_{n}$. The convergence is _fast_ if
$\epsilon_{k}=2^{-k}$.

The sequence is _monotone (decreasing)_ if for all $m>n$, $V_{m}\subset
V_{n}$.

If $(V_{n})$ is an effective lower-Cauchy sequence, then

$\forall m>n,\ \nu(V_{n}\setminus V_{m})\leq\epsilon_{n}.$

If $(V_{n})$ is a fast monotone lower-Cauchy sequence, then

$\forall m>n,\ \nu(V_{n})\geq\nu(V_{m})\geq\nu(V_{n})-2^{-n}.$

######  Definition 13 (Equivalence of lower-Cauchy sequence).

Two $\nu$-lower-Cauchy sequences are _equivalent_ , denoted
$(U_{n})\sim(V_{n})$ if, and only if, for

$\forall\epsilon>0,\;\exists n\in\mathbb{N},\;\forall m\geq n,\ \nu(U_{m}\cap
V_{m})\geq\max(\nu(U_{m}),\nu(V_{m}))-\epsilon.$

######  Lemma 14.

If $(U_{n})$ and $V_{n}$ are fast lower-Cauchy sequences, then $(U_{n})$ and
$(V_{n})$ are equivalent if, and only if

$\forall n\in\mathbb{N},\ \nu(U_{n}\cap
V_{n})\geq\max(\nu(U_{n}),\nu(V_{n}))-2^{-n}.$

######  Lemma 15.

The relation $\sim$ is an equivalence relation on fast lower-Cauchy sequences.

###### Proof.

Reflexivity and commutativity are immediate; it remains to show transitivity.
Suppose $(U_{n})$, $(V_{n})$ and $(W_{n})$ are fast monotone $\nu$-lower-
Cauchy sequences, that $(U_{n})\sim(V_{n})$ and $(V_{n})\sim(W_{n})$. Then for
any $m>n$, $\nu(U_{n}\cap W_{n})\geq\nu(U_{m}\cap V_{m}\cap
W_{m})\geq\nu(U_{m}\cap V_{m})+\nu(V_{m}\cap
W_{m})-\nu(W_{m})\geq\nu(U_{m})+\bigl{(}\nu(U_{m}\cap
V_{m})-\nu(U_{m})\bigr{)}+\bigl{(}\nu(V_{m}\cap
W_{m})-\nu(V_{m})\bigr{)}\geq\nu(U_{m})-2\\!\times\\!2^{-m}\geq\nu(U_{n})-2^{-n}-2\\!\times\\!2^{-m}$.
Since $m$ can be made arbitrarily large, $\nu(U_{n}\cap
W_{n})\geq\nu(U_{n})-2^{-n}$ as required. By symmetry, $\nu(U_{n}\cap
W_{n})\geq\nu(W_{n})-2^{-n}$. ∎

######  Definition 16 (Lower-measurable set).

Let $\mathbb{X}$ be a type, and $\nu$ a valuation on $\mathbb{X}$. The type of
$\nu$-lower-measurable sets is defined as the equivalence classes of fast
monotone $\nu$-lower-Cauchy sequences of open subsets of $\mathbb{X}$.

Note that a fast monotone $\nu$-lower-Cauchy sequence $(U_{n})$ satisfies

$\forall n\in\mathbb{N},\;\forall m>n,\ U_{m}\subset
U_{n}\wedge\nu(U_{m})\geq\nu(U_{n})-2^{-n}.$ (7)

By countable-additivity, the classical measure of $U_{\infty}$ coincides with
its $\nu$-lower-measure.

######  Proposition 17 (Lower-measure is computable).

If $(U_{n})$ is a fast monotone lower-Cauchy sequence of open sets, then
$\sup_{n\in\mathbb{N}}(\nu(U_{n})-2^{-n})$ is computable in
$\mathbb{R}^{+}_{<}$.

###### Proof.

The value $\sup_{n\in\mathbb{N}}\nu(U_{n})-2^{-n}$ is the supremum of a
countable set of lower-reals, so is computable in $\mathbb{R}^{+}_{<}$. ∎

######  Proposition 18 (Lower-measure is well-defined).

If $(U_{n})$ and $(V_{n})$ are equivalent fast monotone $\nu$-lower-Cauchy
sequences, then
$\sup_{n\in\mathbb{N}}\bigl{(}\nu(U_{n})-2^{-n}\bigr{)}=\sup_{n\in\mathbb{N}}\bigl{(}\nu(V_{n})-2^{-n}\bigr{)}$.

###### Proof.

Suppose $U_{n}$ and $V_{n}$ are equivalent $\nu$-lower-Cauchy sequences. Then
for all $n$, we have $\nu(U_{\infty})\geq\nu(U_{n})-2^{-n}\geq\nu(U_{n}\cap
V_{n})-2^{-n}\geq\nu(V_{n})-2\times 2^{-n}\geq\nu(V_{\infty})-2\times 2^{n}$.
Since $n$ is arbitrary, $\nu(U_{\infty})\geq\nu(V_{\infty})$. Switching the
$U$s and $V$s gives $\nu(U_{\infty})\geq\nu(V_{\infty})$. ∎

######  Definition 19 (Lower-measure).

The $\nu$-lower-measure of a lower measurable set $U_{\infty}$ is defined as
$\sup_{n\in\mathbb{N}}\nu(U_{n})-2^{-n}$, where $U_{n}$ is any fast monotone
lower-Cauchy sequence converging to $U_{\infty}$.

######  Lemma 20.

Let $(U_{n})$ be a $\nu$-lower-Cauchy sequence. Then sequence $(U_{n+1})$ is
$\nu$-lower-Cauchy, and $(U_{n+1})\sim_{\nu}(U_{n})$.

###### Proof.

If $m>n$, $\nu(U_{n+1})-\nu(U_{m+1})\leq 2^{-(n+1)}<2^{-n}$. ∎

We first show that given an effective lower-Cauchy sequence, then it is
possible to compute an equivalent fast lower-Cauchy subsequence, and given a
non-monotone lower-Cauchy sequence of lower-measurable sets (notably, of open
sets), we can compute a monotone sequence with the same limit.

######  Lemma 21 (Computing fast monotone lower-Cauchy sequences).

  1. 1.

Suppose $(V_{n})_{n\in\mathbb{N}}$ is an effective $\nu$-lower-Cauchy
sequence. Then $U_{n}=V_{N(2^{-n})}$ is an equivalent fast lower-measurable
subsequence.

  2. 2.

Suppose $(V_{n})_{n\in\mathbb{N}}$ is a fast $\nu$-lower-Cauchy sequence. Then
$U_{n}=\bigcup_{m\geq n+1}V_{m}$ is an equivalent fast monotone $\nu$-lower-
Cauchy sequence.

###### Proof.

  1. 1.

Clearly for $m>n\geq N(2^{-n})$, we have $\nu(U_{m}\cap
U_{n})=\nu(V_{N(2^{-m})}\cap
V_{N(2^{-n})})\leq\nu(V_{N(2^{-m})})+2^{-n}=\nu(U_{m})+2^{-n}$.

  2. 2.

Since $U_{n}=U_{n+1}\cup V_{n+1}$, we have $\nu(U_{n})+\nu(U_{n+1}\cap
V_{n+1})=\nu(U_{n+1}\cup V_{n+1})+\nu(U_{n+1}\cap
V_{n+1})=\nu(U_{n+1})+\nu(V_{n+1})$, and since $V_{n+2}\subset U_{n+1}$, we
have $\nu(U_{n+1}\cap V_{n+1})\geq\nu(V_{n+2}\cap
V_{n+1})\geq\nu(V_{n+1})-2^{-(n+1)}$. Hence
$\nu(U_{n})\leq\nu(U_{n+1})+2^{-(n+1)}$, and by induction, we see
$\nu(U_{n})<\nu(U_{m})+2^{-n}$ wheneve $m>n$. Hence $(U_{n})$ is a fast
monotone lower-Cauchy subsequence.

To show $(U_{n})\sim(V_{n})$, since clearly $\nu(U_{n})\geq\nu(V_{n})$, we
need to show $\nu(U_{n})\leq\nu(V_{n})+\epsilon$ for $n$ sufficiently large.
We first show that for all $m>n$, $\nu(U_{n})\leq 2^{-n}+\nu(V_{m})$. Note
$U_{n}=U_{n+1}\cup V_{n+1}$, and $V_{n+2}\subset U_{n+1}$. Let
$U_{n,m}=\bigcup_{k=n+1}^{m}V_{k}$, noting $U_{m-1,m}=V_{m}$. Then
$\nu(U_{n+1,m})+\nu(V_{n+1})=\nu(U_{n+1,m}\cup V_{n+1})+\nu(U_{n+1,m}\cap
V_{n+1})=\nu(U_{n,m})+\nu(U_{n+1,m}\cap
V_{n+1})\geq\nu(U_{n,m})+\nu(V_{n+2}\cap
V_{n+1})\geq\nu(U_{n,m})+\nu(V_{n+1})-2^{-(n+1)}$, so
$\nu(U_{n+1,m})\geq\nu(U_{n,m})-2^{-(n+1)}$. Hence
$\nu(U_{n,m})\leq\nu(U_{m-1,m})+\sum_{k=n+1}^{m-1}2^{-k}\leq\nu(V_{m})+2^{-n}$.
Since $U_{n}\bigcup_{m=n+1}^{\infty}U_{n,m}$, there exists $m$ such that
$\nu(U_{n,m})\geq\nu(U_{n})-2^{-n}$. Then
$\nu(V_{m})\geq\nu(U_{n})-2\\!\times\\!2^{-n}$, and since
$\nu(U_{m})\geq\nu(U_{n})-2^{-n}$, we have
$\nu(V_{m})\geq\nu(U_{m})-3\\!\times\\!2^{-n}$.

∎

######  Remark 22 (Equivalent definitions of $\nu$-lower-measurable sets).

By Lemma 21, we see that the monotonicity condition on the open sets $U_{n}$
in Definition 16 is unnecessary, and that fast convergence can be weakened to
effective convergence.

By Theorem 26, we see that a second definition would be to say (i) any open
set is $\nu$-lower-measurable, and (ii) any fast $\nu$-lower-Cauchy sequence
$(V_{n})_{n\in\mathbb{N}}$ of $\nu$-lower-measurable sets defines a lower-
measurable set $V_{\infty}$, with then
$V_{\infty}:=\sup_{n\in\mathbb{N}}\nu(V_{n})-2^{-n}$.

A third definition for countably-based topological spaces would be to take a
countable basis, and consider $\nu$-lower-Cauchy sequences of _finite_ unions
of basic sets.

Which definition to take is a matter of taste; our Definition 16 provides
strong properties of the approximating sequences, so is easy to use in
hypotheses, but it requires more work to prove. However, Lemma 21 shows that
it suffices to compute an effectively lower-Cauchy sequence. One advantage of
using fast sequences over effective sequences is that we do not have to
explicitly pass around a counvergence rate.

has the advantage of providing a uniform construction, though for explicit
computations, it may be more appropriate to restrict to finite unions of basic
open sets.

###  4.2 Intersections and unions of lower-measurable sets

We now consider computability of intersections and unions of lower-measurable
sets.

The following lemma compares measures of unions and intersections of
equivalent sets.

######  Lemma 23.

Let $(U_{n})$, $(V_{n})$ and $(W_{n})$ be $\nu$-lower-Cauchy sequences.

  1. 1.

If $\nu\bigl{(}(U\cap V)_{\infty}\bigr{)}=\nu(U_{\infty})=\nu(V_{\infty})$, or
$\nu\bigl{(}(U\cup V)_{\infty}\bigr{)}=\nu(U_{\infty})=\nu(V_{\infty})$, then
$(U_{n})\sim(V_{n})$.

  2. 2.

If $(U_{n})\sim_{\nu}(V_{n})$, then $(U_{n}\cap V_{n})\sim_{\nu}(U_{n+1}\cup
V_{n+1})$, and both are equivalent to $(U_{n})$ and $(V_{n})$.

###### Proof.

  1. 1.

$\nu(U_{n}\cap V_{n})\geq\lim_{n\to\infty}\nu(U_{n}\cap
V_{n})=\nu(U_{\infty})\geq\nu(U_{n})-2^{-n}$. Similarly, $\nu(U_{n}\cup
V_{n})\geq\nu(\lim_{n\to\infty}U_{n}\cup
V_{n})=\nu(U_{\infty})\geq\nu(U_{n})-2^{-n}$.

  2. 2.

$\nu(U_{n}\cap(U_{n}\cap V_{n}))=\nu(U_{n}\cap V_{n})$, and $\nu(U_{n}\cap
V_{n})\geq\nu(U_{n})-2^{-n}$ by definition of $\sim_{\nu}$.
$\nu(U_{n}\cap(U_{n}\cup V_{n}))=\nu(U_{n})$, and $\nu(U_{n}\cup
V_{n})=\nu(U_{n})+\nu(V_{n})-\nu(U_{n}\cap V_{n})\leq\nu(U_{n})+2^{-n}$, so
$\nu(\nu(U_{n}\cap(U_{n}\cup V_{n}))\geq\nu(U_{n}\cup V_{n})-2^{-n}$ as
required. ∎

######  Theorem 24 (Intersections and unions of lower-measurable sets).

Let $\nu$ be a probability valuation on a type $\mathbb{X}$. Then operations
of (1) intersection, and (2) union are computable on $\nu$-lower-measurable
sets.

###### Proof.

Suppose $U_{n}\rightsquigarrow_{\nu}U_{\infty}$ and
$V_{n}\rightsquigarrow_{\nu}V_{\infty}$.

  1. 1.

We show that $(U_{n}\cap V_{n})$ is a fast $\nu$-lower-Cauchy sequence. For
$m>n$ and any $l>m$, $\nu(U_{n}\cap V_{n})-\nu(U_{m}\cap
V_{m})\leq\nu(U_{n})-\nu(U_{l}\cap V_{l})\leq\nu(U_{n})-\nu(U_{l})+2^{-l}\leq
2^{-n}+2^{-l}$. Since $l$ can be made arbitrarily large, $\nu(U_{m}\cap
V_{m})\geq\nu(U_{n}\cap V_{n})-2^{-n}$.

  2. 2.

For $m>n$, we have $U_{m}\subset U_{n}$ and $V_{m}\subset V_{n}$, so by
Proposition 11, $\nu(U_{m})+\nu(V_{m})+\nu(U_{n}\cup
V_{n})\leq\nu(V_{m})+\nu(U_{m}\cup V_{n})+\nu(U_{n})\leq\nu(U_{m}\cup
V_{m})+\nu(U_{n})+\nu(V_{n})$. Hence $\nu(U_{n}\cup V_{n})-\nu(U_{m}\cup
V_{m})\leq(\nu(U_{n})-\nu(U_{m}))+(\nu(V_{n})-\nu(V_{m}))\leq
2\\!\times\\!2^{-n}$, so $\nu(U_{n+1}\cup V_{n+1})-\nu(U_{m+1}\cup
V_{m+1})\leq 2^{-n}$. ∎

######  Theorem 25 (Countable unions of lower-measurable sets).

Let $\nu$ be a probability valuation on a type $\mathbb{X}$. Then the
operation of countable union is computable on $\nu$-lower-measurable sets.

###### Proof.

We can show that if $U_{k}\subset V_{k}$ for $k=1,2,\ldots$, then
$\nu(\bigcup_{k=1}^{\infty}V_{k})-\nu(\bigcup_{k=1}^{\infty}U_{k})\leq\sum_{k=1}^{n}\bigl{(}\nu(V_{k})-\nu(U_{k})\bigr{)}$.

Given $U_{k,n}\rightsquigarrow_{\nu}U_{k}$, we show that
$V_{n}:=\bigcup_{k=0}^{\infty}U_{k,n+k+1}$ is a $\nu$-lower-Cauchy sequence.
For if $m>n$, then
$\nu\bigl{(}\bigcup_{k=0}^{\infty}U_{k,n+k+1}\bigr{)}-\nu\bigl{(}\bigcup_{k=0}^{\infty}U_{k,m+k+1}\bigr{)}\leq\sum_{k=0}^{\infty}\bigl{(}\nu(U_{k,n+k+1})-\nu(U_{k,m+k+1})\bigr{)}\leq\sum_{k=0}^{\infty}2^{-(n+k+1)}=2^{-n}$
as required. ∎

We can similarly compute countable intersections of _effectively_ decreasing
sequences of $\nu$-lower-measurable sets.

######  Theorem 26 (Effective countable intersections of lower-measurable
sets).

Suppose $(V_{n})$ is a fast monotone lower-Cauchy sequence of $\nu$-lower-
measurable sets. Then $V_{n}$ converges effectively to a $\nu$-lower-
measurable set $V_{\infty}$.

###### Proof.

Write $V_{k,\infty}=V_{k}$ and let $V_{k,n}$ be a fast monotone lower-Cauchy
sequence of open sets converging to $V_{k}$. Define
$V_{\infty,n}=V_{n+1,n+1}\cap V_{\infty,n-1}$, which is clearly monotone. Note
that since $V_{n+1,\infty}\subset V_{n+1,n+1}$ and $V_{n+1,\infty}\subset
V_{n,\infty}$, we have $V_{\infty,n}\supset V_{n+1,\infty}=V_{n+1}$. Then for
$m>n$,
$\nu(V_{\infty,n})-\nu(V_{\infty,m})\leq\nu(V_{n+1,n+1})-\nu(V_{m+1})\leq\nu(V_{n+1,n+1})-\nu(V_{n+1,\infty})+\nu(V_{n+1})-\nu(V_{m+1})\leq
2^{-(n+1)}+2^{-(n+1)}=2^{-n}$, so $V_{\infty,n}$ is a fast monotone lower-
Cauchy sequence of open sets, so represents a lower-measurable set
$V_{\infty,\infty}=V_{\infty}$.

Finally, we have
$\nu(V_{n})-\nu(V_{\infty})-\nu(V_{n,\infty})-\nu(V_{\infty,\infty})\leq\nu(V_{\infty,n})-\nu(V_{\infty,\infty})\leq
2^{-n}$, from which we see that $V_{\infty}$ is indeed the limit of $(V_{n})$.
∎

######  Proposition 27 (Lower measure is modular).

$\nu(U_{\infty}\cap V_{\infty})+\nu(U_{\infty}\cup
V_{\infty})=\nu(U_{\infty})+\nu(V_{\infty})$.

###### Proof.

For fixed $n$, $\nu(U_{n}\cap V_{n})+\nu(U_{n}\cup
V_{n})=\nu(U_{n})+\nu(V_{n})$ by modularity of valuations. Then
$\nu(U_{\infty}\cap V_{\infty})+\nu(U_{\infty}\cup
V_{\infty})\geq\nu(U_{n}\cap V_{n})-2^{-n}+\nu(U_{n}\cup
V_{n})-2\\!\times\\!2^{-n}=\nu(U_{n})+\nu(V_{n})-3\times
2^{-n}\geq\nu(U_{\infty})+\nu(V_{\infty})-3\times 2^{-n}$. Taking $n\to\infty$
gives $\nu(U_{\infty}\cap V_{\infty})+\nu(U_{\infty}\cup
V_{\infty})\geq\nu(U_{\infty})+\nu(V_{\infty})$. The reverse inequality is
similar, since
$\nu(U_{\infty})+\nu(V_{\infty})\geq\nu(U_{n})+\nu(V_{n})-2\times 2^{-n}$. ∎

###  4.3 Topology of lower-measurable sets

The representation of $\nu$-lower-measurable sets induces a (non-Hausdorff)
quotient topology on the space. Recall that for open sets, $U_{n}\to
U_{\infty}\iff\forall x\in U_{\infty},\exists N,\forall n\geq N,x\in U_{n}$.

For $\nu$-lower-Cauchy sequences, convergence is given by
$(U_{k,n})\to(U_{\infty,n})$ as $k\to\infty$ if for all $n$, there exists $K$
such that $\nu(U_{k,n}\cap U_{\infty,n})\geq\nu(U_{\infty,n})-2^{-n}$ whenever
$k\geq K(n)$. The convergence is effective if $K(n)$ is known; by restricting
to subsequences we may take $K(n)=n$. In this case, a $\nu$-lower-Cauchy
sequence representing the limit is
$U_{\infty,n}=\bigcup_{k=n+1}^{\infty}U_{k,n+k+1}$.

######  Property 28 (Topology on $\nu$-lower-measurable sets).

A set of $\nu$-lower-measurable sets $\mathcal{W}$ is _open_ if

$\forall W\in\mathcal{W},\ \exists\epsilon>0,\ \forall V,\ \nu(V\cap
W)>\nu(W)-\epsilon\implies V\in\mathcal{W}.$ (8)

######  Property 29.

The convergence relation on $\nu$-lower-Cauchy sequences of $\nu$-lower-
measurable sets is given by $V_{k}\to V_{\infty}$ as ${k\to\infty}$ if
$\liminf_{k\to\infty}\nu(V_{k}\cap V_{\infty})\geq\nu(V_{\infty})$.

The convergence is _effective_ if $\nu(V_{k}\cap
V_{\infty})\geq\nu(V_{\infty})-\epsilon(k)$ for _known_ $\epsilon(k)$, and
_fast_ if $\epsilon(k)=2^{-k}$.

###  4.4 Relationship with classical measure-theory

######  Remark 30 (Outer-regular measures).

In the literature on classical measure theory (see [vG02]), defining
$\nu(U_{\infty})=\bigcap_{n\in\mathbb{N}}\nu(U_{n})=\inf_{n\in\mathbb{N}}\nu(U_{n})$
for a decreasing sequence of open sets corresponds to a _outer-regular
measure_ , since we approximate $U_{\infty}$ from outside. However, since
$U_{n}$ converges to $U_{\infty}$ from above, but the open sets $U_{n}$ are
inherently approximated from below, we cannot compute the measure of an
_arbitrary_ decreasing sequence of open sets. This motivates the use of
$\nu$-lower-Cauchy sequences, which converge rapidly from above. Since we
compute $\nu(U_{\infty})$ from below, we use the terminology “lower measure”.

######  Remark 31 (Relationship with classical Borel measures).

Our lower-measurable sets are all Borel sets, with lower measure equal to the
classical measure. Further, since any outer measure on a separable metric
space is a Borel measure, the measure of any set is the infemum of the measure
of its $\epsilon$-neighbourhoods, we see that any measurable set is equal to a
lower-measurable set up to a set of measure $0$. Hence our lower-measurable
sets capture the measure-theoretic behaviour of all Borel sets, but do so in a
way in which the measure is semicomputable.

###  4.5 Measurable sets

######  Definition 32 (Upper-measurable sets; upper-measure).

The type of _upper-measurable sets_ is the set of increasing sequences of
closed sets $(A_{n})$ such that $\nu(A_{m})\leq\nu(A_{n})+2^{-n}$ for all $n$
and all $m>n$. The _upper-measure_ is
$\inf_{n\in\mathbb{N}}\nu(A_{n})+2^{-n}$.

Note that a representation of an upper-measurable set is the same as the
complement of a lower-measurable set.

######  Definition 33 (Measurable sets).

The type of _measurable sets_ consists of equivalence classes of monotone
sequences of pairs of open and closed sets $(U_{n},A_{n})$ such that
$U_{n}\subset U_{n+1}\subset A_{n+1}\subset U_{n}$ for all $n$, and
$\nu(A_{n}\setminus U_{n})\leq 2^{-n}$, under the equivalence relation
$(U_{n},A_{n})\sim(V_{n},B_{n})$ if, and only if, $\nu(A_{n}\setminus
V_{n}\cup B_{n}\setminus U_{n})\to 0$ as $n\to\infty$.

In other words type of $\nu$-measurable sets in $\mathbb{X}$ is the effective
completion of the type of pairs
$(U,A)\in\mathcal{O}(\mathbb{X})\times\mathcal{A}(\mathbb{X})$ satisfying
$U\subset A$ under the (non-metric) distance $d((U,A),(V,B))=P(A\setminus
V\cup B\setminus U)$. Note that $d((U,A),(U,A))=\nu(A\setminus U)$, which need
not be zero, but from the condition
$d((U_{m},A_{m}),(U_{n},A_{n}))<2^{-\min(m,n)}$, we have $\mu(A_{n}\setminus
U_{n})<2^{-n}$ for all $n$.

The type of measurable sets is equivalent to giving a fast monotone lower-
Cauchy sequence $(U_{n})$ and a fast monotone upper-Cauchy sequence $(A_{n})$
for the same set i.e. such that $\nu(A_{n}\setminus U_{m})\to 0$ whenever
$m,n\to\infty$.

###  4.6 Lower-measurable sets as point-sets

If $(U_{n})$ is a $\nu$-lower-Cauchy sequence, we will write $\nu(U_{\infty})$
for $\sup_{n\in\mathbb{N}}\nu(U_{n})-2^{-n}$. Similarly, we write $\nu((U\cap
V)_{\infty})$ for $\sup_{n\in\mathbb{N}}\nu(U_{n}\cap V_{n})-2^{-n}$. It is
tempting to define the lower-measure of $(U_{n})$ as a property of the
_intersection_ $\bigcap_{n\in\mathbb{N}}U_{n}$. Unfortunately, for general
spaces, it need not be the case that
$\sup_{n\in\mathbb{N}}\nu(U_{n})-2^{-n}=\sup_{n\in\mathbb{N}}\nu(V_{n})-2^{-n}$
even if $\bigcap_{n\in\mathbb{N}}U_{n}=\bigcap_{n\in\mathbb{N}}V_{n}$.
However, for spaces satisfying the conditions of Theorem 3, the $\nu$-lower-
measure is indeed a property of the $G_{\delta}$ intersection. We prove this
directly for Polish (separable completly metrisable) spaces:

######  Theorem 34 (Lower-measurable sets in metric spaces).

If $\mathbb{X}$ is a separable complete metric space, $\nu$ a valuation on
$\mathbb{X}$, and
$\bigcap_{n\in\mathbb{N}}U_{n}=\bigcap_{n\in\mathbb{N}}V_{n}$ for $\nu$-lower-
Cauchy sequences $(U_{n}),(V_{n})$, then
$\sup_{n\in\mathbb{N}}U_{n}-2^{-n}=\sup_{n\in\mathbb{N}}V_{n}-2^{-n}$.

###### Proof.

Since $I_{\epsilon}(U)\subset\overline{I}_{\epsilon}(U)\subset I_{\delta}(U)$
when $\delta<\epsilon$, and since $\nu$ is continuous, there exist closed sets
$A_{n}\subset U_{n}$ such that $\nu(A_{n})\geq\nu(U_{n})-2^{-(n+1)}$. Let
$B_{n}=\bigcap_{m\geq n}A_{m}$, so $B_{n}$ is an increasing sequence of closed
sets such that $B_{n}\subset\bigcap_{m\geq n}U_{m}=U_{\infty}$ for all $n$, so
$\bigcup_{n\in\mathbb{N}}B_{n}\subset\bigcap_{n\in\mathbb{N}}U_{n}$. Further,
since $\nu(A_{n}\cap\cdots\cap A_{m})\geq\nu(U_{n}\cap\cdots\cap
U_{m})+\sum_{l=n}^{m}\bigl{(}\nu(A_{l})-\nu(U_{l})\bigr{)}\geq\nu(U_{m})-2^{-n}$
for all $m$, we have that
$\nu(B_{n})\geq\inf_{m\in\mathbb{N}}\nu(U_{m})-2^{-n}=\sup_{m\in\mathbb{N}}U_{m}-2^{-m}-2^{-n}$,
so
$\inf_{n\in\mathbb{N}}\nu(B_{n})+2^{-n}\geq\sup_{n\in\mathbb{N}}\nu(U_{n})-2^{-n}$,
and $\lim_{n\to\infty}\nu(B_{n})\geq\lim_{n\to\infty}\nu(U_{n})$. Since also
$B_{n}\subset\bigcap_{n\in\mathbb{N}}V_{n}$ for all $n$, we have
$\lim_{n\to\infty}\nu(U_{n})\leq\lim_{n\to\infty}\nu(B_{n})\leq\lim_{n\to\infty}\nu(V_{n})$,
so $\sup_{n\in\mathbb{N}}U_{n}-2^{-n}\leq\sup_{n\in\mathbb{N}}V_{n}-2^{-n}$.
The reverse inequality follows by symmetry. ∎

##  5 Computable Random Variables

In the standard approach to probability theory developed in classical
analysis, one defines random variables as measurable functions over a base
probability space. Given types $\mathbb{X}$ and $\mathbb{Y}$, a representation
of the Borel measurable functions $f$ from $\mathbb{X}$ to $\mathbb{Y}$ was
given in [Bra05], but this does not allow one to compute lower bounds for the
measure of $f^{-1}(V)$ for $V\in\mathcal{O}(\mathbb{Y})$.

A computable theory of random variables should, at a minimum, enable us to
perform certain basic operations, including:

  1. (i)

Given a random variable $X$ and open set $U$, compute lower-approximation to
$\mathbb{P}(X\in U)$.

  2. (ii)

Given random variables $X_{1},X_{2}$, compute the random variable $X_{1}\times
X_{2}$ giving the joint distribution.

  3. (iii)

Given a random variable $X$ and a continuous function $f$, compute the image
$f(X)$.

  4. (iv)

Given a sequence of random variables $X_{1},X_{2},\ldots$ converging
effectively in probability, compute a limit random variable
$X_{\infty}=\lim_{m\to\infty}X_{m}$.

  5. (v)

Given a probability distribution $\nu$ on a sufficiently nice space
$\mathbb{X}$, compute a random variable $X$ with distribution $\nu$.

Property (i) states that we can compute the distribution of a random variable,
while property (ii) implies that a random variable is _more_ than its
distribution; it also allows us to compute its joint distribution with another
random variable. Property (iii) also implies that for random variables
$X_{1},X_{2}$ on a computable metric space $(\mathbb{X},d)$, the random
variable $d(X_{1},X_{2})$ is computable in $\mathbb{R}^{+}$, so the
probability $\mathbb{P}(d(X_{1},X_{2})<\epsilon)$ is computable in
$\mathbb{I}_{<}$, and $\mathbb{P}(d(X_{1},X_{2})\leq\epsilon)$ is computable
in $\mathbb{I}_{>}$. Property (iv) is a completeness property and allows
random variables to be approximated. Property (v) shows that random variables
can realise a given distribution. These properties are similar to those used
in [Ker08].

Ideally, one would like a representation of bounded measurable functions
$f:\mathbb{X}\rightarrow\mathbb{R}$ such that for _every_ finite measure $\mu$
on $\mathbb{X}$, the integral $\int_{\mathbb{X}}f(x)\,d\mu(x)$ is computable.
But then $f(y)=\int_{\mathbb{X}}f(x)\,d\delta_{y}(x)$ would be computable, so
$f$ would be continuous. Any effective approach to measurable functions and
integration must therefore take some information about the measure into
account.

We will consider random variables on a fixed probability space $(\Omega,P)$.
Since any probability distribution on a Polish space is equivalent to a
distribution on the standard Lesbesgue-Rokhlin probability space [Roh52], it
is reasonable to take the base space to be the Cantor space
$\Sigma=\\{0,1\\}^{\omega}$ and $P$ the standard measure.

However, our treatment of random variables will require the notion _lower-
measures_ , and a type of _lower-measurable sets_ , for which we can compute
the measure in $\mathbb{R}^{+}_{<}$.

###  5.1 Measurable functions and random variables

######  Definition 35 (Measurable function).

Let $\mathbb{W},\mathbb{X}$ be types and $\nu$ a finite measure on
$\mathbb{W}$. Then the type of _$\nu$ -measurable functions_ $f$ from
$\mathbb{W}$ to $\mathbb{X}$ is defined by continuous
$f^{-1}:\mathcal{O}(\mathbb{X})\to\mathcal{M_{<}}(\mathbb{W})$ satisfying
$f^{-1}(\emptyset)=_{\nu}\emptyset$, $f^{-1}(X)=_{\nu}W$, $f^{-1}(U_{1}\cap
U_{2})=_{\nu}f^{-1}(U_{1})\cap f^{-1}(U_{2})$ and $f^{-1}(U_{1}\cup
U_{2})=_{\nu}f^{-1}(U_{1})\cup f^{-1}(U_{2})$.

We denote the $\nu$-measurable functions $f$ from $\mathbb{W}$ to $\mathbb{X}$
by $f:\mathbb{W}\rightsquigarrow_{\nu}\mathbb{X}$, or simply
$f:\mathbb{W}\rightsquigarrow\mathbb{X}$ if the measure $\nu$ is clear from
the context.

Measurable functions $f_{1}$ and $f_{2}$ are considered equal if
$f_{1}^{-1}(U)=_{\nu}f_{2}^{-1}(U)$ for all $U\in\mathcal{O}(\mathbb{X})$.

Note that since $f^{-1}$ is continuous, then we must have
$f^{-1}(V_{1})\subset_{\nu}f^{-1}(V_{2})$ if $V_{1}\subset V_{2}$, and
$f^{-1}(\bigcup_{n=0}^{\infty}V_{n})=_{\nu}\bigcup_{n=0}^{\infty}f^{-1}(V_{n})$.

######  Remark 36.

We do not actually define $f$ as a _function_ $\mathbb{W}\to\mathbb{X}$ since
this would involve evaluating at points, though clearly any continuous
function $\mathbb{W}\to\mathbb{X}$ is measurable.

######  Definition 37 (Random variable).

Let $\Omega$ be a separable complete metric space used as a base space, $P$ a
probability measure on $\Omega$, and $\mathbb{X}$ a topological space Then a
_random variable_ $X$ on $\mathbb{X}$ is a $P$-measurable function
$\Omega\rightsquigarrow\mathbb{X}$. We denote the type of random variables on
$\mathbb{X}$ by $\mathcal{R}(\mathbb{X})$ or
$\Omega\rightsquigarrow\mathbb{X}$.

We will sometimes write $\mathcal{P}(X\in U)$ as a shorthand for
$P(\\{\omega\in\Omega\mid X(\omega)\in U\\})$; for a piecewise-continuous
random variable $X$ we implicitly restrict $\omega$ to $\mathrm{dom}(X)$.

Just as for measurable functions, although a random variable $X$ is _defined_
relative to the underlying space $\Omega$, we cannot in general actually
_compute_ $X(\omega)$ in any meaningful sense for fixed $\omega\in\Omega$. The
expression $X(\omega)$ only makes sense for random variables _given_ as
(piecewise) continuous functions $\Omega\rightarrow\mathbb{X}$ as stated
below:

######  Definition 38 ((Piecewise)-continuous random variable).

A _continuous random variable_ on $(\Omega,P)$ with values in $\mathbb{X}$ is
a continuous function $X:\Omega\rightarrow\mathbb{X}$.

A _piecewise-continuous random variable_ is a continuous partial function
$X:\Omega\rightharpoonup\mathbb{X}$ such that
$\mathrm{dom}(X)\in\mathcal{O}(\Omega)$ and $P(\mathrm{dom}(X))=1$.

We use the terminology “piecewise-continuous” since
$X:\Omega\rightharpoonup\mathbb{X}$ may arise as the restriction of a
piecewise-continuous function to its continuity set.

######  Observation 39.

Given a piecewise-continuous random variable
$X:\Omega\rightharpoonup\mathbb{X}$, we can compute
$X^{-1}:\mathcal{O}(\mathbb{X})\to\mathcal{M}_{<}(\Omega)$, since $X^{-1}(U)$
is open for open $U$, and any open set is lower-measurable.

Clearly, for piecewise-continuous random variables $X_{1},X_{2}$, we have
$X_{1}=X_{2}$ if $P(\\{\omega\in\Omega\mid X_{1}(\omega)\neq
X_{2}(\omega)\\})=0$; in other words, $X_{1}$ and $X_{2}$ are _almost-surely
equal_.

By [Wei99, Theorem 2.2.4], machine-computable functions
$\\{0,1\\}^{\omega}\rightarrow\\{0,1\\}^{\omega}$ are defined on a
$G_{\delta}$-subsets of $\\{0,1\\}^{\omega}$. Indeed, any function into a
metric space is continuous on a $G_{\delta}$ set of points. This makes
functions defined and continuous on a full-measure $G_{\delta}$-subset of
$\\{0,1\\}^{\omega}$ a natural class of random variables, where by a full-
measure $G_{\delta}$-set $W$, we require $P(U)=1$ whenever $W\subset U$ for
open $U$.

######  Definition 40 (Almost-surely continuous random variable).

An _almost-surely-continuous random variable_ on $(\Omega,P)$ with values in
$\mathbb{X}$ is a continuous partial function
$X:\Omega\rightharpoonup\mathbb{X}$ such that $\mathrm{dom}(X)$ is a
$G_{\delta}$ set and $P(\mathrm{dom}(X))=1$.

Not all measurable random variables are almost-surely continuous:

######  Example 41.

Define a strong Cauchy sequence $X_{n}$ of piecewise-continuous random
variable taking values in $\\{0,1\\}$ such that $X_{n}=1$ on a decreasing
sequence of closed sets $W_{n}$ of measure $(1+2^{-n})/2$ whose limit is a
Cantor set. Then $X_{\infty}=\lim_{n\to\infty}X_{n}$ is discontinuous on a set
of positive measure, so is not an almost-surely-continuous random variable.

It will often be useful to consider random variables taking finitely many
values:

######  Definition 42 (Simple random variable).

A random variable $X$ on $(\Omega,P)$ with values in $\mathbb{X}$ _simple_ if
it takes finitely many values.

###  5.2 Properties of random variables

We now consider the properties (i)-(iv) that we wish our random variables to
have, and show that they are satisfied.

####  5.2.1 Distribution

######  Definition 43 (Distribution of a measurable random variable).

For a measurable random variable $X$ over base space $(\Omega,\mathcal{P})$,
define its _distribution_ by

$\mathbb{P}(X\in U)=\mathcal{P}(X^{-1}(U)).$

From our definition, the probability distribution of a random variable is
trivially computable:

######  Observation 44.

Let $X$ be a random variable on $\mathbb{X}$. Then the distribution of $X$ is
computable.

####  5.2.2 Products

######  Definition 45.

Suppose $\mathbb{X}_{1}$ and $\mathbb{X}_{2}$ are such that the product space
$\mathbb{X}_{1}\times\mathbb{X}_{2}$ is a sequential space. Then for
$X_{1}:\mathcal{R}(\mathbb{X}_{1})$ and $X_{2}:\mathcal{R}(\mathbb{X}_{2})$,
the product $X_{1}\times
X_{2}:\mathcal{R}(\mathbb{X}_{1}\times\mathbb{X}_{2})$ is defined by setting
$[X_{1}\times X_{2}]^{-1}(U_{1}\times U_{2})=X_{1}^{-1}(U_{1})\cap
X_{2}^{-1}(U_{2})$, and extending to arbitrary sets by taking unions of the
product open sets.

The product of two random variables is computable:

######  Theorem 46 (Computability of products).

Suppose $\mathbb{X}$ and $\mathbb{Y}$ are such that the product space
$\mathbb{X}\times\mathbb{Y}$ is sequential. Then for
$X:\mathcal{R}(\mathbb{X})$ and $\mathbb{Y}:\mathcal{R}(\mathbb{Y})$, the
product $X\times Y:\mathcal{R}(\mathbb{X}\times\mathbb{Y})$ is computable.

###### Proof.

Since $\mathbb{X}\times\mathbb{Y}$ is a sequential space, the topology is
generated by sets of the form $U\times V$ for $U\in\mathcal{O}(\mathbb{X})$
and $V\in\mathcal{O}(\mathbb{Y})$. Then $(X\times Y)^{-1}(U\times
V)=X^{-1}(U)\cap Y^{-1}(V)$, which is computable in
$\mathcal{M_{<}}(\Omega,P)$ by Theorem 24. ∎

######  Lemma 47.

If $X_{1}$, $X_{2}$ are continuous random variables, then the product
$X_{1}\times X_{2}$ is the functional product

$(X_{1}\times X_{2})(\omega)=(X_{1}(\omega),X_{2}(\omega)).$

###### Proof.

$[X_{1}\times X_{2}]^{-1}(U_{1}\times U_{2})=X_{1}^{-1}(U_{1})\cap
X_{2}^{-1}(U_{2})=\\{\omega\in\Omega\mid X_{1}(\omega)\in
U_{1}\\}\times\\{\omega\in\Omega\mid X_{2}(\omega)\in U_{2}\\}$. ∎

####  5.2.3 Image

######  Definition 48.

The image of a random variable $X:\mathcal{R}(\mathbb{X})$ under a continuous
function $f:\mathbb{X}\to\mathbb{Y}$ is defined by
$[f(X)]^{-1}(V):=X^{-1}(f^{-1}(V))$.

######  Theorem 49 (Computability of images).

The image of a random variable under a continuous function is computable.

###### Proof.

$[f(X)]^{-1}(V)=X^{-1}(f^{-1}(V))$, which is computable since $f^{-1}(V)$ is
computable in $\mathcal{O}(\mathbb{X})$. ∎

######  Remark 50.

If $g:\mathbb{X}\rightsquigarrow\mathbb{Y}$ and
$f:\mathbb{Y}\rightsquigarrow\mathbb{Z}$ are measurable then the composition
is not computable. For example, take $g_{c}:\Omega\to\mathbb{R}$ to be the
constant function $g_{c}(\omega)=c$, and
$f:\mathbb{R}\rightsquigarrow\\{0,1\\}$ the Heaviside function $f(x)=0$ if
$x\leq 0$ and $f(x)=1$ for $x>0$. Then for $r=1$ and $c_{n}\searrow
c_{\infty}0$ we have $P((f\circ g_{c_{n}})^{-1}(1))=P(\Omega)=1$, but
$P((f\circ g_{c_{\infty}})^{-1}(1))=P(\emptyset)=0$.

####  5.2.4 Convergence

The convergence relation induced by the standard representation of a function
type is that of _pointwise-convergence_. For random variables (as measurable
functions), this means that $X_{n}\to X_{\infty}$ if, and only if, for all
open $U$, $X_{n}^{-1}(U)\to X_{\infty}^{-1}(U)$ in the type of
$\mathcal{P}$-lower-measurable sets. Explicitly:

######  Property 51.

A sequence of random variables $(X_{n})_{n\in\mathbb{N}}$ _converges_ to a
random variable $X_{\infty}$ if for all open $U$,
$\liminf_{n\to\infty}\mathbb{P}(X_{n}\in U\wedge X_{\infty}\in
U)\geq\mathbb{P}(X_{\infty}\in U)$.

The convergence is _effective_ if $\mathbb{P}(X_{n}\in U\wedge X_{\infty}\in
U)\geq\mathbb{P}(X_{\infty}\in U)-\varepsilon(U,n)$ for known
$\varepsilon(U,n)$, and _fast_ if $\mathbb{P}(X_{n}\in U\wedge X_{\infty}\in
U)\geq\mathbb{P}(X_{\infty}\in U)-2^{-n}$.

We also obtain computability of limits of effectively-converging Cauchy-like
sequences.

######  Definition 52.

A sequence of random variables $(X_{n})_{n\in\mathbb{N}}$ is a _fast Cauchy
sequence_ if for all open $U$, and all $m>n$, $\mathbb{P}(X_{m}\in U\wedge
X_{n}\in U)\geq\mathbb{P}(X_{n}\in U)-2^{-n}$.

######  Theorem 53.

If $(X_{n})$ is a fast Cauchy sequence of random variables, then
$\lim_{n\to\infty}X_{n}$ exists and is computable from $(X_{n})$.

###### Proof.

For every open $U\subset\mathbb{X}$, we need to compute $X_{\infty}^{-1}(U)$
as a $\mathcal{P}$-lower-measurable set. Define $W_{n}=X_{n}^{-1}(U)$, which
is a $\mathcal{P}$-lower-measurable set computable from $X_{n}$. Then for
$m>n$, $\mathcal{P}(W_{m}\cap W_{n})\geq\mathcal{P}(W_{n})-2^{-n}$, so
$(W_{n})$ forms a fast lower-Cauchy sequence on $\mathcal{P}$-lower-measurable
sets, and converges to $W_{\infty}$ with the correct properties by Theorem 26.
∎

###  5.3 Equality of random variables

We now show a result that two random variables are equal if, and only if,
their products with the identity random variable on the base space are equal.

######  Proposition 54.

Let $I$ be the identity random varible on $\Omega$. Then $X_{1}=X_{2}$ if, and
only if $Y_{1}:=I\times X_{1}$ and $Y_{2}:=I\times X_{2}$ have the same
distribution.

###### Proof.

We need to show that for every open $U$,
$X_{1}^{-1}(U)=_{\mathcal{P}}X_{2}^{-1}(U)$, which holds if
$\mathcal{P}(X_{1}^{-1}(U)\cap
X_{2}^{-1}(U))=\mathcal{P}(X_{1}^{-1}(U))=\mathcal{P}(X_{2}^{-1}(U))$
Computing a $\mathcal{P}$-lower-Cauchy sequence representing
$W_{i}=X_{i}^{-1}(U)$ yields open sets $W_{i,n}$ such that
$\mathcal{P}(W_{i,n}\cap W_{i})\geq\mathcal{P}(W_{i})-2^{-n}$. Then
$\mathbb{P}(X_{1}\in U\wedge X_{2}\in U)+2^{-n}=\mathcal{P}(W_{1}\cap
W_{2})+2^{-n}\geq\mathcal{P}(W_{1,n}\cap W_{2})=\mathbb{P}(I\in W_{1,n}\wedge
X_{2}\in U)=\mathbb{P}(Y_{2}\in W_{1,n}\times U)=\mathbb{P}(Y_{1}\in
W_{1,n}\times U)=\mathbb{P}(I\in W_{1,n}\wedge X_{1}\in
U)=\mathcal{P}(W_{1,n}\cap W_{1})=\mathcal{P}(W_{1})=\mathbb{P}(X_{1}\in U)$.
Since $n$ is arbitrary, $\mathbb{P}(X_{1}\in U\wedge X_{2}\in
U)\geq\mathbb{P}(X_{1}\in U)$. The result follows by symmetry. ∎

##  6 Random Variables in Metric Spaces

In this section, we consider random variables in metric spaces. We show that
an equivalent notion to our general random variables is given by completion in
the Fan metric.

###  6.1 Constructions in metric spaces

We first prove some generally-useful results on constructions of topological
partitions in computable metric spaces.

The following decomposition result is essentially a special case of the
effective Baire category theorem [YMT99, Bra01].

######  Lemma 55.

Let $X$ be an effectively separable computable metric space, and $\nu$ be a
valuation on $X$. Then given any $\epsilon>0$, we can compute a topological
partition $\mathcal{B}$ of $X$ such that $\mathrm{diam}(B)\leq\epsilon$ for
all $B\in\mathcal{B}$, and $\nu(X\setminus\bigcup\mathcal{B})=0$.

###### Proof.

For any $\epsilon>0$, any $\delta>0$, and any $x\in\mathbb{X}$,
$\\{r>0\mid\epsilon/2<r<\epsilon\,\wedge\,\nu(\overline{B}(x,r)\setminus
B(x,r))<\delta\\}$ is a computable open dense subset of
$[\epsilon/2,\epsilon]$. We can therefore construct a sequence of rationals
$q_{k}\in(\epsilon/2,\epsilon)$ such that $|q_{k}-q_{k+1}|<2^{-k-1}$ and
$\nu(\overline{B}(x,q_{k})\setminus B(x,q_{k}))<2^{-k}$. Then taking
$r_{\epsilon}(x)=\lim_{k\to\infty}q_{k}$ yields a radius
$r_{\epsilon}(x)\in[\epsilon/2,\epsilon]$ such that
$\nu(B(x,r_{\epsilon}(x))=\nu(\overline{B}(x,r_{\epsilon}(x)))$.

Since $X$ is effectively separable, it has a computable dense sequence
$(x_{n})_{n\in\mathbb{N}}$. For $\epsilon>0$, the sets
$B(x_{n},r_{\epsilon}(x_{n}))$ have radius at least $\epsilon/2$, so cover
$X$. We take as topological partition the sets
$B(x_{n},r_{\epsilon}(x_{n}))\setminus\bigcup_{m=0}^{n-1}\overline{B}(x_{m},r_{\epsilon}(x_{m}))$
for $n\in\mathbb{N}$. ∎

######  Lemma 56.

Let $\mathbb{X}$ be an effectively separable computable metric space, and
$\nu$ a valuation on $\mathbb{X}$. Then for any $\epsilon>0$, we can construct
an open set $U:\mathcal{O}(\mathbb{X})$ and a function $r:U\to X$ such that
$\nu(U)=1$, $r$ has finite range, and $d(r(x),x)<\epsilon$ for all $x\in U$.

###### Proof.

Let $\mathcal{B}$ be the topological partition computed from Lemma 55. For
every $B\in\mathcal{B}$, compute an element $x_{B}$ of $\mathbb{X}$ in $B$.
Define $r(x)$ by for $x\in\bigcup\mathcal{B}$ by $r(x)=x_{B}$ for $x\in B$. ∎

###  6.2 The Fan metric

Let $\mathbb{X}$ be a computable metric space. For a closed set $A$, define
$d(x,A)=\inf\\{d(x,y)\mid y\in A\\}$ and
$\,\overline{\\!N}_{\epsilon}(A):=\\{x\in\mathbb{X}\mid
d(x,A)\leq\varepsilon\\}$ For an open set $U$ define
$I_{\varepsilon}(U):=\mathbb{X}\setminus(\,\overline{\\!N}_{\varepsilon}(\mathbb{X}\setminus
U))=\\{x\in U\mid\exists\delta>0,B(x,\varepsilon+\delta)\subset U\\}$. Since
$d(x,A)$ is computable in $R^{+,\infty}_{<}$ by our definition of a computable
metric space, $\,\overline{\\!N}_{\epsilon}(A)$ is computable as a closed set,
so $I_{\varepsilon}(U)$ is computable as an open set. Note that
$I_{\varepsilon_{1}+\varepsilon_{2}}(U)\subset
I_{\varepsilon_{1}}(I_{\varepsilon_{2}}(U))$.

If $(\mathbb{X},d)$ is a complete metric space, then the _Fan metric_ is a
natural distance function on random variables:

######  Definition 57 (Fan metric).

$\displaystyle d_{F}(X,Y)$
$\displaystyle=\sup\\!\big{\\{}\varepsilon\in\mathbb{Q}^{+}\mid\
\mathcal{P}\big{(}\\{\omega\in\Omega\mid
d(X(\omega),Y(\omega))>\varepsilon\\}\big{)}>\varepsilon\big{\\}}$ (9)
$\displaystyle=\inf\\!\big{\\{}\varepsilon\in\mathbb{Q}^{+}\mid\
\mathcal{P}\big{(}\\{\omega\in\Omega\mid
d(X(\omega),Y(\omega))\geq\varepsilon\\}\big{)}<\varepsilon\big{\\}}.$

Given a computable metric
$d:\mathbb{X}\times\mathbb{X}\rightarrow\mathbb{R}^{+}$, the Fan metric on
continuous random variables is easily seen to be computable: The convergence
relation defined by the Fan metric corresponds to _convergence in probability_
: A sequence of random variables $X_{n}$ taking values in a metric space
converges in probability to a random variable $X_{\infty}$ if
$\mathcal{P}(d(X_{n},X_{\infty})>\epsilon)\to 0$ for all $\epsilon>0$. If the
metric $d$ on $\mathbb{X}$ is bounded, the distance $\textstyle
d(X,Y):=\int_{\Omega}d(X(\omega),Y(\omega))\,dP(\omega).$ is equivalent to the
Fan metric.

Recall that for topological spaces, a sequence of random variables $(X_{n})$
converges to $X_{\infty}$ if all open $U$,
$\liminf_{n\to\infty}\mathcal{P}(X_{n}\in U\wedge X_{\infty}\in
U)\geq\mathcal{P}(X_{\infty}\in U)$, which corresponds to
$\mathcal{P}(X_{n}\in U\wedge X_{\infty}\in U)\to\mathcal{P}(X_{\infty}\in U)$
with convergence of probabilities being considered in $\mathbb{R}^{+}_{<}$.

######  Proposition 58.

The Fan metric is computable.

###### Proof.

The random variable $X\times Y$ is computable given $X,Y$. Then
$\mathcal{P}(\\{\omega\mid
d(X(\omega),Y(\omega))>\varepsilon)=\mathbb{P}\bigl{(}X\times Y\in
d^{-1}(\\{e\mid e>\varepsilon\\})\bigr{)}$ is computable in
$\mathbb{R}^{+}_{<}$, and $\mathcal{P}\bigl{(}\\{\omega\mid
d(X(\omega),Y(\omega))>\varepsilon\bigr{)}>\varepsilon$ is verifiable, so
$d_{F}(X,Y)$ is computable in $\mathbb{R}^{+}_{<}$. Similarly,
$\mathcal{P}(\\{\omega\mid d(X(\omega),Y(\omega))\geq\varepsilon)$ is
computable in $\mathbb{R}^{+}_{>}$, so $d_{F}(X,Y)$ is computable in
$\mathbb{R}^{+}_{>}$. ∎

######  Theorem 59.

Suppose $(X_{n})_{n\in\mathbb{N}}$ is a fast Cauchy sequence of random
variables in the Fan metric. Then $X_{\infty}=\lim_{n\to\infty}X_{n}$ a random
variable which is computable from the $X_{n}$.

The proof is based on the non-effective version of this result from [MW43].

###### Proof.

Given open $U$, we need to compute $X_{\infty}^{-1}(U)$. Let
$U_{k+1}=I_{2^{-k}}(U)$. Then for $m>n$, Now $x_{n}\in U_{n}$ and
$d(x_{n},x_{m})<2^{-n}$, then $x_{m}\in U_{m}$ since $I_{2^{-(n-1)}}(U)\subset
I_{2^{-n}}(I_{2^{-(m-1)}}(U))$, and since
$\mathbb{P}(d(X_{m},X_{n})>2^{-n})\leq 2^{-n}$, we have $\mathbb{P}(X_{m}\in
U_{m}\wedge X_{n}\in U_{n})\geq\mathbb{P}(X_{n}\in U_{n})-2^{-n}$. Let
$W_{n}(U)=X_{n}^{-1}(I_{2^{-(n-1)}}(U))$, so $\mathcal{P}(W_{m}\cap
W_{n})\geq\mathcal{P}(W_{n})-2^{-n}$. Then $W_{n}(U)$ is a fast lower-Cauchy
sequence of $\mathcal{P}$-lower-measurable sets, so converges effectively to
some $\mathcal{P}$-lower-measurable set $W_{\infty}(U)$. We define
$X_{\infty}^{-1}(U)=W_{\infty}(U)$, and note that $\mathcal{P}(W_{n}\cap
W_{\infty})\geq\mathcal{P}(W_{n})-2^{-n}$ for all $n$.

It is straightforward to check
$X_{\infty}^{-1}(U)=\lim_{n\to\infty}X_{n}^{-1}(U)$ in the class of
$\mathcal{P}$-lower-measurable sets. The modularity property of
$X_{\infty}^{-1}$ follows from the equations $\mathcal{P}(X_{n}^{-1}(U_{1}\cup
U_{2}))+\mathcal{P}(X_{n}^{-1}(U_{1}\cap
U_{2}))=\mathcal{P}(X_{n}^{-1}(U_{1}))+\mathcal{P}(X_{n}^{-1}(U_{2}))$ by
passing through the limit. ∎

A random variable can therefore be represented by a sequence
$(X_{0},X_{1},X_{2},\ldots)$ of random variables from some simpler class
satisfying $d(X_{m},X_{n})<2^{-\min(m,n)}$, and two such sequences are
equivalent (represent the same random variable) if $d(X_{1,n},X_{2,n})\to 0$
as $n\to\infty$.

###  6.3 Representation

In this section, we prove two representation results on random variables in
metric spaces. We show that we can _construct_ a random variable with a given
_distribution_ , and that given any random variable, we can construct a
sequence of simple continuous random variables converging effectively to it.
These results depends on the base space $\Omega=\\{0,1\\}^{\omega}$ being
totally disconnected. Clearly, for a connected base space $\Omega$, such as
the interval $[0,1]$, then any continuous random variable takes values in a
single component of $\mathbb{X}$, and any simple continuous random variable is
constant, but if $\mathbb{X}$ is contractible, then the continuous random
variables may still be dense.

The following result shows that random variables can be represented by a
sequence of simple random variables. It is a variant of [SS06b, Theorem 14]
and [HR09, Theorem 1.1.1], which shows that any distribution is effectively
measurably isomorphic to a distribution on $\\{0,1\\}^{\omega}$, and the proof
is similar.

######  Theorem 60.

Let $\mathbb{X}$ be a computable metric space, and $\nu$ be a valuation on
$\mathbb{X}$. Then we can construct a random variable $X$ on base space
$\Omega=\\{0,1\\}^{\omega}$ such that for any open $U$, $\mathbb{P}(X\in
U)=\nu(U)$. Further, $X$ can be constructed as the effective limit of a fast
Cauchy sequence of simple continuous random variables.

###### Proof.

For each $n$, use Lemma 55 to construct a countable topological partition
$\mathcal{B}_{n}$ such that each $B\in B_{n}$ has diameter at most $2^{-n}$,
and $\sum_{B\in\mathcal{B}_{n}}\nu(\partial B)=0$. By taking intersections if
necessary, we can assume that each $\mathcal{B}_{n+1}$ is a refinement of
$\mathcal{B}_{n}$.

We now construct random variables $X_{n}$ as follows. Suppose we have
constructed cylinder sets $W_{n,m}\subset\\{0,1\\}^{\infty}$ such that
$P(W_{n,m})<\nu(B_{n,m})$ and $\sum_{m}P(W_{n,m})>1-2^{-n}$. Since $B_{n,m}$
is a union of open sets
$\\{B_{n+1,m,1},\ldots,B_{n+1,m,k}\\}\subset\mathcal{B}_{n+1}$, we can
effectively compute dyadic numbers $p_{n+1,m}$ such that
$p_{n+1,m,k}<\mu(B_{n+1,m,k})$ and $\sum_{k}p_{n+1,m,k}\geq P(W_{n,m})$. We
then partition $W_{n,m}$ into cylinder sets $W_{n+1,m,k}$ each of measure
$p_{n,m,k}$. For each $n,m,k$ we construct a point $x_{n+1,m,k}\in
B_{n+1,m,k}$, and take $X_{n+1}$ to map $W_{n+1,m,k}$ to a point
$x_{n+1,m,k}\in B_{n+1,m,k}$. It is clear that $X_{n}$ is a strongly-
convergent Cauchy sequence, so is a representation of a measurable random
variable $X_{\infty}$.

It remains to show that $\mathbb{P}(X_{\infty}\in U)=\nu(U)$ for all
$U\in\mathcal{O}(X)$. This follows since for given $n$ we have
$\mathbb{P}(X_{n}\in U)>\nu(I_{2^{1-n}}(U))-2^{-n}\nearrow\nu(U)$ as
$n\to\infty$. ∎

######  Theorem 61.

Let $\mathbb{X}$ be a computable metric space and $X:\mathcal{R}(\mathbb{X})$
a random variable. Then one can construct a fast Cauchy sequence of simple
continuous random variables $X_{n}$ such that
$\lim_{n\to\infty}X_{n}=X_{\infty}$.

Although one could prove this directly, there is a simple proof based on
Theorem 60 and Proposition 54:

###### Proof.

Let $I$ be the identity random variable on $\Omega$, and let $Y=I\times
X:\Omega\rightsquigarrow\Omega\times\mathbb{X}$. Let $Y_{n}=I_{n}\times X_{n}$
be a sequence of simple random variables with limit
$Y_{\infty}=I_{\infty}\times X_{\infty}$ such that
$\mathbb{P}[Y_{\infty}]=\mathbb{P}[Y]$. Then $Y_{\infty}=Y$, so
$X_{\infty}=\lim_{n\to\infty}X_{n}$ as required. ∎

######  Corollary 62.

If $\mathbb{X}$ is a computable metric space, then the representation of
random variable $X$ by its preimage
$X^{-1}:\mathcal{O}(\mathbb{X})\to\mathcal{M}_{<}(\Omega,\mathcal{P})$ is
equivalent to the representation by fast Cauchy sequences of simple
(piecewise-)continuous random variables.

###### Proof.

Given a representation of $X$, we can compute a fast Cauchy sequence of
(piecewise-)continuous random variables by Theorem 61. Conversely, given a
fast Cauchy sequence of piecewise-continuous random variables $X_{n}$, we can
compute $X_{n}$ as a measurable random variable by Observation 39, and the
limit by Theorem 59. ∎

###  6.4 Expectation

For bounded random variables taking values in the reals, the expectation is
defined in the usual way:

######  Definition 63 (Expectation).

If $X:\Omega\rightsquigarrow\mathbb{R}$ is an effectively bounded real-valued
random variable, the _expectation_ of $X$ is given by the integral

$\textstyle\mathbb{E}(X)=\int_{\mathbb{R}}x\,d\mathbb{P}[X],$

where $\mathbb{P}[X]$ is the valuation on $\mathbb{R}$ induced by $X$ i.e.
$\mathbb{P}[X](U)=\mathbb{P}(X\in U)=\mathcal{P}(X^{-1}(U))$, and the integral
is given by Definition 7.

The expectation of possibly unbounded real-valued random variables is not
continuous in the weak topology; for example, we can define continuous random
variables $X_{n}$ taking value $2^{n}$ on a subset of $\Omega$ of measure
$2^{-n}$, so that $X_{n}\to 0$ but $\mathbb{E}(X_{n})=1$ for all $n$. For this
reason, we need a new type of _integrable random variables_.

######  Definition 64 (Integrable random variable).

Let $(\mathbb{X},d)$ be metric space with distinguished element $z$ (e.g. the
zero of a normed space), and let $Z$ be the constant random variable
$Z(\omega)=z$. Let $d_{1}$ be the (possibly infinite-valued) distance function

$d_{1}(X,Y)=\int_{\Omega}d(X(\omega),Y(\omega))dP(\omega).$ (10)

The type of _integrable random variables_ $L^{1}(\mathbb{X})$ is the
completion of the set of all effectively bounded random variables $X$ such
that $d_{1}(X,Z)<\infty$. Then $d_{1}$ is a metric on $L^{1}(\mathbb{X})$.

If $d$ is a bounded metric, then this metric is equivalent to the Fan metric.

For continuous and integrable real-valued random variables, then the
expectation is also given by an integral over the base space $\Omega$.

######  Proposition 65 (Expectation).

  1. (i)

If $X:\Omega\rightarrow\mathbb{R}$ is a continuous real-valued random
variable, then the expectation of $X$ is given by the integral

$\textstyle\mathbb{E}(X)=\int_{\Omega}X(\omega)\,d\mathcal{P}(\omega),$

which always exists since $X$ has compact values.

  2. (ii)

If $X:\Omega\rightsquigarrow\mathbb{R}$ is an integrable real-valued random
variable, and $X$ is presented as $\lim_{n\to\infty}X_{n}$ for some sequence
of continuous random variables satisfying
$\mathbb{E}[|X_{n_{1}}-X_{n_{2}}|]\leq 2^{-\min(n_{1},n_{2})}$, then
$\bigl{(}\mathbb{E}(X_{n})\bigr{)}_{n\in\mathbb{N}}$ is an effective Cauchy
sequence, and

$\textstyle\mathbb{E}(X)=\lim_{n\to\infty}\mathbb{E}(X_{n}).$

###### Proof.

  1. (i)

It suffices to consider the case $X\geq 0$. Then both
$\int_{\mathbb{R}}xd\mathbb{P}[X]$ and
$\int_{\Omega}X(\omega)d\mathcal{P}(\omega)$ yield Choquet integral sums of
the form $\sum_{m=1}^{n}(p_{m}-p_{m-1})\mathcal{P}(X^{-1}(p_{m},\infty))$.

  2. (ii)

The expectation is continuous. ∎

We can effectivise Lesbegue spaces $\mathcal{L}^{p}$ of integrable random
variables through the use of effective Cauchy sequences in the natural way: If
$(\mathbb{X},|\cdot|)$ is a normed space, then the type of $p$-integrable
random variables with values in $\mathbb{X}$ is the effective completion of
the type of $p$-integrable continuous random variables under the metric
$d_{p}(X,Y)=||X-Y||_{p}$ induced by the norm

$\textstyle||X||_{p}=\left(\int_{\Omega}|X(\omega)|^{p}\,dP(\omega)\right)^{1/p}=\bigl{(}\mathbb{E}(|X|^{p})\bigr{)}^{1/p}.$
(11)

We can easily prove the Cauchy-Schwarz and triangle inequalities for
measurable random variables
$||XY||_{pq/(p+q)}\leq||X||_{p}\cdot||Y||_{q}\quad\text{and}\quad||X+Y||_{p}\leq||X||_{p}+||Y||_{p}\,.$

The following result relates the expectation of a random variable to an
integration over its valuation. An analogous result in a different setting
[SS06b, Theorem 15].

######  Theorem 66 (Expectation).

Let $X$ be a positive real-valued random variable such that
$\mathbb{E}(X)<\infty$. Then

$\textstyle\mathbb{E}(X)=\int_{0}^{\infty}\mathbb{P}(X>x)dx=\int_{0}^{\infty}\mathbb{P}(X\geq
x)dx.$

Note that the first integral is computable in $\mathbb{R}^{+}_{<}$, but the
second integral is in general uncomputable in $\mathbb{R}^{+}_{>}$, due to the
need to take the limit as the upper bound of the integral goes to infinity.
However, the second integral may be computable if the tail is bounded, for
example, if $X$ takes bounded values. The proof follows from the definition of
the lower integral:

###### Proof.

First assume $X$ is a continuous random variable, so by definition,
$\mathbb{E}(X)=\int_{\Omega}X(\omega)\,dP(\omega)$.

The definition of the lower horizontal integral gives
$\int_{\Omega}X(\omega)\,dP(\omega)\geq\sum_{i=0}^{n-1}(x_{i}-x_{i-1})P(\\{\omega\mid
X(\omega)>x_{i}\\})$ for all values $0=x_{0}<x_{1}<\cdots<x_{n}$. Take
$x_{i}-x_{i-1}<\epsilon$ for all $i$. Then
$\mathbb{E}(X)+\epsilon=\int_{\Omega}X(\omega)+\epsilon\,dP(\omega)\geq\sum_{i=1}^{n}(x_{i}-x_{i-1})P(\\{\omega\mid
X(\omega)+\epsilon>x_{i}\\})=\sum_{i=1}^{n}\int_{x_{i-1}}^{x_{i}}\mathbb{P}(X(\omega)>x_{i}-\epsilon)\,dx\geq\sum_{i=1}^{n}\int_{x_{i-1}}^{x_{i}}\mathbb{P}(X(\omega)>x_{i-1})\,dx\geq\sum_{i=1}^{n}\int_{x_{i-1}}^{x_{i}}\mathbb{P}(X(\omega)>x)\,dx=\int_{0}^{x_{n-1}}\mathbb{P}(X(\omega)>x)$.
Taking $n\to\infty$ gives
$\mathbb{E}(X)\geq\int_{0}^{\infty}\mathbb{P}(X>x)dx-\epsilon$, and since
$\epsilon$ is arbitrary,
$\mathbb{E}(X)\geq\int_{0}^{\infty}\mathbb{P}(X>x)dx$.

The definition of the lower horizontal integral gives for all $\epsilon>0$,
there exist $0=x_{0}<x_{1}<\cdots<x_{n}$, such that
$\int_{\Omega}X(\omega)\,dP(\omega)\leq\sum_{i=1}^{n}(x_{i}-x_{i-1})P(\\{\omega\mid
X(\omega)>x_{i}\\})+\epsilon$. By refining the partition if necessary, we can
assume $x_{i}-x_{i-1}<\epsilon$ for all $i$. Then
$\mathbb{E}(X)-\epsilon\leq\sum_{i=1}^{n}(x_{i}-x_{i-1})P(\\{\omega\mid
X(\omega)>x_{i}\\})=\sum_{i=1}^{n}\int_{x_{i-1}}^{x_{i}}P(\\{\omega\mid
X(\omega)>x_{i}\\}dx\leq\sum_{i=1}^{n}\int_{x_{i-1}}^{x_{i}}P(\\{\omega\mid
X(\omega)>x\\}dx=\int_{0}^{x_{n}}P(\\{\omega\mid
X(\omega)>x\\}dx\leq\int_{0}^{\infty}P(\\{\omega\mid X(\omega)>x\\}dx$. Hence
$\mathbb{E}(X)\leq\int_{0}^{\infty}\mathbb{P}(X>x)dx+\epsilon$, and since
$\epsilon$ is arbitrary,
$\mathbb{E}(X)\leq\int_{0}^{\infty}\mathbb{P}(X>x)dx$.

The case of measurable random variables follows by taking limits.

We show $\int_{0}^{\infty}\mathbb{P}(X\geq x)dx=\mathbb{E}(X)$ since
$\int_{0}^{\infty}\mathbb{P}(X>x)dx\leq\int_{0}^{\infty}\mathbb{P}(X\geq
x)dx\leq\int_{0}^{\infty}\mathbb{P}(X+\epsilon>x)dx=\epsilon+\int_{0}^{\infty}\mathbb{P}(X\geq
x)dx$ for any $\epsilon>0$. ∎

By changing variables in the integral, we obtain:

######  Corollary 67.

If $X$ is a real-valued random variable, then for any $\alpha\geq 1$,

$\textstyle\mathbb{E}(|X|^{\alpha})=\int_{0}^{\infty}\alpha\,x^{\alpha-1}\,\mathbb{P}(X>x)dx=\int_{0}^{\infty}\alpha
x^{\alpha-1}\mathbb{P}(X\geq x)dx.$

######  Remark 68 (Expectation of a distribution).

Theorem 66 shows that the expectation of a random variable depends only on its
_distribution_. Indeed, we can define the expectation of a probability
_valuation_ $\pi$ on $[0,\infty[$ by

$\textstyle\mathbb{E}(\pi)=\int_{0}^{\infty}\pi(\,]x,\infty[\,)dx=\int_{0}^{\infty}\pi(\,[x,\infty[\,)dx.$

If $f:\mathbb{X}\rightarrow\mathbb{R}^{+}_{<}$, then we can compute the _lower
expectation_ of $f(X)$ by

$\textstyle\mathbb{E}_{<}(f(X)):=\int_{0}^{\infty}\mathbb{P}\bigl{(}X\in
f^{-1}(\,]\lambda,\infty[\,)\bigr{)}d\lambda.$ (12)

We have an effective version of the classical dominated convergence theorem.

######  Theorem 69 (Dominated convergence).

Suppose $X_{n}\to X$ weakly, and there is an integrable function
$Y:\Omega\rightarrow\mathbb{R}$ such that $|X_{n}|\leq Y$ for all $n$ (i.e.
$\mathbb{P}(Y-|X_{n}|\geq 0)=1$) and that $\mathbb{E}|Y|<\infty$. Then $X_{n}$
converges effectively under the metric (10). In particular, the limit of
$\mathbb{E}(X_{n})$ always exists

###### Proof.

Since $\mathbb{E}(Y)<\infty$, the probabilities $\mathbb{P}(Y\geq y)\to 0$ as
$y\to\infty$. For fixed $\epsilon>0$, let
$b(\epsilon)=\sup\\{y\mid\mathbb{P}(Y\geq y)\geq\epsilon$, which is computable
in $\mathbb{R}_{>}$ given $\epsilon$. Then $\sup\\{\int_{A}YdP\mid
P(A)\leq\epsilon\\}\leq\int_{b(\epsilon)}^{\infty}\mathbb{P}(Y\geq
y)dy=\mathbb{E}(Y)-\int_{0}^{b(\epsilon)}\mathbb{P}(Y>y)dy$ in
$\mathbb{R}^{+}_{>}$. For continuous random variables $X_{m}$, $X_{n}$ with
$2^{-m},2^{-n}<\epsilon$, taking $A_{\epsilon}=\\{\omega\mid
d(X_{m}(\omega),X_{n}(\omega))\geq\epsilon\\}$ gives
$\mathbb{E}(|X_{m}-X_{n}|)\leq\epsilon+\int_{A_{\epsilon}}|X_{m}(\omega)-X_{n}(\omega)|\,dP(\omega)\leq\epsilon+\int_{A_{\epsilon}}|X_{m}(\omega)|+|X_{n}(\omega)|dP(\omega)\leq\epsilon+\int_{A_{\epsilon}}2|Y|dP\leq\epsilon+2\int_{b(\epsilon)}^{\infty}\mathbb{P}(Y\geq
y)dy,$ which converges effectively to $0$ as $\epsilon\to 0$. ∎

##  7 Conditioning

The concept of conditional random variable is subtle even in classical
probability theory. The basic idea is that if we condition a random quantity
$Y$ on some information of kind $\mathcal{X}$, then we can reconstruct $Y$
given a value $x$ describable by $\mathcal{X}$. Classically, conditional
_random variables_ are _not_ defined, but conditional distributions and
expectations are. Conditional expectations can be shown to exist using the
Radon-Nikodym derivative, but this is uncomputable [HRW11].

###  7.1 Independence

In the classical case, we condition relative to a sub-sigma-algebra of the
measure space. In the computable case, it makes sense to consider instead a
sub-topology $\mathcal{T}$ on $\Omega$. We first need to define concepts of
$\mathcal{T}$ measurability and $\mathcal{T}$ independence

######  Definition 70 (Measure-topologies).

Let $\nu$ be a valuation on $\mathbb{X}$. A _$\nu$ -topology_ is a collection
of $\nu$-lower-measurable sets which contains $\emptyset,\mathbb{X}$ and is
closed under intersection and countable union.

The $P$-topology _generated_ by a random variable
$X:\Omega\rightsquigarrow\mathbb{X}$ is simply $\\{X^{-1}(U)\mid
U\in\mathcal{O}(\mathbb{X})\\}$. A random variable $X$ is
$\mathcal{T}$-measurable if $X^{-1}(U)\in\mathcal{T}$ for all
$U\in\mathcal{O}(\mathbb{X})$

We write $\mathcal{R}_{\mathcal{T}}(\mathbb{X})$ for the type of
$\mathcal{T}$-measurable random variables with values in $\mathbb{X}$.

Note that a $\nu$-topology is not a topology on $\mathbb{X}$ in the standard
sense, since it consists of equivalence-classes of subsets of $\mathbb{X}$,
rather than sets themselves.

Recall that classically, we say random variables $X_{1},X_{2}$ taking values
in $\mathbb{X}_{1}$, $\mathbb{X}_{2}$ are independent if for all open
$U_{1}\subset\mathbb{X}_{1}$ and $U_{2}\subset\mathbb{X}_{2}$, we have
$\mathbb{P}(X_{1}\in U_{1}\wedge X_{2}\in U_{2})=\mathbb{P}(X_{1}\in
U_{1})\cdot\mathbb{P}(X_{2}\in U_{2}).$ This classical definition does not
relate well with computability theory, as the following example shows:

######  Example 71.

Consider the result $X$ of throwing a $6$-sided die, and the random variables
$X_{\mathrm{even}}$ which is $1$ if $X$ is even and $0$ otherwise, and
$X_{\mathrm{high}}$ which is $1$ is $X$ is a 5 or 6. Then $X_{\mathrm{even}}$
and $X_{\mathrm{high}}$ are independent for a fair die, but not if the
probability of a 6 is $\tfrac{1}{6}+5\epsilon$ and of a 1 to 5 is
$\tfrac{1}{6}-\epsilon$ for $\epsilon\neq 0$.

It is therefore useful to consider different versions of independence
properties.

######  Definition 72 (Independence).

$P$-topologies $\mathcal{T}_{1,2}$ on $\Omega$ are _independent_ if
$P(U_{1}\cap U_{2})=P(U_{1})P(U_{2})$ for all $U_{1}\in\mathcal{T}_{1}$,
$U_{2}\in\mathcal{T}_{2}$.

$P$-topologies $\mathcal{T}_{1,2}$ are _strongly independent_ if we can write
$\Omega=\Omega_{1}\times\Omega_{2}$, with projections $p_{1,2}$ and inclusion
$q:\Omega_{1}\times\Omega_{2}\to\Omega$ such that
$q(p_{1}(U_{1}),\omega_{2})=U_{1}$ for all $U_{i}\in\mathcal{T}_{i}$, there
exists $V_{i}\subset\Omega_{i}$ such that $U_{i}=p_{i}^{-1}(V_{i})$ for
$i=1,2$.

Random variables $X_{1,2}:\Omega\rightsquigarrow\mathbb{X}_{1,2}$ are
_effectively independent_ if
$X_{1}:\mathcal{R}_{\mathcal{T}_{1}}(\mathbb{X}_{1})$ and
$X_{2}:\mathcal{R}_{\mathcal{T}_{2}}(\mathbb{X}_{2})$ for independent
topologies $\mathcal{T}_{1,2}$.

Random variables $X_{1},\ldots,X_{k}$ are _jointly_ independent of
$\mathcal{T}$ if the product $\prod_{i=1}^{k}X_{i}$ is independent of
$\mathcal{T}$, and $X_{1},X_{2},\ldots$ are jointly independent of
$\mathcal{T}$ if every finite product is independent of $\mathcal{T}$.

A random variable $X$ is _effectively independent_ of a topology $\mathcal{T}$
on $\Omega$ if $X:\mathcal{R}_{\mathcal{X}}(\mathbb{X}_{1})$ for some topology
$\mathcal{X}$ independent of $\mathcal{T}$.

We can express independence relative to sub-topologies using the identity
random variable $I:\Omega\rightarrow\Omega$. If
$X:\Omega\rightsquigarrow\mathbb{X}$ is independent of $\mathcal{T}$, then
$\mathbb{P}(X\times I\in U\times W)=\mathbb{P}(X\in U)P(W)$ whenever
$U\in\mathcal{O}(\mathbb{X})$ and $W\in\mathcal{T}$. We write
$\mathcal{R}_{\perp\mathcal{T}}(\mathbb{X})$ for $\mathcal{T}$-independent
random variable with values in $\mathbb{X}$. Note that
$\mathcal{R}_{\perp\mathcal{T}}(\mathbb{X})$ does not form a natural type,
since it is possible for $X_{1}$, $X_{2}$ to be independent of $\mathcal{T}$,
but $X_{1}\times X_{2}$ not to be. If $X$ is effectively independent of
$\mathcal{T}$, and $Y$ is $\mathcal{T}$-measurable, then $X$ is effectively
independent of $Y$.

###  7.2 Conditional Random Variables

We now proceed to our notion of conditional random variable $Y|\mathcal{X}$,
where $\mathcal{X}$ is a measure-topology on $\Omega$. Recall that
classically, the conditional expectation $\mathbb{E}(Y|\mathcal{X})$ for a
random variable $Y$ is a $\mathcal{X}$-measurable random variable.

######  Definition 73 (Conditional random variable).

Let $\mathcal{X}$ be a measure-topology. A $\mathcal{X}$-independent
conditional random variable is a function
$Y|:\mathbb{X}\to\mathcal{R}(\mathbb{Y})$ such that the $Y|x$ are jointly-
independent of $\mathcal{X}$.

If $Y|:\mathbb{X}\to\mathcal{R}(\mathbb{Y})$ is $\mathcal{X}$-independent, and
$X:\mathcal{R}(\mathbb{X})$ is simple and $\mathcal{X}$-measurable, then we
can define the _joint random variable_

######  Definition 74 (Joint random variable).

The _joint random variable_ of $X\rtimes Y|$ of a $\mathcal{X}$-measurable
simple random variable $X:\mathcal{R}(\mathbb{X})$ and a
$\mathcal{X}$-independent conditional random variable
$Y|:\mathbb{X}\to\mathcal{R}(\mathbb{Y})$ is defined by

$\textstyle(X\rtimes Y|)^{-1}(U\times V)=\bigcup_{x_{i}\in
U}X^{-1}(x_{i})\cap(Y|x_{i})^{-1}(V).$ (13)

The _joint random variable_ of a $\mathcal{X}$-measurable random variable
$X:\mathcal{R}(\mathbb{X})$ and a $\mathcal{X}$-independent conditional random
variable $Y|:\mathbb{X}\to\mathcal{R}(\mathbb{Y})$ is defined to be
$\lim_{n\to\infty}X_{n}\rtimes Y|$, where $X_{n}$ is a sequence of
$\mathcal{X}$-measurable simple random variables converging to $\mathcal{X}$.

Note that if $X$ is a simple random variable,

$\textstyle\mathcal{P}\bigl{(}\bigcup_{x_{i}\in
U}X^{-1}(x_{i})\cap(Y|x_{i})^{-1}(V)\bigr{)}=\sum_{x_{i}\in
U}\mathbb{P}(X=x_{i})\times\mathbb{P}(Y|x_{i}\in V).$

To show Definition 74 makes sense in the general case, we need to show that it
is independent of the sequence of simple random variables used to specify $X$.

######  Lemma 75.

Let $X$ be a $\mathcal{X}$-measurable random variable in a metric space
$\mathbb{X}$. Then we can construct a sequence of $\mathcal{X}$-measurable
simple continuous random variables converging effectively to $X$.

###### Proof.

Let $r_{n}:U_{n}\to\mathbb{X}$ be a finite-valued map defined on an open set
$U_{n}$ with $\mathbb{P}(X\in U_{n})=1$ such that $d(r_{n}(x),x)<2^{-n}$ for
all $n$, as guaranteed by Lemma 56. Take $X_{n}=r_{n+1}\circ X$, which is
$\mathcal{X}$-measurable since $X$ is. Then $(X_{n})$ is sequence of random
variables with $d(X_{n},X)\leq 2^{-(n+1)}$, and $d(X_{n_{1}},X_{n_{2}})\leq
2^{-\min(n_{1},n_{2})}$ as required. ∎

######  Theorem 76.

The joint random variable of a $\mathcal{X}$-measurable random variable
$X:\mathcal{R}(\mathbb{X})$ and a $\mathcal{X}$-independent conditional random
variable $Y|:\mathbb{X}\to\mathcal{R}(\mathbb{Y})$ is independent of the
sequence of simple approximations $X_{n}$ to $X$ used in the definition, so is
computable.

###### Proof.

Define the continuity sets

$C_{\delta,\epsilon}=\\{x\in\mathbb{X}\mid\forall\tilde{x}\in\mathbb{X},\
d(x,\tilde{x})\leq\delta\implies d_{F}(Y|x,Y|\tilde{x})<\epsilon\\}.$

Note that every $C_{\delta,\epsilon}$ is open, and for any fixed $\epsilon$,
continuity of $Y|:\mathbb{X}\rightarrow\mathcal{R}(\mathbb{Y})$ implies
$\bigcup_{\delta>0}C_{\delta,\epsilon}=\mathbb{X}$. Hence for fixed $\epsilon$
and some $\delta<\epsilon/8$ sufficiently small, $\mathbb{P}(X\in
C_{\delta,\epsilon/4})>1-\epsilon/4$.

Now suppose that $X_{1},X_{2}$ are simple $\mathcal{X}$-measurable random
variables such that $\mathbb{P}(d(X,X_{i})<\delta)>1-\epsilon/8$. Let

$U=\\{(x,x_{1},x_{2})\mid x\in C_{\delta,\epsilon/4}\wedge
d(x,x_{1})<\delta\wedge d(x,x_{2})<\delta\\},$

and

$V=\\{(x_{1},x_{2})\mid d(Y|x_{1},Y|x_{2})<\epsilon/2\wedge
d(x,x_{1})<\delta\wedge d(x,x_{2})<\delta\\}.$

Then $(x,x_{1},x_{2})\in U\implies(x_{1},x_{2})\in V$, so

$\mathbb{P}(X_{1}\\!\times\\!X_{2}\in
V)\geq\mathbb{P}(X\\!\times\\!X_{1}\\!\times\\!X_{2}\in U)\geq
1-\epsilon/4-\epsilon/8-\epsilon/8=1-\epsilon/2.$

Since each $Y|x$ is $\mathcal{X}$-independent,

$\displaystyle\textstyle\mathbb{P}(d(Y|X_{1},Y|X_{2})>\epsilon/2)$
$\displaystyle\qquad\textstyle=\sum_{x_{1},x_{2}}\mathbb{P}(X_{1}=x_{1}\wedge
X_{2}=x_{2})\mathbb{P}(d(Y|x_{1},Y|x_{2})>\epsilon/2)$
$\displaystyle\qquad\textstyle\leq\sum_{(x_{1},x_{2})\in
V}\mathbb{P}(X_{1}=x_{1}\wedge X_{2}=x_{2})\times\epsilon/2$
$\displaystyle\qquad\qquad\qquad\textstyle+\sum_{(x_{1},x_{2})\not\in
V}\mathbb{P}(X_{1}=x_{1}\wedge X_{2}=x_{2})\times 1$
$\displaystyle\qquad\qquad\textstyle=\mathbb{P}(X_{1}\\!\times\\!X_{2}\in
V)\times\epsilon/2+(1-\mathbb{P}(X_{1}\\!\times\\!X_{2}\in V))\times 1$
$\displaystyle\qquad\qquad\textstyle\leq\epsilon/2+\epsilon/2=\epsilon.$

Hence if $d_{F}(X,X_{1}),d_{F}(X,X_{2})<\delta$, we have
$d_{F}(Y|X_{1},Y|X_{2})<\epsilon$. ∎

###  7.3 Random functions

In the definition of conditional random variable, we use objects of type
$\mathbb{X}\rightarrow\mathcal{R}(\mathbb{Y})$, which are random-variable-
valued functions, rather than _random functions_ with type
$\mathcal{R}(\mathbb{X}\rightarrow\mathbb{Y})$, alternatively written
$\mathcal{R}(\mathcal{C}(\mathbb{X};\mathbb{Y}))$.

Given a random function $F:\mathcal{R}\bigl{(}\mathbb{X}\to\mathbb{Y}\bigr{)}$
and a random variable $X:\mathcal{R}(\mathbb{X})$, since the evaluation map
$\varepsilon:(\mathbb{X}\to\mathbb{Y})\times\mathbb{X}\to\mathbb{Y}$ is
computable, we can apply it to $F$ and $X$ to obtain a random variable
$Y=\varepsilon(F,X):\mathcal{R}(\mathbb{Y})$.

The information provided by a random function
$\mathcal{R}(\mathbb{X}\to\mathbb{Y})$ is strictly stronger than that provided
by a function $\mathbb{X}\to\mathcal{R}(\mathbb{Y})$:

######  Proposition 77 (Random function).

The natural bijection
$\mathcal{R}(\mathbb{X}\rightarrow\mathbb{Y})\hookrightarrow(\mathbb{X}\rightarrow\mathcal{R}(\mathbb{Y}))$
is computable, but its inverse is not continuous.

###### Proof.

For fixed $x$, evaluation
$\varepsilon_{x}:(\mathbb{X}\rightarrow\mathbb{Y})\rightarrow\mathbb{Y}:f\mapsto
f(x)$ is computable, so by Theorem 49,
$\varepsilon(F):\mathcal{R}(\mathbb{Y})$ is computable for any
$F:\mathcal{R}(\mathbb{X}\rightarrow\mathbb{Y})$ given $x$. Hence the function
$x\mapsto\varepsilon_{x}(F)$ is computable.

Conversely, let $X=\\{0,1\\}^{\omega}$ and $Y=\\{0,1\\}$. Define
$F(x,\omega,n)=1$ if $x|_{n}=\omega|_{n}$, and $0$ otherwise. Then for fixed
$x$, $F(d(x,\cdot,n),0)=2^{-n}$, so $F(x,\cdot,n)$ converges to $0$ uniformly
in $x$.

For fixed $\omega$, $d(F(\cdot,\omega,n_{1}),F(\cdot,\omega,n_{2}))=\sup_{x\in
X}d(F(x,\omega,n_{1}),F(x,\omega,n_{2}))=1$, since (for $n_{1}<n_{2}$) there
exists $x$ such that $x|_{n_{1}}=\omega|_{n_{1}}$ but
$x|_{n_{2}}\neq\omega|_{n_{2}}$. Hence
$d(F(\cdot,\cdot,n_{1}),F(\cdot,\cdot,n_{2}))=1$ for all $n_{1},n_{2}$, and
the sequence is not a Cauchy sequence in
$\mathcal{R}(\mathbb{X}\rightarrow\mathbb{Y})$. ∎

However, if $Y|:\mathbb{X}\to\mathcal{R}(\mathbb{Y})$ is such that each $Y|x$
is a continuous random variable i.e. a continuous function
$\Omega\to\mathbb{Y}$, then $Y|$ corresponds to a continuous random function
$F$ by $[F(\omega)](x)=Y|x(\omega)$, and $Y|X$ is the random variable
$\varepsilon(F,X)$.

##  8 Conclusions

In this paper, we have developed a theory of probability and random variables.
The theory uses type-two effectivity to provide an underlying machine model of
computation, but is largely developed using type theory in the cartesian-
closed category of quotients of countably-based spaces, which has an effective
interpretation. The approach extends existing work on probability via
valuations and random variables in metric spaces via limits of Cauchy
sequences.

The approach has been used to give a computable theory for stochastic
processes which is sufficiently powerful to effectively compute the solution
of stochastic differential equations [Col14]. Ultimately, we hope that this
work will form a basic for practical software tools for the rigorous
computational analysis of stochastic systems.

Acknowledgement: The author would like to thank Bas Spitters for many
interesting discussions on measurable functions and type theory, and pointing
out the connection with monads.

## References

  * [AM02] Mauricio Alvarez-Manilla.  Extension of valuations on locally compact sober spaces.  Topology Appl., 124:397–433, 2002.
  * [BB85] Errett Bishop and Douglas Bridges.  Constructive analysis, volume 279 of Grundlehren der Mathematischen Wissenschaften.  Springer, 1985.
  * [BC72] Errett Bishop and Henry Cheng.  Constructive measure theory.  American Mathematical Society, 1972.
  * [Bra01] Vasco Brattka.  Computable versions of Baire’s category theorem.  In Proc. 26th International Symposium on Mathematical Foundations of Computer Science, pages 224–235. Springer, 2001.
  * [Bra05] Vasco Brattka.  Effective Borel measurability and reducibility of functions.  Math. Logic Quarterly, 51:19–44, 2005.
  * [Cha74] Y. K. Chan.  Notes on constructive probability theory.  Ann. Probability, 2(1):51–75, 1974.
  * [Col14] Pieter Collins.  Computable stochastic processes.  Technical report, 2014.  arXiv:1409.4667.
  * [CP02] Thierry Coquand and Erik Palmgren.  Metric boolean algebras and constructive measure theory.  Archive for Mathematical Logic, 41(7):687–704, 2002.
  * [CS09] Thierry Coquand and Bas Spitters.  Integrals and valuations.  J. Logic Analysis, 1(3):1–22, 2009.
  * [Eda95a] Abbas Edalat.  Domain theory and integration.  Theor. Comput. Sci., 151:163–193, November 1995.
  * [Eda95b] Abbas Edalat.  Dynamical systems, measures, and fractals via domain theory.  Inf. Comput., 120:32–48, July 1995.
  * [Esc09] Martín Escardó.  Semi-decidability of may, must and probabilistic testing in a higher-type setting.  Electron. Notes Theor. Comput. Sci., 249:219–242, August 2009.
  * [GL05] Jean Goubault-Larrecq.  Extensions of valuations.  Mathematical. Structures in Comp. Sci., 15:271–297, April 2005\.
  * [GLV11] Jean Goubault-Larrecq and Daniele Varacca.  Continuous random variables.  In Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pages 97–106, Washington, DC, USA, 2011.
  * [HR09] Mathieu Hoyrup and Cristóbal Rojas.  Computability of probability measures and Martin-Löf randomness over metric spaces.  Information and Computation, 207:830–847, 2009.
  * [HRW11] Mathieu Hoyrup, Cristóbal Rojas, and Klaus Weihrauch.  Computability of the radon-nikodym derivative.  In Benedikt Löwe, Dag Normann, Ivan Soskov, and Alexandra Soskova, editors, Models of Computation in Context, volume 6735 of Lecture Notes in Computer Science, pages 132–141. Springer, 2011.
  * [JP89] C. Jones and G. Plotkin.  A probabilistic powerdomain of evaluations.  In Proceedings of the Fourth Annual Symposium on Logic in computer science, pages 186–195, Piscataway, NJ, USA, 1989.
  * [Ker08] Götz Kersting.  Random vaiables — without basic space.  In J. Blath, P. Mörters, and M. Scheutzow, editors, Trends in Stochastic Analysis. Cambridge University Press, 2008.
  * [Kön97] H. König.  Measure and Integration.  Springer-Verlag, 1997.
  * [Law04] Jimmie D. Lawson.  Domains, integration and ‘positive analysis’.  Mathematical. Structures in Comp. Sci., 14:815–832, December 2004\.
  * [Mis07] Michael Mislove.  Discrete random variables over domains.  Theor. Comput. Sci., 380:181–198, July 2007.
  * [MW43] H.B. Mann and A. Wald.  On stochastic limit and order relationships.  Ann. Math. Statistics, 14(3):217–226, 1943.
  * [Pol02] David Pollard.  A User’s Guide to Measure Theoretic Probability.  Cambridge Series in Statistical and Probabilistic Mathematics. 2002.
  * [Roh52] V. A. Rohlin.  On the fundamental ideas of measure theory, volume 71 of Translations.  American Mathematical Society, 1952.  Translated from Russian.
  * [Sch04] Jean Schmets.  Théorie de la mesure.  Notes de cours, Université de Liège, 2004.
  * [Sch07] Matthias Schröder.  Admissible representations of probability measures.  Electron. Notes Theor. Comput. Sci., 167:61–78, January 2007.
  * [Sch09] Matthias Schröder.  An effective Tietze-Urysohn theorem for QCB-spaces.  J. Univers. Comput. Sci., 15(6):1317–1336, 2009.
  * [Shi95] Al’bert Nikolaevich Shiryaev.  Probability.  Springer, 1995.
  * [Spi06] Bas Spitters.  Constructive algebraic integration theory.  Ann. Pure Appl. Logic, 137(1-3):380–390, 2006.
  * [SS06a] Matthias Schröder and Alex Simpson.  Probabilistic observations and valuations.  Electron. Notes Theor. Comput. Sci., 155:605–615, May 2006.
  * [SS06b] Matthias Schröder and Alex Simpson.  Representing probability measures using probabilistic processes.  J. Complexity, 22(6):768 – 782, 2006.  Computability and Complexity in Analysis.
  * [Str72] Ross Street.  The formal theory of monads.  J. Pure Appl. Math., 2:149–168, 1972.
  * [Tix95] R. Tix.  Stetige Bewertungen auf topologischen Räumen.  PhD thesis, Master’s Thesis, Technische Universität Darmstadt, 1995\.
  * [Var02] Daniele Varacca.  The powerdomain of indexed valuations.  In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 299–, Washington, DC, USA, 2002.
  * [vG02] Onno van Gaans.  Probability measures on metric spaces.  2002\.
  * [Vic08] Steven Vickers.  A localic theory of lower and upper integrals.  Math. Log. Quart., 54(1):109–123, 2008.
  * [Vic11] Steven Vickers.  A monad of valuation locales.  http://www.cs.bham.ac.uk/~sjv/Riesz.pdf, 2011.
  * [WD05] Yongcheng Wu and Decheng Ding.  Computability of measurable sets via effective metrics.  Mathematical Logic Quarterly, 51(6):543–559, 2005.
  * [WD06] Yongcheng Wu and Decheng Ding.  Computability of measurable sets via effective topologies.  Archive for Mathematical Logic, 45(3):365–379, 2006.
  * [Wei99] Klaus Weihrauch.  Computability on the probability measures on the Borel sets of the unit interval.  Theor. Comput. Sci., 219:421–437, May 1999.
  * [YMT99] M. Yasugi, T. Mori, and Y. Tsujii.  Effective properties of sets and functions in metric spaces with computability structure.  Theor. Comput. Sci., 219(1-2):467–486, 1999.