S-Finite Measure Monad on Quasi-Borel Spaces

The s-finite measure monad on quasi-Borel spaces provides a suitable denotational model for higher-order probabilistic programs with conditioning. This entry is a formalization of the s-finite measure monad and related notions, including s-finite measures, s-finite kernels, and a proof automation for quasi-Borel spaces which is an extension of our previous entry Quasi-Borel Spaces. We also implement several examples of probabilistic programs in previous works and prove their property. This work is a part of the work by Hirata, Minamide, and Sato, Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL presented at the 14th Conference on Interactive Theorem Proving (ITP2023).