The category of measurable spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

def Meas :

Type (u+1)

The category of measurable spaces and measurable functions.

Equations

Meas = category_theory.bundled measurable_space

Instances for Meas

source

@[protected, instance]

def Meas.has_coe_to_sort :

has_coe_to_sort Meas (Type u_1)

Equations

Meas.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def Meas.measurable_space (X : Meas) :

measurable_space ↥X

Equations

X.measurable_space = X.str

source

def Meas.of (α : Type u) [measurable_space α] :

Meas

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

Equations

Meas.of α = {α := α, str := _inst_1}

source

@[simp]

theorem Meas.coe_of (X : Type u) [measurable_space X] :

↥(Meas.of X) = X

source

@[protected, instance]

def Meas.unbundled_hom :

category_theory.unbundled_hom measurable

Equations

Meas.unbundled_hom = {hom_id := measurable_id, hom_comp := measurable.comp}

source

@[protected, instance]

def Meas.large_category :

category_theory.large_category Meas

source

@[protected, instance]

def Meas.concrete_category :

category_theory.concrete_category Meas

source

@[protected, instance]

def Meas.inhabited :

inhabited Meas

Equations

Meas.inhabited = {default := Meas.of empty empty.measurable_space}

source

noncomputable def Meas.Measure :

Meas ⥤ Meas

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

Meas.Measure = {obj := λ (X : Meas), {α := measure_theory.measure X.α X.str, str := measure_theory.measure.measurable_space X.str}, map := λ (X Y : Meas) (f : X ⟶ Y), ⟨measure_theory.measure.map ↑f, _⟩, map_id' := Meas.Measure._proof_2, map_comp' := Meas.Measure._proof_3}

source

noncomputable def Meas.Giry :

category_theory.monad Meas

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

Equations

Meas.Giry = {to_functor := Meas.Measure, η' := {app := λ (X : Meas), ⟨measure_theory.measure.dirac X.str, _⟩, naturality' := Meas.Giry._proof_2}, μ' := {app := λ (X : Meas), ⟨measure_theory.measure.join X.str, _⟩, naturality' := Meas.Giry._proof_4}, assoc' := Meas.Giry._proof_5, left_unit' := Meas.Giry._proof_6, right_unit' := Meas.Giry._proof_7}

source

noncomputable def Meas.Integral :

Meas.Giry.algebra

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

Equations

Meas.Integral = {A := Meas.of ennreal ennreal.measurable_space, a := ⟨λ (m : measure_theory.measure ennreal), ∫⁻ (x : ennreal), x ∂m, Meas.Integral._proof_1⟩, unit' := Meas.Integral._proof_2, assoc' := Meas.Integral._proof_3}

source

@[protected, instance]

def Top.has_forget_to_Meas :

category_theory.has_forget₂ Top Meas

Equations

Top.has_forget_to_Meas = category_theory.bundled_hom.mk_has_forget₂ borel (λ (X Y : category_theory.bundled topological_space) (f : X ⟶ Y), ⟨f.to_fun, _⟩) Top.has_forget_to_Meas._proof_2

source

@[reducible]

def Borel :

Top ⥤ Meas

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

Equations

Borel = category_theory.forget₂ Top Meas