Lean4
/-- `Measure X` is the measurable space of measures over the measurable space `X`. It is the
weakest measurable space, s.t. `fun μ ↦ μ s` is measurable for all measurable sets `s` in `X`. An
important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad,
the pure values are the Dirac measure, and the bind operation maps to the integral:
`(μ >>= ν) s = ∫ x. (ν x) s dμ`.
In probability theory, the `MeasCat`-morphisms `X → Prob X` are (sub-)Markov kernels (here `Prob` is
the restriction of `Measure` to (sub-)probability space.)
-/
def Measure : MeasCat ⥤ MeasCat where
obj X := of (@MeasureTheory.Measure X.1 X.2)
map f := ⟨Measure.map (⇑f), Measure.measurable_map f.1 f.2⟩
map_id X := Subtype.eq <| funext fun μ => @Measure.map_id X.carrier X.str μ
map_comp := fun ⟨_, hf⟩ ⟨_, hg⟩ => Subtype.eq <| funext fun _ => (Measure.map_map hg hf).symm
