# The Giry monad #

Let X be a measurable space. The collection of all measures on X again forms a measurable space. This construction forms a monad on measurable spaces and measurable functions, called the Giry monad.

Note that most sources use the term "Giry monad" for the restriction to probability measures. Here we include all measures on X.

See also MeasureTheory/Category/MeasCat.lean, containing an upgrade of the type-level monad to an honest monad of the functor measure : MeasCat ⥤ MeasCat.

## Tags #

Measurability structure on Measure: Measures are measurable w.r.t. all projections

Equations
theorem MeasureTheory.Measure.measurable_coe {α : Type u_1} [] {s : Set α} (hs : ) :
Measurable fun (μ : ) => μ s
theorem MeasureTheory.Measure.measurable_of_measurable_coe {α : Type u_1} {β : Type u_2} [] [] (f : ) (h : ∀ (s : Set α), Measurable fun (b : β) => (f b) s) :
Equations
• =
theorem MeasureTheory.Measure.measurable_measure {α : Type u_1} {β : Type u_2} [] [] {μ : } :
∀ (s : Set β), Measurable fun (b : α) => (μ b) s
theorem MeasureTheory.Measure.measurable_map {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) :
Measurable fun (μ : ) =>
theorem MeasureTheory.Measure.measurable_dirac {α : Type u_1} [] :
Measurable MeasureTheory.Measure.dirac
theorem MeasureTheory.Measure.measurable_lintegral {α : Type u_1} [] {f : αENNReal} (hf : ) :
Measurable fun (μ : ) => ∫⁻ (x : α), f xμ
def MeasureTheory.Measure.join {α : Type u_1} [] :

Monadic join on Measure in the category of measurable spaces and measurable functions.

Equations
Instances For
@[simp]
theorem MeasureTheory.Measure.join_apply {α : Type u_1} [] {s : Set α} (hs : ) :
m.join s = ∫⁻ (μ : ), μ sm
@[simp]
theorem MeasureTheory.Measure.join_zero {α : Type u_1} [] :
theorem MeasureTheory.Measure.measurable_join {α : Type u_1} [] :
Measurable MeasureTheory.Measure.join
theorem MeasureTheory.Measure.lintegral_join {α : Type u_1} [] {f : αENNReal} (hf : ) :
∫⁻ (x : α), f xm.join = ∫⁻ (μ : ), ∫⁻ (x : α), f xμm
def MeasureTheory.Measure.bind {α : Type u_1} {β : Type u_2} [] [] (m : ) (f : ) :

Monadic bind on Measure, only works in the category of measurable spaces and measurable functions. When the function f is not measurable the result is not well defined.

Equations
• m.bind f = .join
Instances For
@[simp]
theorem MeasureTheory.Measure.bind_zero_left {α : Type u_1} {β : Type u_2} [] [] (f : ) :
@[simp]
theorem MeasureTheory.Measure.bind_zero_right {α : Type u_1} {β : Type u_2} [] [] (m : ) :
m.bind 0 = 0
@[simp]
theorem MeasureTheory.Measure.bind_zero_right' {α : Type u_1} {β : Type u_2} [] [] (m : ) :
(m.bind fun (x : α) => 0) = 0
@[simp]
theorem MeasureTheory.Measure.bind_apply {α : Type u_1} {β : Type u_2} [] [] {m : } {f : } {s : Set β} (hs : ) (hf : ) :
(m.bind f) s = ∫⁻ (a : α), (f a) sm
theorem MeasureTheory.Measure.measurable_bind' {α : Type u_1} {β : Type u_2} [] [] {g : } (hg : ) :
Measurable fun (m : ) => m.bind g
theorem MeasureTheory.Measure.lintegral_bind {α : Type u_1} {β : Type u_2} [] [] {m : } {μ : } {f : βENNReal} (hμ : ) (hf : ) :
∫⁻ (x : β), f xm.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f xμ am
theorem MeasureTheory.Measure.bind_bind {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_3} [] {m : } {f : } {g : } (hf : ) (hg : ) :
(m.bind f).bind g = m.bind fun (a : α) => (f a).bind g
theorem MeasureTheory.Measure.bind_dirac {α : Type u_1} {β : Type u_2} [] [] {f : } (hf : ) (a : α) :
.bind f = f a
theorem MeasureTheory.Measure.dirac_bind {α : Type u_1} [] {m : } :
m.bind MeasureTheory.Measure.dirac = m
theorem MeasureTheory.Measure.join_eq_bind {α : Type u_1} [] :
μ.join = μ.bind id
theorem MeasureTheory.Measure.join_map_map {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
theorem MeasureTheory.Measure.join_map_join {α : Type u_1} [] :
(MeasureTheory.Measure.map MeasureTheory.Measure.join μ).join = μ.join.join
theorem MeasureTheory.Measure.join_map_dirac {α : Type u_1} [] (μ : ) :
(MeasureTheory.Measure.map MeasureTheory.Measure.dirac μ).join = μ
theorem MeasureTheory.Measure.join_dirac {α : Type u_1} [] (μ : ) :
.join = μ