Meas.of

Construct a bundled Meas from the underlying type and the typeclass.

Meas.Measure

Measure X is the measurable space of measures over the measurable space X. It is the weakest measurable space, s.t. λμ, μ s is measurable for all measurable sets s in X. An 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μ.

In probability theory, the Meas-morphisms X Prob X are (sub-)Markov kernels (here Prob is the restriction of Measure to (sub-)probability space.)

Meas.category_theory.monad

The Giry monad, i.e. the monadic structure associated with Measure.

Meas.Integral

An example for an algebra on Measure: the nonnegative Lebesgue integral is a hom, behaving nicely under the monad operations.

Borel

The Borel functor, the canonical embedding of topological spaces into measurable spaces.