From 74b1327abef92ff57d71d9d7b37031f94664070f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 24 Jul 2019 00:01:31 +0200 Subject: [PATCH 1/5] 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 From e9bdeb325d4d69e59aba4eb62813bd3b427c302a Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 24 Jul 2019 12:22:41 +0200 Subject: [PATCH 2/5] Add spaces to fix alignment --- src/measure_theory/Meas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/measure_theory/Meas.lean b/src/measure_theory/Meas.lean index 61fc5a38f7a10..dbb734a023230 100644 --- a/src/measure_theory/Meas.lean +++ b/src/measure_theory/Meas.lean @@ -41,7 +41,7 @@ instance : category_theory.monad Measure.{u} := 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⟩, + { 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 μ, From 707832d77a56f96fa52ca3034a1fb599432d3fec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Thu, 25 Jul 2019 00:23:10 +0200 Subject: [PATCH 3/5] document Measure --- src/measure_theory/Meas.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/measure_theory/Meas.lean b/src/measure_theory/Meas.lean index dbb734a023230..4e970973d244e 100644 --- a/src/measure_theory/Meas.lean +++ b/src/measure_theory/Meas.lean @@ -28,6 +28,15 @@ def of (X : Type u) [measurable_space X] : Meas := ⟨X⟩ -- 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⟩, @@ -35,6 +44,7 @@ def Measure : Meas ⥤ Meas := 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⟩, @@ -48,8 +58,10 @@ instance : category_theory.monad Measure.{u} := 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 := @category_theory.bundled.mk _ ennreal (borel ennreal), +{ 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), @@ -62,5 +74,6 @@ def Integral : monad.algebra Measure := 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 From c96869889904337f82c5227583c34e480b10e8fd Mon Sep 17 00:00:00 2001 From: Reid Barton Date: Tue, 3 Sep 2019 15:25:08 -0400 Subject: [PATCH 4/5] Add documentation --- src/measure_theory/Meas.lean | 19 ++++++++- src/measure_theory/giry_monad.lean | 22 ++++++++++- src/measure_theory/measurable_space.lean | 50 ++++++++++++++++++++++++ 3 files changed, 87 insertions(+), 4 deletions(-) diff --git a/src/measure_theory/Meas.lean b/src/measure_theory/Meas.lean index 4e970973d244e..a69e13347f2e0 100644 --- a/src/measure_theory/Meas.lean +++ b/src/measure_theory/Meas.lean @@ -1,14 +1,29 @@ /- 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.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 measure_theory diff --git a/src/measure_theory/giry_monad.lean b/src/measure_theory/giry_monad.lean index 0fdbf5f1d92a4..cac74c8e9ff84 100644 --- a/src/measure_theory/giry_monad.lean +++ b/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 local attribute [instance, priority 0] classical.prop_decidable diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index cf6fcc58a99b5..3187d76454d93 100644 --- a/src/measure_theory/measurable_space.lean +++ b/src/measure_theory/measurable_space.lean @@ -7,6 +7,56 @@ Measurable spaces -- σ-algberas -/ import data.set.disjointed order.galois_connection data.set.countable open set lattice encodable + +/-! +# 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 universes u v w x From de52f18ff5ea9bdec2d449260d77ff6e62d71f44 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 3 Sep 2019 21:44:05 +0200 Subject: [PATCH 5/5] Add space before colon --- src/measure_theory/measurable_space.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index e24b9fc53f71d..4965014cc6597 100644 --- a/src/measure_theory/measurable_space.lean +++ b/src/measure_theory/measurable_space.lean @@ -514,7 +514,7 @@ 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)): + (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)