src/HOL/Probability/Product_Measure.thy
 changeset 41661 baf1964bc468 parent 41659 a5d1b2df5e97 child 41689 3e39b0e730d6
1.1 --- a/src/HOL/Probability/Product_Measure.thy	Fri Jan 21 11:39:26 2011 +0100
1.2 +++ b/src/HOL/Probability/Product_Measure.thy	Mon Jan 24 22:29:50 2011 +0100
1.3 @@ -523,22 +523,6 @@
1.4      unfolding * by (rule measurable_comp)
1.5  qed
1.7 -lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:
1.8 -  "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \<times> space M1) (\<lambda>(x, y). (y, x)))"
1.9 -  unfolding vimage_algebra_def
1.10 -  apply (simp add: sets_sigma)
1.11 -  apply (subst sigma_sets_vimage[symmetric])
1.12 -  apply (fastsimp simp: pair_algebra_def)
1.13 -  using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)
1.14 -proof -
1.15 -  have "(\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E
1.16 -    = sets (pair_algebra M2 M1)" (is "?S = _")
1.17 -    by (rule pair_algebra_swap)
1.18 -  then show "sigma (pair_algebra M2 M1) = \<lparr>space = space M2 \<times> space M1,
1.19 -       sets = sigma_sets (space M2 \<times> space M1) ?S\<rparr>"
1.20 -    by (simp add: pair_algebra_def sigma_def)
1.21 -qed
1.22 -
1.23  definition (in pair_sigma_finite)
1.24    "pair_measure A = M1.positive_integral (\<lambda>x.
1.25      M2.positive_integral (\<lambda>y. indicator A (x, y)))"
1.26 @@ -644,6 +628,17 @@
1.27    qed
1.28  qed
1.30 +lemma (in pair_sigma_algebra) sets_swap:
1.31 +  assumes "A \<in> sets P"
1.32 +  shows "(\<lambda>(x, y). (y, x)) -` A \<inter> space (sigma (pair_algebra M2 M1)) \<in> sets (sigma (pair_algebra M2 M1))"
1.33 +    (is "_ -` A \<inter> space ?Q \<in> sets ?Q")
1.34 +proof -
1.35 +  have *: "(\<lambda>(x, y). (y, x)) -` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A"
1.36 +    using `A \<in> sets P` sets_into_space by (auto simp: space_pair_algebra)
1.37 +  show ?thesis
1.38 +    unfolding * using assms by (rule sets_pair_sigma_algebra_swap)
1.39 +qed
1.40 +
1.41  lemma (in pair_sigma_finite) pair_measure_alt2:
1.42    assumes "A \<in> sets P"
1.43    shows "pair_measure A = M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A))"
1.44 @@ -657,13 +652,19 @@
1.45        using F by auto
1.46      show "measure_space P pair_measure" by default
1.47      interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.48 -    have space_P: "space P = space M1 \<times> space M2" unfolding pair_algebra_def by simp
1.49 -    have "measure_space (Q.vimage_algebra (space P) (\<lambda>(x,y). (y,x))) (\<lambda>A. Q.pair_measure ((\<lambda>(x,y). (y,x)) ` A))"
1.50 -      by (rule Q.measure_space_isomorphic) (auto simp add: pair_algebra_def bij_betw_def intro!: inj_onI)
1.51 -    then show "measure_space P ?\<nu>" unfolding space_P Q.pair_sigma_algebra_swap[symmetric]
1.52 -      by (rule measure_space.measure_space_cong)
1.53 -         (auto intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1]
1.54 -               simp: Q.pair_measure_alt inj_vimage_image_eq sets_pair_sigma_algebra_swap)
1.55 +    have P: "sigma_algebra P" by default
1.56 +    show "measure_space P ?\<nu>"
1.57 +      apply (rule Q.measure_space_vimage[OF P])
1.58 +      apply (rule Q.pair_sigma_algebra_swap_measurable)
1.59 +    proof -
1.60 +      fix A assume "A \<in> sets P"
1.61 +      from sets_swap[OF this]
1.62 +      show "M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A)) =
1.63 +            Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P)"
1.64 +        using sets_into_space[OF `A \<in> sets P`]
1.65 +        by (auto simp add: Q.pair_measure_alt space_pair_algebra
1.66 +                 intro!: M2.positive_integral_cong arg_cong[where f=\<mu>1])
1.67 +    qed
1.68      fix X assume "X \<in> sets E"
1.69      then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
1.70        unfolding pair_algebra_def by auto
1.71 @@ -787,31 +788,40 @@
1.72      unfolding F_SUPR by simp
1.73  qed
1.75 +lemma (in pair_sigma_finite) positive_integral_product_swap:
1.76 +  assumes f: "f \<in> borel_measurable P"
1.77 +  shows "measure_space.positive_integral
1.78 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x))) =
1.79 +  positive_integral f"
1.80 +proof -
1.81 +  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.82 +  have P: "sigma_algebra P" by default
1.83 +  show ?thesis
1.84 +    unfolding Q.positive_integral_vimage[OF P Q.pair_sigma_algebra_swap_measurable f, symmetric]
1.85 +  proof (rule positive_integral_cong_measure)
1.86 +    fix A
1.87 +    assume A: "A \<in> sets P"
1.88 +    from Q.pair_sigma_algebra_swap_measurable[THEN measurable_sets, OF this] this sets_into_space[OF this]
1.89 +    show "Q.pair_measure ((\<lambda>(x, y). (y, x)) -` A \<inter> space Q.P) = pair_measure A"
1.90 +      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
1.91 +               simp: pair_measure_alt Q.pair_measure_alt2 space_pair_algebra)
1.92 +  qed
1.93 +qed
1.94 +
1.95  lemma (in pair_sigma_finite) positive_integral_snd_measurable:
1.96    assumes f: "f \<in> borel_measurable P"
1.97    shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
1.98        positive_integral f"
1.99  proof -
1.100    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.101 -  have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp
1.102 -  have t: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by (auto simp: fun_eq_iff)
1.103 -  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
1.104 -    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
1.105    note pair_sigma_algebra_measurable[OF f]
1.106    from Q.positive_integral_fst_measurable[OF this]
1.107    have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
1.108      Q.positive_integral (\<lambda>(x, y). f (y, x))"
1.109      by simp
1.110 -  also have "\<dots> = positive_integral f"
1.111 -    unfolding positive_integral_vimage[OF bij, of f] t
1.112 -    unfolding pair_sigma_algebra_swap[symmetric]
1.113 -  proof (rule Q.positive_integral_cong_measure[symmetric])
1.114 -    fix A assume "A \<in> sets Q.P"
1.115 -    from this Q.sets_pair_sigma_algebra_swap[OF this]
1.116 -    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
1.117 -      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
1.118 -               simp: pair_measure_alt Q.pair_measure_alt2)
1.119 -  qed
1.120 +  also have "Q.positive_integral (\<lambda>(x, y). f (y, x)) = positive_integral f"
1.121 +    unfolding positive_integral_product_swap[OF f, symmetric]
1.122 +    by (auto intro!: Q.positive_integral_cong)
1.123    finally show ?thesis .
1.124  qed
1.126 @@ -848,28 +858,6 @@
1.127    qed
1.128  qed
1.130 -lemma (in pair_sigma_finite) positive_integral_product_swap:
1.131 -  "measure_space.positive_integral
1.132 -    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
1.133 -  positive_integral (\<lambda>(x,y). f (y,x))"
1.134 -proof -
1.135 -  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.136 -  have t: "(\<lambda>y. case case y of (y, x) \<Rightarrow> (x, y) of (x, y) \<Rightarrow> f (y, x)) = f"
1.137 -    by (auto simp: fun_eq_iff)
1.138 -  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
1.139 -    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
1.140 -  show ?thesis
1.141 -    unfolding positive_integral_vimage[OF bij, of "\<lambda>(y,x). f (x,y)"]
1.142 -    unfolding pair_sigma_algebra_swap[symmetric] t
1.143 -  proof (rule Q.positive_integral_cong_measure[symmetric])
1.144 -    fix A assume "A \<in> sets Q.P"
1.145 -    from this Q.sets_pair_sigma_algebra_swap[OF this]
1.146 -    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
1.147 -      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
1.148 -               simp: pair_measure_alt Q.pair_measure_alt2)
1.149 -  qed
1.150 -qed
1.152  lemma (in pair_sigma_algebra) measurable_product_swap:
1.153    "f \<in> measurable (sigma (pair_algebra M2 M1)) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M"
1.154  proof -
1.155 @@ -880,27 +868,42 @@
1.156  qed
1.158  lemma (in pair_sigma_finite) integrable_product_swap:
1.159 -  "measure_space.integrable
1.160 -    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f \<longleftrightarrow>
1.161 -  integrable (\<lambda>(x,y). f (y,x))"
1.162 +  assumes "integrable f"
1.163 +  shows "measure_space.integrable
1.164 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x))"
1.165  proof -
1.166    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.167 -  show ?thesis
1.168 -    unfolding Q.integrable_def integrable_def
1.169 -    unfolding positive_integral_product_swap
1.170 -    unfolding measurable_product_swap
1.171 -    by (simp add: case_prod_distrib)
1.172 +  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
1.173 +  show ?thesis unfolding *
1.174 +    using assms unfolding Q.integrable_def integrable_def
1.175 +    apply (subst (1 2) positive_integral_product_swap)
1.176 +    using `integrable f` unfolding integrable_def
1.177 +    by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
1.178 +qed
1.180 +lemma (in pair_sigma_finite) integrable_product_swap_iff:
1.181 +  "measure_space.integrable
1.182 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow>
1.183 +  integrable f"
1.184 +proof -
1.185 +  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.186 +  from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
1.187 +  show ?thesis by auto
1.188  qed
1.190  lemma (in pair_sigma_finite) integral_product_swap:
1.191 -  "measure_space.integral
1.192 -    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) f =
1.193 -  integral (\<lambda>(x,y). f (y,x))"
1.194 +  assumes "integrable f"
1.195 +  shows "measure_space.integral
1.196 +    (sigma (pair_algebra M2 M1)) (pair_sigma_finite.pair_measure M2 \<mu>2 M1 \<mu>1) (\<lambda>(x,y). f (y,x)) =
1.197 +  integral f"
1.198  proof -
1.199    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.200 +  have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
1.201    show ?thesis
1.202 -    unfolding integral_def Q.integral_def positive_integral_product_swap
1.203 -    by (simp add: case_prod_distrib)
1.204 +    unfolding integral_def Q.integral_def *
1.205 +    apply (subst (1 2) positive_integral_product_swap)
1.206 +    using `integrable f` unfolding integrable_def
1.207 +    by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric])
1.208  qed
1.210  lemma (in pair_sigma_finite) integrable_fst_measurable:
1.211 @@ -973,10 +976,10 @@
1.212  proof -
1.213    interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
1.214    have Q_int: "Q.integrable (\<lambda>(x, y). f (y, x))"
1.215 -    using f unfolding integrable_product_swap by simp
1.216 +    using f unfolding integrable_product_swap_iff .
1.217    show ?INT
1.218      using Q.integrable_fst_measurable(2)[OF Q_int]
1.219 -    unfolding integral_product_swap by simp
1.220 +    using integral_product_swap[OF f] by simp
1.221    show ?AE
1.222      using Q.integrable_fst_measurable(1)[OF Q_int]
1.223      by simp
1.224 @@ -1340,18 +1343,6 @@
1.225              pair_algebra_sets_into_space product_algebra_sets_into_space)
1.226       auto
1.228 -lemma (in product_sigma_algebra) product_product_vimage_algebra:
1.229 -  assumes [simp]: "I \<inter> J = {}"
1.230 -  shows "sigma_algebra.vimage_algebra
1.231 -    (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
1.232 -    (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
1.233 -    sigma (product_algebra M (I \<union> J))"
1.234 -  unfolding sigma_pair_algebra_sigma_eq using sets_into_space
1.235 -  by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
1.236 -            pair_algebra_sets_into_space product_algebra_sets_into_space
1.237 -            measurable_merge_on_generating measurable_restrict_on_generating)
1.238 -     auto
1.240  lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
1.241    assumes [simp]: "I \<inter> J = {}"
1.242    shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
1.243 @@ -1363,24 +1354,6 @@
1.244              measurable_merge_on_generating measurable_restrict_on_generating)
1.245       auto
1.247 -lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
1.248 -  assumes [simp]: "i \<notin> I"
1.249 -  shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
1.250 -    (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
1.251 -    (sigma (product_algebra M (insert i I)))"
1.252 -  unfolding sigma_pair_algebra_product_singleton using sets_into_space
1.253 -  by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
1.254 -            pair_algebra_sets_into_space product_algebra_sets_into_space
1.255 -            measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
1.256 -      auto
1.258 -lemma (in product_sigma_algebra) singleton_vimage_algebra:
1.259 -  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
1.260 -  using sets_into_space
1.261 -  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
1.262 -             product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
1.263 -     auto
1.265  lemma (in product_sigma_algebra) measurable_restrict_iff:
1.266    assumes IJ[simp]: "I \<inter> J = {}"
1.267    shows "f \<in> measurable (sigma (pair_algebra
1.268 @@ -1415,6 +1388,13 @@
1.269    then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
1.270  qed
1.272 +lemma (in product_sigma_algebra) singleton_vimage_algebra:
1.273 +  "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
1.274 +  using sets_into_space
1.275 +  by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
1.276 +            product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
1.277 +     auto
1.279  lemma (in product_sigma_algebra) measurable_component_singleton:
1.280    "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
1.281      f \<in> measurable (M i) M'"
1.282 @@ -1464,6 +1444,55 @@
1.283    using sets_into_space unfolding measurable_component_singleton[symmetric]
1.284    by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
1.287 +lemma (in pair_sigma_algebra) measurable_pair_split:
1.288 +  assumes "sigma_algebra M1'" "sigma_algebra M2'"
1.289 +  assumes f: "f \<in> measurable M1 M1'" and g: "g \<in> measurable M2 M2'"
1.290 +  shows "(\<lambda>(x, y). (f x, g y)) \<in> measurable P (sigma (pair_algebra M1' M2'))"
1.291 +proof (rule measurable_sigma)
1.292 +  interpret M1': sigma_algebra M1' by fact
1.293 +  interpret M2': sigma_algebra M2' by fact
1.294 +  interpret Q: pair_sigma_algebra M1' M2' by default
1.295 +  show "sets Q.E \<subseteq> Pow (space Q.E)"
1.296 +    using M1'.sets_into_space M2'.sets_into_space by (auto simp: pair_algebra_def)
1.297 +  show "(\<lambda>(x, y). (f x, g y)) \<in> space P \<rightarrow> space Q.E"
1.298 +    using f g unfolding measurable_def pair_algebra_def by auto
1.299 +  fix A assume "A \<in> sets Q.E"
1.300 +  then obtain X Y where A: "A = X \<times> Y" "X \<in> sets M1'" "Y \<in> sets M2'"
1.301 +    unfolding pair_algebra_def by auto
1.302 +  then have *: "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P =
1.303 +      (f -` X \<inter> space M1) \<times> (g -` Y \<inter> space M2)"
1.304 +    by (auto simp: pair_algebra_def)
1.305 +  then show "(\<lambda>(x, y). (f x, g y)) -` A \<inter> space P \<in> sets P"
1.306 +    using f g A unfolding measurable_def *
1.307 +    by (auto intro!: pair_algebraI in_sigma)
1.308 +qed
1.310 +lemma (in product_sigma_algebra) measurable_add_dim:
1.311 +  assumes "i \<notin> I" "finite I"
1.312 +  shows "(\<lambda>(f, y). f(i := y)) \<in> measurable (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
1.313 +                         (sigma (product_algebra M (insert i I)))"
1.314 +proof (subst measurable_cong)
1.315 +  interpret I: finite_product_sigma_algebra M I by default fact
1.316 +  interpret i: finite_product_sigma_algebra M "{i}" by default auto
1.317 +  interpret Ii: pair_sigma_algebra I.P "M i" by default
1.318 +  interpret Ii': pair_sigma_algebra I.P i.P by default
1.319 +  have disj: "I \<inter> {i} = {}" using `i \<notin> I` by auto
1.320 +  have "(\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y)) \<in> measurable Ii.P Ii'.P"
1.321 +  proof (intro Ii.measurable_pair_split I.measurable_ident)
1.322 +    show "(\<lambda>y. \<lambda>_\<in>{i}. y) \<in> measurable (M i) i.P"
1.323 +      apply (rule measurable_singleton[THEN iffD1])
1.324 +      using i.measurable_ident unfolding id_def .
1.325 +  qed default
1.326 +  from measurable_comp[OF this measurable_merge[OF disj]]
1.327 +  show "(\<lambda>(x, y). merge I x {i} y) \<circ> (\<lambda>(x, y). (id x, \<lambda>_\<in>{i}. y))
1.328 +    \<in> measurable (sigma (pair_algebra I.P (M i))) (sigma (product_algebra M (insert i I)))"
1.329 +    (is "?f \<in> _") by simp
1.330 +  fix x assume "x \<in> space Ii.P"
1.331 +  with assms show "(\<lambda>(f, y). f(i := y)) x = ?f x"
1.332 +    by (cases x) (simp add: merge_def fun_eq_iff pair_algebra_def extensional_def)
1.333 +qed
1.335  locale product_sigma_finite =
1.336    fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
1.337    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i) (\<mu> i)"
1.338 @@ -1534,29 +1563,24 @@
1.339    interpret I: sigma_finite_measure P \<nu> by fact
1.340    interpret P: pair_sigma_finite P \<nu> "M i" "\<mu> i" ..
1.342 -  let ?h = "\<lambda>x. (restrict x I, x i)"
1.343 -  let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
1.344 +  let ?h = "(\<lambda>(f, y). f(i := y))"
1.345 +  let ?\<nu> = "\<lambda>A. P.pair_measure (?h -` A \<inter> space P.P)"
1.346 +  have I': "sigma_algebra I'.P" by default
1.347    interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
1.348 -    apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
1.349 -    apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
1.350 -    unfolding sigma_pair_algebra_product_singleton
1.351 -    by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
1.352 +    apply (rule P.measure_space_vimage[OF I'])
1.353 +    apply (rule measurable_add_dim[OF `i \<notin> I` `finite I`])
1.354 +    by simp
1.355    show ?case
1.356    proof (intro exI[of _ ?\<nu>] conjI ballI)
1.357      { fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
1.358 -      moreover then have "A \<in> (\<Pi> i\<in>I. sets (M i))" by auto
1.359 -      moreover have "(\<lambda>x. (restrict x I, x i)) ` Pi\<^isub>E (insert i I) A = Pi\<^isub>E I A \<times> A i"
1.360 -        using `i \<notin> I`
1.361 -        apply auto
1.362 -        apply (rule_tac x="a(i:=b)" in image_eqI)
1.363 -        apply (auto simp: extensional_def fun_eq_iff)
1.364 -        done
1.365 -      ultimately show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
1.366 -        apply simp
1.367 +      then have *: "?h -` Pi\<^isub>E (insert i I) A \<inter> space P.P = Pi\<^isub>E I A \<times> A i"
1.368 +        using `i \<notin> I` M.sets_into_space by (auto simp: pair_algebra_def) blast
1.369 +      show "?\<nu> (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. \<mu> i (A i))"
1.370 +        unfolding * using A
1.371          apply (subst P.pair_measure_times)
1.372 -        apply fastsimp
1.373 -        apply fastsimp
1.374 -        using `i \<notin> I` `finite I` prod[of A] by (auto simp: ac_simps) }
1.375 +        using A apply fastsimp
1.376 +        using A apply fastsimp
1.377 +        using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
1.378      note product = this
1.379      show "sigma_finite_measure I'.P ?\<nu>"
1.380      proof
1.381 @@ -1656,7 +1680,7 @@
1.382    shows "pair_sigma_finite.pair_measure
1.383       (sigma (product_algebra M I)) (product_measure I)
1.384       (sigma (product_algebra M J)) (product_measure J)
1.385 -     ((\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) ` A) =
1.386 +     ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) =
1.387     product_measure (I \<union> J) A"
1.388  proof -
1.389    interpret I: finite_product_sigma_finite M \<mu> I by default fact
1.390 @@ -1664,51 +1688,52 @@
1.391    have "finite (I \<union> J)" using fin by auto
1.392    interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
1.393    interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
1.394 -  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
1.395 -    from IJ.sigma_finite_pairs obtain F where
1.396 -      F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
1.397 -         "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
1.398 -         "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
1.399 -      by auto
1.400 -    let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
1.401 -  have split_f_image[simp]: "\<And>F. ?f ` (Pi\<^isub>E (I \<union> J) F) = (Pi\<^isub>E I F) \<times> (Pi\<^isub>E J F)"
1.402 -    apply auto apply (rule_tac x="merge I a J b" in image_eqI)
1.403 -    by (auto dest: extensional_restrict)
1.404 -    show "P.pair_measure (?f ` A) = IJ.measure A"
1.405 +  let ?g = "\<lambda>(x,y). merge I x J y"
1.406 +  let "?X S" = "?g -` S \<inter> space P.P"
1.407 +  from IJ.sigma_finite_pairs obtain F where
1.408 +    F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
1.409 +       "(\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k) \<up> space IJ.G"
1.410 +       "\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
1.411 +    by auto
1.412 +  let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
1.413 +  show "P.pair_measure (?X A) = IJ.measure A"
1.414    proof (rule measure_unique_Int_stable[OF _ _ _ _ _ _ _ _ A])
1.415 -      show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
1.416 -      show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
1.417 -      show "?F \<up> space IJ.G " using F(2) by simp
1.418 -      show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
1.419 -      apply (subst product_product_vimage_algebra[OF IJ, symmetric])
1.420 -      apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
1.421 -      unfolding sigma_pair_algebra_sigma_eq
1.422 -      by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
1.423 -      show "measure_space IJ.P IJ.measure" by fact
1.424 -    next
1.425 -      fix A assume "A \<in> sets IJ.G"
1.426 -      then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I \<union> J. sets (M i))"
1.427 -        by (auto simp: product_algebra_def)
1.428 -      then have F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M i)" "\<And>i. i \<in> J \<Longrightarrow> F i \<in> sets (M i)"
1.429 -        by auto
1.430 -      have "P.pair_measure (?f ` A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
1.431 -        using `finite J` `finite I` F
1.432 -        by (simp add: P.pair_measure_times I.measure_times J.measure_times)
1.433 -      also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
1.434 -        using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
1.435 -      also have "\<dots> = IJ.measure A"
1.436 -        using `finite J` `finite I` F unfolding A
1.437 -        by (intro IJ.measure_times[symmetric]) auto
1.438 -      finally show "P.pair_measure (?f ` A) = IJ.measure A" .
1.439 -    next
1.440 -      fix k
1.441 -      have "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
1.442 -      then have "P.pair_measure (?f ` ?F k) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
1.443 -        by (simp add: P.pair_measure_times I.measure_times J.measure_times)
1.444 -      then show "P.pair_measure (?f ` ?F k) \<noteq> \<omega>"
1.445 -        using `finite I` F by (simp add: setprod_\<omega>)
1.446 -    qed simp
1.447 -  qed
1.448 +    show "Int_stable IJ.G" by (simp add: PiE_Int Int_stable_def product_algebra_def) auto
1.449 +    show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
1.450 +    show "?F \<up> space IJ.G " using F(2) by simp
1.451 +    have "sigma_algebra IJ.P" by default
1.452 +    then show "measure_space IJ.P (\<lambda>A. P.pair_measure (?X A))"
1.453 +      apply (rule P.measure_space_vimage)
1.454 +      apply (rule measurable_merge[OF `I \<inter> J = {}`])
1.455 +      by simp
1.456 +    show "measure_space IJ.P IJ.measure" by fact
1.457 +  next
1.458 +    fix A assume "A \<in> sets IJ.G"
1.459 +    then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
1.460 +      and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
1.461 +      by (auto simp: product_algebra_def)
1.462 +    then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
1.463 +      using sets_into_space by (auto simp: space_pair_algebra) blast+
1.464 +    then have "P.pair_measure (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
1.465 +      using `finite J` `finite I` F
1.466 +      by (simp add: P.pair_measure_times I.measure_times J.measure_times)
1.467 +    also have "\<dots> = (\<Prod>i\<in>I \<union> J. \<mu> i (F i))"
1.468 +      using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
1.469 +    also have "\<dots> = IJ.measure A"
1.470 +      using `finite J` `finite I` F unfolding A
1.471 +      by (intro IJ.measure_times[symmetric]) auto
1.472 +    finally show "P.pair_measure (?X A) = IJ.measure A" .
1.473 +  next
1.474 +    fix k
1.475 +    have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
1.476 +    then have "?X (?F k) = (\<Pi>\<^isub>E i\<in>I. F i k) \<times> (\<Pi>\<^isub>E i\<in>J. F i k)"
1.477 +      using sets_into_space by (auto simp: space_pair_algebra) blast+
1.478 +    with k have "P.pair_measure (?X (?F k)) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
1.479 +     by (simp add: P.pair_measure_times I.measure_times J.measure_times)
1.480 +    then show "P.pair_measure (?X (?F k)) \<noteq> \<omega>"
1.481 +      using `finite I` F by (simp add: setprod_\<omega>)
1.482 +  qed simp
1.483 +qed
1.485  lemma (in product_sigma_finite) product_positive_integral_fold:
1.486    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
1.487 @@ -1721,23 +1746,18 @@
1.488    have "finite (I \<union> J)" using fin by auto
1.489    interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
1.490    interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
1.491 -  let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
1.492    have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
1.493      unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
1.494 -  have bij: "bij_betw ?f (space IJ.P) (space P.P)"
1.495 -    unfolding sigma_pair_algebra_sigma_eq
1.496 -    by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
1.497 -  have "IJ.positive_integral f =  IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
1.498 -    by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
1.499 -  also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
1.500 +  show ?thesis
1.501      unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
1.502 -    unfolding P.positive_integral_vimage[OF bij]
1.503 -    unfolding product_product_vimage_algebra[OF IJ]
1.504 -    apply simp
1.505 -    apply (rule IJ.positive_integral_cong_measure[symmetric])
1.506 -    apply (rule measure_fold)
1.507 -    using assms by auto
1.508 -  finally show ?thesis .
1.509 +    apply (subst IJ.positive_integral_cong_measure[symmetric])
1.510 +    apply (rule measure_fold[OF IJ fin])
1.511 +    apply assumption
1.512 +  proof (rule P.positive_integral_vimage)
1.513 +    show "sigma_algebra IJ.P" by default
1.514 +    show "(\<lambda>(x, y). merge I x J y) \<in> measurable P.P IJ.P" by (rule measurable_merge[OF IJ])
1.515 +    show "f \<in> borel_measurable IJ.P" using f .
1.516 +  qed
1.517  qed
1.519  lemma (in product_sigma_finite) product_positive_integral_singleton:
1.520 @@ -1745,31 +1765,18 @@
1.521    shows "product_positive_integral {i} (\<lambda>x. f (x i)) = M.positive_integral i f"
1.522  proof -
1.523    interpret I: finite_product_sigma_finite M \<mu> "{i}" by default simp
1.524 -  have bij: "bij_betw (\<lambda>x. \<lambda>j\<in>{i}. x) (space (M i)) (space I.P)"
1.525 -    by (auto intro!: bij_betwI ext simp: extensional_def)
1.526 -  have *: "(\<lambda>x. (\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i)) ` (\<Pi> i\<in>{i}. sets (M i)) = sets (M i)"
1.527 -  proof (subst image_cong, rule refl)
1.528 -    fix x assume "x \<in> (\<Pi> i\<in>{i}. sets (M i))"
1.529 -    then show "(\<lambda>x. \<lambda>j\<in>{i}. x) -` Pi\<^isub>E {i} x \<inter> space (M i) = x i"
1.530 -      using sets_into_space by auto
1.531 -  qed auto
1.532 -  have vimage: "I.vimage_algebra (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
1.533 -    unfolding I.vimage_algebra_def
1.534 -    unfolding product_sigma_algebra_def sets_sigma
1.535 -    apply (subst sigma_sets_vimage[symmetric])
1.536 -    apply (simp_all add: image_image sigma_sets_eq product_algebra_def * del: vimage_Int)
1.537 -    using sets_into_space by blast
1.538 +  have T: "(\<lambda>x. x i) \<in> measurable (sigma (product_algebra M {i})) (M i)"
1.539 +    using measurable_component_singleton[of "\<lambda>x. x" i]
1.540 +          measurable_ident[unfolded id_def] by auto
1.541    show "I.positive_integral (\<lambda>x. f (x i)) = M.positive_integral i f"
1.542 -    unfolding I.positive_integral_vimage[OF bij]
1.543 -    unfolding vimage
1.544 -    apply (subst positive_integral_cong_measure)
1.545 -  proof -
1.546 -    fix A assume A: "A \<in> sets (M i)"
1.547 -    have "(\<lambda>x. \<lambda>j\<in>{i}. x) ` A = (\<Pi>\<^isub>E i\<in>{i}. A)"
1.548 -      by (auto intro!: image_eqI ext[where 'b='a] simp: extensional_def)
1.549 -    with A show "product_measure {i} ((\<lambda>x. \<lambda>j\<in>{i}. x) ` A) = \<mu> i A"
1.550 -      using I.measure_times[of "\<lambda>i. A"] by simp
1.551 -  qed simp
1.552 +    unfolding I.positive_integral_vimage[OF sigma_algebras T f, symmetric]
1.553 +  proof (rule positive_integral_cong_measure)
1.554 +    fix A let ?P = "(\<lambda>x. x i) -` A \<inter> space (sigma (product_algebra M {i}))"
1.555 +    assume A: "A \<in> sets (M i)"
1.556 +    then have *: "?P = {i} \<rightarrow>\<^isub>E A" using sets_into_space by auto
1.557 +    show "product_measure {i} ?P = \<mu> i A" unfolding *
1.558 +      using A I.measure_times[of "\<lambda>_. A"] by auto
1.559 +  qed
1.560  qed
1.562  lemma (in product_sigma_finite) product_positive_integral_insert: