feat(measure_theory): prove that the Giry monad is a monad in the category_theory sense

src/measure_theory/Meas.lean

@@ -1,14 +1,32 @@
 /- Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
-
-Basic setup for measurable spaces.
 -/
 
 import topology.Top.basic
-import measure_theory.borel_space
+import measure_theory.giry_monad
+import category_theory.monad.algebra
+
+/-
+* Meas, the category of measurable spaces
+
+Measurable spaces and measurable functions form a (concrete) category Meas.
+
+Measure : Meas ⥤ Meas is the functor which sends a measurable space X
+to the space of measures on X; it is a monad (the "Giry monad").
+
+Borel : Top ⥤ Meas sends a topological space X to X equipped with the
+σ-algebra of Borel sets (the σ-algebra generated by the open subsets of X).
+
+## Tags
+
+measurable space, giry monad, borel
+
+-/
+
+noncomputable theory
 
-open category_theory
+open category_theory measure_theory
 universes u v
 
 @[reducible] def Meas : Type (u+1) := bundled measurable_space
@@ -24,7 +42,53 @@ def of (X : Type u) [measurable_space X] : Meas := ⟨X⟩
 -- -- If `measurable` were a class, we would summon instances:
 -- local attribute [class] measurable
 -- instance {X Y : Meas} (f : X ⟶ Y) : measurable (f : X → Y) := f.2
+
+/-- `Measure X` is the measurable space of measures over the measurable space `X`. It is the
+weakest measurable space, s.t. λμ, μ 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 `Meas`-morphisms `X → Prob X` are (sub-)Markov kernels (here `Prob` is
+the restriction of `Measure` to (sub-)probability space.)
+-/
+def Measure : Meas ⥤ Meas :=
+{ obj      := λX, ⟨@measure_theory.measure X.1 X.2⟩,
+  map      := λX Y f, ⟨measure.map f, measure.measurable_map f f.2⟩,
+  map_id'  := assume ⟨α, I⟩, subtype.eq $ funext $ assume μ, @measure.map_id α I μ,
+  map_comp':=
+    assume X Y Z ⟨f, hf⟩ ⟨g, hg⟩, subtype.eq $ funext $ assume μ, (measure.map_map hg hf).symm }
+
+/-- The Giry monad, i.e. the monadic structure associated with `Measure`. -/
+instance : category_theory.monad Measure.{u} :=
+{ η :=
+  { app         := λX, ⟨@measure.dirac X.1 X.2, measure.measurable_dirac⟩,
+    naturality' :=
+      assume X Y ⟨f, hf⟩, subtype.eq $ funext $ assume a, (measure.map_dirac hf a).symm },
+  μ :=
+  { app         := λX, ⟨@measure.join X.1 X.2, measure.measurable_join⟩,
+    naturality' :=
+      assume X Y ⟨f, hf⟩, subtype.eq $ funext $ assume μ, measure.join_map_map hf μ },
+  assoc' := assume ⟨α, I⟩, subtype.eq $ funext $ assume μ, @measure.join_map_join α I μ,
+  left_unit' := assume ⟨α, I⟩, subtype.eq $ funext $ assume μ, @measure.join_dirac α I μ,
+  right_unit' := assume ⟨α, I⟩, subtype.eq $ funext $ assume μ, @measure.join_map_dirac α I μ }
+
+/-- An example for an algebra on `Measure`: the nonnegative Lebesgue integral is a hom, behaving
+nicely under the monad operations. -/
+def Integral : monad.algebra Measure :=
+{ A      := Meas.of ennreal ,
+  a      := ⟨ λm:measure ennreal, m.integral id, measure.measurable_integral _ measurable_id ⟩,
+  unit'  := subtype.eq $ funext $ assume r:ennreal, measure.integral_dirac _ measurable_id,
+  assoc' := subtype.eq $ funext $ assume μ : measure (measure ennreal),
+    show μ.join.integral id = measure.integral (μ.map (λm:measure ennreal, m.integral id)) id, from
+    begin
+      rw [measure.integral_join measurable_id, measure.integral_map measurable_id],
+      refl,
+      exact measure.measurable_integral _ measurable_id
+    end }
+
 end Meas
 
+/-- The Borel functor, the canonical embedding of topological spaces into measurable spaces. -/
 def Borel : Top ⥤ Meas :=
 concrete_functor @measure_theory.borel @measure_theory.measurable_of_continuous

src/measure_theory/giry_monad.lean

@@ -2,10 +2,28 @@
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
-
-Giry monad: `measure` is a monad in the category of `measurable_space` and `measurable` functions.
 -/
 import measure_theory.integration
+
+/-!
+# 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.
+
+## References
+
+* https://ncatlab.org/nlab/show/Giry+monad
+
+## Tags
+
+giry monad
+-/
+
 noncomputable theory
 open_locale classical
 
@@ -184,6 +202,40 @@ begin
   exact one_mul _
 end
 
+lemma map_dirac {f : α → β} (hf : measurable f) (a : α) :
+  map f (dirac a) = dirac (f a) :=
+measure.ext $ assume s hs,
+  by rw [dirac_apply (f a) hs, map_apply hf hs, dirac_apply a (hf s hs), set.mem_preimage]
+
+lemma join_eq_bind (μ : measure (measure α)) : join μ = bind μ id :=
+by rw [bind, map_id]
+
+lemma join_map_map {f : α → β} (hf : measurable f) (μ : measure (measure α)) :
+  join (map (map f) μ) = map f (join μ) :=
+measure.ext $ assume s hs,
+  begin
+    rw [join_apply hs, map_apply hf hs, join_apply,
+      integral_map (measurable_coe hs) (measurable_map f hf)],
+    { congr, funext ν, exact map_apply hf hs },
+    exact hf s hs
+  end
+
+lemma join_map_join (μ : measure (measure (measure α))) :
+  join (map join μ) = join (join μ) :=
+begin
+  show bind μ join = join (join μ),
+  rw [join_eq_bind, join_eq_bind, bind_bind measurable_id measurable_id],
+  apply congr_arg (bind μ),
+  funext ν,
+  exact join_eq_bind ν
+end
+
+lemma join_map_dirac (μ : measure α) : join (map dirac μ) = μ :=
+dirac_bind
+
+lemma join_dirac (μ : measure α) : join (dirac μ) = μ :=
+eq.trans (join_eq_bind (dirac μ)) (bind_dirac measurable_id _)
+
 end measure
 
 end measure_theory

src/measure_theory/measurable_space.lean

@@ -6,6 +6,57 @@ Authors: Johannes Hölzl, Mario Carneiro
 Measurable spaces -- σ-algberas
 -/
 import data.set.disjointed order.galois_connection data.set.countable
+
+/-!
+# Measurable spaces and measurable functions
+
+This file defines measurable spaces and the functions and isomorphisms
+between them.
+
+A measurable space is a set equipped with a σ-algebra, a collection of
+subsets closed under complementation and countable union. A function
+between measurable spaces is measurable if the preimage of each
+measurable subset is measurable.
+
+σ-algebras on a fixed set α form a complete lattice. Here we order
+σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is
+also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any
+collection of subsets of α generates a smallest σ-algebra which
+contains all of them. A function f : α → β induces a Galois connection
+between the lattices of σ-algebras on α and β.
+
+A measurable equivalence between measurable spaces is an equivalence
+which respects the σ-algebras, that is, for which both directions of
+the equivalence are measurable functions.
+
+## Main statements
+
+The main theorem of this file is Dynkin's π-λ theorem, which appears
+here as an induction principle `induction_on_inter`. Suppose s is a
+collection of subsets of α such that the intersection of two members
+of s belongs to s whenever it is nonempty. Let m be the σ-algebra
+generated by s. In order to check that a predicate C holds on every
+member of m, it suffices to check that C holds on the members of s and
+that C is preserved by complementation and *disjoint* countable
+unions.
+
+## Implementation notes
+
+Measurability of a function f : α → β between measurable spaces is
+defined in terms of the Galois connection induced by f.
+
+## References
+
+* https://en.wikipedia.org/wiki/Measurable_space
+* https://en.wikipedia.org/wiki/Sigma-algebra
+* https://en.wikipedia.org/wiki/Dynkin_system
+
+## Tags
+
+measurable space, measurable function, dynkin system
+-/
+
+local attribute [instance] classical.prop_decidable
 open set lattice encodable
 open_locale classical
 
@@ -451,6 +502,24 @@ is_measurable.inter (measurable_fst measurable_id _ hs) (measurable_snd measurab
 
 end prod
 
+section pi
+
+instance measurable_space.pi {α : Type u} {β : α → Type v} [m : Πa, measurable_space (β a)] :
+  measurable_space (Πa, β a) :=
+⨆a, (m a).comap (λb, b a)
+
+lemma measurable_pi_apply {α : Type u} {β : α → Type v} [Πa, measurable_space (β a)] (a : α) :
+  measurable (λf:Πa, β a, f a) :=
+measurable_space.comap_le_iff_le_map.1 $ lattice.le_supr _ a
+
+lemma measurable_pi_lambda {α : Type u} {β : α → Type v} {γ : Type w}
+  [Πa, measurable_space (β a)] [measurable_space γ]
+  (f : γ → Πa, β a) (hf : ∀a, measurable (λc, f c a)):
+  measurable f :=
+lattice.supr_le $ assume a, measurable_space.comap_le_iff_le_map.2 (hf a)
+
+end pi
+
 instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α ⊕ β) :=
 m₁.map sum.inl ⊓ m₂.map sum.inr