feat(analysis/measure_theory): add Giry monad

src/analysis/measure_theory/borel_space.lean

@@ -25,7 +25,7 @@ variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort y}
 namespace measure_theory
 open measurable_space topological_space
 
-@[instance] def borel (α : Type u) [topological_space α] : measurable_space α :=
+@[instance, priority 900] def borel (α : Type u) [topological_space α] : measurable_space α :=
 generate_from {s : set α | is_open s}
 
 lemma borel_eq_generate_from_of_subbasis {s : set (set α)}
@@ -172,16 +172,23 @@ lemma measurable_of_continuous2
 show measurable ((λp:α×β, c p.1 p.2) ∘ (λa, (f a, g a))),
 begin
   apply measurable.comp,
-  { rw ← borel_prod,
-    exact measurable_prod_mk hf hg },
-  { exact measurable_of_continuous h }
+  { exact measurable_prod_mk hf hg },
+  { rw borel_prod,
+    exact measurable_of_continuous h }
 end
 
 lemma measurable_add
   [add_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β]
   {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a + g a) :=
 measurable_of_continuous2 continuous_add'
 
+lemma measurable_finset_sum {ι : Type*}
+  [add_comm_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β]
+  {f : ι → β → α} (s : finset ι) (hf : ∀i, measurable (f i)) : measurable (λa, s.sum (λi, f i a)) :=
+finset.induction_on s
+  (by simpa using measurable_const)
+  (assume i s his ih, by simpa [his] using measurable_add (hf i) ih)
+
 lemma measurable_neg
   [add_group α] [topological_add_group α] [measurable_space β] {f : β → α}
   (hf : measurable f) : measurable (λa, - f a) :=
@@ -201,18 +208,17 @@ lemma measurable_le {α β}
   [topological_space α] [partial_order α] [ordered_topology α] [second_countable_topology α]
   [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
   is_measurable {a | f a ≤ g a} :=
-have is_measurable {p : α × α | p.1 ≤ p.2}, from
-  is_measurable_of_is_closed (ordered_topology.is_closed_le' _),
+have is_measurable {p : α × α | p.1 ≤ p.2},
+  by rw borel_prod; exact is_measurable_of_is_closed (ordered_topology.is_closed_le' _),
 show is_measurable {a | (f a, g a).1 ≤ (f a, g a).2},
 begin
   refine measurable.preimage _ this,
-  rw ← borel_prod,
   exact measurable_prod_mk hf hg
 end
 
 -- generalize
 lemma measurable_coe_int_real : measurable (λa, a : ℤ → ℝ) :=
-assume s (hs : is_measurable s), is_measurable_of_is_open $ by trivial
+assume s (hs : is_measurable s), by trivial
 
 section ordered_topology
 variables [linear_order α] [topological_space α] [ordered_topology α] {a b c : α}