The Giry monad #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 measure_theory/category/Meas.lean, containing an upgrade of the type-level
monad to an honest monad of the functor Measure : Meas ⥤ Meas.
References #
Tags #
giry monad
@[protected, instance]
Measurability structure on measure: Measures are measurable w.r.t. all projections
Equations
- measure_theory.measure.measurable_space = ⨆ (s : set α) (hs : measurable_set s), measurable_space.comap (λ (μ : measure_theory.measure α), ⇑μ s) (borel ennreal)
theorem
measure_theory.measure.measurable_coe
{α : Type u_1}
[measurable_space α]
{s : set α}
(hs : measurable_set s) :
measurable (λ (μ : measure_theory.measure α), ⇑μ s)
theorem
measure_theory.measure.measurable_of_measurable_coe
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : β → measure_theory.measure α)
(h : ∀ (s : set α), measurable_set s → measurable (λ (b : β), ⇑(f b) s)) :
@[protected, instance]
theorem
measure_theory.measure.measurable_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : α → measure_theory.measure β} :
measurable μ ↔ ∀ (s : set β), measurable_set s → measurable (λ (b : α), ⇑(μ b) s)
theorem
measure_theory.measure.measurable_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β)
(hf : measurable f) :
measurable (λ (μ : measure_theory.measure α), measure_theory.measure.map f μ)
theorem
measure_theory.measure.measurable_lintegral
{α : Type u_1}
[measurable_space α]
{f : α → ennreal}
(hf : measurable f) :
measurable (λ (μ : measure_theory.measure α), ∫⁻ (x : α), f x ∂μ)
noncomputable
def
measure_theory.measure.join
{α : Type u_1}
[measurable_space α]
(m : measure_theory.measure (measure_theory.measure α)) :
Monadic join on measure in the category of measurable spaces and measurable
functions.
Equations
- m.join = measure_theory.measure.of_measurable (λ (s : set α) (hs : measurable_set s), ∫⁻ (μ : measure_theory.measure α), ⇑μ s ∂m) _ _
@[simp]
theorem
measure_theory.measure.join_apply
{α : Type u_1}
[measurable_space α]
{m : measure_theory.measure (measure_theory.measure α)}
{s : set α}
(hs : measurable_set s) :
@[simp]
theorem
measure_theory.measure.lintegral_join
{α : Type u_1}
[measurable_space α]
{m : measure_theory.measure (measure_theory.measure α)}
{f : α → ennreal}
(hf : measurable f) :
noncomputable
def
measure_theory.measure.bind
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(m : measure_theory.measure α)
(f : α → measure_theory.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 = (measure_theory.measure.map f m).join
@[simp]
theorem
measure_theory.measure.bind_zero_left
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → measure_theory.measure β) :
@[simp]
theorem
measure_theory.measure.bind_zero_right
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(m : measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.bind_zero_right'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(m : measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.bind_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{m : measure_theory.measure α}
{f : α → measure_theory.measure β}
{s : set β}
(hs : measurable_set s)
(hf : measurable f) :
theorem
measure_theory.measure.measurable_bind'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{g : α → measure_theory.measure β}
(hg : measurable g) :
measurable (λ (m : measure_theory.measure α), m.bind g)
theorem
measure_theory.measure.lintegral_bind
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{m : measure_theory.measure α}
{μ : α → measure_theory.measure β}
{f : β → ennreal}
(hμ : measurable μ)
(hf : measurable f) :
theorem
measure_theory.measure.bind_bind
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{γ : Type u_3}
[measurable_space γ]
{m : measure_theory.measure α}
{f : α → measure_theory.measure β}
{g : β → measure_theory.measure γ}
(hf : measurable f)
(hg : measurable g) :
theorem
measure_theory.measure.bind_dirac
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → measure_theory.measure β}
(hf : measurable f)
(a : α) :
(measure_theory.measure.dirac a).bind f = f a
theorem
measure_theory.measure.dirac_bind
{α : Type u_1}
[measurable_space α]
{m : measure_theory.measure α} :
theorem
measure_theory.measure.join_eq_bind
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure (measure_theory.measure α)) :
theorem
measure_theory.measure.join_map_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
(hf : measurable f)
(μ : measure_theory.measure (measure_theory.measure α)) :
theorem
measure_theory.measure.join_map_join
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure (measure_theory.measure (measure_theory.measure α))) :
theorem
measure_theory.measure.join_map_dirac
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
theorem
measure_theory.measure.join_dirac
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :