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.6  
     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.29  
    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.74  
    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.125  
   1.126 @@ -848,28 +858,6 @@
   1.127    qed
   1.128  qed
   1.129  
   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.151 -
   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.157  
   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.179 +
   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.189  
   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.209  
   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.227  
   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.239 -
   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.246  
   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.257 -
   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.264 -
   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.271  
   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.278 +
   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.285  
   1.286 +
   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.309 +
   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.334 +
   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.341  
   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.484  
   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.518  
   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.561  
   1.562  lemma (in product_sigma_finite) product_positive_integral_insert: