# HG changeset patch
# User hoelzl
# Date 1349959138 -7200
# Node ID bb5db3d1d6dda3fb049e2cdd1786f4a2ad676ffa
# Parent  c26665a197dcf6986558fb1b610d0a2188e186cf
cleanup borel_measurable_positive_integral_(fst|snd)

diff -r c26665a197dc -r bb5db3d1d6dd src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu Oct 11 11:56:43 2012 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Oct 11 14:38:58 2012 +0200
@@ -476,7 +476,7 @@
   "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
   by (rule measurable_compose[OF measurable_Pair]) auto
 
-lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
+lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst':
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
   shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
 using f proof induct
@@ -512,7 +512,7 @@
 qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add
                    positive_integral_monotone_convergence_SUP
                    measurable_compose_Pair1 positive_integral_positive
-                   borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def
+                   borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
               cong: positive_integral_cong)
 
 lemma (in pair_sigma_finite) positive_integral_fst_measurable:
@@ -521,10 +521,21 @@
       (is "?C f \<in> borel_measurable M1")
     and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
   using f
-    borel_measurable_positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
+    borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
     positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
   unfolding positive_integral_max_0 by auto
 
+lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
+  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
+  using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
+
+lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
+  assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2"
+proof -
+  interpret Q: pair_sigma_finite M2 M1 by default
+  from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
+qed
+
 lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
diff -r c26665a197dc -r bb5db3d1d6dd src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Oct 11 11:56:43 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Thu Oct 11 14:38:58 2012 +0200
@@ -1007,17 +1007,6 @@
   "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
     (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
 
-lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
-  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
-  using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
-
-lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
-  assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2"
-proof -
-  interpret Q: pair_sigma_finite M2 M1 by default
-  from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
-qed
-
 lemma (in information_space)
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
   assumes Px: "distributed M S X Px"