The category of measurable spaces #
Measurable spaces and measurable functions form a (concrete) category
Main definitions #
measurable space, giry monad, borel
Measure X is the measurable space of measures over the measurable space
X. It is the
weakest measurable space, s.t.
fun μ ↦ μ s is measurable for all measurable sets
important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad,
the pure values are the Dirac measure, and the bind operation maps to the integral:
(μ >>= ν) s = ∫ x. (ν x) s dμ.