Dependencies

The category of quasi-Borel spaces is cartesian closed.

Given a standard Borel space \(M\) with encoding \(f : M \to \mathbb {R}\) and decoding \(g : \mathbb {R} \to M\), and a probability \(P\) on \(\mathbb {R}\), the QBS probability \((\mathrm{id}, P)\) on \(R(M)\) represents \(P\).

\(\mathrm{bin\_ digit}(x, n)\) extracts the \(n\)-th binary digit of \(x \in [0,1)\) via the doubling map. \(\mathrm{bin\_ partial\_ sum}(d, n) = \sum _{i{\lt}n} d(i) \cdot 2^{-(i+1)}\) and \(\mathrm{bin\_ sum}(d) = \lim _n \mathrm{bin\_ partial\_ sum}(d, n)\).

\(\mathtt{realQ} = R(m\mathbb {R})\), \(\mathtt{natQ} = R(\mathbb {N})\), \(\mathtt{boolQ} = R(\mathbb {B})\).

Every QBS probability \(p\) on a standard Borel space induces a constant kernel: \(x \mapsto \texttt{qbs\_ to\_ giry}(p)\).

The coproduct \(X + Y\) has random elements that factor through \(\mathrm{inl}\), through \(\mathrm{inr}\), or through a measurable boolean predicate switching between the two.

\(\mathrm{encode}(x, y) = \psi (\mathrm{pair\_ to\_ unit}(\phi (x), \phi (y)))\) and \(\mathrm{decode}(r) = (\psi (u_1), \psi (u_2))\) where \((u_1, u_2) = \mathrm{unit\_ to\_ pair}(\phi (r))\).

\(Z = \int \! \! \int \mathrm{obs}(s, b)\, d\pi (s)\, d\pi (b)\) where \(\pi = \mathcal{N}(0, 3)\).

The exponential \(X \Rightarrow Y\) has carrier the set of QBS morphisms \(X \to Y\), with a function \(g : \mathbb {R} \to (X \to Y)\) random iff the uncurried map \((r, x) \mapsto g(r)(x)\) is a QBS morphism \(\mathbb {R} \times X \to Y\).

Closed-form expressions for the combined mean, standard deviation, and scalar factor from the product of two Gaussians.

For a measurable index type \(I\) and a family \(X : I \to \mathbf{QBS}\), the general coproduct \(\coprod _{i:I} X_i\) has carrier \(\{ i : I ~ \& ~ X_i\} \) (dependent sum). A random element \(\alpha \) factors as \(\alpha (r) = (P(r), F_{P(r)}(r))\) for measurable \(P : \mathbb {R} \to I\) and family \(F_i \in M_{X_i}\).

Given a set \(G\) of functions \(\mathbb {R} \to T\), the generating QBS is the smallest QBS containing \(G\), constructed by inductive closure under composition, constants, and gluing.

For a probability \(P\) on a standard Borel \(M\), the QBS probability uses the standard Borel encoding/decoding.

\(\mathrm{interleave}(d_1, d_2)(n) = \begin{cases} d_1(n/2) & \text{if } n \text{ even} \\ d_2(n/2) & \text{if } n \text{ odd} \end{cases}\). Deinterleaving extracts even-indexed and odd-indexed subsequences.

A measurable space \(M\) is standard Borel if there exist measurable \(f : M \to \mathbb {R}\) and \(g : \mathbb {R} \to M\) with \(g \circ f = \mathrm{id}\).

A quasi-Borel space (QBS) over \(R\) is a type \(T\) equipped with a set \(M_X \subseteq (\mathbb {R} \to T)\) of random elements satisfying three axioms:

1. Composition (qbs_Mx_comp): If \(\alpha \in M_X\) and \(f : \texttt{\{ mfun mR {\gt}-{\gt} mR\} }\) (a bundled measurable function), then \(\alpha \circ f \in M_X\).

2. Constants (qbs_Mx_const): For every \(x : T\), the constant function \(\lambda r.\; x\) is in \(M_X\).

3. Gluing (qbs_Mx_glue): If \(P : \texttt{\{ mfun mR {\gt}-{\gt} nat\} }\) and \(F_i \in M_X\) for all \(i\), then \(\lambda r.\; F_{P(r)}(r) \in M_X\).

The HB structure QBSpace packages this mixin with a short type name qbsType R. All type constructions (prodQ, expQ, unitQ, etc.) use the Section + HB.instance Definition pattern recommended by mathcomp maintainers.

The functor \(L : \mathbf{QBS} \to \sigma \text{-}\mathbf{Alg}\) sends a QBS \(X\) to its induced sigma-algebra \(\sigma _{M_X}\).

For a QBS \(X\) with inhabitant \(x_0 : X\), the list QBS \(\mathrm{list}(X)\) has \(\alpha \) random iff there exist measurable \(\mathrm{len} : \mathbb {R} \to \mathbb {N}\) and random \(F_i \in M_X\) such that \(\alpha (r) = \mathrm{mkseq}(\lambda i.\; F_i(r), \mathrm{len}(r))\).

Given a QBS morphism \(f : X \to Y\), the image QBS \(\mathrm{im}(f)\) is \(\mathrm{gen}(\{ f \circ \alpha \mid \alpha \in M_X\} )\).

Every measurable function \(f : M_1 \to M_2\) induces a Dirac probability kernel \(x \mapsto \delta _{f(x)}\).

The probability monad \(P(X)\) is a QBS on qbs_prob X, with \(\beta : \mathbb {R} \to P(X)\) random iff for all \(r\), \(\alpha _{\beta (r)} \in M_X\).

For a QBS morphism \(f : X \to Y\), the functorial map \(P(f) : P(X) \to P(Y)\) sends \((\alpha , \mu )\) to \((f \circ \alpha , \mu )\).

A digit sequence \(d\) has no trailing ones if for every \(N\), there exists \(n \geq N\) with \(d(n) = \mathrm{false}\).

\(\mathrm{norm\_ qbs}(g, \mathrm{obs})\) returns \(\mathrm{Some}(d)\) if the evidence is positive and finite, \(\mathrm{None}\) otherwise.

Given \(p : P(X \times \mathbb {R})\) with weight function \(w(r) = \mathrm{snd}(\alpha _p(r)) \geq 0\) and evidence \(Z = \int w \, d\mu _p \in (0,+\infty )\), the normalized measure is \(\nu (A) = \int _A (w/Z) \, d\mu _p\). This is a probability measure (\(\nu (\Omega ) = 1\)).

Constructs \(q : P(X)\) with \(\alpha _q(r) = \mathrm{fst}(\alpha _p(r))\) and \(\mu _q = \nu \).

The observation likelihood for parameters \((s, b)\):

where \((y_1, \ldots , y_5) = (2.5, 3.8, 4.5, 6.2, 8.0)\).

\(\mathrm{pair\_ to\_ unit}(x, y) = \mathrm{bin\_ sum}(\mathrm{interleave}(\mathrm{bin\_ digits}(x), \mathrm{bin\_ digits}(y)))\). \(\mathrm{unit\_ to\_ pair}\) deinterleaves and reconstructs both components.

The final combined mean, standard deviation, and accumulated constant from all 10 Gaussian combination steps.

\(\phi (x) = \frac{\arctan x}{\pi } + \frac{1}{2}\) maps \(\mathbb {R} \to (0,1)\). \(\psi (y) = \tan (\pi (y - 1/2))\) is the inverse.

For a family \(X : I \to \mathbf{QBS}\), the dependent product \(\prod _{i:I} X_i\) has \(\alpha \) random iff for every \(i : I\), \(\lambda r.\; \alpha (r)(i) \in M_{X_i}\).

\(\mathbb {E}_{\mathrm{post}}[g] = \frac{\mathbb {E}_{\mathrm{prior}}[g \cdot \mathrm{obs}]}{Z}\).

The joint prior on \((s, b)\) is constructed via nested bind: \(\mathrm{prior} = \mathrm{slope\_ prior} \mathbin {{\gt}\! \! {\gt}\! \! =} (\lambda s.\; \mathrm{str}(s, \mathrm{intercept\_ prior}))\).

\(\mathrm{slope\_ prior} = \mathcal{N}(0, 3)\) and \(\mathrm{intercept\_ prior} = \mathcal{N}(0, 3)\).

The product \(X \times Y\) of two QBS has random elements \(M_{X \times Y} = \{ \alpha \mid \pi _1 \circ \alpha \in M_X \text{ and } \pi _2 \circ \alpha \in M_Y\} \).

\(\mathrm{program} = \mathrm{norm\_ qbs}(\lambda \_ .\; 1, \mathrm{obs})\).

\(\mathrm{Bernoulli}(p)\) as a QBS probability on \(\mathtt{boolQ}\).

Given \(p = (\alpha , \mu )\) on \(X\) and \(f : X \to P(Y)\), the bind \(p \mathbin {{\gt}\! \! {\gt}\! \! =} f\) is \((\lambda r.\; \alpha _{f(\alpha (r))}(r),\; \mu )\). The key obligation is that the diagonal \(r \mapsto \alpha _{f(\alpha (r))}(r)\) is random in \(Y\).

Specialized bind that uses the strong morphism proof to discharge the diagonal obligation.

\(\mathbb {E}_p[h] = \int _p (h(x))^{e}\) where \((-)^{e}\) embeds \(\mathbb {R}\) into \(\bar{\mathbb {R}}\).

Random variables \(f : Z \to X\) and \(g : Z \to Y\) are independent under \(p\) if the joint distribution \((f, g)_*(p)\) equals the product \(f_*(p) \otimes g_*(p)\).

A function \(h : X \to \bar{\mathbb {R}}\) is integrable against \(p\) if \(h \circ \alpha \) is integrable against \(\mu \).

For \(p = (\alpha , \mu )\) on \(X\) and \(h : X \to \bar{\mathbb {R}}\),

\(\mathrm{join} : P(P(X)) \to P(X)\) is defined as \(\mathrm{bind}(p, \mathrm{id})\), flattening nested probability.

For QBS structures on the same carrier \(T\), \(M_X \leq M_Y\) iff \(M_X \subseteq M_Y\) (more random elements means coarser structure).

A function \(h : X \to \bar{\mathbb {R}}\) is QBS measurable if for every \(\alpha \in M_X\), \(h \circ \alpha \) is Borel measurable.

A QBS morphism between standard Borel spaces lifts to a Dirac probability kernel.

A function \(f : X \to Y\) between QBS is a QBS morphism if for every \(\alpha \in M_X\), we have \(f \circ \alpha \in M_Y\).

A function \(f : X \to P(Y)\) is a strong morphism if for every random \(\alpha \in M_X\), the composition \(f \circ \alpha \) is random in \(P(Y)\) (in the strong sense: sharing a single underlying \(\alpha _Y\)).

\(\mathcal{N}(\mu , \sigma )\) as a QBS probability on \(\mathtt{realQ}\), using \((\mathrm{id}, \mathrm{normal\_ prob}\; \mu \; \sigma )\).

Returns Some(normalize_prob ...) when \(0 {\lt} Z {\lt} +\infty \), None otherwise. Uses classical decidability (boolp.pselect).

\(\int _{p \otimes q} h = \int _{\mu _p \otimes \mu _q} h(\alpha _p(r_1), \alpha _q(r_2))\).

\(\mathrm{Var}_{p \otimes q}[f + g] = \mathrm{variance}(\mu _p \otimes \mu _q,\; r \mapsto f(\alpha _p(r_1)) + g(\alpha _q(r_2)))\).

A QBS probability on \(X\) is a triple \((\alpha , \mu , \mathrm{proof})\) where \(\alpha \in M_X\) is a random element and \(\mu \) is a probability measure on \(\mathbb {R}\). The pushforward \(\alpha _*(\mu )\) is the induced distribution on \(X\).

Two triples \((\alpha _1, \mu _1) \sim (\alpha _2, \mu _2)\) iff they induce the same pushforward on \(\sigma _{M_X}\): \(\mu _1(\alpha _1^{-1}(U)) = \mu _2(\alpha _2^{-1}(U))\) for all \(U \in \sigma _{M_X}\).

\(\Pr _p[U] = \mu (\alpha ^{-1}(U))\).

For independent probabilities \(p\) on \(X\) and \(q\) on \(Y\), the product probability on \(X \times Y\) uses the product measure \(\mu _p \otimes \mu _q\) and the paired random element \(r \mapsto (\alpha _p(r_1), \alpha _q(r_2))\).

A setoid-style quotient wrapping qbs_prob X, with equality given by qbs_prob_equiv.

\(\eta (x) = (\lambda r.\; x,\; \mu )\) for any probability measure \(\mu \).

\(\mathrm{str}(w, p) = (\lambda r.\; (w, \alpha _p(r)),\; \mu _p)\), pairing a constant \(w : W\) with a probability \(p\) on \(X\).

The supremum of two QBS structures on \(T\) is \(\mathrm{gen}(M_X \cup M_Y)\).

For \(p = (\alpha , \mu )\) on \(R(M)\), the pushforward \(\alpha _*(\mu )\) is a probability measure on \(M\).

\(\mathrm{Uniform}[0,1]\) as a QBS probability on \(\mathtt{realQ}\).

\(\mathrm{Var}_p[f] = \mathrm{variance}(\mu , f \circ \alpha )\), delegating to math-comp analysis.

\(p_1 =_Q p_2\) iff \(\mathrm{repr}(p_1) \sim \mathrm{repr}(p_2)\).

Lifted operations on the quotient: return, bind, integration, functorial map, expectation, and event probability.

The functor \(R : \mathbf{Meas} \to \mathbf{QBS}\) sends a measurable space \(M\) to the QBS with \(M_{R(M)} = \{ f : \mathbb {R} \to M \mid f \text{ measurable}\} \).

The result of integrating \(\mathrm{obs}(s, b)\) over \(b\) against \(\mathcal{N}(0, 3)\): a scalar depending only on \(s\).

For a QBS \(X\), the induced sigma-algebra is \(\sigma _{M_X} = \{ U \subseteq X \mid \forall \alpha \in M_X,\; \alpha ^{-1}(U) \text{ is Borel measurable}\} \).

Given a QBS \(X\) and a predicate \(P \subseteq X\), the subspace QBS has carrier \(\{ x : X \mid P(x)\} \) with \(\alpha \) random iff \(\mathrm{proj}_1 \circ \alpha \in M_X\).

The unit QBS has carrier \(\mathtt{unit}\) with every function random: \(M_{\mathtt{unit}} = \{ f : \mathbb {R} \to \mathtt{unit}\} \).

If \(U\) is measurable in \(M\), then \(U \in L(R(M))\).

If \(\alpha \in M_X\) and \(U \in \sigma _{M_X}\), then \(\alpha ^{-1}(U)\) is Borel measurable.

The QBS probability recovers the original measure: \(\mu _{\mathrm{qbs}}(g^{-1}(U)) = P(g^{-1}(U))\) and \(\Pr _{\mathrm{qbs}}[U] = P(f(U))\).

If \(\mathrm{no\_ trailing\_ ones}(d)\), then \(\mathrm{bin\_ digits}(\mathrm{bin\_ sum}(d)) =_1 d\).

For \(0 \leq x {\lt} 1\): \(\mathrm{no\_ trailing\_ ones}(\mathrm{bin\_ digits}(x))\).

Partial sums converge, are non-decreasing, and the limit satisfies \(0 \leq \mathrm{bin\_ sum}(d) \leq 1\).

\(\mathrm{bin\_ sum}(d) = d(0) \cdot \tfrac {1}{2} + \mathrm{bin\_ sum}(d \circ S) \cdot \tfrac {1}{2}\).

\(\mathrm{bool}\) is standard Borel.

For \(a \neq 0\): \(ax^2 + bx + c = a\bigl(x + \tfrac {b}{2a}\bigr)^2 - \tfrac {b^2 - 4ac}{4a}\).

The constant-kernel construction is a measurable family.

The binary coproduct \(X + Y\) embeds into (and out of) the general coproduct over \(\mathbb {B}\).

\(\mathrm{inl} : X \to X + Y\) and \(\mathrm{inr} : Y \to X + Y\) are QBS morphisms.

The standard-Borel encode/decode round-trip lifts to the kernel level via kcomp.

The extended reals \(\bar{\mathbb {R}}\) form a standard Borel space.

\(0 \leq Z\).

\(0 {\lt} Z\) and \(Z {\lt} +\infty \).

\(\mathbb {E}_{p \otimes q}[h \circ \pi _1] = \mathbb {E}_p[h]\), and symmetrically for \(\pi _2\). For independent variables, \(\mathbb {E}_{p \otimes q}[h_1 \circ \pi _1 \cdot h_2 \circ \pi _2] = \mathbb {E}_p[h_1] \cdot \mathbb {E}_q[h_2]\).

The combined \(\sigma \) is nonzero when both inputs are nonzero. The scalar factor is positive.

\(G \subseteq M_{\mathrm{gen}(G)}\).

If \(M'\) satisfies the QBS axioms and \(G \subseteq M'\), then \(M_{\mathrm{gen}(G)} \subseteq M'\).

\(\sum _{i{\lt}n} (1/2)^{i+1} = 1 - (1/2)^n\).

\(\mathrm{giry\_ to\_ qbs}(\mathrm{qbs\_ to\_ giry}(p)) \sim p\) (up to equivalence).

\(\int _{\mathcal{N}(m, \sigma )} f = \int _{\mathrm{Lebesgue}} f(x) \cdot \mathrm{normal\_ pdf}(m, \sigma , x)\, dx\), converting QBS integration to Lebesgue integration with density.

If both \(d_1\) and \(d_2\) have no trailing ones, then so does \(\mathrm{interleave}(d_1, d_2)\).

Interleaving then deinterleaving (and vice versa) recovers the original sequences.

Pointwise: \(\mathrm{kdirac}(g \circ f) = \mathrm{kdirac}(g) \circ _{\mathrm{ker}} f\).

Composition of Dirac kernels equals the Dirac kernel of the function composition (functoriality at the kernel level).

Sending a Dirac kernel through the QBS-Giry round-trip preserves it.

Pointwise: \(\mathrm{kdirac}(f)(x)(U) = \delta _{f(x)}(U)\).

The QBS integral against a probability \(p\) equals the Lebesgue integral against \(\texttt{qbs\_ to\_ giry}(p)\).

General kernel round-trip property via the QBS-Giry bridge.

\(L\) preserves identity and composition.

If \(f : X \to Y\) is a QBS morphism and \(U \in L(Y)\), then \(f^{-1}(U) \in L(X)\).

\(L(X)\) satisfies \(\emptyset , T \in L(X)\), closure under complement, and closure under countable union.

Each single-observation likelihood factor is a QBS morphism.

Each single-observation likelihood is a strong morphism.

If \(\alpha \in M_{\mathrm{list}(X)}\), then \(\lambda r.\; \mathrm{nth}\; x_0\; (\alpha (r))\; i \in M_X\).

Postcomposition with a measurable \(\psi : M \to M'\) commutes with the hom-set bijection on the measurable side: if \(f : X \to M\) is a QBS morphism into \(R(M)\), then \(\psi \circ f : X \to M'\) is a QBS morphism into \(R(M')\).

If every measurable \(U \subseteq M\) has \(f^{-1}(U) \in L(X)\), then for measurable \(\psi : M \to M'\) and every measurable \(V \subseteq M'\), \((\psi \circ f)^{-1}(V) \in L(X)\).

Precomposition with a QBS morphism \(\phi : X' \to X\) commutes with the hom-set bijection on the QBS side: if \(\phi \) is a QBS morphism and \(f : X \to M\) is a QBS morphism into \(R(M)\), then \(f \circ \phi : X' \to M\) is also a QBS morphism into \(R(M)\).

The measurable-preimage characterization transports along \(\phi \): if \(\phi : X' \to X\) is a QBS morphism and every measurable \(U \subseteq M\) has \(f^{-1}(U) \in L(X)\), then every measurable \(U\) has \((f \circ \phi )^{-1}(U) \in L(X')\).

Full commuting square for \(L \dashv R\) naturality: given a QBS morphism \(\phi : X' \to X\), a measurable \(\psi : M \to M'\), and a QBS morphism \(f : X \to M\) into \(R(M)\), the composite \(\psi \circ f \circ \phi \) is a QBS morphism \(X' \to R(M')\) and its measurable preimages land in \(L(X')\).

\(f\) is a QBS morphism \(X \to \mathrm{im}(f)\).

If \(g : Y \to Z\) is a QBS morphism, then \(g\) is also a morphism from the image QBS.

If \(\alpha \in M_X\), then \(f \circ \alpha \in M_{\mathrm{im}(f)}\).

\(M_{\mathrm{im}(f)} \subseteq M_Y\).

The Dirac kernel of a measurable function is a probability kernel (not just s-finite).

Both \(\mathrm{encode}\) and \(\mathrm{decode}\) are measurable functions.

If \(P : \mathbb {R} \to \mathbb {N}\) and each \(F_i : \mathbb {R} \to M\) are measurable, then \(\lambda r.\; F_{P(r)}(r)\) is measurable. This justifies the gluing axiom for \(R(M)\).

\(\mathrm{pair\_ to\_ unit}\) is measurable, established by showing each partial sum of interleaved digits is measurable and applying \(\mathrm{measurable\_ fun\_ cvg}\).

Both projections of \(\mathrm{unit\_ to\_ pair}\) are measurable.

\(P(g \circ f)(p) \sim P(g)(P(f)(p))\).

\(P(\mathrm{id})(p) \sim p\).

\(P(f)\) is a QBS morphism \(P(X) \to P(Y)\).

\(\mathbb {N}\) is standard Borel.

\(\mathcal{N}(sk + b, \sigma )(y) = \mathcal{N}(y - ks, \sigma )(b)\), used to convert observations from intercept-centered to slope-centered form.

\(K \cdot \mathcal{N}(m, s)(x) \cdot \mathcal{N}(m', s')(x) = K \cdot K' \cdot \mathcal{N}(\mu _{\mathrm{new}}, \sigma _{\mathrm{new}})(x)\), allowing iterative combination.

\(\mathrm{obs}(s, b) \geq 0\) for all \((s, b)\).

The observation likelihood is integrable against the joint prior, established by bounding \(\mathrm{obs}\) by the normal peak raised to the 5th power.

The 5-observation product rewrites as a product of centered normal densities suitable for Phase 1 integration.

For \(0 \leq x, y {\lt} 1\): \(\mathrm{unit\_ to\_ pair}(\mathrm{pair\_ to\_ unit}(x, y)) = (x, y)\).

\(\int _{\mathcal{N}(0,3)} \mathrm{obs}(s, b)\, db = \mathrm{scalar\_ of\_ s}(s)\).

Each intermediate variance is positive and its square root is nonzero, ensuring the chain of Gaussian products is well-defined.

Each step computes the combined variance (\(\sigma ^2 \in \{ 9/37, 9/73, 9/109, 9/145, 9/181\} \)) and the combined mean (a linear function of the slope parameter \(s\)).

The full 5-step slope combination yields the final Gaussian times the accumulated constant.

The final \(\sigma \) is nonzero and the accumulated constant is positive.

\(\int _{\mathcal{N}(0,3)} \mathrm{scalar\_ of\_ s}(s)\, ds = \mathrm{phase2\_ const}\).

Each step combines the accumulated Gaussian for the slope with the next observation’s contribution.

\(\psi (\phi (x)) = x\) unconditionally. \(\phi (\psi (y)) = y\) for \(y \in (0,1)\).

\(\phi \) is measurable on all of \(\mathbb {R}\). \(\psi \) is measurable on \((0,1)\) and (via an approximation argument) on all of \(\mathbb {R}\).

\(0 {\lt} \phi (x) {\lt} 1\) for all \(x \in \mathbb {R}\).

When \(Z {\gt} 0\) and \(Z {\lt} +\infty \), the posterior integrates to \(1\).

The posterior measure is characterized by its density against the prior.

Every probability measure is s-finite, since it is finite (and hence \(\sigma \)-finite).

Every probability measure assigns a finite extended-real value to every measurable set.

If \(M_1\) and \(M_2\) are standard Borel, then \(M_1 \times M_2\) is standard Borel.

If \(\alpha \in M_Y\), then \(\lambda r.\; (x, \alpha (r)) \in M_{X \times Y}\).

If \(\alpha \in M_X\), then \(\lambda r.\; (\alpha (r), y) \in M_{X \times Y}\).

The program returns \(\mathrm{Some}(d)\) (evidence is positive and finite).

Pushforward of a probability measure along a measurable map is a probability measure.

\(m \mathbin {{\gt}\! \! {\gt}\! \! =} f \sim \mathrm{join}(P(f)(m))\) (modulo strength).

If \(p_1 \sim p_2\) and the diagonal factors through a morphism \(g\), then \(p_1 \mathbin {{\gt}\! \! {\gt}\! \! =} f \sim p_2 \mathbin {{\gt}\! \! {\gt}\! \! =} f\).

Specialization of bind congruence when \(f(x) = \eta (g(x))\) for a morphism \(g\).

Binding the return of a function with \(f\) equals the return of the function (the monad law at the kernel level).

Specialization of bind congruence for strong morphisms.

\(\Pr [|f(x) - \mathbb {E}[f]| \geq \varepsilon ] \leq \mathrm{Var}[f] / \varepsilon ^2\).

\(\mathbb {E}[\mathrm{Bernoulli}(p)] = p\).

\(\mathbb {E}[\mathcal{N}(\mu , \sigma )] = \mu \).

\(\mathbb {E}[\mathrm{Uniform}] = 1/2\).

The pushforward through a QBS morphism agrees with the classical Giry pushforward.

QBS integrability is closed under addition, subtraction, negation, and scalar multiplication.

\(\int _p h = \int _{\mathrm{pushforward}(\mu , h \circ \alpha )} \mathrm{id}\).

\(\int _{m \mathbin {{\gt}\! \! {\gt}\! \! =} f} h = \int _m (\lambda x.\; h(\alpha _{f(\alpha (r))}(r)))\).

\(\int _p c = c\) for any constant \(c\).

If \(p_1 \sim p_2\) and \(h\) is QBS measurable, then \(\int _{p_1} h = \int _{p_2} h\).

Genuine independence factorization. For random variables \(f : Z \to X\) and \(g : Z \to Y\) on a common probability space \(p : \mathrm{qbs\_ prob}(Z)\) that are independent in the sense of Definition 146, and real-valued test functions \(\phi : X \to \mathbb {R}\), \(\psi : Y \to \mathbb {R}\):

Unlike Lemma 147, the hypothesis qbs_indep is used non-trivially: the proof rewrites the joint integral against the pushforward \((f, g)_*(p)\) through the product \(f_*(p) \otimes g_*(p)\) via qbs_prob_equiv, then reduces to the product-measure factorization.

QBS integration is linear: additive, subtractive, and homogeneous.

\(\int _{\eta (x)} h = h(x)\).

Join is a QBS morphism \(P(P(X)) \to P(X)\).

\(\leq \) is reflexive, transitive, and antisymmetric.

For non-negative integrable \(f\) and \(\varepsilon {\gt} 0\): \(\Pr [f(x) \geq \varepsilon ] \leq \mathbb {E}[f] / \varepsilon \).

If \(h\) is QBS measurable and \(V\) is Borel measurable, then \(h^{-1}(V) \in \sigma _{M_X}\).

Every QBS morphism between standard Borel spaces is measurable (full faithfulness of the \(R\) functor).

The Dirac kernel of a QBS morphism between standard Borel spaces is a probability kernel.

\((x, y) \mapsto x + y\) is a QBS morphism \(\mathtt{realQ} \times \mathtt{realQ} \to \mathtt{realQ}\).

\(((x,y),z) \mapsto (x,(y,z))\) is a QBS morphism.

\((x,(y,z)) \mapsto ((x,y),z)\) is a QBS morphism.

If \(f : X \to Z\) and \(g : Y \to Z\) are QBS morphisms, then the case-analysis function \([f, g] : X + Y \to Z\) is a QBS morphism.

If \(f : X \to Y\) and \(g : Y \to Z\) are QBS morphisms, then \(g \circ f : X \to Z\) is a QBS morphism.

For any \(y : Y\), the constant function \(\lambda x.\; y\) is a QBS morphism.

Given QBS morphisms \(f : W \to (X \Rightarrow Y)\) and \(g : W \to X\), the pointwise application \(w \mapsto f(w)(g(w))\) is a QBS morphism \(W \to Y\).

\(\mathrm{fst} : X \times Y \to X\) is a QBS morphism.

For each \(i : I\), the injection \(x \mapsto (i, x)\) is a QBS morphism \(X_i \to \coprod _j X_j\).

The identity function \(\mathrm{id} : X \to X\) is a QBS morphism.

\(\mathrm{size} : \mathrm{list}(X) \to \mathtt{natQ}\) is a QBS morphism.

\((x, y) \mapsto (x {\lt} y)\) is a QBS morphism \(\mathtt{realQ} \times \mathtt{realQ} \to \mathtt{boolQ}\).

\((x, y) \mapsto x \cdot y\) is a QBS morphism \(\mathtt{realQ} \times \mathtt{realQ} \to \mathtt{realQ}\).

\(\mathtt{negb}\) is a QBS morphism \(\mathtt{boolQ} \to \mathtt{boolQ}\).

If \(f : W \to X\) and \(g : W \to Y\) are QBS morphisms, then \(\langle f, g \rangle : W \to X \times Y\) is a QBS morphism.

For each \(i : I\), the projection \(f \mapsto f(i)\) is a QBS morphism \(\prod _j X_j \to X_i\).

\(\mathrm{snd} : X \times Y \to Y\) is a QBS morphism.

\((x, y) \mapsto (y, x)\) is a QBS morphism \(X \times Y \to Y \times X\).

If \(f_i : W \to X_i\) are QBS morphisms for all \(i\), then \(w \mapsto (\lambda i.\; f_i(w))\) is a QBS morphism \(W \to \prod _i X_i\).

The unique map \(X \to \mathtt{unit}\) is a QBS morphism (terminality).

The normal distribution is a QBS morphism in the mean parameter: \(\mu \mapsto \mathcal{N}(\mu , \sigma )\) is a morphism \(\mathtt{realQ} \to P(\mathtt{realQ})\).

Conditional expectation formula: \(\mathbb {E}_{q}[g] = \mathbb {E}_{p}[g \cdot w] / Z\).

The normalized probability integrates to 1: \(\int 1 \, dq = 1\).

\(\int _{p \otimes q} h = \int _{q \otimes p} h \circ \mathrm{swap}\).

For functions \(f, g\) depending on disjoint coordinates of a product measure: \(\int _{p_X \otimes p_Y} f(x) \cdot g(y) = \mathbb {E}_{p_X}[f] \cdot \mathbb {E}_{p_Y}[g]\). This is product-measure factorization (a tautology of products), not a non-trivial statistical independence theorem – the lemma has no independence hypothesis. The genuine independence factorization, using the qbs_indep predicate, is Lemma 148.

Integration over the first component marginalizes the second.

Integration over the second component marginalizes the first.

Equivalent QBS probabilities (via qbs_prob_equiv) yield equal classical Giry probability measures.

\(\sim \) is reflexive, symmetric, and transitive.

The product probability equals bind composed with strength (Prop. 22 of HKSY17).

For any QBS probability \(p : P(X)\) with \(X\) standard Borel, the induced measure \(\texttt{qbs\_ to\_ giry}(p)\) is s-finite.

Equivalent triples yield the same pushforward through a QBS measurable function.

Integrability transfers through the pushforward.

All returns with the same point are equivalent regardless of \(\mu \): \(\eta _{\mu _1}(x) \sim \eta _{\mu _2}(x)\).

\(\eta ^{\mu } : X \to P(X)\) is a QBS morphism.

For standard Borel \(M\), transporting a Dirac measure through giry_to_qbs and back recovers the original Dirac measure.

\(P(\mathrm{assoc})(\mathrm{str}((u,v), p)) \sim \mathrm{str}(u, \mathrm{str}(v, p))\).

Strength is a QBS morphism \(W \times P(X) \to P(W \times X)\).

Strength commutes with morphisms: \(P(f \times g)(\mathrm{str}(w, p)) \sim \mathrm{str}(f(w), P(g)(p))\).

\(\mathrm{str}(w, \eta (x)) \sim \eta ((w, x))\).

\(P(\pi _2)(\mathrm{str}(\mathtt{tt}, p)) \sim p\).

The supremum is an upper bound for both components and is the least such upper bound.

Applying qbs_to_giry to a mapped probability equals the pushforward of the original Giry measure.

\(\mathrm{qbs\_ to\_ giry}(\mathrm{giry\_ to\_ qbs}(P)) = P\).

\(\mathrm{Var}[f] = \mathbb {E}[f^2] - (\mathbb {E}[f])^2\).

\(\mathrm{Var}[a \cdot f] = a^2 \cdot \mathrm{Var}[f]\).

\(=_Q\) is reflexive, symmetric, and transitive.

Return, integration, map, and event probability respect quotient equality.

\(R(M_1 \times M_2)\) and \(R(M_1) \times R(M_2)\) have the same random elements.

If \(f, g\) are measurable, then \(g \circ f\) is a QBS morphism \(R(M_1) \to R(M_3)\).

\(\mathrm{id}\) is a QBS morphism \(R(M) \to R(M)\).

If \(f : M_1 \to M_2\) is measurable, then \(f\) is a QBS morphism \(R(M_1) \to R(M_2)\).

\(\mathbb {R}\) is standard Borel via the identity functions.

\(\sigma _{M_X}\) is a sigma-algebra: it contains the full set, is closed under complement, and is closed under countable union.

For a standard Borel space \(M\), the \(L(R(M))\)-measurable sets coincide with the original measurable sets.

For \(0 \leq r {\lt} 1\) with no-trailing-ones on deinterleaved subsequences: \(\mathrm{pair\_ to\_ unit}(\mathrm{unit\_ to\_ pair}(r)) = r\).

Algebraic identity for the recurrence \(\frac{1}{V_{n+1}} = \frac{1}{V_n} + \frac{1}{s^2}\) relating successive combined variances.

\(\mathrm{Var}_{p \otimes q}[h \circ \pi _1] = \mathrm{Var}_p[h]\), and symmetrically for \(\pi _2\).

For \(0 \leq x {\lt} 1\): \(\mathrm{bin\_ sum}(\mathrm{bin\_ digits}(x)) = x\).

\(\mathrm{encode}(\mathrm{decode}(r)) = r\) under additional no-trailing-ones hypotheses (not needed for is_standard_borel).

\(\mathrm{decode}(\mathrm{encode}(x, y)) = (x, y)\) for all \(x, y \in \mathbb {R}\).

\(Z = \mathrm{phase2\_ const}\), an explicit closed-form constant computed by iterating the product-of-Gaussians identity through 10 combination steps.

A function \(f : X \to M\) is a QBS morphism \(X \to R(M)\) if and only if it pulls back measurable sets to \(L(X)\)-measurable sets:

Naturality of this bijection in both arguments is formalized by the five lemmas lr_adj_natural_dom, lr_adj_natural_dom_preimage, lr_adj_natural_cod, lr_adj_natural_cod_preimage, and lr_adj_natural_square below.

For \(s, s' \neq 0\):

where \(\mu _{\mathrm{new}} = \frac{m s'^2 + m' s^2}{s^2 + s'^2}\), \(\sigma _{\mathrm{new}} = \frac{s s'}{\sqrt{s^2 + s'^2}}\), and \(K\) is a scalar involving \(|m - m'|\) and \(\sqrt{s^2 + s'^2}\).

There exist measurable \(f : \mathbb {R}^2 \to \mathbb {R}\) and \(g : \mathbb {R} \to \mathbb {R}^2\) with \(g(f(x,y)) = (x,y)\).

The posterior distribution integrates to \(1\) (unconditionally). This is the main theorem of the Bayesian regression formalization.

\(\eta (x) \mathbin {{\gt}\! \! {\gt}\! \! =} f \sim f(x)\).

\(m \mathbin {{\gt}\! \! {\gt}\! \! =} \eta \sim m\).

\((m \mathbin {{\gt}\! \! {\gt}\! \! =} f) \mathbin {{\gt}\! \! {\gt}\! \! =} g \sim m \mathbin {{\gt}\! \! {\gt}\! \! =} (\lambda x.\; f(x) \mathbin {{\gt}\! \! {\gt}\! \! =} g)\).

QBS integration equals classical Lebesgue integration against the pushforward: \(\int _p f = \int _{\alpha _*(\mu )} f\).

If \(f : X \times Y \to Z\) is a QBS morphism, then \(\hat{f} : X \to (Y \Rightarrow Z)\) defined by \(\hat{f}(x)(y) = f(x,y)\) is a QBS morphism.

Evaluation \((f, x) \mapsto f(x)\) is a QBS morphism \((X \Rightarrow Y) \times X \to Y\).

The joint integral equals the iterated integral: \(\int _{p \otimes q} h = \int _p \int _q h(x, y)\). This is a special case of Fubini for the specific QBS product measure construction, not the full Fubini theorem on arbitrary product measures.

For independent random variables \(f\) and \(g\): \(\mathrm{Var}[f + g] = \mathrm{Var}[f] + \mathrm{Var}[g]\).

The monad laws hold on the quotient (as \(=_Q\) equalities): left unit, right unit, and associativity.

If \(M_1\) and \(M_2\) are standard Borel and \(f : M_1 \to M_2\) is a QBS morphism \(R(M_1) \to R(M_2)\), then \(f\) is measurable.