Continuous Probabilistic Languages and Quasi-Borel Semantics

Proof. Let $\mathcal{H}=\bigcup \{\sigma ({\mathcal{G}}_0)\mid {\mathcal{G}}_0\subseteq \mathcal{G}\text{ countable}\}$. Then $\mathcal{G}\subseteq \mathcal{H}$, and $\mathcal{H}$ is a $\sigma$-algebra: it contains $Z$; it is closed under complement, since $\sigma ({\mathcal{G}}_0)$ is; and if $A_n\in \sigma ({\mathcal{G}}_{0,n})$ for each $n$, then $\bigcup _n{A}_n\in \sigma (\bigcup _n{\mathcal{G}}_{0,n})$, a countable union of countable families. Hence $\sigma (\mathcal{G})\subseteq \mathcal{H}$. The second claim is the first applied to the generating family of rectangles, followed by collecting the countably many first components that occur. ◻

Proof. Suppose it were. Then lies in ${\mathrm{\Sigma }}_{\mathrm{ev}}\otimes \mathcal{B}(\mathbb{R})$, so by lemma 174.2 there is a countable $\mathcal{C}\subseteq {\mathrm{\Sigma }}_{\mathrm{ev}}$ with $E\in \sigma (\{C\times B\mid C\in \mathcal{C},B\in \mathcal{B}(\mathbb{R})\})$. Applying lemma 174.2 once more to each $C\in \mathcal{C}$, which lies in the $\sigma$-algebra generated by point evaluations, produces a countable set $R_0\subseteq \mathbb{R}$ such that every $C\in \mathcal{C}$ lies in $\sigma (\{\{f\mid f(r)\in B\}\mid r\in R_0,B\text{ Borel}\})$.

Two functions agreeing on $R_0$ therefore lie in exactly the same members of $\mathcal{C}$, hence in the same members of the generated $\sigma$-algebra; so for such $f,g$ and every $r$, $(f,r)\in E$ if and only if $(g,r)\in E$. Now let $r_1\notin R_0$, which exists because $R_0$ is countable, and take $f=0$ and $g=1_{\{r_1\}}$. Both are Borel measurable and agree on $R_0$, yet $(f,r_1)\notin E$ while $(g,r_1)\in E$. ◻

Proof. Each clause of definition 174.6 is checked coordinatewise: for (i), ${\pi }_i\circ (f\circ g)=({\pi }_i\circ f)\circ g\in M_{X_i}$; for (ii), a constant into the product is coordinatewise constant; for (iii), the glued function has ${\pi }_i\circ \beta$ equal to the gluing of ${\pi }_i\circ {\alpha }_j$, which lies in $M_{X_i}$. The projections are morphisms by the definition of $M_{\prod _i{X}_i}$. For the universal property, given morphisms $g_i:Z\to X_i$, the pairing $⟨g_i{⟩}_i$ satisfies ${\pi }_i\circ ⟨g_i{⟩}_i\circ \gamma =g_i\circ \gamma \in M_{X_i}$ for $\gamma \in M_Z$, so it is a morphism, and it is the unique such function. ◻

Proof. Clause (i): precomposing with a measurable $g$ replaces $f$ by $f\circ g$ and ${\alpha }_i$ by ${\alpha }_i\circ g$. Clause (ii): a constant is obtained with constant $f$. Clause (iii): given a Borel partition $\mathbb{R}=\underset{j}{⨄}{S}_j$ and elements ${\beta }_j$ of the displayed form with data $(f_j,{\alpha }_i^j)$, define $f$ by $f(r)=f_j(r)$ for $r\in S_j$, measurable since $I$ is countable and discrete, and define ${\alpha }_i$ by gluing the ${\alpha }_i^j$ over the partition, which lies in $M_{X_i}$ by clause (iii) for $X_i$. For the universal property, let $g_i:X_i\to Z$ be morphisms and let $\gamma =\lambda r.(f(r),{\alpha }_{f(r)}(r))$ be a random element of the coproduct. Then $[g_i{]}_i\circ \gamma$ is the gluing over the Borel partition $\mathbb{R}=\underset{i}{⨄}{f}^{-1}(\{i\})$ of the maps $g_i\circ {\alpha }_i\in M_Z$, hence lies in $M_Z$ by clause (iii) for $Z$. This is the step for which clause (iii) exists. ◻

Proof. Here $\mathbb{R}$ carries $M_{\mathbb{R}}^{\mathrm{\Sigma }}$, the measurable functions $\mathbb{R}\to \mathbb{R}$, and $\mathbb{R}\times X$ the product structure of proposition 174.8.

Clause (i). If $\mathrm{uncurry}(\alpha )$ is a morphism and $g:\mathbb{R}\to \mathbb{R}$ is measurable, then $\mathrm{uncurry}(\alpha \circ g)=\mathrm{uncurry}(\alpha )\circ (g\times \mathrm{id})$, a composite of morphisms.

Clause (ii). For a constant $\alpha =\lambda r.h$ with $h$ a morphism, the uncurried map sends $(r,x)$ to $h(x)$, so it sends a random element of $\mathbb{R}\times X$ with second component $\chi$ to $h\circ \chi$, which lies in $M_Y$.

Clause (iii). Let $\mathbb{R}=\underset{i}{⨄}{S}_i$ be Borel and ${\alpha }_i\in M_{Y^X}$, and let $\beta$ glue them. Let $⟨\rho ,\chi ⟩\in M_{\mathbb{R}\times X}$. Then each of which lies in $M_Y$; the partition is Borel because $\rho$ is measurable, so clause (iii) for $Y$ gives $\mathrm{uncurry}(\beta )\circ ⟨\rho ,\chi ⟩\in M_Y$. This is where the countable gluing of proposition 174.9 is used in disguise.

Evaluation and the universal property. Let $⟨\alpha ,\chi ⟩\in M_{Y^X\times X}$. Then $\mathrm{ev}\circ ⟨\alpha ,\chi ⟩=\mathrm{uncurry}(\alpha )\circ ⟨\mathrm{id},\chi ⟩\in M_Y$, so $\mathrm{ev}$ is a morphism. For $h:Z\times X\to Y$ a morphism, its curry $\mathrm{\Lambda }h:Z\to Y^X$ satisfies, for $\gamma \in M_Z$, $\mathrm{uncurry}(\mathrm{\Lambda }h\circ \gamma )=h\circ (\gamma \times \mathrm{id})$, a morphism; so $\mathrm{\Lambda }h$ is a morphism, and it is the unique function with $\mathrm{ev}\circ (\mathrm{\Lambda }h\times \mathrm{id})=h$. ◻

Proof. Clause (i): if $\beta (r)=[\alpha ,g(r)]$ and $f$ is measurable, then $\beta (f(r))=[\alpha ,(g\circ f)(r)]$ and $g\circ f$ is a kernel by proposition 172.18 applied to $\mathrm{ret}$ composed with $f$, or directly because $r\mapsto g(f(r))(A)$ is a composite of measurable maps. Clause (ii): a constant $[\alpha ,\mu ]$ is obtained with the constant kernel $g(r)=\mu$. Clause (iii): let $\mathbb{R}=\underset{i}{⨄}{S}_i$ be Borel with ${\beta }_i(r)=[{\alpha }_i,g_i(r)]$. Choose a Borel partition $\mathbb{R}=\underset{i}{⨄}{T}_i$ into uncountable Borel pieces together with Borel isomorphisms ${\phi }_i:\mathbb{R}\to T_i$, and let ${\psi }_i:\mathbb{R}\to \mathbb{R}$ be a measurable map restricting to ${\phi }_i^{-1}$ on $T_i$. Each ${\alpha }_i\circ {\psi }_i$ lies in $M_X$ by clause (i), so their gluing $\alpha$ along $(T_i{)}_i$ lies in $M_X$ by clause (iii) for $X$, and $\alpha \circ {\phi }_i={\alpha }_i$. Setting $g(r)=({\phi }_i{)}_{\ast }{g}_i(r)$ for $r\in S_i$ defines a kernel, and $${\alpha }_{\ast }g(r)={\alpha }_{\ast }({\phi }_i{)}_{\ast }{g}_i(r)\stackrel{lemma172.11}{=}(\alpha \circ {\phi }_i{)}_{\ast }{g}_i(r)=({\alpha }_i{)}_{\ast }{g}_i(r),$$ so $[\alpha ,g(r)]=[{\alpha }_i,g_i(r)]={\beta }_i(r)$ for $r\in S_i$. ◻

Proof. Compute the underlying measure of the right-hand side. For $U\in {\mathrm{\Sigma }}_{M_Y}$, So the underlying measure of $[\beta ,\mu \gg =g]$ equals the displayed right-hand side, which mentions neither $(\beta ,g)$ nor the representative $\alpha$ except through ${\alpha }_{\ast }\mu$. Since the equivalence of definition 174.12 is exactly equality of underlying measures, the class is determined. ◻

Proof. By lemma 174.15 the underlying measure of each side may be computed, and two elements of $P(X)$ with the same underlying measure are equal by definition 174.12. Transporting the three equations through $l$ turns them into the three equations of theorem 172.20 for the kernels $x\mapsto l_Y(f(x))$ and $y\mapsto l_Z(h(y))$, with $l_X(\eta (x))={\delta }_x$. For the functorial action, $l_Y(P(g)[\alpha ,\mu ])=(g\circ \alpha {)}_{\ast }\mu =g_{\ast }({\alpha }_{\ast }\mu )$ by lemma 172.11, which is the pushforward of the underlying measure, and this coincides with $[\alpha ,\mu ]\gg =(\eta \circ g)$ by lemma 172.22. Strength is the statement that $\gg =$ is itself a morphism $P(Y{)}^X\to P(Y{)}^{P(X)}$; by proposition 174.10 this amounts to the joint claim that $(\alpha ,f)\mapsto [\alpha ,\mu ]\gg =f$ sends random elements to random elements, which the construction of $(\beta ,g)$ in definition 174.14 produces uniformly in a random element of the function space. ◻

Proof. Write $p=[\alpha ,\mu ]$, $q=[\gamma ,\nu ]$, and apply $l_Z$ to both sides. By lemma 174.15 and theorem 172.14, the left-hand side becomes $$\int \int l_Z(f(\alpha (r),\gamma (s)))(U)d\nu (s)d\mu (r),$$ and the right-hand side is the same double integral in the opposite order. The integrand is nonnegative and jointly measurable, because $f$ is a morphism and the pair of projections composed with $\alpha$ and $\gamma$ is a random element of $X\times Y$. Both $\mu$ and $\nu$ are probability measures, hence $\sigma$-finite, so Tonelli’s theorem exchanges the two integrations by convention 172.12. ◻