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
The category of measurable spaces and measurable functions.
Equations
Instances For
Equations
 MeasCat.instCoeSortMeasCatType = CategoryTheory.Bundled.coeSort
Equations
 MeasCat.instMeasurableSpaceα X = X.str
Construct a bundled MeasCat
from the underlying type and the typeclass.
Equations
 MeasCat.of α = { α := α, str := ms }
Instances For
Equations
Equations
 MeasCat.instInhabitedMeasCat = { default := MeasCat.of Empty }
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.)
Equations
 One or more equations did not get rendered due to their size.
Instances For
The Giry monad, i.e. the monadic structure associated with Measure
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
An example for an algebra on Measure
: the nonnegative Lebesgue integral is a hom, behaving
nicely under the monad operations.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Equations
 One or more equations did not get rendered due to their size.
The Borel functor, the canonical embedding of topological spaces into measurable spaces.