The category of measurable spaces #
Measurable spaces and measurable functions form a (concrete) category MeasCat
.
Main definitions #
-
Measure : MeasCat ⥤ MeasCat
: the functor which sends a measurable spaceX
to the space of measures onX
; it is a monad (the "Giry monad"). -
Borel : TopCat ⥤ MeasCat
: sends a topological spaceX
toX
equipped with theσ
-algebra of Borel sets (theσ
-algebra generated by the open subsets ofX
).
Tags #
measurable space, giry monad, borel
Construct a bundled MeasCat
from the underlying type and the typeclass.
Instances For
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 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 MeasCat
-morphisms X → Prob X
are (sub-)Markov kernels (here Prob
is
the restriction of Measure
to (sub-)probability space.)
Instances For
The Giry monad, i.e. the monadic structure associated with Measure
.
Instances For
An example for an algebra on Measure
: the nonnegative Lebesgue integral is a hom, behaving
nicely under the monad operations.
Instances For
The Borel functor, the canonical embedding of topological spaces into measurable spaces.