--- 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:
--- 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: