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.

References

• https://ncatlab.org/nlab/show/Giry+monad

Tags

giry monad

instance MeasureTheory.Measure.instMeasurableSpace {α : Type u_1} [MeasurableSpace α] : MeasurableSpace (MeasureTheory.Measure α)

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

Equations

• MeasureTheory.Measure.instMeasurableSpace = ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), MeasurableSpace.comap (fun (μ : MeasureTheory.Measure α) => μ s) (borel ENNReal)

theorem MeasureTheory.Measure.measurable_coe {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) : Measurable fun (μ : MeasureTheory.Measure α) => μ s

theorem MeasureTheory.Measure.measurable_of_measurable_coe {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : β → MeasureTheory.Measure α) (h : ∀ (s : Set α), MeasurableSet s → Measurable fun (b : β) => (f b) s) : Measurable f

instance MeasureTheory.Measure.instMeasurableAdd₂ {α : Type u_3} {m : MeasurableSpace α} : MeasurableAdd₂ (MeasureTheory.Measure α)

Equations

• ⋯ = ⋯

theorem MeasureTheory.Measure.measurable_measure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : α → MeasureTheory.Measure β} : Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable fun (b : α) => (μ b) s

theorem MeasureTheory.Measure.measurable_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (hf : Measurable f) : Measurable fun (μ : MeasureTheory.Measure α) => MeasureTheory.Measure.map f μ

theorem MeasureTheory.Measure.measurable_dirac {α : Type u_1} [MeasurableSpace α] : Measurable MeasureTheory.Measure.dirac

theorem MeasureTheory.Measure.measurable_lintegral {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) : Measurable fun (μ : MeasureTheory.Measure α) => ∫⁻ (x : α), f x ∂μ

def MeasureTheory.Measure.join {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.Measure (MeasureTheory.Measure α)) : MeasureTheory.Measure α

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

Equations

• m.join = MeasureTheory.Measure.ofMeasurable (fun (s : Set α) (x : MeasurableSet s) => ∫⁻ (μ : MeasureTheory.Measure α), μ s ∂m) ⋯ ⋯

@[simp]

theorem MeasureTheory.Measure.join_apply {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {s : Set α} (hs : MeasurableSet s) : m.join s = ∫⁻ (μ : MeasureTheory.Measure α), μ s ∂m

@[simp]

theorem MeasureTheory.Measure.join_zero {α : Type u_1} [MeasurableSpace α] : MeasureTheory.Measure.join 0 = 0

theorem MeasureTheory.Measure.measurable_join {α : Type u_1} [MeasurableSpace α] : Measurable MeasureTheory.Measure.join

theorem MeasureTheory.Measure.lintegral_join {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : MeasureTheory.Measure α), ∫⁻ (x : α), f x ∂μ ∂m

def MeasureTheory.Measure.bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (m : MeasureTheory.Measure α) (f : α → MeasureTheory.Measure β) : MeasureTheory.Measure β

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 = (MeasureTheory.Measure.map f m).join

@[simp]

theorem MeasureTheory.Measure.bind_zero_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → MeasureTheory.Measure β) : MeasureTheory.Measure.bind 0 f = 0

@[simp]

theorem MeasureTheory.Measure.bind_zero_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (m : MeasureTheory.Measure α) : m.bind 0 = 0

@[simp]

theorem MeasureTheory.Measure.bind_zero_right' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (m : MeasureTheory.Measure α) : (m.bind fun (x : α) => 0) = 0

@[simp]

theorem MeasureTheory.Measure.bind_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) (hf : Measurable f) : (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m

@[simp]

theorem MeasureTheory.Measure.bind_const {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {m : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} : (m.bind fun (x : α) => ν) = m Set.univ • ν

theorem MeasureTheory.Measure.measurable_bind' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {g : α → MeasureTheory.Measure β} (hg : Measurable g) : Measurable fun (m : MeasureTheory.Measure α) => m.bind g

theorem MeasureTheory.Measure.lintegral_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {m : MeasureTheory.Measure α} {μ : α → MeasureTheory.Measure β} {f : β → ENNReal} (hμ : Measurable μ) (hf : Measurable f) : ∫⁻ (x : β), f x ∂m.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m

theorem MeasureTheory.Measure.bind_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {γ : Type u_3} [MeasurableSpace γ] {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {g : β → MeasureTheory.Measure γ} (hf : Measurable f) (hg : Measurable g) : (m.bind f).bind g = m.bind fun (a : α) => (f a).bind g

theorem MeasureTheory.Measure.dirac_bind {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → MeasureTheory.Measure β} (hf : Measurable f) (a : α) : (MeasureTheory.Measure.dirac a).bind f = f a

@[simp]

theorem MeasureTheory.Measure.bind_dirac {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure α} : m.bind MeasureTheory.Measure.dirac = m

@[simp]

theorem MeasureTheory.Measure.bind_dirac_eq_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (m : MeasureTheory.Measure α) {f : α → β} (hf : Measurable f) : (m.bind fun (x : α) => MeasureTheory.Measure.dirac (f x)) = MeasureTheory.Measure.map f m

theorem MeasureTheory.Measure.join_eq_bind {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure (MeasureTheory.Measure α)) : μ.join = μ.bind id

theorem MeasureTheory.Measure.join_map_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Measurable f) (μ : MeasureTheory.Measure (MeasureTheory.Measure α)) : (MeasureTheory.Measure.map (MeasureTheory.Measure.map f) μ).join = MeasureTheory.Measure.map f μ.join

theorem MeasureTheory.Measure.join_map_join {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure (MeasureTheory.Measure (MeasureTheory.Measure α))) : (MeasureTheory.Measure.map MeasureTheory.Measure.join μ).join = μ.join.join

theorem MeasureTheory.Measure.join_map_dirac {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : (MeasureTheory.Measure.map MeasureTheory.Measure.dirac μ).join = μ

theorem MeasureTheory.Measure.join_dirac {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) : (MeasureTheory.Measure.dirac μ).join = μ