src/HOL/Probability/Binary_Product_Measure.thy
changeset 49999 dfb63b9b8908
parent 49825 bb5db3d1d6dd
child 50002 ce0d316b5b44
     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')