# 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

source
instance MeasureTheory.Measure.instMeasurableSpace {α : Type u_1} {mα : MeasurableSpace α} :
MeasurableSpace (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)

source
theorem MeasureTheory.Measure.measurable_coe {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) :
Measurable fun (μ : Measure α) => μ s
source
theorem MeasureTheory.Measure.measurable_of_measurable_coe {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : β → Measure α) (h : ∀ (s : Set α), MeasurableSet s → Measurable fun (b : β) => (f b) s) :
Measurable f
source
instance MeasureTheory.Measure.instMeasurableAdd₂ {α : Type u_3} {m : MeasurableSpace α} :
MeasurableAdd₂ (Measure α)
source
theorem Measurable.smul_measure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → ENNReal} (hf : Measurable f) (μ : MeasureTheory.Measure β) :
Measurable fun (x : α) => f x • μ
source
theorem MeasureTheory.Measure.measurable_measure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → Measure β} :
Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable fun (b : α) => (μ b) s
source
theorem Measurable.measure_of_isPiSystem {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → MeasureTheory.Measure β} [∀ (a : α), MeasureTheory.IsFiniteMeasure (μ a)] {S : Set (Set β)} (hgen : mβ = MeasurableSpace.generateFrom S) (hpi : IsPiSystem S) (h_basic : ∀ s ∈ S, Measurable fun (a : α) => (μ a) s) (h_univ : Measurable fun (a : α) => (μ a) Set.univ) :
Measurable μ
source
theorem Measurable.measure_of_isPiSystem_of_isProbabilityMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → MeasureTheory.Measure β} [∀ (a : α), MeasureTheory.IsProbabilityMeasure (μ a)] {S : Set (Set β)} (hgen : mβ = MeasurableSpace.generateFrom S) (hpi : IsPiSystem S) (h_basic : ∀ s ∈ S, Measurable fun (a : α) => (μ a) s) :
Measurable μ
source
theorem MeasureTheory.Measure.measurable_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) (hf : Measurable f) :
Measurable fun (μ : Measure α) => map f μ
source
theorem MeasureTheory.Measure.measurable_dirac {α : Type u_1} {mα : MeasurableSpace α} :
Measurable dirac
source
theorem MeasureTheory.Measure.measurable_lintegral {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal} (hf : Measurable f) :
Measurable fun (μ : Measure α) => ∫⁻ (x : α), f x ∂μ
source
def MeasureTheory.Measure.join {α : Type u_1} {mα : MeasurableSpace α} (m : Measure (Measure α)) :
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) ⋯ ⋯

Instances For

source
@[simp]
theorem MeasureTheory.Measure.join_apply {α : Type u_1} {mα : MeasurableSpace α} {m : Measure (Measure α)} {s : Set α} (hs : MeasurableSet s) :
m.join s = ∫⁻ (μ : Measure α), μ s ∂m
source
theorem MeasureTheory.Measure.le_join_apply {α : Type u_1} {mα : MeasurableSpace α} (m : Measure (Measure α)) (s : Set α) :
∫⁻ (μ : Measure α), μ s ∂m ≤ m.join s
source
@[simp]
theorem MeasureTheory.Measure.join_smul {α : Type u_1} {mα : MeasurableSpace α} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (m : Measure (Measure α)) :
(c • m).join = c • m.join
source
@[simp]
theorem MeasureTheory.Measure.join_dirac {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) :
(dirac μ).join = μ
source
theorem MeasureTheory.Measure.le_ae_join {α : Type u_1} {mα : MeasurableSpace α} (m : Measure (Measure α)) :
(ae m).bind ae ≤ ae m.join
source
theorem MeasureTheory.Measure.ae_ae_of_ae_join {α : Type u_1} {mα : MeasurableSpace α} {m : Measure (Measure α)} {p : α → Prop} (h : ∀ᵐ (a : α) ∂m.join, p a) :
∀ᵐ (μ : Measure α) ∂m, ∀ᵐ (a : α) ∂μ, p a
source
theorem AEMeasurable.ae_of_join {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {f : α → β} (h : AEMeasurable f m.join) :
∀ᵐ (μ : MeasureTheory.Measure α) ∂m, AEMeasurable f μ
source
theorem MeasureTheory.Measure.aemeasurable_lintegral {α : Type u_1} {mα : MeasurableSpace α} {m : Measure (Measure α)} {f : α → ENNReal} (h : AEMeasurable f m.join) :
AEMeasurable (fun (μ : Measure α) => ∫⁻ (a : α), f a ∂μ) m
source
@[simp]
theorem MeasureTheory.Measure.join_zero {α : Type u_1} {mα : MeasurableSpace α} :
join 0 = 0
source
theorem MeasureTheory.Measure.measurable_join {α : Type u_1} {mα : MeasurableSpace α} :
Measurable join
source
theorem MeasureTheory.Measure.lintegral_join {α : Type u_1} {mα : MeasurableSpace α} {m : Measure (Measure α)} {f : α → ENNReal} (hf : AEMeasurable f m.join) :
∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
source
theorem MeasureTheory.Measure.lintegral_join_le {α : Type u_1} {mα : MeasurableSpace α} (f : α → ENNReal) (m : Measure (Measure α)) :
∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
source
def MeasureTheory.Measure.bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : Measure α) (f : α → Measure β) :
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

Instances For

source
@[simp]
theorem MeasureTheory.Measure.bind_zero_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → Measure β) :
bind 0 f = 0
source
@[simp]
theorem MeasureTheory.Measure.bind_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : Measure α} {f : α → Measure β} {s : Set β} (hs : MeasurableSet s) (hf : AEMeasurable f m) :
(m.bind f) s = ∫⁻ (a : α), (f a) s ∂m
source
theorem MeasureTheory.Measure.bind_apply_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : Measure α} (f : α → Measure β) {s : Set β} (hs : MeasurableSet s) :
(m.bind f) s ≤ ∫⁻ (a : α), (f a) s ∂m
source
theorem MeasureTheory.Measure.ae_ae_of_ae_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : Measure α} {f : α → Measure β} {p : β → Prop} (hf : AEMeasurable f m) (h : ∀ᵐ (b : β) ∂m.bind f, p b) :
∀ᵐ (a : α) ∂m, ∀ᵐ (b : β) ∂f a, p b
source
theorem AEMeasurable.ae_of_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} {x✝ : MeasurableSpace γ} {m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {g : β → γ} (hf : AEMeasurable f m) (hg : AEMeasurable g (m.bind f)) :
∀ᵐ (a : α) ∂m, AEMeasurable g (f a)
source
theorem MeasureTheory.Measure.bind_congr_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {f g : α → Measure β} (h : f =ᶠ[ae μ] g) :
μ.bind f = μ.bind g
source
@[simp]
theorem MeasureTheory.Measure.bind_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : Measure α} {ν : Measure β} :
(m.bind fun (x : α) => ν) = m Set.univ • ν
source
theorem MeasureTheory.Measure.bind_zero_right' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : Measure α) :
(m.bind fun (x : α) => 0) = 0
source
@[simp]
theorem MeasureTheory.Measure.bind_zero_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : Measure α) :
m.bind 0 = 0
source
theorem MeasureTheory.Measure.measurable_bind' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {g : α → Measure β} (hg : Measurable g) :
Measurable fun (m : Measure α) => m.bind g
source
theorem MeasureTheory.Measure.aemeasurable_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {g : α → Measure β} {m : Measure (Measure α)} (hg : AEMeasurable g m.join) :
AEMeasurable (fun (x : Measure α) => x.bind g) m
source
theorem MeasureTheory.Measure.lintegral_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : Measure α} {μ : α → Measure β} {f : β → ENNReal} (hμ : AEMeasurable μ m) (hf : AEMeasurable f (m.bind μ)) :
∫⁻ (x : β), f x ∂m.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
source
theorem MeasureTheory.Measure.lintegral_bind_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : β → ENNReal) (m : Measure α) (μ : α → Measure β) :
∫⁻ (x : β), f x ∂m.bind μ ≤ ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
source
theorem MeasureTheory.Measure.bind_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3} [MeasurableSpace γ] {m : Measure α} {f : α → Measure β} {g : β → Measure γ} (hf : AEMeasurable f m) (hg : AEMeasurable g (m.bind f)) :
(m.bind f).bind g = m.bind fun (a : α) => (f a).bind g
source
@[simp]
theorem MeasureTheory.Measure.dirac_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → Measure β} (hf : Measurable f) (a : α) :
(dirac a).bind f = f a
source
@[simp]
theorem MeasureTheory.Measure.bind_dirac {α : Type u_1} {mα : MeasurableSpace α} {m : Measure α} :
m.bind dirac = m
source
@[simp]
theorem MeasureTheory.Measure.bind_dirac_eq_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : Measure α) {f : α → β} (hf : Measurable f) :
(m.bind fun (x : α) => dirac (f x)) = map f m
source
theorem MeasureTheory.Measure.join_eq_bind {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure (Measure α)) :
μ.join = μ.bind id
source
theorem MeasureTheory.Measure.join_map_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) (μ : Measure (Measure α)) :
(map (map f) μ).join = map f μ.join
source
theorem MeasureTheory.Measure.join_map_join {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure (Measure (Measure α))) :
(map join μ).join = μ.join.join
source
theorem MeasureTheory.Measure.join_map_dirac {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) :
(map dirac μ).join = μ