From 74b1327abef92ff57d71d9d7b37031f94664070f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Wed, 24 Jul 2019 00:01:31 +0200
Subject: [PATCH] feat(measure_theory): prove that the Giry monad is a monad in
 the category_theory sense

---
 src/measure_theory/Meas.lean             | 40 ++++++++++++++++++++++--
 src/measure_theory/giry_monad.lean       | 34 ++++++++++++++++++++
 src/measure_theory/measurable_space.lean | 18 +++++++++++
 3 files changed, 90 insertions(+), 2 deletions(-)

diff --git a/src/measure_theory/Meas.lean b/src/measure_theory/Meas.lean
index 1404341517fc7..61fc5a38f7a10 100644
--- a/src/measure_theory/Meas.lean
+++ b/src/measure_theory/Meas.lean
@@ -6,9 +6,12 @@ Basic setup for measurable spaces.
 -/
 
 import topology.Top.basic
-import measure_theory.borel_space
+import measure_theory.giry_monad
+import category_theory.monad.algebra
 
-open category_theory
+noncomputable theory
+
+open category_theory measure_theory
 universes u v
 
 @[reducible] def Meas : Type (u+1) := bundled measurable_space
@@ -24,6 +27,39 @@ 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
+
+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 }
+
+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 μ }
+
+def Integral : monad.algebra Measure :=
+{ A      := @category_theory.bundled.mk _ ennreal (borel 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
 
 def Borel : Top ⥤ Meas :=
diff --git a/src/measure_theory/giry_monad.lean b/src/measure_theory/giry_monad.lean
index 5bc5511f75beb..0fdbf5f1d92a4 100644
--- a/src/measure_theory/giry_monad.lean
+++ b/src/measure_theory/giry_monad.lean
@@ -184,6 +184,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
diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean
index a719dc69c27a6..cf6fcc58a99b5 100644
--- a/src/measure_theory/measurable_space.lean
+++ b/src/measure_theory/measurable_space.lean
@@ -451,6 +451,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