1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:34 2012 +0200
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:34 2012 +0200
     1.3 @@ -331,7 +331,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -sublocale pair_sigma_finite \<subseteq> sigma_finite_measure "M1 \<Otimes>\<^isub>M M2"
     1.8 +sublocale pair_sigma_finite \<subseteq> P: sigma_finite_measure "M1 \<Otimes>\<^isub>M M2"
     1.9  proof
    1.10    from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
    1.11    show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets (M1 \<Otimes>\<^isub>M M2) \<and> (\<Union>i. F i) = space (M1 \<Otimes>\<^isub>M M2) \<and> (\<forall>i. emeasure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<infinity>)"
    1.12 @@ -472,105 +472,58 @@
    1.13  
    1.14  section "Fubinis theorem"
    1.15  
    1.16 -lemma (in pair_sigma_finite) simple_function_cut:
    1.17 -  assumes f: "simple_function (M1 \<Otimes>\<^isub>M M2) f" "\<And>x. 0 \<le> f x"
    1.18 -  shows "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
    1.19 -    and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
    1.20 -proof -
    1.21 -  have f_borel: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
    1.22 -    using f(1) by (rule borel_measurable_simple_function)
    1.23 -  let ?F = "\<lambda>z. f -` {z} \<inter> space (M1 \<Otimes>\<^isub>M M2)"
    1.24 -  let ?F' = "\<lambda>x z. Pair x -` ?F z"
    1.25 -  { fix x assume "x \<in> space M1"
    1.26 -    have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y"
    1.27 -      by (auto simp: indicator_def)
    1.28 -    have "\<And>y. y \<in> space M2 \<Longrightarrow> (x, y) \<in> space (M1 \<Otimes>\<^isub>M M2)" using `x \<in> space M1`
    1.29 -      by (simp add: space_pair_measure)
    1.30 -    moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel
    1.31 -      by (rule sets_Pair1[OF measurable_sets]) auto
    1.32 -    ultimately have "simple_function M2 (\<lambda> y. f (x, y))"
    1.33 -      apply (rule_tac simple_function_cong[THEN iffD2, OF _])
    1.34 -      apply (rule simple_function_indicator_representation[OF f(1)])
    1.35 -      using `x \<in> space M1` by auto }
    1.36 -  note M2_sf = this
    1.37 -  { fix x assume x: "x \<in> space M1"
    1.38 -    then have "(\<integral>\<^isup>+y. f (x, y) \<partial>M2) = (\<Sum>z\<in>f ` space (M1 \<Otimes>\<^isub>M M2). z * emeasure M2 (?F' x z))"
    1.39 -      unfolding positive_integral_eq_simple_integral[OF M2_sf[OF x] f(2)]
    1.40 -      unfolding simple_integral_def
    1.41 -    proof (safe intro!: setsum_mono_zero_cong_left)
    1.42 -      from f(1) show "finite (f ` space (M1 \<Otimes>\<^isub>M M2))" by (rule simple_functionD)
    1.43 -    next
    1.44 -      fix y assume "y \<in> space M2" then show "f (x, y) \<in> f ` space (M1 \<Otimes>\<^isub>M M2)"
    1.45 -        using `x \<in> space M1` by (auto simp: space_pair_measure)
    1.46 -    next
    1.47 -      fix x' y assume "(x', y) \<in> space (M1 \<Otimes>\<^isub>M M2)"
    1.48 -        "f (x', y) \<notin> (\<lambda>y. f (x, y)) ` space M2"
    1.49 -      then have *: "?F' x (f (x', y)) = {}"
    1.50 -        by (force simp: space_pair_measure)
    1.51 -      show  "f (x', y) * emeasure M2 (?F' x (f (x', y))) = 0"
    1.52 -        unfolding * by simp
    1.53 -    qed (simp add: vimage_compose[symmetric] comp_def
    1.54 -                   space_pair_measure) }
    1.55 -  note eq = this
    1.56 -  moreover have "\<And>z. ?F z \<in> sets (M1 \<Otimes>\<^isub>M M2)"
    1.57 -    by (auto intro!: f_borel borel_measurable_vimage)
    1.58 -  moreover then have "\<And>z. (\<lambda>x. emeasure M2 (?F' x z)) \<in> borel_measurable M1"
    1.59 -    by (auto intro!: measurable_emeasure_Pair1 simp del: vimage_Int)
    1.60 -  moreover have *: "\<And>i x. 0 \<le> emeasure M2 (Pair x -` (f -` {i} \<inter> space (M1 \<Otimes>\<^isub>M M2)))"
    1.61 -    using f(1)[THEN simple_functionD(2)] f(2) by (intro emeasure_nonneg)
    1.62 -  moreover { fix i assume "i \<in> f`space (M1 \<Otimes>\<^isub>M M2)"
    1.63 -    with * have "\<And>x. 0 \<le> i * emeasure M2 (Pair x -` (f -` {i} \<inter> space (M1 \<Otimes>\<^isub>M M2)))"
    1.64 -      using f(2) by auto }
    1.65 -  ultimately
    1.66 -  show "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
    1.67 -    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(2)
    1.68 -    by (auto simp del: vimage_Int cong: measurable_cong intro!: setsum_cong
    1.69 -             simp add: positive_integral_setsum simple_integral_def
    1.70 -                       positive_integral_cmult
    1.71 -                       positive_integral_cong[OF eq]
    1.72 -                       positive_integral_eq_simple_integral[OF f]
    1.73 -                       M2.emeasure_pair_measure_alt[symmetric])
    1.74 -qed
    1.75 +lemma measurable_compose_Pair1:
    1.76 +  "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.77 +  by (rule measurable_compose[OF measurable_Pair]) auto
    1.78 +
    1.79 +lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
    1.80 +  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
    1.81 +  shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
    1.82 +using f proof induct
    1.83 +  case (cong u v)
    1.84 +  then have "\<And>w x. w \<in> space M1 \<Longrightarrow> x \<in> space M2 \<Longrightarrow> u (w, x) = v (w, x)"
    1.85 +    by (auto simp: space_pair_measure)
    1.86 +  show ?case
    1.87 +    apply (subst measurable_cong)
    1.88 +    apply (rule positive_integral_cong)
    1.89 +    apply fact+
    1.90 +    done
    1.91 +next
    1.92 +  case (set Q)
    1.93 +  have [simp]: "\<And>x y. indicator Q (x, y) = indicator (Pair x -` Q) y"
    1.94 +    by (auto simp: indicator_def)
    1.95 +  have "\<And>x. x \<in> space M1 \<Longrightarrow> emeasure M2 (Pair x -` Q) = \<integral>\<^isup>+ y. indicator Q (x, y) \<partial>M2"
    1.96 +    by (simp add: sets_Pair1[OF set])
    1.97 +  from this M2.measurable_emeasure_Pair[OF set] show ?case
    1.98 +    by (rule measurable_cong[THEN iffD1])
    1.99 +qed (simp_all add: positive_integral_add positive_integral_cmult measurable_compose_Pair1
   1.100 +                   positive_integral_monotone_convergence_SUP incseq_def le_fun_def
   1.101 +              cong: measurable_cong)
   1.102 +
   1.103 +lemma (in pair_sigma_finite) positive_integral_fst:
   1.104 +  assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)" "\<And>x. 0 \<le> f x"
   1.105 +  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.106 +using f proof induct
   1.107 +  case (cong u v)
   1.108 +  moreover then have "?I u = ?I v"
   1.109 +    by (intro positive_integral_cong) (auto simp: space_pair_measure)
   1.110 +  ultimately show ?case
   1.111 +    by (simp cong: positive_integral_cong)
   1.112 +qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add
   1.113 +                   positive_integral_monotone_convergence_SUP
   1.114 +                   measurable_compose_Pair1 positive_integral_positive
   1.115 +                   borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def
   1.116 +              cong: positive_integral_cong)
   1.117  
   1.118  lemma (in pair_sigma_finite) positive_integral_fst_measurable:
   1.119    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.120    shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
   1.121        (is "?C f \<in> borel_measurable M1")
   1.122      and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
   1.123 -proof -
   1.124 -  from borel_measurable_implies_simple_function_sequence'[OF f] guess F . note F = this
   1.125 -  then have F_borel: "\<And>i. F i \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.126 -    by (auto intro: borel_measurable_simple_function)
   1.127 -  note sf = simple_function_cut[OF F(1,5)]
   1.128 -  then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
   1.129 -    using F(1) by auto
   1.130 -  moreover
   1.131 -  { fix x assume "x \<in> space M1"
   1.132 -    from F measurable_Pair2[OF F_borel `x \<in> space M1`]
   1.133 -    have "(\<integral>\<^isup>+y. (SUP i. F i (x, y)) \<partial>M2) = (SUP i. ?C (F i) x)"
   1.134 -      by (intro positive_integral_monotone_convergence_SUP)
   1.135 -         (auto simp: incseq_Suc_iff le_fun_def)
   1.136 -    then have "(SUP i. ?C (F i) x) = ?C f x"
   1.137 -      unfolding F(4) positive_integral_max_0 by simp }
   1.138 -  note SUPR_C = this
   1.139 -  ultimately show "?C f \<in> borel_measurable M1"
   1.140 -    by (simp cong: measurable_cong)
   1.141 -  have "(\<integral>\<^isup>+x. (SUP i. F i x) \<partial>(M1 \<Otimes>\<^isub>M M2)) = (SUP i. integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) (F i))"
   1.142 -    using F_borel F
   1.143 -    by (intro positive_integral_monotone_convergence_SUP) auto
   1.144 -  also have "(SUP i. integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) (F i)) = (SUP i. \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1)"
   1.145 -    unfolding sf(2) by simp
   1.146 -  also have "\<dots> = \<integral>\<^isup>+ x. (SUP i. \<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1" using F sf(1)
   1.147 -    by (intro positive_integral_monotone_convergence_SUP[symmetric])
   1.148 -       (auto intro!: positive_integral_mono positive_integral_positive
   1.149 -             simp: incseq_Suc_iff le_fun_def)
   1.150 -  also have "\<dots> = \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. (SUP i. F i (x, y)) \<partial>M2) \<partial>M1"
   1.151 -    using F_borel F(2,5)
   1.152 -    by (auto intro!: positive_integral_cong positive_integral_monotone_convergence_SUP[symmetric] measurable_Pair2
   1.153 -             simp: incseq_Suc_iff le_fun_def)
   1.154 -  finally show "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P (M1 \<Otimes>\<^isub>M M2) f"
   1.155 -    using F by (simp add: positive_integral_max_0)
   1.156 -qed
   1.157 +  using f
   1.158 +    borel_measurable_positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
   1.159 +    positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
   1.160 +  unfolding positive_integral_max_0 by auto
   1.161  
   1.162  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   1.163    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"

     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:34 2012 +0200
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:34 2012 +0200
     2.3 @@ -2320,6 +2320,11 @@
     2.4    apply (auto simp: f T)
     2.5    done
     2.6  
     2.7 +lemma integral_distr:
     2.8 +  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>L (distr M M' T) f = (\<integral> x. f (T x) \<partial>M)"
     2.9 +  unfolding lebesgue_integral_def
    2.10 +  by (subst (1 2) positive_integral_distr) auto
    2.11 +
    2.12  lemma integrable_distr_eq:
    2.13    assumes T: "T \<in> measurable M M'" "f \<in> borel_measurable M'"
    2.14    shows "integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"