# HG changeset patch
# User Andreas Lochbihler
# Date 1429013631 -7200
# Node ID 14efa7f4ee7b440fdb166d84e77431e1c83788f5
# Parent  390de6d3a7b8eae8c1b68381e9896903e45d9120
add lemmas

diff -r 390de6d3a7b8 -r 14efa7f4ee7b src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Apr 14 14:13:06 2015 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Apr 14 14:13:51 2015 +0200
@@ -1056,6 +1056,13 @@
   finally show ?thesis .
 qed
 
+lemma measurable_pair_measure_countable1:
+  assumes "countable A"
+  and [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N K"
+  shows "f \<in> measurable (count_space A \<Otimes>\<^sub>M N) K"
+using _ _ assms(1)
+by(rule measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all
+
 subsection {* Product of Borel spaces *}
 
 lemma borel_Times:
diff -r 390de6d3a7b8 -r 14efa7f4ee7b src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Tue Apr 14 14:13:06 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Apr 14 14:13:51 2015 +0200
@@ -1875,6 +1875,15 @@
   qed
 qed (simp add: integrable_restrict_space)
 
+lemma integral_empty:
+  assumes "space M = {}"
+  shows "integral\<^sup>L M f = 0"
+proof -
+  have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
+    by(rule integral_cong)(simp_all add: assms)
+  thus ?thesis by simp
+qed
+
 subsection {* Measure spaces with an associated density *}
 
 lemma integrable_density: