The Giry monad #
Let X be a measurable space. The collection of all measures on X again
forms a measurable space. This construction forms a monad on
measurable spaces and measurable functions, called the Giry monad.
Note that most sources use the term "Giry monad" for the restriction
to probability measures. Here we include all measures on X.
measure_theory/category/Meas.lean, containing an upgrade of the type-level
monad to an honest monad of the functor
Measure : Meas ⥤ Meas.
Measurability structure on
measure: Measures are measurable w.r.t. all projections
Monadic join on
measure in the category of measurable spaces and measurable
Monadic bind on
measure, only works in the category of measurable spaces and measurable
functions. When the function
f is not measurable the result is not well defined.