Quasi-Borel Spaces in Rocq

3 QBS–Giry Bridge and Classical Distributions

This chapter connects the QBS probability monad to the classical Giry monad and provides concrete distributions (normal, Bernoulli, uniform) with their expected values.

3.1 Classical Distribution Embedding

Definition 154 Classical-to-QBS Embedding

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\).

Definition 155 Normal Distribution

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

Definition 156 Bernoulli Distribution

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

Definition 157 Uniform Distribution

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

Lemma 158 Recovery Theorems

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))\).

Proof
Lemma 159 Normal Distribution Is a Morphism

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})\).

Proof
Lemma 160 Expected Value of Bernoulli

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

Proof
Lemma 161 Expected Value of Uniform

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

Proof
Lemma 162 Expected Value of Normal

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

Proof

3.2 QBS–Giry Monad Connection

Definition 163 QBS to Giry

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

Definition 164 Giry to QBS

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

Lemma 165 QBS–Giry Round-Trip (Giry direction)

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

Proof
Lemma 166 QBS–Giry Round-Trip (QBS direction)

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

Proof
Theorem 167 Integral Correspondence

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

Proof

Both sides reduce to \(\int _\mu f(\alpha (r))\, d\mu (r)\).