# mathlibdocumentation

measure_theory.category.Meas

# The category of measurable spaces #

Measurable spaces and measurable functions form a (concrete) category Meas.

## Main definitions #

• Measure : Meas ⥤ Meas: the functor which sends a measurable space X to the space of measures on X; it is a monad (the "Giry monad").

• Borel : Top ⥤ Meas: sends a topological space X to X equipped with the σ-algebra of Borel sets (the σ-algebra generated by the open subsets of X).

## Tags #

measurable space, giry monad, borel

def Meas  :
Type (u+1)

The category of measurable spaces and measurable functions.

Equations
Instances for Meas
@[protected, instance]
def Meas.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
Equations
def Meas.of (α : Type u)  :

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

Equations
@[simp]
theorem Meas.coe_of (X : Type u)  :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
noncomputable def 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.)

Equations
noncomputable def Meas.Giry  :

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

Equations
noncomputable def Meas.Integral  :

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

Equations
@[protected, instance]
Equations
def Borel  :

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

Equations