1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu Oct 11 11:56:43 2012 +0200
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Oct 11 14:38:58 2012 +0200
     1.3 @@ -476,7 +476,7 @@
     1.4    "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
     1.5    by (rule measurable_compose[OF measurable_Pair]) auto
     1.6  
     1.7 -lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
     1.8 +lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst':
     1.9    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
    1.10    shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
    1.11  using f proof induct
    1.12 @@ -512,7 +512,7 @@
    1.13  qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add
    1.14                     positive_integral_monotone_convergence_SUP
    1.15                     measurable_compose_Pair1 positive_integral_positive
    1.16 -                   borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def
    1.17 +                   borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
    1.18                cong: positive_integral_cong)
    1.19  
    1.20  lemma (in pair_sigma_finite) positive_integral_fst_measurable:
    1.21 @@ -521,10 +521,21 @@
    1.22        (is "?C f \<in> borel_measurable M1")
    1.23      and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
    1.24    using f
    1.25 -    borel_measurable_positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
    1.26 +    borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
    1.27      positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
    1.28    unfolding positive_integral_max_0 by auto
    1.29  
    1.30 +lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
    1.31 +  "(\<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"
    1.32 +  using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
    1.33 +
    1.34 +lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
    1.35 +  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"
    1.36 +proof -
    1.37 +  interpret Q: pair_sigma_finite M2 M1 by default
    1.38 +  from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
    1.39 +qed
    1.40 +
    1.41  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
    1.42    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
    1.43    shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"

     2.1 --- a/src/HOL/Probability/Information.thy	Thu Oct 11 11:56:43 2012 +0200
     2.2 +++ b/src/HOL/Probability/Information.thy	Thu Oct 11 14:38:58 2012 +0200
     2.3 @@ -1007,17 +1007,6 @@
     2.4    "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
     2.5      (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
     2.6  
     2.7 -lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
     2.8 -  "(\<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"
     2.9 -  using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
    2.10 -
    2.11 -lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
    2.12 -  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"
    2.13 -proof -
    2.14 -  interpret Q: pair_sigma_finite M2 M1 by default
    2.15 -  from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
    2.16 -qed
    2.17 -
    2.18  lemma (in information_space)
    2.19    assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
    2.20    assumes Px: "distributed M S X Px"