Quasi-Borel Spaces

Source: arxiv:1701.02547, doi:10.1109/LICS.2017.8005137 Authors: Anthony Vandikas, Kiarash Sotoudeh Status: verified Main declarations: QuasiBorelSpace, OmegaQuasiBorelSpace, QuasiBorelSpace.ProbabilityMeasure Tags: probability, category-theory, measure-theory, denotational-semantics MSC: 60A05, 18C50, 68Q55

Mathematical overview

A formalization of quasi-Borel spaces (Heunen, Kammar, Staton, Yang 2017) and quasi-Borel pre-domains (Vákár, Kammar, Staton 2019) in Lean 4. Quasi-Borel spaces are a convenient category for higher-order probability theory: they support function spaces while still allowing standard probability-theoretic constructions.

Main results

• QuasiBorelSpace — definition of a quasi-Borel space as a type together with a set of random variables closed under constants, measurable precomposition, and gluing.
• QuasiBorelSpace.IsHom — morphisms between quasi-Borel spaces.
• OmegaQuasiBorelSpace — quasi-Borel spaces enriched with an ω-complete partial order structure compatible with the underlying randomness.
• ProbabilityMeasure — the probability-measure monad on quasi-Borel spaces, obtained by quotienting pre-probability measures by integral equivalence.