merge should operate on pairs
authorhoelzl
Wed Oct 10 12:12:21 2012 +0200 (2012-10-10)
changeset 4978092a58f80b20c
parent 49779 1484b4b82855
child 49781 59b219ca3513
merge should operate on pairs
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:20 2012 +0200
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 10 12:12:21 2012 +0200
     1.3 @@ -44,45 +44,45 @@
     1.4    unfolding extensional_def by auto
     1.5  
     1.6  definition
     1.7 -  "merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
     1.8 +  "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
     1.9  
    1.10  lemma merge_apply[simp]:
    1.11 -  "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
    1.12 -  "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
    1.13 -  "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
    1.14 -  "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
    1.15 -  "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I x J y i = undefined"
    1.16 +  "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
    1.17 +  "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
    1.18 +  "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
    1.19 +  "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
    1.20 +  "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined"
    1.21    unfolding merge_def by auto
    1.22  
    1.23  lemma merge_commute:
    1.24 -  "I \<inter> J = {} \<Longrightarrow> merge I x J y = merge J y I x"
    1.25 +  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
    1.26    by (auto simp: merge_def intro!: ext)
    1.27  
    1.28  lemma Pi_cancel_merge_range[simp]:
    1.29 -  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
    1.30 -  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
    1.31 -  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
    1.32 -  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
    1.33 +  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    1.34 +  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
    1.35 +  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
    1.36 +  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
    1.37    by (auto simp: Pi_def)
    1.38  
    1.39  lemma Pi_cancel_merge[simp]:
    1.40 -  "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    1.41 -  "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    1.42 -  "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    1.43 -  "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    1.44 +  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    1.45 +  "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
    1.46 +  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    1.47 +  "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
    1.48    by (auto simp: Pi_def)
    1.49  
    1.50 -lemma extensional_merge[simp]: "merge I x J y \<in> extensional (I \<union> J)"
    1.51 +lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
    1.52    by (auto simp: extensional_def)
    1.53  
    1.54  lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
    1.55    by (auto simp: restrict_def Pi_def)
    1.56  
    1.57  lemma restrict_merge[simp]:
    1.58 -  "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
    1.59 -  "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
    1.60 -  "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
    1.61 -  "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
    1.62 +  "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    1.63 +  "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    1.64 +  "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
    1.65 +  "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
    1.66    by (auto simp: restrict_def)
    1.67  
    1.68  lemma extensional_insert_undefined[intro, simp]:
    1.69 @@ -95,7 +95,7 @@
    1.70    shows "a \<in> extensional (insert i I)"
    1.71    using assms unfolding extensional_def by auto
    1.72  
    1.73 -lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
    1.74 +lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
    1.75    unfolding merge_def by (auto simp: fun_eq_iff)
    1.76  
    1.77  lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
    1.78 @@ -118,24 +118,24 @@
    1.79  
    1.80  lemma restrict_vimage:
    1.81    assumes "I \<inter> J = {}"
    1.82 -  shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
    1.83 +  shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I J (E, F))"
    1.84    using assms by (auto simp: restrict_Pi_cancel)
    1.85  
    1.86  lemma merge_vimage:
    1.87    assumes "I \<inter> J = {}"
    1.88 -  shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
    1.89 +  shows "merge I J -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
    1.90    using assms by (auto simp: restrict_Pi_cancel)
    1.91  
    1.92  lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
    1.93    by (auto simp: restrict_def)
    1.94  
    1.95  lemma merge_restrict[simp]:
    1.96 -  "merge I (restrict x I) J y = merge I x J y"
    1.97 -  "merge I x J (restrict y J) = merge I x J y"
    1.98 +  "merge I J (restrict x I, y) = merge I J (x, y)"
    1.99 +  "merge I J (x, restrict y J) = merge I J (x, y)"
   1.100    unfolding merge_def by auto
   1.101  
   1.102  lemma merge_x_x_eq_restrict[simp]:
   1.103 -  "merge I x J x = restrict x (I \<union> J)"
   1.104 +  "merge I J (x, x) = restrict x (I \<union> J)"
   1.105    unfolding merge_def by auto
   1.106  
   1.107  lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
   1.108 @@ -518,17 +518,17 @@
   1.109  qed (auto simp: space_pair_measure space_PiM)
   1.110  
   1.111  lemma measurable_merge:
   1.112 -  "(\<lambda>(x, y). merge I x J y) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
   1.113 +  "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
   1.114      (is "?f \<in> measurable ?P ?U")
   1.115  proof (rule measurable_PiM_single)
   1.116    fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
   1.117 -  then have "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} =
   1.118 +  then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
   1.119      (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
   1.120      by (auto simp: merge_def)
   1.121    also have "\<dots> \<in> sets ?P"
   1.122      using A
   1.123      by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
   1.124 -  finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>x y. merge I x J y) \<omega> i \<in> A} \<in> sets ?P" .
   1.125 +  finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
   1.126  qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
   1.127  
   1.128  lemma measurable_restrict:
   1.129 @@ -585,29 +585,34 @@
   1.130    qed
   1.131  qed
   1.132  
   1.133 +lemma
   1.134 +  shows space_PiM_empty: "space (Pi\<^isub>M {} M) = {\<lambda>k. undefined}"
   1.135 +    and sets_PiM_empty: "sets (Pi\<^isub>M {} M) = { {}, {\<lambda>k. undefined} }"
   1.136 +  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
   1.137 +
   1.138 +lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
   1.139 +proof -
   1.140 +  let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
   1.141 +  have "emeasure (Pi\<^isub>M {} M) (prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = 1"
   1.142 +  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
   1.143 +    show "positive (PiM {} M) ?\<mu>"
   1.144 +      by (auto simp: positive_def)
   1.145 +    show "countably_additive (PiM {} M) ?\<mu>"
   1.146 +      by (rule countably_additiveI_finite)
   1.147 +         (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
   1.148 +  qed (auto simp: prod_emb_def)
   1.149 +  also have "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
   1.150 +    by (auto simp: prod_emb_def)
   1.151 +  finally show ?thesis
   1.152 +    by simp
   1.153 +qed
   1.154 +
   1.155 +lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
   1.156 +  by (rule measure_eqI) (auto simp add: sets_PiM_empty one_ereal_def)
   1.157 +
   1.158  lemma (in product_sigma_finite) emeasure_PiM:
   1.159    "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   1.160  proof (induct I arbitrary: A rule: finite_induct)
   1.161 -  case empty
   1.162 -  let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
   1.163 -  have "prod_algebra {} M = {{\<lambda>_. undefined}}"
   1.164 -    by (auto simp: prod_algebra_def prod_emb_def intro!: image_eqI)
   1.165 -  then have sets_empty: "sets (PiM {} M) = {{}, {\<lambda>_. undefined}}"
   1.166 -    by (simp add: sets_PiM)
   1.167 -  have "emeasure (Pi\<^isub>M {} M) (prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = 1"
   1.168 -  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
   1.169 -    have "finite (space (PiM {} M))"
   1.170 -      by (simp add: space_PiM)
   1.171 -    moreover show "positive (PiM {} M) ?\<mu>"
   1.172 -      by (auto simp: positive_def)
   1.173 -    ultimately show "countably_additive (PiM {} M) ?\<mu>"
   1.174 -      by (rule countably_additiveI_finite) (auto simp: additive_def space_PiM sets_empty)
   1.175 -  qed (auto simp: prod_emb_def)
   1.176 -  also have *: "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
   1.177 -    by (auto simp: prod_emb_def)
   1.178 -  finally show ?case
   1.179 -    using * by simp
   1.180 -next
   1.181    case (insert i I)
   1.182    interpret finite_product_sigma_finite M I by default fact
   1.183    have "finite (insert i I)" using `finite I` by auto
   1.184 @@ -660,7 +665,7 @@
   1.185    qed (auto intro!: setprod_cong)
   1.186    with insert show ?case
   1.187      by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
   1.188 -qed
   1.189 +qed (simp add: emeasure_PiM_empty)
   1.190  
   1.191  lemma (in product_sigma_finite) sigma_finite: 
   1.192    assumes "finite I"
   1.193 @@ -696,18 +701,6 @@
   1.194    "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^isub>M I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   1.195    using emeasure_PiM[OF finite_index] by auto
   1.196  
   1.197 -lemma (in product_sigma_finite) product_measure_empty[simp]:
   1.198 -  "emeasure (Pi\<^isub>M {} M) {\<lambda>x. undefined} = 1"
   1.199 -proof -
   1.200 -  interpret finite_product_sigma_finite M "{}" by default auto
   1.201 -  from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
   1.202 -qed
   1.203 -
   1.204 -lemma
   1.205 -  shows space_PiM_empty: "space (Pi\<^isub>M {} M) = {\<lambda>k. undefined}"
   1.206 -    and sets_PiM_empty: "sets (Pi\<^isub>M {} M) = { {}, {\<lambda>k. undefined} }"
   1.207 -  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
   1.208 -
   1.209  lemma (in product_sigma_finite) positive_integral_empty:
   1.210    assumes pos: "0 \<le> f (\<lambda>k. undefined)"
   1.211    shows "integral\<^isup>P (Pi\<^isub>M {} M) f = f (\<lambda>k. undefined)"
   1.212 @@ -727,7 +720,7 @@
   1.213  
   1.214  lemma (in product_sigma_finite) distr_merge:
   1.215    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   1.216 -  shows "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M) (\<lambda>(x,y). merge I x J y) = Pi\<^isub>M (I \<union> J) M"
   1.217 +  shows "distr (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M) (merge I J) = Pi\<^isub>M (I \<union> J) M"
   1.218     (is "?D = ?P")
   1.219  proof -
   1.220    interpret I: finite_product_sigma_finite M I by default fact
   1.221 @@ -735,7 +728,7 @@
   1.222    have "finite (I \<union> J)" using fin by auto
   1.223    interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   1.224    interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   1.225 -  let ?g = "\<lambda>(x,y). merge I x J y"
   1.226 +  let ?g = "merge I J"
   1.227  
   1.228    from IJ.sigma_finite_pairs obtain F where
   1.229      F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
   1.230 @@ -793,12 +786,12 @@
   1.231    assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   1.232    and f: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   1.233    shows "integral\<^isup>P (Pi\<^isub>M (I \<union> J) M) f =
   1.234 -    (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I x J y) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
   1.235 +    (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^isub>M J M)) \<partial>(Pi\<^isub>M I M))"
   1.236  proof -
   1.237    interpret I: finite_product_sigma_finite M I by default fact
   1.238    interpret J: finite_product_sigma_finite M J by default fact
   1.239    interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   1.240 -  have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   1.241 +  have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   1.242      using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
   1.243    show ?thesis
   1.244      apply (subst distr_merge[OF IJ, symmetric])
   1.245 @@ -833,7 +826,7 @@
   1.246  qed
   1.247  
   1.248  lemma (in product_sigma_finite) product_positive_integral_insert:
   1.249 -  assumes [simp]: "finite I" "i \<notin> I"
   1.250 +  assumes I[simp]: "finite I" "i \<notin> I"
   1.251      and f: "f \<in> borel_measurable (Pi\<^isub>M (insert i I) M)"
   1.252    shows "integral\<^isup>P (Pi\<^isub>M (insert i I) M) f = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^isub>M I M))"
   1.253  proof -
   1.254 @@ -842,17 +835,17 @@
   1.255    have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
   1.256      using f by auto
   1.257    show ?thesis
   1.258 -    unfolding product_positive_integral_fold[OF IJ, unfolded insert, simplified, OF f]
   1.259 -  proof (rule positive_integral_cong, subst product_positive_integral_singleton)
   1.260 +    unfolding product_positive_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
   1.261 +  proof (rule positive_integral_cong, subst product_positive_integral_singleton[symmetric])
   1.262      fix x assume x: "x \<in> space (Pi\<^isub>M I M)"
   1.263 -    let ?f = "\<lambda>y. f (restrict (x(i := y)) (insert i I))"
   1.264 -    have f'_eq: "\<And>y. ?f y = f (x(i := y))"
   1.265 -      using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def space_PiM)
   1.266 -    show "?f \<in> borel_measurable (M i)" unfolding f'_eq
   1.267 +    let ?f = "\<lambda>y. f (x(i := y))"
   1.268 +    show "?f \<in> borel_measurable (M i)"
   1.269        using measurable_comp[OF measurable_component_update f, OF x `i \<notin> I`]
   1.270        unfolding comp_def .
   1.271 -    show "integral\<^isup>P (M i) ?f = \<integral>\<^isup>+ y. f (x(i:=y)) \<partial>M i"
   1.272 -      unfolding f'_eq by simp
   1.273 +    show "(\<integral>\<^isup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^isub>M {i} M) = (\<integral>\<^isup>+ y. f (x(i := y i)) \<partial>Pi\<^isub>M {i} M)"
   1.274 +      using x
   1.275 +      by (auto intro!: positive_integral_cong arg_cong[where f=f]
   1.276 +               simp add: space_PiM extensional_def)
   1.277    qed
   1.278  qed
   1.279  
   1.280 @@ -895,18 +888,18 @@
   1.281  lemma (in product_sigma_finite) product_integral_fold:
   1.282    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   1.283    and f: "integrable (Pi\<^isub>M (I \<union> J) M) f"
   1.284 -  shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I x J y) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
   1.285 +  shows "integral\<^isup>L (Pi\<^isub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^isub>M J M) \<partial>Pi\<^isub>M I M)"
   1.286  proof -
   1.287    interpret I: finite_product_sigma_finite M I by default fact
   1.288    interpret J: finite_product_sigma_finite M J by default fact
   1.289    have "finite (I \<union> J)" using fin by auto
   1.290    interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   1.291    interpret P: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" by default
   1.292 -  let ?M = "\<lambda>(x, y). merge I x J y"
   1.293 +  let ?M = "merge I J"
   1.294    let ?f = "\<lambda>x. f (?M x)"
   1.295    from f have f_borel: "f \<in> borel_measurable (Pi\<^isub>M (I \<union> J) M)"
   1.296      by auto
   1.297 -  have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   1.298 +  have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   1.299      using measurable_comp[OF measurable_merge f_borel] by (simp add: comp_def)
   1.300    have f_int: "integrable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ?f"
   1.301      by (rule integrable_distr[OF measurable_merge]) (simp add: distr_merge[OF IJ fin] f)
   1.302 @@ -921,14 +914,14 @@
   1.303  lemma (in product_sigma_finite)
   1.304    assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
   1.305    shows emeasure_fold_integral:
   1.306 -    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
   1.307 +    "emeasure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. emeasure (Pi\<^isub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^isub>M J M)) \<partial>Pi\<^isub>M I M)" (is ?I)
   1.308      and emeasure_fold_measurable:
   1.309 -    "(\<lambda>x. emeasure (Pi\<^isub>M J M) (merge I x J -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
   1.310 +    "(\<lambda>x. emeasure (Pi\<^isub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^isub>M J M))) \<in> borel_measurable (Pi\<^isub>M I M)" (is ?B)
   1.311  proof -
   1.312    interpret I: finite_product_sigma_finite M I by default fact
   1.313    interpret J: finite_product_sigma_finite M J by default fact
   1.314    interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
   1.315 -  have merge: "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   1.316 +  have merge: "merge I J -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) \<in> sets (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)"
   1.317      by (intro measurable_sets[OF _ A] measurable_merge assms)
   1.318  
   1.319    show ?I
   1.320 @@ -950,7 +943,7 @@
   1.321  proof -
   1.322    have "integral\<^isup>L (Pi\<^isub>M (insert i I) M) f = integral\<^isup>L (Pi\<^isub>M (I \<union> {i}) M) f"
   1.323      by simp
   1.324 -  also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I x {i} y) \<partial>Pi\<^isub>M {i} M) \<partial>Pi\<^isub>M I M)"
   1.325 +  also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) \<partial>Pi\<^isub>M I M)"
   1.326      using f I by (intro product_integral_fold) auto
   1.327    also have "\<dots> = (\<integral>x. (\<integral>y. f (x(i := y)) \<partial>M i) \<partial>Pi\<^isub>M I M)"
   1.328    proof (rule integral_cong, subst product_integral_singleton[symmetric])
   1.329 @@ -960,7 +953,7 @@
   1.330      show "(\<lambda>y. f (x(i := y))) \<in> borel_measurable (M i)"
   1.331        using measurable_comp[OF measurable_component_update f_borel, OF x `i \<notin> I`]
   1.332        unfolding comp_def .
   1.333 -    from x I show "(\<integral> y. f (merge I x {i} y) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
   1.334 +    from x I show "(\<integral> y. f (merge I {i} (x,y)) \<partial>Pi\<^isub>M {i} M) = (\<integral> xa. f (x(i := xa i)) \<partial>Pi\<^isub>M {i} M)"
   1.335        by (auto intro!: integral_cong arg_cong[where f=f] simp: merge_def space_PiM extensional_def)
   1.336    qed
   1.337    finally show ?thesis .
   1.338 @@ -998,22 +991,24 @@
   1.339  
   1.340  lemma (in product_sigma_finite) product_integral_setprod:
   1.341    fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   1.342 -  assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   1.343 +  assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   1.344    shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^isub>M I M) = (\<Prod>i\<in>I. integral\<^isup>L (M i) (f i))"
   1.345 -using assms proof (induct rule: finite_ne_induct)
   1.346 -  case (singleton i)
   1.347 -  then show ?case by (simp add: product_integral_singleton integrable_def)
   1.348 +using assms proof induct
   1.349 +  case empty
   1.350 +  interpret finite_measure "Pi\<^isub>M {} M"
   1.351 +    by rule (simp add: space_PiM)
   1.352 +  show ?case by (simp add: space_PiM measure_def)
   1.353  next
   1.354    case (insert i I)
   1.355    then have iI: "finite (insert i I)" by auto
   1.356    then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
   1.357      integrable (Pi\<^isub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
   1.358 -    by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
   1.359 +    by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
   1.360    interpret I: finite_product_sigma_finite M I by default fact
   1.361    have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
   1.362      using `i \<notin> I` by (auto intro!: setprod_cong)
   1.363    show ?case
   1.364 -    unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
   1.365 +    unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
   1.366      by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI)
   1.367  qed
   1.368  
     2.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:20 2012 +0200
     2.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:21 2012 +0200
     2.3 @@ -14,10 +14,10 @@
     2.4  lemma restrict_restrict[simp]: "restrict (restrict f A) B = restrict f (A \<inter> B)"
     2.5    unfolding restrict_def by (simp add: fun_eq_iff)
     2.6  
     2.7 -lemma split_merge: "P (merge I x J y i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
     2.8 +lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
     2.9    unfolding merge_def by auto
    2.10  
    2.11 -lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I x J y \<in> extensional K"
    2.12 +lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
    2.13    unfolding merge_def extensional_def by auto
    2.14  
    2.15  lemma injective_vimage_restrict:
    2.16 @@ -32,7 +32,7 @@
    2.17    show "x \<in> A \<longleftrightarrow> x \<in> B"
    2.18    proof cases
    2.19      assume x: "x \<in> (\<Pi>\<^isub>E i\<in>J. S i)"
    2.20 -    have "x \<in> A \<longleftrightarrow> merge J x (I - J) y \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
    2.21 +    have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. S i)"
    2.22        using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub split: split_merge)
    2.23      then show "x \<in> A \<longleftrightarrow> x \<in> B"
    2.24        using y x `J \<subseteq> I` by (auto simp add: Pi_iff extensional_restrict extensional_merge_sub eq split: split_merge)
    2.25 @@ -131,7 +131,7 @@
    2.26    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
    2.27      using sets[THEN sets_into_space] by (auto simp: space_PiM)
    2.28    have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
    2.29 -    using M.not_empty by auto
    2.30 +      using M.not_empty by auto
    2.31    from bchoice[OF this]
    2.32    show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
    2.33    show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
    2.34 @@ -230,23 +230,19 @@
    2.35  qed
    2.36  
    2.37  lemma (in product_prob_space) merge_sets:
    2.38 -  assumes "finite J" "finite K" "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
    2.39 -  shows "merge J x K -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
    2.40 -proof -
    2.41 -  from sets_Pair1[OF
    2.42 -    measurable_merge[THEN measurable_sets, OF `J \<inter> K = {}`], OF A, of x] x
    2.43 -  show ?thesis
    2.44 -      by (simp add: space_pair_measure comp_def vimage_compose[symmetric])
    2.45 -qed
    2.46 +  assumes "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
    2.47 +  shows "(\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
    2.48 +  by (rule measurable_sets[OF _ A] measurable_compose[OF measurable_Pair measurable_merge]  
    2.49 +           measurable_const x measurable_ident)+
    2.50  
    2.51  lemma (in product_prob_space) merge_emb:
    2.52    assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
    2.53 -  shows "(merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
    2.54 -    emb I (K - J) (merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
    2.55 +  shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) =
    2.56 +    emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))"
    2.57  proof -
    2.58 -  have [simp]: "\<And>x J K L. merge J y K (restrict x L) = merge J y (K \<inter> L) x"
    2.59 +  have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
    2.60      by (auto simp: restrict_def merge_def)
    2.61 -  have [simp]: "\<And>x J K L. restrict (merge J y K x) L = merge (J \<inter> L) y (K \<inter> L) x"
    2.62 +  have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
    2.63      by (auto simp: restrict_def merge_def)
    2.64    have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
    2.65    have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
    2.66 @@ -331,16 +327,16 @@
    2.67        "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = emeasure (Pi\<^isub>M K M) X"
    2.68        by (auto simp: subset_insertI)
    2.69  
    2.70 -    let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
    2.71 +    let ?M = "\<lambda>y. (\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
    2.72      { fix y assume y: "y \<in> space (Pi\<^isub>M J M)"
    2.73        note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
    2.74        moreover
    2.75        have **: "?M y \<in> sets (Pi\<^isub>M (K - J) M)"
    2.76          using J K y by (intro merge_sets) auto
    2.77        ultimately
    2.78 -      have ***: "(merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
    2.79 +      have ***: "((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
    2.80          using J K by (intro generatorI) auto
    2.81 -      have "\<mu>G (merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
    2.82 +      have "\<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
    2.83          unfolding * using K J by (subst \<mu>G_eq[OF _ _ _ **]) auto
    2.84        note * ** *** this }
    2.85      note merge_in_G = this
    2.86 @@ -354,7 +350,7 @@
    2.87        using K J by simp
    2.88      also have "\<dots> = (\<integral>\<^isup>+ x. emeasure (Pi\<^isub>M (K - J) M) (?M x) \<partial>Pi\<^isub>M J M)"
    2.89        using K J by (subst emeasure_fold_integral) auto
    2.90 -    also have "\<dots> = (\<integral>\<^isup>+ y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<partial>Pi\<^isub>M J M)"
    2.91 +    also have "\<dots> = (\<integral>\<^isup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<partial>Pi\<^isub>M J M)"
    2.92        (is "_ = (\<integral>\<^isup>+x. \<mu>G (?MZ x) \<partial>Pi\<^isub>M J M)")
    2.93      proof (intro positive_integral_cong)
    2.94        fix x assume x: "x \<in> space (Pi\<^isub>M J M)"
    2.95 @@ -370,7 +366,7 @@
    2.96          by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
    2.97      note le_1 = this
    2.98  
    2.99 -    let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
   2.100 +    let ?q = "\<lambda>y. \<mu>G ((\<lambda>x. merge J (I - J) (y,x)) -` Z \<inter> space (Pi\<^isub>M I M))"
   2.101      have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
   2.102        unfolding `Z = emb I K X` using J K merge_in_G(3)
   2.103        by (simp add: merge_in_G  \<mu>G_eq emeasure_fold_measurable cong: measurable_cong)
   2.104 @@ -416,7 +412,7 @@
   2.105          using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
   2.106          by (auto intro!: INF_lower2[of 0] J.measure_le_1)
   2.107  
   2.108 -      let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
   2.109 +      let ?M = "\<lambda>K Z y. (\<lambda>x. merge K (I - K) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)"
   2.110  
   2.111        { fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
   2.112          then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
   2.113 @@ -524,9 +520,9 @@
   2.114              from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
   2.115              obtain w' where w': "w' \<in> space (Pi\<^isub>M ?D M)"
   2.116                "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) (w k)) w')" by auto
   2.117 -            let ?w = "merge (J k) (w k) ?D w'"
   2.118 -            have [simp]: "\<And>x. merge (J k) (w k) (I - J k) (merge ?D w' (I - ?D) x) =
   2.119 -              merge (J (Suc k)) ?w (I - (J (Suc k))) x"
   2.120 +            let ?w = "merge (J k) ?D (w k, w')"
   2.121 +            have [simp]: "\<And>x. merge (J k) (I - J k) (w k, merge ?D (I - ?D) (w', x)) =
   2.122 +              merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
   2.123                using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
   2.124                by (auto intro!: ext split: split_merge)
   2.125              have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
   2.126 @@ -552,7 +548,7 @@
   2.127            using positive_\<mu>G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
   2.128            by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
   2.129          then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
   2.130 -        then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto
   2.131 +        then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
   2.132          then have "\<exists>x\<in>A k. restrict x (J k) = w k"
   2.133            using `w k \<in> space (Pi\<^isub>M (J k) M)`
   2.134            by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)