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 148 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 149 Normal Distribution

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

Definition 150 Bernoulli Distribution

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

Definition 151 Uniform Distribution

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

Lemma 152 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 153 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 154 Expected Value of Bernoulli

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

Proof
Lemma 155 Expected Value of Uniform

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

Proof
Lemma 156 Expected Value of Normal

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

Proof

3.2 QBS–Giry Monad Connection

Definition 157 QBS to Giry

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

Definition 158 Giry to QBS

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

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

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

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

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

Proof
Theorem 161 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)\).