Introduction
1
Core QBS Theory
▶
1.1
QBS Definition
1.2
Morphisms
1.3
The R Functor
1.4
Binary Products
1.5
Exponentials (Function Spaces)
1.6
Unit QBS
1.7
Induced Sigma-Algebra
1.8
Arithmetic Morphisms
1.9
Subspaces
1.10
Generating QBS
1.11
Image QBS
1.12
Order Structure on QBS
1.13
The L Functor and L–R Adjunction
1.14
Standard Borel Spaces (Definition)
1.15
Coproducts (Binary)
1.16
Coproducts (General / Sigma Type)
1.17
Dependent Products (Pi Type)
1.18
List Type
2
Probability Monad
▶
2.1
QBS Probability Triple
2.2
The Probability Monad \(P(X)\)
2.3
Return
2.4
Bind
2.5
Monad Laws
2.6
Integration
2.7
Pushforward Infrastructure
2.8
Functorial Map
2.9
Expectation, Events, and Variance
2.10
Integrability
2.11
Variance Properties
2.12
Monad Join
2.13
Monad Strength
2.14
Bind Respects Equivalence
2.15
General Normalizer
2.16
Quotient Type for QBS Probability
2.17
Product Measures and Fubini
2.18
Independence
2.19
Variance of Independent Sums
3
QBS–Giry Bridge and Classical Distributions
▶
3.1
Classical Distribution Embedding
3.2
QBS–Giry Monad Connection
4
Standard Borel Spaces (\(\mathbb {R} \cong \mathbb {R} \times \mathbb {R}\))
▶
4.1
R to (0,1) Bijection
4.2
Binary Digit Machinery
4.3
Digit Interleaving
4.4
Pairing Functions
4.5
Composed Bijection \(\mathbb {R} \times \mathbb {R} \to \mathbb {R}\)
4.6
Measurability
4.7
The Punchline
5
Normal Density Algebra
▶
5.1
Completing the Square
5.2
Product of Gaussian Densities
5.3
Phase 1: Intercept Combinations
5.4
Phase 2: Slope Combinations
6
Bayesian Linear Regression
▶
6.1
Priors and Likelihood
6.2
Evidence (Normalizing Constant)
6.3
Posterior Density
6.4
Monadic Prior
6.5
Normalizer Program
6.6
Evidence Computation
6.7
Main Results
7
QBS–Kernel Bridge
▶
7.1
S-Finiteness of Probability Measures
7.2
Dirac Kernels and QBS Return
7.3
QBS Morphisms as Kernels
7.4
Constant Kernels and Equivalence
7.5
Pushforward and Kernel Composition
7.6
Bind, Return, and Integration at the Kernel Level
Dependency graph
Quasi-Borel Spaces in Rocq
Guillaume Baudart with Claude Opus 4.6 and Rocq-MCP
Introduction
1
Core QBS Theory
1.1
QBS Definition
1.2
Morphisms
1.3
The R Functor
1.4
Binary Products
1.5
Exponentials (Function Spaces)
1.6
Unit QBS
1.7
Induced Sigma-Algebra
1.8
Arithmetic Morphisms
1.9
Subspaces
1.10
Generating QBS
1.11
Image QBS
1.12
Order Structure on QBS
1.13
The L Functor and L–R Adjunction
1.14
Standard Borel Spaces (Definition)
1.15
Coproducts (Binary)
1.16
Coproducts (General / Sigma Type)
1.17
Dependent Products (Pi Type)
1.18
List Type
2
Probability Monad
2.1
QBS Probability Triple
2.2
The Probability Monad \(P(X)\)
2.3
Return
2.4
Bind
2.5
Monad Laws
2.6
Integration
2.7
Pushforward Infrastructure
2.8
Functorial Map
2.9
Expectation, Events, and Variance
2.10
Integrability
2.11
Variance Properties
2.12
Monad Join
2.13
Monad Strength
2.14
Bind Respects Equivalence
2.15
General Normalizer
2.16
Quotient Type for QBS Probability
2.17
Product Measures and Fubini
2.18
Independence
2.19
Variance of Independent Sums
3
QBS–Giry Bridge and Classical Distributions
3.1
Classical Distribution Embedding
3.2
QBS–Giry Monad Connection
4
Standard Borel Spaces (\(\mathbb {R} \cong \mathbb {R} \times \mathbb {R}\))
4.1
R to (0,1) Bijection
4.2
Binary Digit Machinery
4.3
Digit Interleaving
4.4
Pairing Functions
4.5
Composed Bijection \(\mathbb {R} \times \mathbb {R} \to \mathbb {R}\)
4.6
Measurability
4.7
The Punchline
5
Normal Density Algebra
5.1
Completing the Square
5.2
Product of Gaussian Densities
5.3
Phase 1: Intercept Combinations
5.4
Phase 2: Slope Combinations
6
Bayesian Linear Regression
6.1
Priors and Likelihood
6.2
Evidence (Normalizing Constant)
6.3
Posterior Density
6.4
Monadic Prior
6.5
Normalizer Program
6.6
Evidence Computation
6.7
Main Results
7
QBS–Kernel Bridge
7.1
S-Finiteness of Probability Measures
7.2
Dirac Kernels and QBS Return
7.3
QBS Morphisms as Kernels
7.4
Constant Kernels and Equivalence
7.5
Pushforward and Kernel Composition
7.6
Bind, Return, and Integration at the Kernel Level