Quasi-Borel Spaces formalization for Mathlib

Stream: general

[Kiarash Sotoudeh]

Hi all,

@Anthony Vandikas and I have been formalizing Quasi-Borel Spaces in Lean over the past couple of months, and we’re now at a stage where feedback from the mathlib community would be really valuable. For context, Quasi-Borel Spaces (QBS) were introduced by Heunen et al. in A Convenient Category for Higher-Order Probability Theory as a semantic foundation for higher-order probabilistic programming. They provide a cartesian closed setting where higher-order functions and continuous distributions fit together and they form the basis for much of the modern work in higher-order probabilistic programming languages.

Our formalization is still a work in progress, but a substantial portion of the core development is in place, including the basic QBS structure, many standard closure properties, and a strong probability-measure monad. If this feels like something that could eventually belong in mathlib, we’d really appreciate comments on design, structure, naming, or anything that stands out. The repo is here.

Thanks in advance to anyone who takes a look!