2 Probability Monad
This chapter develops the QBS probability monad \(P(X)\): the type of probability distributions on a QBS \(X\). We define the monad operations (return, bind), prove the monad laws, develop integration theory with Fubini, and establish independence and variance results.
2.1 QBS Probability Triple
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}\).
\(\sim \) is reflexive, symmetric, and transitive.
2.2 The Probability Monad \(P(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\).
2.3 Return
\(\eta (x) = (\lambda r.\; x,\; \mu )\) for any probability measure \(\mu \).
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.
2.4 Bind
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\)).
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.
2.5 Monad Laws
\(\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)\).
2.6 Integration
For \(p = (\alpha , \mu )\) on \(X\) and \(h : X \to \bar{\mathbb {R}}\),
A function \(h : X \to \bar{\mathbb {R}}\) is QBS measurable if for every \(\alpha \in M_X\), \(h \circ \alpha \) is Borel measurable.
If \(h\) is QBS measurable and \(V\) is Borel measurable, then \(h^{-1}(V) \in \sigma _{M_X}\).
If \(p_1 \sim p_2\) and \(h\) is QBS measurable, then \(\int _{p_1} h = \int _{p_2} h\).
\(\int _p c = c\) for any constant \(c\).
\(\int _{\eta (x)} h = h(x)\).
\(\int _{m \mathbin {{\gt}\! \! {\gt}\! \! =} f} h = \int _m (\lambda x.\; h(\alpha _{f(\alpha (r))}(r)))\).
2.7 Pushforward Infrastructure
\(\int _p h = \int _{\mathrm{pushforward}(\mu , h \circ \alpha )} \mathrm{id}\).
Integrability transfers through the pushforward.
Equivalent triples yield the same pushforward through a QBS measurable function.
2.8 Functorial Map
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 )\).
\(P(f)\) is a QBS morphism \(P(X) \to P(Y)\).
\(P(\mathrm{id})(p) \sim p\).
\(P(g \circ f)(p) \sim P(g)(P(f)(p))\).
2.9 Expectation, Events, and Variance
\(\mathbb {E}_p[h] = \int _p (h(x))^{e}\) where \((-)^{e}\) embeds \(\mathbb {R}\) into \(\bar{\mathbb {R}}\).
\(\Pr _p[U] = \mu (\alpha ^{-1}(U))\).
\(\mathrm{Var}_p[f] = \mathrm{variance}(\mu , f \circ \alpha )\), delegating to math-comp analysis.
2.10 Integrability
A function \(h : X \to \bar{\mathbb {R}}\) is integrable against \(p\) if \(h \circ \alpha \) is integrable against \(\mu \).
QBS integrability is closed under addition, subtraction, negation, and scalar multiplication.
QBS integration is linear: additive, subtractive, and homogeneous.
2.11 Variance Properties
\(\mathrm{Var}[f] = \mathbb {E}[f^2] - (\mathbb {E}[f])^2\).
\(\mathrm{Var}[a \cdot f] = a^2 \cdot \mathrm{Var}[f]\).
For non-negative integrable \(f\) and \(\varepsilon {\gt} 0\): \(\Pr [f(x) \geq \varepsilon ] \leq \mathbb {E}[f] / \varepsilon \).
\(\Pr [|f(x) - \mathbb {E}[f]| \geq \varepsilon ] \leq \mathrm{Var}[f] / \varepsilon ^2\).
2.12 Monad Join
\(\mathrm{join} : P(P(X)) \to P(X)\) is defined as \(\mathrm{bind}(p, \mathrm{id})\), flattening nested probability.
Join is a QBS morphism \(P(P(X)) \to P(X)\).
2.13 Monad Strength
\(\mathrm{str}(w, p) = (\lambda r.\; (w, \alpha _p(r)),\; \mu _p)\), pairing a constant \(w : W\) with a probability \(p\) on \(X\).
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))\).
\(P(\pi _2)(\mathrm{str}(\mathtt{tt}, p)) \sim p\).
\(P(\mathrm{assoc})(\mathrm{str}((u,v), p)) \sim \mathrm{str}(u, \mathrm{str}(v, p))\).
\(\mathrm{str}(w, \eta (x)) \sim \eta ((w, x))\).
\(m \mathbin {{\gt}\! \! {\gt}\! \! =} f \sim \mathrm{join}(P(f)(m))\) (modulo strength).
2.14 Bind Respects Equivalence
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 for strong morphisms.
Specialization of bind congruence when \(f(x) = \eta (g(x))\) for a morphism \(g\).
2.15 General Normalizer
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 \).
Returns Some(normalize_prob ...) when \(0 {\lt} Z {\lt} +\infty \), None otherwise. Uses classical decidability (boolp.pselect).
The normalized probability integrates to 1: \(\int 1 \, dq = 1\).
Conditional expectation formula: \(\mathbb {E}_{q}[g] = \mathbb {E}_{p}[g \cdot w] / Z\).
2.16 Quotient Type for QBS Probability
A setoid-style quotient wrapping qbs_prob X, with equality given by qbs_prob_equiv.
\(p_1 =_Q p_2\) iff \(\mathrm{repr}(p_1) \sim \mathrm{repr}(p_2)\).
\(=_Q\) is reflexive, symmetric, and transitive.
Lifted operations on the quotient: return, bind, integration, functorial map, expectation, and event probability.
Return, integration, map, and event probability respect quotient equality.
The monad laws hold on the quotient (as \(=_Q\) equalities): left unit, right unit, and associativity.
2.17 Product Measures and Fubini
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))\).
\(\int _{p \otimes q} h = \int _{\mu _p \otimes \mu _q} h(\alpha _p(r_1), \alpha _q(r_2))\).
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.
By Fubini’s theorem on the product measure \(\mu _p \otimes \mu _q\).
Integration over the first component marginalizes the second.
Integration over the second component marginalizes the first.
\(\int _{p \otimes q} h = \int _{q \otimes p} h \circ \mathrm{swap}\).
2.18 Independence
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)\).
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.
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.
2.19 Variance of Independent Sums
\(\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)))\).
\(\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]\).
\(\mathrm{Var}_{p \otimes q}[h \circ \pi _1] = \mathrm{Var}_p[h]\), and symmetrically for \(\pi _2\).
For independent random variables \(f\) and \(g\): \(\mathrm{Var}[f + g] = \mathrm{Var}[f] + \mathrm{Var}[g]\).
Decompose \(\mathrm{Var}(f+g) = \mathrm{Var}(f) + \mathrm{Var}(g) + 2\, \mathrm{Cov}(f,g)\), then show \(\mathrm{Cov}(f,g) = 0\) because \(\mathbb {E}[fg] = \mathbb {E}[f] \cdot \mathbb {E}[g]\) by Fubini.
The product probability equals bind composed with strength (Prop. 22 of HKSY17).