author hoelzl Fri Nov 02 14:00:39 2012 +0100 (2012-11-02) changeset 49999 dfb63b9b8908 parent 49998 ad8a6db0b480 child 50000 cfe8ee8a1371
for the product measure it is enough if only one measure is sigma-finite
```     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 12:00:51 2012 +0100
1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
1.3 @@ -476,12 +476,12 @@
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 -  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
1.9 -  shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
1.10 +lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
1.11 +  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)" "\<And>x. 0 \<le> f x"
1.12 +  shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M) \<in> borel_measurable M1"
1.13  using f proof induct
1.14    case (cong u v)
1.15 -  then have "\<And>w x. w \<in> space M1 \<Longrightarrow> x \<in> space M2 \<Longrightarrow> u (w, x) = v (w, x)"
1.16 +  then have "\<And>w x. w \<in> space M1 \<Longrightarrow> x \<in> space M \<Longrightarrow> u (w, x) = v (w, x)"
1.17      by (auto simp: space_pair_measure)
1.18    show ?case
1.19      apply (subst measurable_cong)
1.20 @@ -492,57 +492,49 @@
1.21    case (set Q)
1.22    have [simp]: "\<And>x y. indicator Q (x, y) = indicator (Pair x -` Q) y"
1.23      by (auto simp: indicator_def)
1.24 -  have "\<And>x. x \<in> space M1 \<Longrightarrow> emeasure M2 (Pair x -` Q) = \<integral>\<^isup>+ y. indicator Q (x, y) \<partial>M2"
1.25 +  have "\<And>x. x \<in> space M1 \<Longrightarrow> emeasure M (Pair x -` Q) = \<integral>\<^isup>+ y. indicator Q (x, y) \<partial>M"
1.26      by (simp add: sets_Pair1[OF set])
1.27 -  from this M2.measurable_emeasure_Pair[OF set] show ?case
1.28 +  from this measurable_emeasure_Pair[OF set] show ?case
1.29      by (rule measurable_cong[THEN iffD1])
1.30  qed (simp_all add: positive_integral_add positive_integral_cmult measurable_compose_Pair1
1.31                     positive_integral_monotone_convergence_SUP incseq_def le_fun_def
1.32                cong: measurable_cong)
1.33
1.34 -lemma (in pair_sigma_finite) positive_integral_fst:
1.35 -  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
1.36 -  shows "(\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2 \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f" (is "?I f = _")
1.37 +lemma (in sigma_finite_measure) positive_integral_fst:
1.38 +  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)" "\<And>x. 0 \<le> f x"
1.39 +  shows "(\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M) f" (is "?I f = _")
1.40  using f proof induct
1.41    case (cong u v)
1.42    moreover then have "?I u = ?I v"
1.43      by (intro positive_integral_cong) (auto simp: space_pair_measure)
1.44    ultimately show ?case
1.45      by (simp cong: positive_integral_cong)
1.46 -qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add
1.47 +qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
1.48                     positive_integral_monotone_convergence_SUP
1.49                     measurable_compose_Pair1 positive_integral_positive
1.50                     borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
1.51                cong: positive_integral_cong)
1.52
1.53 -lemma (in pair_sigma_finite) positive_integral_fst_measurable:
1.54 -  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.55 -  shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
1.56 +lemma (in sigma_finite_measure) positive_integral_fst_measurable:
1.57 +  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)"
1.58 +  shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M) \<in> borel_measurable M1"
1.59        (is "?C f \<in> borel_measurable M1")
1.60 -    and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
1.61 +    and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M) f"
1.62    using f
1.63      borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
1.64      positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
1.65    unfolding positive_integral_max_0 by auto
1.66
1.67 -lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
1.68 -  "(\<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.69 -  using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
1.70 -
1.71 -lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
1.72 -  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.73 -proof -
1.74 -  interpret Q: pair_sigma_finite M2 M1 by default
1.75 -  from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
1.76 -qed
1.77 +lemma (in sigma_finite_measure) borel_measurable_positive_integral:
1.78 +  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable M1"
1.79 +  using positive_integral_fst_measurable(1)[of "split f" M1] by simp
1.80
1.81  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
1.82    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.83    shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
1.84  proof -
1.85 -  interpret Q: pair_sigma_finite M2 M1 by default
1.86    note measurable_pair_swap[OF f]
1.87 -  from Q.positive_integral_fst_measurable[OF this]
1.88 +  from M1.positive_integral_fst_measurable[OF this]
1.89    have "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^isub>M M1))"
1.90      by simp
1.91    also have "(\<integral>\<^isup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
1.92 @@ -555,7 +547,7 @@
1.93    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.94    shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
1.95    unfolding positive_integral_snd_measurable[OF assms]
1.96 -  unfolding positive_integral_fst_measurable[OF assms] ..
1.97 +  unfolding M2.positive_integral_fst_measurable[OF assms] ..
1.98
1.99  lemma (in pair_sigma_finite) integrable_product_swap:
1.100    assumes "integrable (M1 \<Otimes>\<^isub>M M2) f"
1.101 @@ -599,9 +591,9 @@
1.102      using assms by auto
1.103    have "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>"
1.104       "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (- f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>"
1.105 -    using borel[THEN positive_integral_fst_measurable(1)] int
1.106 -    unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all
1.107 -  with borel[THEN positive_integral_fst_measurable(1)]
1.108 +    using borel[THEN M2.positive_integral_fst_measurable(1)] int
1.109 +    unfolding borel[THEN M2.positive_integral_fst_measurable(2)] by simp_all
1.110 +  with borel[THEN M2.positive_integral_fst_measurable(1)]
1.111    have AE_pos: "AE x in M1. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
1.112      "AE x in M1. (\<integral>\<^isup>+y. ereal (- f (x, y)) \<partial>M2) \<noteq> \<infinity>"
1.113      by (auto intro!: positive_integral_PInf_AE )
1.114 @@ -621,12 +613,12 @@
1.115      have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
1.116      proof (intro integrable_def[THEN iffD2] conjI)
1.117        show "?f \<in> borel_measurable M1"
1.118 -        using borel by (auto intro!: positive_integral_fst_measurable)
1.119 +        using borel by (auto intro!: M2.positive_integral_fst_measurable)
1.120        have "(\<integral>\<^isup>+x. ereal (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (f (x, y))  \<partial>M2) \<partial>M1)"
1.121          using AE positive_integral_positive[of M2]
1.122          by (auto intro!: positive_integral_cong_AE simp: ereal_real)
1.123        then show "(\<integral>\<^isup>+x. ereal (?f x) \<partial>M1) \<noteq> \<infinity>"
1.124 -        using positive_integral_fst_measurable[OF borel] int by simp
1.125 +        using M2.positive_integral_fst_measurable[OF borel] int by simp
1.126        have "(\<integral>\<^isup>+x. ereal (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
1.127          by (intro positive_integral_cong_pos)
1.128             (simp add: positive_integral_positive real_of_ereal_pos)
1.129 @@ -635,7 +627,7 @@
1.130    with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)]
1.131    show ?INT
1.132      unfolding lebesgue_integral_def[of "M1 \<Otimes>\<^isub>M M2"] lebesgue_integral_def[of M2]
1.133 -      borel[THEN positive_integral_fst_measurable(2), symmetric]
1.134 +      borel[THEN M2.positive_integral_fst_measurable(2), symmetric]
1.135      using AE[THEN integral_real]
1.136      by simp
1.137  qed
1.138 @@ -659,7 +651,7 @@
1.139  lemma (in pair_sigma_finite) positive_integral_fst_measurable':
1.140    assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.141    shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
1.142 -  using positive_integral_fst_measurable(1)[OF f] by simp
1.143 +  using M2.positive_integral_fst_measurable(1)[OF f] by simp
1.144
1.145  lemma (in pair_sigma_finite) integral_fst_measurable:
1.146    "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M2) \<in> borel_measurable M1"
1.147 @@ -765,7 +757,7 @@
1.148    have g_snd: "(\<lambda>p. g (snd p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
1.149      using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def)
1.150    have "(\<lambda>x. \<integral>\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
1.151 -    using g_snd Pair_A A by (intro R.positive_integral_fst_measurable) auto
1.152 +    using g_snd Pair_A A by (intro M2.positive_integral_fst_measurable) auto
1.153    then have int_g: "(\<lambda>x. \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
1.154      by simp
1.155
1.156 @@ -778,7 +770,7 @@
1.157        apply (simp add: indicator_eq Pair_A)
1.158      apply (subst positive_integral_density[OF f])
1.159        apply (rule int_g)
1.160 -    apply (subst R.positive_integral_fst_measurable(2)[symmetric])
1.161 +    apply (subst M2.positive_integral_fst_measurable(2)[symmetric])
1.162        using f g A Pair_A f_fst g_snd
1.163        apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1
1.164                    simp: positive_integral_cmult indicator_eq split_beta')
```
```     2.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 12:00:51 2012 +0100
2.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
2.3 @@ -795,7 +795,7 @@
2.4    show ?thesis
2.5      apply (subst distr_merge[OF IJ, symmetric])
2.6      apply (subst positive_integral_distr[OF measurable_merge f])
2.7 -    apply (subst P.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
2.8 +    apply (subst J.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
2.9      apply simp
2.10      done
2.11  qed
```
```     3.1 --- a/src/HOL/Probability/Information.thy	Fri Nov 02 12:00:51 2012 +0100
3.2 +++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:00:39 2012 +0100
3.3 @@ -1128,8 +1128,8 @@
3.4      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
3.5      apply (intro TP.AE_pair_measure)
3.6      apply (auto simp: comp_def measurable_split_conv
3.7 -                intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
3.8 -                        SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
3.9 +                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
3.10 +                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
3.11                          measurable_Pair
3.12                  dest: distributed_real_AE distributed_real_measurable)
3.13      done
3.14 @@ -1142,7 +1142,7 @@
3.15             measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
3.16             measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
3.17             measurable_compose[OF _ Px[THEN distributed_real_measurable]]
3.18 -           STP.borel_measurable_positive_integral_snd
3.19 +           TP.borel_measurable_positive_integral
3.20    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
3.21      apply (subst positive_integral_density)
3.22      apply (rule distributed_borel_measurable[OF Pxyz])
3.23 @@ -1418,8 +1418,8 @@
3.24      using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
3.25      apply (intro TP.AE_pair_measure)
3.26      apply (auto simp: comp_def measurable_split_conv
3.27 -                intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
3.28 -                        SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
3.29 +                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
3.30 +                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
3.31                          measurable_Pair
3.32                  dest: distributed_real_AE distributed_real_measurable)
3.33      done
3.34 @@ -1432,7 +1432,7 @@
3.35             measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
3.36             measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
3.37             measurable_compose[OF _ Px[THEN distributed_real_measurable]]
3.38 -           STP.borel_measurable_positive_integral_snd
3.39 +           TP.borel_measurable_positive_integral
3.40    have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
3.41      apply (subst positive_integral_density)
3.42      apply (rule distributed_borel_measurable[OF Pxyz])
```