src/HOL/Probability/Binary_Product_Measure.thy
changeset 50003 8c213922ed49
parent 50002 ce0d316b5b44
child 50104 de19856feb54
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
     1.5    unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
     1.6  
     1.7 -lemma pair_measureI[intro, simp]:
     1.8 +lemma pair_measureI[intro, simp, measurable]:
     1.9    "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
    1.10    by (auto simp: sets_pair_measure)
    1.11  
    1.12 @@ -61,7 +61,11 @@
    1.13    unfolding pair_measure_def using 1 2
    1.14    by (intro measurable_measure_of) (auto dest: sets_into_space)
    1.15  
    1.16 -lemma measurable_Pair:
    1.17 +lemma measurable_split_replace[measurable (raw)]:
    1.18 +  "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
    1.19 +  unfolding split_beta' .
    1.20 +
    1.21 +lemma measurable_Pair[measurable (raw)]:
    1.22    assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2"
    1.23    shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
    1.24  proof (rule measurable_pair_measureI)
    1.25 @@ -75,34 +79,38 @@
    1.26    finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
    1.27  qed
    1.28  
    1.29 +lemma measurable_Pair_compose_split[measurable_dest]:
    1.30 +  assumes f: "split f \<in> measurable (M1 \<Otimes>\<^isub>M M2) N"
    1.31 +  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
    1.32 +  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
    1.33 +  using measurable_compose[OF measurable_Pair f, OF g h] by simp
    1.34 +
    1.35  lemma measurable_pair:
    1.36    assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
    1.37    shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
    1.38    using measurable_Pair[OF assms] by simp
    1.39  
    1.40 -lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
    1.41 +lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
    1.42    by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
    1.43  
    1.44 -lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
    1.45 +lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
    1.46    by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
    1.47  
    1.48 -lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N"
    1.49 -  using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def)
    1.50 -
    1.51 -lemma measurable_snd': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. snd (f x)) \<in> measurable M P"
    1.52 -    using measurable_comp[OF _ measurable_snd] by (auto simp: comp_def)
    1.53 +lemma 
    1.54 +  assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)" 
    1.55 +  shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
    1.56 +    and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P"
    1.57 +  by simp_all
    1.58  
    1.59 -lemma measurable_fst'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
    1.60 -  using measurable_comp[OF measurable_fst _] by (auto simp: comp_def)
    1.61 -
    1.62 -lemma measurable_snd'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
    1.63 -  using measurable_comp[OF measurable_snd _] by (auto simp: comp_def)
    1.64 +lemma
    1.65 +  assumes f[measurable]: "f \<in> measurable M N"
    1.66 +  shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
    1.67 +    and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
    1.68 +  by simp_all
    1.69  
    1.70  lemma measurable_pair_iff:
    1.71    "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
    1.72 -  using measurable_pair[of f M M1 M2]
    1.73 -  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
    1.74 -  by auto
    1.75 +  by (auto intro: measurable_pair[of f M M1 M2]) 
    1.76  
    1.77  lemma measurable_split_conv:
    1.78    "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
    1.79 @@ -117,16 +125,13 @@
    1.80  
    1.81  lemma measurable_pair_swap_iff:
    1.82    "f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M"
    1.83 -  using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"]
    1.84 -  by (auto intro!: measurable_pair_swap)
    1.85 -
    1.86 -lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
    1.87 -  unfolding measurable_def by auto
    1.88 +  by (auto dest: measurable_pair_swap)
    1.89  
    1.90  lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)"
    1.91 -  by (auto intro!: measurable_Pair)
    1.92 +  by simp
    1.93  
    1.94 -lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
    1.95 +lemma sets_Pair1[measurable (raw)]:
    1.96 +  assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
    1.97  proof -
    1.98    have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
    1.99      using A[THEN sets_into_space] by (auto simp: space_pair_measure)
   1.100 @@ -163,8 +168,11 @@
   1.101    unfolding Int_stable_def
   1.102    by safe (auto simp add: times_Int_times)
   1.103  
   1.104 +lemma disjoint_family_vimageI: "disjoint_family F \<Longrightarrow> disjoint_family (\<lambda>i. f -` F i)"
   1.105 +  by (auto simp: disjoint_family_on_def)
   1.106 +
   1.107  lemma (in finite_measure) finite_measure_cut_measurable:
   1.108 -  assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
   1.109 +  assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^isub>M M)"
   1.110    shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
   1.111      (is "?s Q \<in> _")
   1.112    using Int_stable_pair_measure_generator pair_measure_closed assms
   1.113 @@ -179,11 +187,10 @@
   1.114      by (auto intro!: measurable_If simp: space_pair_measure)
   1.115  next
   1.116    case (union F)
   1.117 -  moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
   1.118 -    unfolding sets_pair_measure[symmetric]
   1.119 -    by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
   1.120 +  moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
   1.121 +    by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
   1.122    ultimately show ?case
   1.123 -    by (auto simp: vimage_UN)
   1.124 +    unfolding sets_pair_measure[symmetric] by simp
   1.125  qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
   1.126  
   1.127  lemma (in sigma_finite_measure) measurable_emeasure_Pair:
   1.128 @@ -226,6 +233,17 @@
   1.129      by auto
   1.130  qed
   1.131  
   1.132 +lemma (in sigma_finite_measure) measurable_emeasure[measurable (raw)]:
   1.133 +  assumes space: "\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M"
   1.134 +  assumes A: "{x\<in>space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^isub>M M)"
   1.135 +  shows "(\<lambda>x. emeasure M (A x)) \<in> borel_measurable N"
   1.136 +proof -
   1.137 +  from space have "\<And>x. x \<in> space N \<Longrightarrow> Pair x -` {x \<in> space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} = A x"
   1.138 +    by (auto simp: space_pair_measure)
   1.139 +  with measurable_emeasure_Pair[OF A] show ?thesis
   1.140 +    by (auto cong: measurable_cong)
   1.141 +qed
   1.142 +
   1.143  lemma (in sigma_finite_measure) emeasure_pair_measure:
   1.144    assumes "X \<in> sets (N \<Otimes>\<^isub>M M)"
   1.145    shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
   1.146 @@ -476,7 +494,7 @@
   1.147  
   1.148  lemma measurable_compose_Pair1:
   1.149    "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.150 -  by (rule measurable_compose[OF measurable_Pair]) auto
   1.151 +  by simp
   1.152  
   1.153  lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
   1.154    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)" "\<And>x. 0 \<le> f x"
   1.155 @@ -527,9 +545,13 @@
   1.156      positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
   1.157    unfolding positive_integral_max_0 by auto
   1.158  
   1.159 -lemma (in sigma_finite_measure) borel_measurable_positive_integral:
   1.160 -  "(\<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.161 -  using positive_integral_fst_measurable(1)[of "split f" M1] by simp
   1.162 +lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
   1.163 +  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable N"
   1.164 +  using positive_integral_fst_measurable(1)[of "split f" N] by simp
   1.165 +
   1.166 +lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
   1.167 +  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M) \<in> borel_measurable N"
   1.168 +  by (simp add: lebesgue_integral_def)
   1.169  
   1.170  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   1.171    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.172 @@ -650,29 +672,6 @@
   1.173      by simp
   1.174  qed
   1.175  
   1.176 -lemma (in pair_sigma_finite) positive_integral_fst_measurable':
   1.177 -  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.178 -  shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
   1.179 -  using M2.positive_integral_fst_measurable(1)[OF f] by simp
   1.180 -
   1.181 -lemma (in pair_sigma_finite) integral_fst_measurable:
   1.182 -  "(\<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.183 -  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_fst_measurable')
   1.184 -
   1.185 -lemma (in pair_sigma_finite) positive_integral_snd_measurable':
   1.186 -  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.187 -  shows "(\<lambda>y. \<integral>\<^isup>+ x. f x y \<partial>M1) \<in> borel_measurable M2"
   1.188 -proof -
   1.189 -  interpret Q: pair_sigma_finite M2 M1 ..
   1.190 -  show ?thesis
   1.191 -    using measurable_pair_swap[OF f]
   1.192 -    by (intro Q.positive_integral_fst_measurable') (simp add: split_beta')
   1.193 -qed
   1.194 -
   1.195 -lemma (in pair_sigma_finite) integral_snd_measurable:
   1.196 -  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>y. \<integral> x. f x y \<partial>M1) \<in> borel_measurable M2"
   1.197 -  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_snd_measurable')
   1.198 -
   1.199  lemma (in pair_sigma_finite) Fubini_integral:
   1.200    assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f"
   1.201    shows "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1)"
   1.202 @@ -739,48 +738,21 @@
   1.203  lemma pair_measure_density:
   1.204    assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
   1.205    assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x"
   1.206 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
   1.207 -  assumes "sigma_finite_measure (density M1 f)" "sigma_finite_measure (density M2 g)"
   1.208 +  assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)"
   1.209    shows "density M1 f \<Otimes>\<^isub>M density M2 g = density (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x,y). f x * g y)" (is "?L = ?R")
   1.210  proof (rule measure_eqI)
   1.211 -  interpret M1: sigma_finite_measure M1 by fact
   1.212    interpret M2: sigma_finite_measure M2 by fact
   1.213 -  interpret D1: sigma_finite_measure "density M1 f" by fact
   1.214    interpret D2: sigma_finite_measure "density M2 g" by fact
   1.215 -  interpret L: pair_sigma_finite "density M1 f" "density M2 g" ..
   1.216 -  interpret R: pair_sigma_finite M1 M2 ..
   1.217  
   1.218    fix A assume A: "A \<in> sets ?L"
   1.219 -  then have indicator_eq: "\<And>x y. indicator A (x, y) = indicator (Pair x -` A) y"
   1.220 -   and Pair_A: "\<And>x. Pair x -` A \<in> sets M2"
   1.221 -    by (auto simp: indicator_def sets_Pair1)
   1.222 -  have f_fst: "(\<lambda>p. f (fst p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.223 -    using measurable_comp[OF measurable_fst f(1)] by (simp add: comp_def)
   1.224 -  have g_snd: "(\<lambda>p. g (snd p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
   1.225 -    using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def)
   1.226 -  have "(\<lambda>x. \<integral>\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
   1.227 -    using g_snd Pair_A A by (intro M2.positive_integral_fst_measurable) auto
   1.228 -  then have int_g: "(\<lambda>x. \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
   1.229 -    by simp
   1.230 -
   1.231 -  show "emeasure ?L A = emeasure ?R A"
   1.232 -    apply (subst D2.emeasure_pair_measure[OF A])
   1.233 -    apply (subst emeasure_density)
   1.234 -        using f_fst g_snd apply (simp add: split_beta')
   1.235 -      using A apply simp
   1.236 -    apply (subst positive_integral_density[OF g])
   1.237 -      apply (simp add: indicator_eq Pair_A)
   1.238 -    apply (subst positive_integral_density[OF f])
   1.239 -      apply (rule int_g)
   1.240 -    apply (subst M2.positive_integral_fst_measurable(2)[symmetric])
   1.241 -      using f g A Pair_A f_fst g_snd
   1.242 -      apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1
   1.243 -                  simp: positive_integral_cmult indicator_eq split_beta')
   1.244 -    apply (intro AE_I2 impI)
   1.245 -    apply (subst mult_assoc)
   1.246 -    apply (subst positive_integral_cmult)
   1.247 -          apply auto
   1.248 -    done
   1.249 +  with f g have "(\<integral>\<^isup>+ x. f x * \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
   1.250 +    (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
   1.251 +    by (intro positive_integral_cong_AE)
   1.252 +       (auto simp add: positive_integral_cmult[symmetric] ac_simps)
   1.253 +  with A f g show "emeasure ?L A = emeasure ?R A"
   1.254 +    by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
   1.255 +                  M2.positive_integral_fst_measurable(2)[symmetric]
   1.256 +             cong: positive_integral_cong)
   1.257  qed simp
   1.258  
   1.259  lemma sigma_finite_measure_distr:
   1.260 @@ -792,7 +764,7 @@
   1.261    show ?thesis
   1.262    proof (unfold_locales, intro conjI exI allI)
   1.263      show "range (\<lambda>i. f -` A i \<inter> space M) \<subseteq> sets M"
   1.264 -      using A f by (auto intro!: measurable_sets)
   1.265 +      using A f by auto
   1.266      show "(\<Union>i. f -` A i \<inter> space M) = space M"
   1.267        using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def)
   1.268      fix i show "emeasure M (f -` A i \<inter> space M) \<noteq> \<infinity>"
   1.269 @@ -800,47 +772,19 @@
   1.270    qed
   1.271  qed
   1.272  
   1.273 -lemma measurable_cong':
   1.274 -  assumes sets: "sets M = sets M'" "sets N = sets N'"
   1.275 -  shows "measurable M N = measurable M' N'"
   1.276 -  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
   1.277 -
   1.278  lemma pair_measure_distr:
   1.279    assumes f: "f \<in> measurable M S" and g: "g \<in> measurable N T"
   1.280 -  assumes "sigma_finite_measure (distr M S f)" "sigma_finite_measure (distr N T g)"
   1.281 +  assumes "sigma_finite_measure (distr N T g)"
   1.282    shows "distr M S f \<Otimes>\<^isub>M distr N T g = distr (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). (f x, g y))" (is "?P = ?D")
   1.283  proof (rule measure_eqI)
   1.284 -  show "sets ?P = sets ?D"
   1.285 -    by simp
   1.286 -  interpret S: sigma_finite_measure "distr M S f" by fact
   1.287    interpret T: sigma_finite_measure "distr N T g" by fact
   1.288 -  interpret ST: pair_sigma_finite "distr M S f"  "distr N T g" ..
   1.289 -  interpret M: sigma_finite_measure M by (rule sigma_finite_measure_distr) fact+
   1.290    interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+
   1.291 -  interpret MN: pair_sigma_finite M N ..
   1.292 -  interpret SN: pair_sigma_finite "distr M S f" N ..
   1.293 -  have [simp]: 
   1.294 -    "\<And>f g. fst \<circ> (\<lambda>(x, y). (f x, g y)) = f \<circ> fst" "\<And>f g. snd \<circ> (\<lambda>(x, y). (f x, g y)) = g \<circ> snd"
   1.295 -    by auto
   1.296 -  then have fg: "(\<lambda>(x, y). (f x, g y)) \<in> measurable (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T)"
   1.297 -    using measurable_comp[OF measurable_fst f] measurable_comp[OF measurable_snd g]
   1.298 -    by (auto simp: measurable_pair_iff)
   1.299 +
   1.300    fix A assume A: "A \<in> sets ?P"
   1.301 -  then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \<partial>distr M S f)"
   1.302 -    by (rule T.emeasure_pair_measure_alt)
   1.303 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair x -` A) \<inter> space N) \<partial>distr M S f)"
   1.304 -    using g A by (simp add: sets_Pair1 emeasure_distr)
   1.305 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \<inter> space N) \<partial>M)"
   1.306 -    using f g A ST.measurable_emeasure_Pair1[OF A]
   1.307 -    by (intro positive_integral_distr) (auto simp add: sets_Pair1 emeasure_distr)
   1.308 -  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x -` ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)"
   1.309 -    by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure)
   1.310 -  also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))"
   1.311 -    using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
   1.312 -                (auto cong: measurable_cong')
   1.313 -  also have "\<dots> = emeasure ?D A"
   1.314 -    using fg A by (subst emeasure_distr) auto
   1.315 -  finally show "emeasure ?P A = emeasure ?D A" .
   1.316 -qed
   1.317 +  with f g show "emeasure ?P A = emeasure ?D A"
   1.318 +    by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
   1.319 +                       T.emeasure_pair_measure_alt positive_integral_distr
   1.320 +             intro!: positive_integral_cong arg_cong[where f="emeasure N"])
   1.321 +qed simp
   1.322  
   1.323  end
   1.324 \ No newline at end of file