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 #
Tags #
giry monad
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)
:
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
Measurable.measure_of_isPiSystem
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : α → MeasureTheory.Measure β}
[∀ (a : α), MeasureTheory.IsFiniteMeasure (μ a)]
{S : Set (Set β)}
(hgen : inst✝ = MeasurableSpace.generateFrom S)
(hpi : IsPiSystem S)
(h_basic : ∀ s ∈ S, Measurable fun (a : α) => (μ a) s)
(h_univ : Measurable fun (a : α) => (μ a) Set.univ)
:
theorem
Measurable.measure_of_isPiSystem_of_isProbabilityMeasure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : α → MeasureTheory.Measure β}
[∀ (a : α), MeasureTheory.IsProbabilityMeasure (μ a)]
{S : Set (Set β)}
(hgen : inst✝ = MeasurableSpace.generateFrom S)
(hpi : IsPiSystem S)
(h_basic : ∀ s ∈ S, Measurable fun (a : α) => (μ a) 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 α))
:
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
@[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.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 β)
:
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
@[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 β}
:
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 = μ