Documentation

Mathlib.MeasureTheory.Measure.GiryMonad

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
theorem MeasureTheory.Measure.measurable_of_measurable_coe {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : βMeasureTheory.Measure α) (h : ∀ (s : Set α), MeasurableSet sMeasurable fun (b : β) => (f b) s) :
theorem MeasureTheory.Measure.measurable_measure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : αMeasureTheory.Measure β} :
Measurable μ ∀ (s : Set β), MeasurableSet sMeasurable fun (b : α) => (μ b) s
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μ

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} [MeasurableSpace α] {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {s : Set α} (hs : MeasurableSet s) :
    m.join s = ∫⁻ (μ : MeasureTheory.Measure α), μ sm
    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 xm.join = ∫⁻ (μ : MeasureTheory.Measure α), ∫⁻ (x : α), f xμm

    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
    Instances For
      @[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) sm
      @[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 xm.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f xμ am
      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 : α) :
      @[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_map_dirac {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) :
      (MeasureTheory.Measure.map MeasureTheory.Measure.dirac μ).join = μ