src/HOL/Probability/Infinite_Product_Measure.thy
changeset 47694 05663f75964c
parent 46905 6b1c0a80a57a
child 47762 d31085f07f60
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Apr 23 12:23:23 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Apr 23 12:14:35 2012 +0200
     1.3 @@ -5,9 +5,49 @@
     1.4  header {*Infinite Product Measure*}
     1.5  
     1.6  theory Infinite_Product_Measure
     1.7 -  imports Probability_Measure
     1.8 +  imports Probability_Measure Caratheodory
     1.9  begin
    1.10  
    1.11 +lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
    1.12 +proof
    1.13 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
    1.14 +    by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros)
    1.15 +qed
    1.16 +
    1.17 +lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
    1.18 +proof
    1.19 +  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
    1.20 +    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
    1.21 +qed
    1.22 +
    1.23 +lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
    1.24 +  by (auto intro: sigma_sets.Basic)
    1.25 +
    1.26 +lemma (in product_sigma_finite)
    1.27 +  assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
    1.28 +  shows emeasure_fold_integral:
    1.29 +    "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.30 +    and emeasure_fold_measurable:
    1.31 +    "(\<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.32 +proof -
    1.33 +  interpret I: finite_product_sigma_finite M I by default fact
    1.34 +  interpret J: finite_product_sigma_finite M J by default fact
    1.35 +  interpret IJ: pair_sigma_finite "Pi\<^isub>M I M" "Pi\<^isub>M J M" ..
    1.36 +  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.37 +    by (intro measurable_sets[OF _ A] measurable_merge assms)
    1.38 +
    1.39 +  show ?I
    1.40 +    apply (subst distr_merge[symmetric, OF IJ])
    1.41 +    apply (subst emeasure_distr[OF measurable_merge[OF IJ(1)] A])
    1.42 +    apply (subst IJ.emeasure_pair_measure_alt[OF merge])
    1.43 +    apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
    1.44 +    done
    1.45 +
    1.46 +  show ?B
    1.47 +    using IJ.measurable_emeasure_Pair1[OF merge]
    1.48 +    by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
    1.49 +qed
    1.50 +
    1.51  lemma restrict_extensional_sub[intro]: "A \<subseteq> B \<Longrightarrow> restrict f A \<in> extensional B"
    1.52    unfolding restrict_def extensional_def by auto
    1.53  
    1.54 @@ -41,189 +81,178 @@
    1.55    qed
    1.56  qed
    1.57  
    1.58 -lemma (in product_prob_space) measure_preserving_restrict:
    1.59 +lemma prod_algebraI_finite:
    1.60 +  "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
    1.61 +  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
    1.62 +
    1.63 +lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
    1.64 +proof (safe intro!: Int_stableI)
    1.65 +  fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
    1.66 +  then show "\<exists>G. Pi\<^isub>E J E \<inter> Pi\<^isub>E J F = Pi\<^isub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
    1.67 +    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"])
    1.68 +qed
    1.69 +
    1.70 +lemma prod_emb_trans[simp]:
    1.71 +  "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
    1.72 +  by (auto simp add: Int_absorb1 prod_emb_def)
    1.73 +
    1.74 +lemma prod_emb_Pi:
    1.75 +  assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
    1.76 +  shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
    1.77 +  using assms space_closed
    1.78 +  by (auto simp: prod_emb_def Pi_iff split: split_if_asm) blast+
    1.79 +
    1.80 +lemma prod_emb_id:
    1.81 +  "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
    1.82 +  by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
    1.83 +
    1.84 +lemma measurable_prod_emb[intro, simp]:
    1.85 +  "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^isub>M L M)"
    1.86 +  unfolding prod_emb_def space_PiM[symmetric]
    1.87 +  by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
    1.88 +
    1.89 +lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^isub>M L M) (Pi\<^isub>M J M)"
    1.90 +  by (intro measurable_restrict measurable_component_singleton) auto
    1.91 +
    1.92 +lemma (in product_prob_space) distr_restrict:
    1.93    assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
    1.94 -  shows "(\<lambda>f. restrict f J) \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i)" (is "?R \<in> _")
    1.95 -proof -
    1.96 -  interpret K: finite_product_prob_space M K by default fact
    1.97 -  have J: "J \<noteq> {}" "finite J" using assms by (auto simp add: finite_subset)
    1.98 -  interpret J: finite_product_prob_space M J
    1.99 -    by default (insert J, auto)
   1.100 -  from J.sigma_finite_pairs guess F .. note F = this
   1.101 -  then have [simp,intro]: "\<And>k i. k \<in> J \<Longrightarrow> F k i \<in> sets (M k)"
   1.102 -    by auto
   1.103 -  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. F k i"
   1.104 -  let ?J = "product_algebra_generator J M \<lparr> measure := measure (Pi\<^isub>M J M) \<rparr>"
   1.105 -  have "?R \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (sigma ?J)"
   1.106 -  proof (rule K.measure_preserving_Int_stable)
   1.107 -    show "Int_stable ?J"
   1.108 -      by (auto simp: Int_stable_def product_algebra_generator_def PiE_Int)
   1.109 -    show "range ?F \<subseteq> sets ?J" "incseq ?F" "(\<Union>i. ?F i) = space ?J"
   1.110 -      using F by auto
   1.111 -    show "\<And>i. measure ?J (?F i) \<noteq> \<infinity>"
   1.112 -      using F by (simp add: J.measure_times setprod_PInf)
   1.113 -    have "measure_space (Pi\<^isub>M J M)" by default
   1.114 -    then show "measure_space (sigma ?J)"
   1.115 -      by (simp add: product_algebra_def sigma_def)
   1.116 -    show "?R \<in> measure_preserving (Pi\<^isub>M K M) ?J"
   1.117 -    proof (simp add: measure_preserving_def measurable_def product_algebra_generator_def del: vimage_Int,
   1.118 -           safe intro!: restrict_extensional)
   1.119 -      fix x k assume "k \<in> J" "x \<in> (\<Pi> i\<in>K. space (M i))"
   1.120 -      then show "x k \<in> space (M k)" using `J \<subseteq> K` by auto
   1.121 -    next
   1.122 -      fix E assume "E \<in> (\<Pi> i\<in>J. sets (M i))"
   1.123 -      then have E: "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)" by auto
   1.124 -      then have *: "?R -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i)) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
   1.125 -        (is "?X = Pi\<^isub>E K ?M")
   1.126 -        using `J \<subseteq> K` sets_into_space by (auto simp: Pi_iff split: split_if_asm) blast+
   1.127 -      with E show "?X \<in> sets (Pi\<^isub>M K M)"
   1.128 -        by (auto intro!: product_algebra_generatorI)
   1.129 -      have "measure (Pi\<^isub>M J M) (Pi\<^isub>E J E) = (\<Prod>i\<in>J. measure (M i) (?M i))"
   1.130 -        using E by (simp add: J.measure_times)
   1.131 -      also have "\<dots> = measure (Pi\<^isub>M K M) ?X"
   1.132 -        unfolding * using E `finite K` `J \<subseteq> K`
   1.133 -        by (auto simp: K.measure_times M.measure_space_1
   1.134 -                 cong del: setprod_cong
   1.135 -                 intro!: setprod_mono_one_left)
   1.136 -      finally show "measure (Pi\<^isub>M J M) (Pi\<^isub>E J E) = measure (Pi\<^isub>M K M) ?X" .
   1.137 -    qed
   1.138 -  qed
   1.139 -  then show ?thesis
   1.140 -    by (simp add: product_algebra_def sigma_def)
   1.141 +  shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
   1.142 +proof (rule measure_eqI_generator_eq)
   1.143 +  have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
   1.144 +  interpret J: finite_product_prob_space M J proof qed fact
   1.145 +  interpret K: finite_product_prob_space M K proof qed fact
   1.146 +
   1.147 +  let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
   1.148 +  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
   1.149 +  let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
   1.150 +  show "Int_stable ?J"
   1.151 +    by (rule Int_stable_PiE)
   1.152 +  show "range ?F \<subseteq> ?J" "incseq ?F" "(\<Union>i. ?F i) = ?\<Omega>"
   1.153 +    using `finite J` by (auto intro!: prod_algebraI_finite)
   1.154 +  { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
   1.155 +  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
   1.156 +  show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
   1.157 +    using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
   1.158 +  
   1.159 +  fix X assume "X \<in> ?J"
   1.160 +  then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
   1.161 +  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)" by auto
   1.162 +
   1.163 +  have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
   1.164 +    using E by (simp add: J.measure_times)
   1.165 +  also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
   1.166 +    by simp
   1.167 +  also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
   1.168 +    using `finite K` `J \<subseteq> K`
   1.169 +    by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
   1.170 +  also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
   1.171 +    using E by (simp add: K.measure_times)
   1.172 +  also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
   1.173 +    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
   1.174 +  finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
   1.175 +    using X `J \<subseteq> K` apply (subst emeasure_distr)
   1.176 +    by (auto intro!: measurable_restrict_subset simp: space_PiM)
   1.177  qed
   1.178  
   1.179 -lemma (in product_prob_space) measurable_restrict:
   1.180 -  assumes *: "J \<noteq> {}" "J \<subseteq> K" "finite K"
   1.181 -  shows "(\<lambda>f. restrict f J) \<in> measurable (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i)"
   1.182 -  using measure_preserving_restrict[OF *]
   1.183 -  by (rule measure_preservingD2)
   1.184 +abbreviation (in product_prob_space)
   1.185 +  "emb L K X \<equiv> prod_emb L M K X"
   1.186 +
   1.187 +lemma (in product_prob_space) emeasure_prod_emb[simp]:
   1.188 +  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)"
   1.189 +  shows "emeasure (Pi\<^isub>M L M) (emb L J X) = emeasure (Pi\<^isub>M J M) X"
   1.190 +  by (subst distr_restrict[OF L])
   1.191 +     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
   1.192  
   1.193 -definition (in product_prob_space)
   1.194 -  "emb J K X = (\<lambda>x. restrict x K) -` X \<inter> space (Pi\<^isub>M J M)"
   1.195 +lemma (in product_prob_space) prod_emb_injective:
   1.196 +  assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
   1.197 +  assumes "prod_emb L M J X = prod_emb L M J Y"
   1.198 +  shows "X = Y"
   1.199 +proof (rule injective_vimage_restrict)
   1.200 +  show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
   1.201 +    using sets[THEN sets_into_space] by (auto simp: space_PiM)
   1.202 +  have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
   1.203 +    using M.not_empty by auto
   1.204 +  from bchoice[OF this]
   1.205 +  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
   1.206 +  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))"
   1.207 +    using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
   1.208 +qed fact
   1.209  
   1.210 -lemma (in product_prob_space) emb_trans[simp]:
   1.211 -  "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> emb L K (emb K J X) = emb L J X"
   1.212 -  by (auto simp add: Int_absorb1 emb_def)
   1.213 -
   1.214 -lemma (in product_prob_space) emb_empty[simp]:
   1.215 -  "emb K J {} = {}"
   1.216 -  by (simp add: emb_def)
   1.217 +definition (in product_prob_space) generator :: "('i \<Rightarrow> 'a) set set" where
   1.218 +  "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
   1.219  
   1.220 -lemma (in product_prob_space) emb_Pi:
   1.221 -  assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
   1.222 -  shows "emb K J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
   1.223 -  using assms space_closed
   1.224 -  by (auto simp: emb_def Pi_iff split: split_if_asm) blast+
   1.225 +lemma (in product_prob_space) generatorI':
   1.226 +  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator"
   1.227 +  unfolding generator_def by auto
   1.228  
   1.229 -lemma (in product_prob_space) emb_injective:
   1.230 -  assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
   1.231 -  assumes "emb L J X = emb L J Y"
   1.232 -  shows "X = Y"
   1.233 -proof -
   1.234 -  interpret J: finite_product_sigma_finite M J by default fact
   1.235 -  show "X = Y"
   1.236 -  proof (rule injective_vimage_restrict)
   1.237 -    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
   1.238 -      using J.sets_into_space sets by auto
   1.239 -    have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
   1.240 -      using M.not_empty by auto
   1.241 -    from bchoice[OF this]
   1.242 -    show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
   1.243 -    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))"
   1.244 -      using `emb L J X = emb L J Y` by (simp add: emb_def)
   1.245 -  qed fact
   1.246 +lemma (in product_prob_space) algebra_generator:
   1.247 +  assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
   1.248 +proof
   1.249 +  let ?G = generator
   1.250 +  show "?G \<subseteq> Pow ?\<Omega>"
   1.251 +    by (auto simp: generator_def prod_emb_def)
   1.252 +  from `I \<noteq> {}` obtain i where "i \<in> I" by auto
   1.253 +  then show "{} \<in> ?G"
   1.254 +    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
   1.255 +             simp: sigma_sets.Empty generator_def prod_emb_def)
   1.256 +  from `i \<in> I` show "?\<Omega> \<in> ?G"
   1.257 +    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"]
   1.258 +             simp: generator_def prod_emb_def)
   1.259 +  fix A assume "A \<in> ?G"
   1.260 +  then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA"
   1.261 +    by (auto simp: generator_def)
   1.262 +  fix B assume "B \<in> ?G"
   1.263 +  then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB"
   1.264 +    by (auto simp: generator_def)
   1.265 +  let ?RA = "emb (JA \<union> JB) JA XA"
   1.266 +  let ?RB = "emb (JA \<union> JB) JB XB"
   1.267 +  have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
   1.268 +    using XA A XB B by auto
   1.269 +  show "A - B \<in> ?G" "A \<union> B \<in> ?G"
   1.270 +    unfolding * using XA XB by (safe intro!: generatorI') auto
   1.271  qed
   1.272  
   1.273 -lemma (in product_prob_space) emb_id:
   1.274 -  "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> emb L L B = B"
   1.275 -  by (auto simp: emb_def Pi_iff subset_eq extensional_restrict)
   1.276 -
   1.277 -lemma (in product_prob_space) emb_simps:
   1.278 -  shows "emb L K (A \<union> B) = emb L K A \<union> emb L K B"
   1.279 -    and "emb L K (A \<inter> B) = emb L K A \<inter> emb L K B"
   1.280 -    and "emb L K (A - B) = emb L K A - emb L K B"
   1.281 -  by (auto simp: emb_def)
   1.282 -
   1.283 -lemma (in product_prob_space) measurable_emb[intro,simp]:
   1.284 -  assumes *: "J \<noteq> {}" "J \<subseteq> L" "finite L" "X \<in> sets (Pi\<^isub>M J M)"
   1.285 -  shows "emb L J X \<in> sets (Pi\<^isub>M L M)"
   1.286 -  using measurable_restrict[THEN measurable_sets, OF *] by (simp add: emb_def)
   1.287 -
   1.288 -lemma (in product_prob_space) measure_emb[intro,simp]:
   1.289 -  assumes *: "J \<noteq> {}" "J \<subseteq> L" "finite L" "X \<in> sets (Pi\<^isub>M J M)"
   1.290 -  shows "measure (Pi\<^isub>M L M) (emb L J X) = measure (Pi\<^isub>M J M) X"
   1.291 -  using measure_preserving_restrict[THEN measure_preservingD, OF *]
   1.292 -  by (simp add: emb_def)
   1.293 -
   1.294 -definition (in product_prob_space) generator :: "('i \<Rightarrow> 'a) measure_space" where
   1.295 -  "generator = \<lparr>
   1.296 -    space = (\<Pi>\<^isub>E i\<in>I. space (M i)),
   1.297 -    sets = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M)),
   1.298 -    measure = undefined
   1.299 -  \<rparr>"
   1.300 +lemma (in product_prob_space) sets_PiM_generator:
   1.301 +  assumes "I \<noteq> {}" shows "sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
   1.302 +proof
   1.303 +  show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator"
   1.304 +    unfolding sets_PiM
   1.305 +  proof (safe intro!: sigma_sets_subseteq)
   1.306 +    fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
   1.307 +      by (auto intro!: generatorI' elim!: prod_algebraE)
   1.308 +  qed
   1.309 +qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
   1.310  
   1.311  lemma (in product_prob_space) generatorI:
   1.312 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> sets generator"
   1.313 -  unfolding generator_def by auto
   1.314 -
   1.315 -lemma (in product_prob_space) generatorI':
   1.316 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> sets generator"
   1.317 +  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
   1.318    unfolding generator_def by auto
   1.319  
   1.320 -lemma (in product_sigma_finite)
   1.321 -  assumes "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
   1.322 -  shows measure_fold_integral:
   1.323 -    "measure (Pi\<^isub>M (I \<union> J) M) A = (\<integral>\<^isup>+x. measure (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.324 -    and measure_fold_measurable:
   1.325 -    "(\<lambda>x. measure (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.326 -proof -
   1.327 -  interpret I: finite_product_sigma_finite M I by default fact
   1.328 -  interpret J: finite_product_sigma_finite M J by default fact
   1.329 -  interpret IJ: pair_sigma_finite I.P J.P ..
   1.330 -  show ?I
   1.331 -    unfolding measure_fold[OF assms]
   1.332 -    apply (subst IJ.pair_measure_alt)
   1.333 -    apply (intro measurable_sets[OF _ A] measurable_merge assms)
   1.334 -    apply (auto simp: vimage_compose[symmetric] comp_def space_pair_measure
   1.335 -      intro!: I.positive_integral_cong)
   1.336 -    done
   1.337 -
   1.338 -  have "(\<lambda>(x, y). merge I x J y) -` A \<inter> space (I.P \<Otimes>\<^isub>M J.P) \<in> sets (I.P \<Otimes>\<^isub>M J.P)"
   1.339 -    by (intro measurable_sets[OF _ A] measurable_merge assms)
   1.340 -  from IJ.measure_cut_measurable_fst[OF this]
   1.341 -  show ?B
   1.342 -    apply (auto simp: vimage_compose[symmetric] comp_def space_pair_measure)
   1.343 -    apply (subst (asm) measurable_cong)
   1.344 -    apply auto
   1.345 -    done
   1.346 -qed
   1.347 -
   1.348  definition (in product_prob_space)
   1.349    "\<mu>G A =
   1.350 -    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = measure (Pi\<^isub>M J M) X))"
   1.351 +    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (Pi\<^isub>M J M) X))"
   1.352  
   1.353  lemma (in product_prob_space) \<mu>G_spec:
   1.354    assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
   1.355 -  shows "\<mu>G A = measure (Pi\<^isub>M J M) X"
   1.356 +  shows "\<mu>G A = emeasure (Pi\<^isub>M J M) X"
   1.357    unfolding \<mu>G_def
   1.358  proof (intro the_equality allI impI ballI)
   1.359    fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
   1.360 -  have "measure (Pi\<^isub>M K M) Y = measure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) K Y)"
   1.361 +  have "emeasure (Pi\<^isub>M K M) Y = emeasure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) K Y)"
   1.362      using K J by simp
   1.363    also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
   1.364 -    using K J by (simp add: emb_injective[of "K \<union> J" I])
   1.365 -  also have "measure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) J X) = measure (Pi\<^isub>M J M) X"
   1.366 +    using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
   1.367 +  also have "emeasure (Pi\<^isub>M (K \<union> J) M) (emb (K \<union> J) J X) = emeasure (Pi\<^isub>M J M) X"
   1.368      using K J by simp
   1.369 -  finally show "measure (Pi\<^isub>M J M) X = measure (Pi\<^isub>M K M) Y" ..
   1.370 +  finally show "emeasure (Pi\<^isub>M J M) X = emeasure (Pi\<^isub>M K M) Y" ..
   1.371  qed (insert J, force)
   1.372  
   1.373  lemma (in product_prob_space) \<mu>G_eq:
   1.374 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = measure (Pi\<^isub>M J M) X"
   1.375 +  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (Pi\<^isub>M J M) X"
   1.376    by (intro \<mu>G_spec) auto
   1.377  
   1.378  lemma (in product_prob_space) generator_Ex:
   1.379 -  assumes *: "A \<in> sets generator"
   1.380 -  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = measure (Pi\<^isub>M J M) X"
   1.381 +  assumes *: "A \<in> generator"
   1.382 +  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (Pi\<^isub>M J M) X"
   1.383  proof -
   1.384    from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
   1.385      unfolding generator_def by auto
   1.386 @@ -231,11 +260,11 @@
   1.387  qed
   1.388  
   1.389  lemma (in product_prob_space) generatorE:
   1.390 -  assumes A: "A \<in> sets generator"
   1.391 -  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = measure (Pi\<^isub>M J M) X"
   1.392 +  assumes A: "A \<in> generator"
   1.393 +  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (Pi\<^isub>M J M) X"
   1.394  proof -
   1.395    from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
   1.396 -    "\<mu>G A = measure (Pi\<^isub>M J M) X" by auto
   1.397 +    "\<mu>G A = emeasure (Pi\<^isub>M J M) X" by auto
   1.398    then show thesis by (intro that) auto
   1.399  qed
   1.400  
   1.401 @@ -243,11 +272,7 @@
   1.402    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)"
   1.403    shows "merge J x K -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
   1.404  proof -
   1.405 -  interpret J: finite_product_sigma_algebra M J by default fact
   1.406 -  interpret K: finite_product_sigma_algebra M K by default fact
   1.407 -  interpret JK: pair_sigma_algebra J.P K.P ..
   1.408 -
   1.409 -  from JK.measurable_cut_fst[OF
   1.410 +  from sets_Pair1[OF
   1.411      measurable_merge[THEN measurable_sets, OF `J \<inter> K = {}`], OF A, of x] x
   1.412    show ?thesis
   1.413        by (simp add: space_pair_measure comp_def vimage_compose[symmetric])
   1.414 @@ -266,75 +291,27 @@
   1.415    have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
   1.416    have [simp]: "(K - J) \<inter> K = K - J" by auto
   1.417    from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
   1.418 -    by (simp split: split_merge add: emb_def Pi_iff extensional_merge_sub set_eq_iff) auto
   1.419 -qed
   1.420 -
   1.421 -definition (in product_prob_space) infprod_algebra :: "('i \<Rightarrow> 'a) measure_space" where
   1.422 -  "infprod_algebra = sigma generator \<lparr> measure :=
   1.423 -    (SOME \<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and>
   1.424 -       prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>"
   1.425 -
   1.426 -syntax
   1.427 -  "_PiP"  :: "[pttrn, 'i set, ('b, 'd) measure_space_scheme] => ('i => 'b, 'd) measure_space_scheme"  ("(3PIP _:_./ _)" 10)
   1.428 -
   1.429 -syntax (xsymbols)
   1.430 -  "_PiP" :: "[pttrn, 'i set, ('b, 'd) measure_space_scheme] => ('i => 'b, 'd) measure_space_scheme"  ("(3\<Pi>\<^isub>P _\<in>_./ _)"   10)
   1.431 -
   1.432 -syntax (HTML output)
   1.433 -  "_PiP" :: "[pttrn, 'i set, ('b, 'd) measure_space_scheme] => ('i => 'b, 'd) measure_space_scheme"  ("(3\<Pi>\<^isub>P _\<in>_./ _)"   10)
   1.434 -
   1.435 -abbreviation
   1.436 -  "Pi\<^isub>P I M \<equiv> product_prob_space.infprod_algebra M I"
   1.437 -
   1.438 -translations
   1.439 -  "PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)"
   1.440 -
   1.441 -lemma (in product_prob_space) algebra_generator:
   1.442 -  assumes "I \<noteq> {}" shows "algebra generator"
   1.443 -proof
   1.444 -  let ?G = generator
   1.445 -  show "sets ?G \<subseteq> Pow (space ?G)"
   1.446 -    by (auto simp: generator_def emb_def)
   1.447 -  from `I \<noteq> {}` obtain i where "i \<in> I" by auto
   1.448 -  then show "{} \<in> sets ?G"
   1.449 -    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
   1.450 -      simp: product_algebra_def sigma_def sigma_sets.Empty generator_def emb_def)
   1.451 -  from `i \<in> I` show "space ?G \<in> sets ?G"
   1.452 -    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"]
   1.453 -      simp: generator_def emb_def)
   1.454 -  fix A assume "A \<in> sets ?G"
   1.455 -  then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA"
   1.456 -    by (auto simp: generator_def)
   1.457 -  fix B assume "B \<in> sets ?G"
   1.458 -  then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB"
   1.459 -    by (auto simp: generator_def)
   1.460 -  let ?RA = "emb (JA \<union> JB) JA XA"
   1.461 -  let ?RB = "emb (JA \<union> JB) JB XB"
   1.462 -  interpret JAB: finite_product_sigma_algebra M "JA \<union> JB"
   1.463 -    by default (insert XA XB, auto)
   1.464 -  have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
   1.465 -    using XA A XB B by (auto simp: emb_simps)
   1.466 -  then show "A - B \<in> sets ?G" "A \<union> B \<in> sets ?G"
   1.467 -    using XA XB by (auto intro!: generatorI')
   1.468 +    by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
   1.469 +       auto
   1.470  qed
   1.471  
   1.472  lemma (in product_prob_space) positive_\<mu>G: 
   1.473    assumes "I \<noteq> {}"
   1.474    shows "positive generator \<mu>G"
   1.475  proof -
   1.476 -  interpret G!: algebra generator by (rule algebra_generator) fact
   1.477 +  interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
   1.478    show ?thesis
   1.479    proof (intro positive_def[THEN iffD2] conjI ballI)
   1.480      from generatorE[OF G.empty_sets] guess J X . note this[simp]
   1.481      interpret J: finite_product_sigma_finite M J by default fact
   1.482      have "X = {}"
   1.483 -      by (rule emb_injective[of J I]) simp_all
   1.484 +      by (rule prod_emb_injective[of J I]) simp_all
   1.485      then show "\<mu>G {} = 0" by simp
   1.486    next
   1.487 -    fix A assume "A \<in> sets generator"
   1.488 +    fix A assume "A \<in> generator"
   1.489      from generatorE[OF this] guess J X . note this[simp]
   1.490      interpret J: finite_product_sigma_finite M J by default fact
   1.491 -    show "0 \<le> \<mu>G A" by simp
   1.492 +    show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
   1.493    qed
   1.494  qed
   1.495  
   1.496 @@ -342,102 +319,47 @@
   1.497    assumes "I \<noteq> {}"
   1.498    shows "additive generator \<mu>G"
   1.499  proof -
   1.500 -  interpret G!: algebra generator by (rule algebra_generator) fact
   1.501 +  interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
   1.502    show ?thesis
   1.503    proof (intro additive_def[THEN iffD2] ballI impI)
   1.504 -    fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this
   1.505 -    fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this
   1.506 +    fix A assume "A \<in> generator" with generatorE guess J X . note J = this
   1.507 +    fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
   1.508      assume "A \<inter> B = {}"
   1.509      have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
   1.510        using J K by auto
   1.511      interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
   1.512      have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
   1.513 -      apply (rule emb_injective[of "J \<union> K" I])
   1.514 +      apply (rule prod_emb_injective[of "J \<union> K" I])
   1.515        apply (insert `A \<inter> B = {}` JK J K)
   1.516 -      apply (simp_all add: JK.Int emb_simps)
   1.517 +      apply (simp_all add: Int prod_emb_Int)
   1.518        done
   1.519      have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
   1.520        using J K by simp_all
   1.521      then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
   1.522 -      by (simp add: emb_simps)
   1.523 -    also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   1.524 -      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un)
   1.525 +      by simp
   1.526 +    also have "\<dots> = emeasure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   1.527 +      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
   1.528      also have "\<dots> = \<mu>G A + \<mu>G B"
   1.529 -      using J K JK_disj by (simp add: JK.measure_additive[symmetric])
   1.530 +      using J K JK_disj by (simp add: plus_emeasure[symmetric])
   1.531      finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
   1.532    qed
   1.533  qed
   1.534  
   1.535 -lemma (in product_prob_space) finite_index_eq_finite_product:
   1.536 -  assumes "finite I"
   1.537 -  shows "sets (sigma generator) = sets (Pi\<^isub>M I M)"
   1.538 -proof safe
   1.539 -  interpret I: finite_product_sigma_algebra M I by default fact
   1.540 -  have space_generator[simp]: "space generator = space (Pi\<^isub>M I M)"
   1.541 -    by (simp add: generator_def product_algebra_def)
   1.542 -  { fix A assume "A \<in> sets (sigma generator)"
   1.543 -    then show "A \<in> sets I.P" unfolding sets_sigma
   1.544 -    proof induct
   1.545 -      case (Basic A)
   1.546 -      from generatorE[OF this] guess J X . note J = this
   1.547 -      with `finite I` have "emb I J X \<in> sets I.P" by auto
   1.548 -      with `emb I J X = A` show "A \<in> sets I.P" by simp
   1.549 -    qed auto }
   1.550 -  { fix A assume A: "A \<in> sets I.P"
   1.551 -    show "A \<in> sets (sigma generator)"
   1.552 -    proof cases
   1.553 -      assume "I = {}"
   1.554 -      with I.P_empty[OF this] A
   1.555 -      have "A = space generator \<or> A = {}" 
   1.556 -        unfolding space_generator by auto
   1.557 -      then show ?thesis
   1.558 -        by (auto simp: sets_sigma simp del: space_generator
   1.559 -                 intro: sigma_sets.Empty sigma_sets_top)
   1.560 -    next
   1.561 -      assume "I \<noteq> {}"
   1.562 -      note A this
   1.563 -      moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto
   1.564 -      ultimately show "A \<in> sets (sigma generator)"
   1.565 -        using `finite I` unfolding sets_sigma
   1.566 -        by (intro sigma_sets.Basic generatorI[of I A]) auto
   1.567 -  qed }
   1.568 -qed
   1.569 -
   1.570 -lemma (in product_prob_space) extend_\<mu>G:
   1.571 -  "\<exists>\<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and>
   1.572 -       prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
   1.573 +lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
   1.574 +  assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
   1.575 +  shows "emeasure (Pi\<^isub>M I M) (emb I J (Pi\<^isub>E J X)) = emeasure (Pi\<^isub>M J M) (Pi\<^isub>E J X)"
   1.576  proof cases
   1.577 -  assume "finite I"
   1.578 -  interpret I: finite_product_prob_space M I by default fact
   1.579 -  show ?thesis
   1.580 -  proof (intro exI[of _ "measure (Pi\<^isub>M I M)"] ballI conjI)
   1.581 -    fix A assume "A \<in> sets generator"
   1.582 -    from generatorE[OF this] guess J X . note J = this
   1.583 -    from J(1-4) `finite I` show "measure I.P A = \<mu>G A"
   1.584 -      unfolding J(6)
   1.585 -      by (subst J(5)[symmetric]) (simp add: measure_emb)
   1.586 -  next
   1.587 -    have [simp]: "space generator = space (Pi\<^isub>M I M)"
   1.588 -      by (simp add: generator_def product_algebra_def)
   1.589 -    have "\<lparr>space = space generator, sets = sets (sigma generator), measure = measure I.P\<rparr>
   1.590 -      = I.P" (is "?P = _")
   1.591 -      by (auto intro!: measure_space.equality simp: finite_index_eq_finite_product[OF `finite I`])
   1.592 -    show "prob_space ?P"
   1.593 -    proof
   1.594 -      show "measure_space ?P" using `?P = I.P` by simp default
   1.595 -      show "measure ?P (space ?P) = 1"
   1.596 -        using I.measure_space_1 by simp
   1.597 -    qed
   1.598 -  qed
   1.599 +  assume "finite I" with X show ?thesis by simp
   1.600  next
   1.601 +  let ?\<Omega> = "\<Pi>\<^isub>E i\<in>I. space (M i)"
   1.602    let ?G = generator
   1.603    assume "\<not> finite I"
   1.604    then have I_not_empty: "I \<noteq> {}" by auto
   1.605 -  interpret G!: algebra generator by (rule algebra_generator) fact
   1.606 +  interpret G!: algebra ?\<Omega> generator by (rule algebra_generator) fact
   1.607    note \<mu>G_mono =
   1.608      G.additive_increasing[OF positive_\<mu>G[OF I_not_empty] additive_\<mu>G[OF I_not_empty], THEN increasingD]
   1.609  
   1.610 -  { fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> sets ?G"
   1.611 +  { fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> ?G"
   1.612  
   1.613      from `infinite I` `finite J` obtain k where k: "k \<in> I" "k \<notin> J"
   1.614        by (metis rev_finite_subset subsetI)
   1.615 @@ -445,7 +367,7 @@
   1.616      moreover def K \<equiv> "insert k K'"
   1.617      moreover def X \<equiv> "emb K K' X'"
   1.618      ultimately have K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "X \<in> sets (Pi\<^isub>M K M)" "Z = emb I K X"
   1.619 -      "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = measure (Pi\<^isub>M K M) X"
   1.620 +      "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = emeasure (Pi\<^isub>M K M) X"
   1.621        by (auto simp: subset_insertI)
   1.622  
   1.623      let ?M = "\<lambda>y. merge J y (K - J) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M)"
   1.624 @@ -455,9 +377,9 @@
   1.625        have **: "?M y \<in> sets (Pi\<^isub>M (K - J) M)"
   1.626          using J K y by (intro merge_sets) auto
   1.627        ultimately
   1.628 -      have ***: "(merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> sets ?G"
   1.629 +      have ***: "(merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
   1.630          using J K by (intro generatorI) auto
   1.631 -      have "\<mu>G (merge J y (I - J) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = measure (Pi\<^isub>M (K - J) M) (?M y)"
   1.632 +      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)"
   1.633          unfolding * using K J by (subst \<mu>G_eq[OF _ _ _ **]) auto
   1.634        note * ** *** this }
   1.635      note merge_in_G = this
   1.636 @@ -467,16 +389,16 @@
   1.637      interpret J: finite_product_prob_space M J by default fact+
   1.638      interpret KmJ: finite_product_prob_space M "K - J" by default fact+
   1.639  
   1.640 -    have "\<mu>G Z = measure (Pi\<^isub>M (J \<union> (K - J)) M) (emb (J \<union> (K - J)) K X)"
   1.641 +    have "\<mu>G Z = emeasure (Pi\<^isub>M (J \<union> (K - J)) M) (emb (J \<union> (K - J)) K X)"
   1.642        using K J by simp
   1.643 -    also have "\<dots> = (\<integral>\<^isup>+ x. measure (Pi\<^isub>M (K - J) M) (?M x) \<partial>Pi\<^isub>M J M)"
   1.644 -      using K J by (subst measure_fold_integral) auto
   1.645 +    also have "\<dots> = (\<integral>\<^isup>+ x. emeasure (Pi\<^isub>M (K - J) M) (?M x) \<partial>Pi\<^isub>M J M)"
   1.646 +      using K J by (subst emeasure_fold_integral) auto
   1.647      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)"
   1.648        (is "_ = (\<integral>\<^isup>+x. \<mu>G (?MZ x) \<partial>Pi\<^isub>M J M)")
   1.649 -    proof (intro J.positive_integral_cong)
   1.650 +    proof (intro positive_integral_cong)
   1.651        fix x assume x: "x \<in> space (Pi\<^isub>M J M)"
   1.652        with K merge_in_G(2)[OF this]
   1.653 -      show "measure (Pi\<^isub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
   1.654 +      show "emeasure (Pi\<^isub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
   1.655          unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst \<mu>G_eq) auto
   1.656      qed
   1.657      finally have fold: "\<mu>G Z = (\<integral>\<^isup>+x. \<mu>G (?MZ x) \<partial>Pi\<^isub>M J M)" .
   1.658 @@ -490,21 +412,18 @@
   1.659      let ?q = "\<lambda>y. \<mu>G (merge J y (I - J) -` Z \<inter> space (Pi\<^isub>M I M))"
   1.660      have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
   1.661        unfolding `Z = emb I K X` using J K merge_in_G(3)
   1.662 -      by (simp add: merge_in_G  \<mu>G_eq measure_fold_measurable
   1.663 -               del: space_product_algebra cong: measurable_cong)
   1.664 +      by (simp add: merge_in_G  \<mu>G_eq emeasure_fold_measurable cong: measurable_cong)
   1.665      note this fold le_1 merge_in_G(3) }
   1.666    note fold = this
   1.667  
   1.668 -  have "\<exists>\<mu>. (\<forall>s\<in>sets ?G. \<mu> s = \<mu>G s) \<and>
   1.669 -    measure_space \<lparr>space = space ?G, sets = sets (sigma ?G), measure = \<mu>\<rparr>"
   1.670 -    (is "\<exists>\<mu>. _ \<and> measure_space (?ms \<mu>)")
   1.671 +  have "\<exists>\<mu>. (\<forall>s\<in>?G. \<mu> s = \<mu>G s) \<and> measure_space ?\<Omega> (sigma_sets ?\<Omega> ?G) \<mu>"
   1.672    proof (rule G.caratheodory_empty_continuous[OF positive_\<mu>G additive_\<mu>G])
   1.673 -    fix A assume "A \<in> sets ?G"
   1.674 +    fix A assume "A \<in> ?G"
   1.675      with generatorE guess J X . note JX = this
   1.676      interpret JK: finite_product_prob_space M J by default fact+
   1.677      from JX show "\<mu>G A \<noteq> \<infinity>" by simp
   1.678    next
   1.679 -    fix A assume A: "range A \<subseteq> sets ?G" "decseq A" "(\<Inter>i. A i) = {}"
   1.680 +    fix A assume A: "range A \<subseteq> ?G" "decseq A" "(\<Inter>i. A i) = {}"
   1.681      then have "decseq (\<lambda>i. \<mu>G (A i))"
   1.682        by (auto intro!: \<mu>G_mono simp: decseq_def)
   1.683      moreover
   1.684 @@ -515,7 +434,7 @@
   1.685          using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
   1.686        ultimately have "0 < ?a" by auto
   1.687  
   1.688 -      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = measure (Pi\<^isub>M J M) X"
   1.689 +      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (Pi\<^isub>M J M) X"
   1.690          using A by (intro allI generator_Ex) auto
   1.691        then obtain J' X' where J': "\<And>n. J' n \<noteq> {}" "\<And>n. finite (J' n)" "\<And>n. J' n \<subseteq> I" "\<And>n. X' n \<in> sets (Pi\<^isub>M (J' n) M)"
   1.692          and A': "\<And>n. A n = emb I (J' n) (X' n)"
   1.693 @@ -524,8 +443,8 @@
   1.694        moreover def X \<equiv> "\<lambda>n. emb (J n) (J' n) (X' n)"
   1.695        ultimately have J: "\<And>n. J n \<noteq> {}" "\<And>n. finite (J n)" "\<And>n. J n \<subseteq> I" "\<And>n. X n \<in> sets (Pi\<^isub>M (J n) M)"
   1.696          by auto
   1.697 -      with A' have A_eq: "\<And>n. A n = emb I (J n) (X n)" "\<And>n. A n \<in> sets ?G"
   1.698 -        unfolding J_def X_def by (subst emb_trans) (insert A, auto)
   1.699 +      with A' have A_eq: "\<And>n. A n = emb I (J n) (X n)" "\<And>n. A n \<in> ?G"
   1.700 +        unfolding J_def X_def by (subst prod_emb_trans) (insert A, auto)
   1.701  
   1.702        have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"
   1.703          unfolding J_def by force
   1.704 @@ -538,8 +457,8 @@
   1.705  
   1.706        let ?M = "\<lambda>K Z y. merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
   1.707  
   1.708 -      { fix Z k assume Z: "range Z \<subseteq> sets ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
   1.709 -        then have Z_sets: "\<And>n. Z n \<in> sets ?G" by auto
   1.710 +      { fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
   1.711 +        then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
   1.712          fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
   1.713          interpret J': finite_product_prob_space M J' by default fact+
   1.714  
   1.715 @@ -552,13 +471,13 @@
   1.716              by (rule measurable_sets) auto }
   1.717          note Q_sets = this
   1.718  
   1.719 -        have "?a / 2^(k+1) \<le> (INF n. measure (Pi\<^isub>M J' M) (?Q n))"
   1.720 +        have "?a / 2^(k+1) \<le> (INF n. emeasure (Pi\<^isub>M J' M) (?Q n))"
   1.721          proof (intro INF_greatest)
   1.722            fix n
   1.723            have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
   1.724            also have "\<dots> \<le> (\<integral>\<^isup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^isub>M J' M)"
   1.725 -            unfolding fold(2)[OF J' `Z n \<in> sets ?G`]
   1.726 -          proof (intro J'.positive_integral_mono)
   1.727 +            unfolding fold(2)[OF J' `Z n \<in> ?G`]
   1.728 +          proof (intro positive_integral_mono)
   1.729              fix x assume x: "x \<in> space (Pi\<^isub>M J' M)"
   1.730              then have "?q n x \<le> 1 + 0"
   1.731                using J' Z fold(3) Z_sets by auto
   1.732 @@ -568,15 +487,15 @@
   1.733              with x show "?q n x \<le> indicator (?Q n) x + ?a / 2^(k+1)"
   1.734                by (auto split: split_indicator simp del: power_Suc)
   1.735            qed
   1.736 -          also have "\<dots> = measure (Pi\<^isub>M J' M) (?Q n) + ?a / 2^(k+1)"
   1.737 -            using `0 \<le> ?a` Q_sets J'.measure_space_1
   1.738 -            by (subst J'.positive_integral_add) auto
   1.739 -          finally show "?a / 2^(k+1) \<le> measure (Pi\<^isub>M J' M) (?Q n)" using `?a \<le> 1`
   1.740 -            by (cases rule: ereal2_cases[of ?a "measure (Pi\<^isub>M J' M) (?Q n)"])
   1.741 +          also have "\<dots> = emeasure (Pi\<^isub>M J' M) (?Q n) + ?a / 2^(k+1)"
   1.742 +            using `0 \<le> ?a` Q_sets J'.emeasure_space_1
   1.743 +            by (subst positive_integral_add) auto
   1.744 +          finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^isub>M J' M) (?Q n)" using `?a \<le> 1`
   1.745 +            by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^isub>M J' M) (?Q n)"])
   1.746                 (auto simp: field_simps)
   1.747          qed
   1.748 -        also have "\<dots> = measure (Pi\<^isub>M J' M) (\<Inter>n. ?Q n)"
   1.749 -        proof (intro J'.continuity_from_above)
   1.750 +        also have "\<dots> = emeasure (Pi\<^isub>M J' M) (\<Inter>n. ?Q n)"
   1.751 +        proof (intro INF_emeasure_decseq)
   1.752            show "range ?Q \<subseteq> sets (Pi\<^isub>M J' M)" using Q_sets by auto
   1.753            show "decseq ?Q"
   1.754              unfolding decseq_def
   1.755 @@ -587,13 +506,13 @@
   1.756              also have "?q n x \<le> ?q m x"
   1.757              proof (rule \<mu>G_mono)
   1.758                from fold(4)[OF J', OF Z_sets x]
   1.759 -              show "?M J' (Z n) x \<in> sets ?G" "?M J' (Z m) x \<in> sets ?G" by auto
   1.760 +              show "?M J' (Z n) x \<in> ?G" "?M J' (Z m) x \<in> ?G" by auto
   1.761                show "?M J' (Z n) x \<subseteq> ?M J' (Z m) x"
   1.762                  using `decseq Z`[THEN decseqD, OF `m \<le> n`] by auto
   1.763              qed
   1.764              finally show "?a / 2^(k+1) \<le> ?q m x" .
   1.765            qed
   1.766 -        qed (intro J'.finite_measure Q_sets)
   1.767 +        qed simp
   1.768          finally have "(\<Inter>n. ?Q n) \<noteq> {}"
   1.769            using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
   1.770          then have "\<exists>w\<in>space (Pi\<^isub>M J' M). \<forall>n. ?a / 2 ^ (k + 1) \<le> ?q n w" by auto }
   1.771 @@ -631,12 +550,12 @@
   1.772                show "w k \<in> space (Pi\<^isub>M (J (Suc k)) M)"
   1.773                  using Suc by simp
   1.774                then show "restrict (w k) (J k) = w k"
   1.775 -                by (simp add: extensional_restrict)
   1.776 +                by (simp add: extensional_restrict space_PiM)
   1.777              qed
   1.778            next
   1.779              assume "J k \<noteq> J (Suc k)"
   1.780              with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
   1.781 -            have "range (\<lambda>n. ?M (J k) (A n) (w k)) \<subseteq> sets ?G"
   1.782 +            have "range (\<lambda>n. ?M (J k) (A n) (w k)) \<subseteq> ?G"
   1.783                "decseq (\<lambda>n. ?M (J k) (A n) (w k))"
   1.784                "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) (w k))"
   1.785                using `decseq A` fold(4)[OF J(1-3) A_eq(2), of "w k" k] Suc
   1.786 @@ -651,11 +570,11 @@
   1.787                by (auto intro!: ext split: split_merge)
   1.788              have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
   1.789                using w'(1) J(3)[of "Suc k"]
   1.790 -              by (auto split: split_merge intro!: extensional_merge_sub) force+
   1.791 +              by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
   1.792              show ?thesis
   1.793                apply (rule exI[of _ ?w])
   1.794                using w' J_mono[of k "Suc k"] wk unfolding *
   1.795 -              apply (auto split: split_merge intro!: extensional_merge_sub ext)
   1.796 +              apply (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM)
   1.797                apply (force simp: extensional_def)
   1.798                done
   1.799            qed
   1.800 @@ -675,7 +594,7 @@
   1.801          then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto
   1.802          then have "\<exists>x\<in>A k. restrict x (J k) = w k"
   1.803            using `w k \<in> space (Pi\<^isub>M (J k) M)`
   1.804 -          by (intro rev_bexI) (auto intro!: ext simp: extensional_def)
   1.805 +          by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)
   1.806          ultimately have "w k \<in> space (Pi\<^isub>M (J k) M)"
   1.807            "\<exists>x\<in>A k. restrict x (J k) = w k"
   1.808            "k \<noteq> 0 \<Longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1)"
   1.809 @@ -707,17 +626,17 @@
   1.810        have w'_simps2: "\<And>i. i \<notin> (\<Union>k. J k) \<Longrightarrow> i \<in> I \<Longrightarrow> w' i \<in> space (M i)"
   1.811          using J by (auto simp: w'_def intro!: someI_ex[OF M.not_empty[unfolded ex_in_conv[symmetric]]])
   1.812        { fix i assume "i \<in> I" then have "w' i \<in> space (M i)"
   1.813 -          using w(1) by (cases "i \<in> (\<Union>k. J k)") (force simp: w'_simps2 w'_eq)+ }
   1.814 +          using w(1) by (cases "i \<in> (\<Union>k. J k)") (force simp: w'_simps2 w'_eq space_PiM)+ }
   1.815        note w'_simps[simp] = w'_eq w'_simps1 w'_simps2 this
   1.816  
   1.817        have w': "w' \<in> space (Pi\<^isub>M I M)"
   1.818 -        using w(1) by (auto simp add: Pi_iff extensional_def)
   1.819 +        using w(1) by (auto simp add: Pi_iff extensional_def space_PiM)
   1.820  
   1.821        { fix n
   1.822          have "restrict w' (J n) = w n" using w(1)
   1.823 -          by (auto simp add: fun_eq_iff restrict_def Pi_iff extensional_def)
   1.824 +          by (auto simp add: fun_eq_iff restrict_def Pi_iff extensional_def space_PiM)
   1.825          with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
   1.826 -        then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: emb_def) }
   1.827 +        then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
   1.828        then have "w' \<in> (\<Inter>i. A i)" by auto
   1.829        with `(\<Inter>i. A i) = {}` show False by auto
   1.830      qed
   1.831 @@ -726,276 +645,76 @@
   1.832    qed fact+
   1.833    then guess \<mu> .. note \<mu> = this
   1.834    show ?thesis
   1.835 -  proof (intro exI[of _ \<mu>] conjI)
   1.836 -    show "\<forall>S\<in>sets ?G. \<mu> S = \<mu>G S" using \<mu> by simp
   1.837 -    show "prob_space (?ms \<mu>)"
   1.838 -    proof
   1.839 -      show "measure_space (?ms \<mu>)" using \<mu> by simp
   1.840 -      obtain i where "i \<in> I" using I_not_empty by auto
   1.841 -      interpret i: finite_product_sigma_finite M "{i}" by default auto
   1.842 -      let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)"
   1.843 -      have X: "?X \<in> sets (Pi\<^isub>M {i} M)"
   1.844 -        by auto
   1.845 -      with `i \<in> I` have "emb I {i} ?X \<in> sets generator"
   1.846 -        by (intro generatorI') auto
   1.847 -      with \<mu> have "\<mu> (emb I {i} ?X) = \<mu>G (emb I {i} ?X)" by auto
   1.848 -      with \<mu>G_eq[OF _ _ _ X] `i \<in> I` 
   1.849 -      have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
   1.850 -        by (simp add: i.measure_times)
   1.851 -      also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
   1.852 -        using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def)
   1.853 -      finally show "measure (?ms \<mu>) (space (?ms \<mu>)) = 1"
   1.854 -        using M.measure_space_1 by (simp add: infprod_algebra_def)
   1.855 -    qed
   1.856 +  proof (subst emeasure_extend_measure_Pair[OF PiM_def, of I M \<mu> J X])
   1.857 +    from assms show "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
   1.858 +      by (simp add: Pi_iff)
   1.859 +  next
   1.860 +    fix J X assume J: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
   1.861 +    then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
   1.862 +      by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
   1.863 +    have "emb I J (Pi\<^isub>E J X) \<in> generator"
   1.864 +      using J `I \<noteq> {}` by (intro generatorI') auto
   1.865 +    then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
   1.866 +      using \<mu> by simp
   1.867 +    also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
   1.868 +      using J  `I \<noteq> {}` by (subst \<mu>G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff)
   1.869 +    also have "\<dots> = (\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}.
   1.870 +      if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
   1.871 +      using J `I \<noteq> {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1)
   1.872 +    finally show "\<mu> (emb I J (Pi\<^isub>E J X)) = \<dots>" .
   1.873 +  next
   1.874 +    let ?F = "\<lambda>j. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j))"
   1.875 +    have "(\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}. ?F j) = (\<Prod>j\<in>J. ?F j)"
   1.876 +      using X `I \<noteq> {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1)
   1.877 +    then show "(\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}. ?F j) =
   1.878 +      emeasure (Pi\<^isub>M J M) (Pi\<^isub>E J X)"
   1.879 +      using X by (auto simp add: emeasure_PiM) 
   1.880 +  next
   1.881 +    show "positive (sets (Pi\<^isub>M I M)) \<mu>" "countably_additive (sets (Pi\<^isub>M I M)) \<mu>"
   1.882 +      using \<mu> unfolding sets_PiM_generator[OF `I \<noteq> {}`] by (auto simp: measure_space_def)
   1.883    qed
   1.884  qed
   1.885  
   1.886 -lemma (in product_prob_space) infprod_spec:
   1.887 -  "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> prob_space (Pi\<^isub>P I M)"
   1.888 -  (is "?Q infprod_algebra")
   1.889 -  unfolding infprod_algebra_def
   1.890 -  by (rule someI2_ex[OF extend_\<mu>G])
   1.891 -     (auto simp: sigma_def generator_def)
   1.892 -
   1.893 -sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
   1.894 -  using infprod_spec by simp
   1.895 -
   1.896 -lemma (in product_prob_space) measure_infprod_emb:
   1.897 -  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
   1.898 -  shows "\<mu> (emb I J X) = measure (Pi\<^isub>M J M) X"
   1.899 -proof -
   1.900 -  have "emb I J X \<in> sets generator"
   1.901 -    using assms by (rule generatorI')
   1.902 -  with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
   1.903 -qed
   1.904 -
   1.905 -lemma (in product_prob_space) measurable_component:
   1.906 -  assumes "i \<in> I"
   1.907 -  shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)"
   1.908 -proof (unfold measurable_def, safe)
   1.909 -  fix x assume "x \<in> space (Pi\<^isub>P I M)"
   1.910 -  then show "x i \<in> space (M i)"
   1.911 -    using `i \<in> I` by (auto simp: infprod_algebra_def generator_def)
   1.912 -next
   1.913 -  fix A assume "A \<in> sets (M i)"
   1.914 -  with `i \<in> I` have
   1.915 -    "(\<Pi>\<^isub>E x \<in> {i}. A) \<in> sets (Pi\<^isub>M {i} M)"
   1.916 -    "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) = emb I {i} (\<Pi>\<^isub>E x \<in> {i}. A)"
   1.917 -    by (auto simp: infprod_algebra_def generator_def emb_def)
   1.918 -  from generatorI[OF _ _ _ this] `i \<in> I`
   1.919 -  show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)"
   1.920 -    unfolding infprod_algebra_def by auto
   1.921 -qed
   1.922 -
   1.923 -lemma (in product_prob_space) emb_in_infprod_algebra[intro]:
   1.924 -  fixes J assumes J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (Pi\<^isub>M J M)"
   1.925 -  shows "emb I J X \<in> sets (\<Pi>\<^isub>P i\<in>I. M i)"
   1.926 -proof cases
   1.927 -  assume "J = {}"
   1.928 -  with X have "emb I J X = space (\<Pi>\<^isub>P i\<in>I. M i) \<or> emb I J X = {}"
   1.929 -    by (auto simp: emb_def infprod_algebra_def generator_def
   1.930 -                   product_algebra_def product_algebra_generator_def image_constant sigma_def)
   1.931 -  then show ?thesis by auto
   1.932 -next
   1.933 -  assume "J \<noteq> {}"
   1.934 -  show ?thesis unfolding infprod_algebra_def
   1.935 -    by simp (intro in_sigma generatorI'  `J \<noteq> {}` J X)
   1.936 -qed
   1.937 -
   1.938 -lemma (in product_prob_space) finite_measure_infprod_emb:
   1.939 -  assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
   1.940 -  shows "\<mu>' (emb I J X) = finite_measure.\<mu>' (Pi\<^isub>M J M) X"
   1.941 -proof -
   1.942 -  interpret J: finite_product_prob_space M J by default fact+
   1.943 -  from assms have "emb I J X \<in> sets (Pi\<^isub>P I M)" by auto
   1.944 -  with assms show "\<mu>' (emb I J X) = J.\<mu>' X"
   1.945 -    unfolding \<mu>'_def J.\<mu>'_def
   1.946 -    unfolding measure_infprod_emb[OF assms]
   1.947 -    by auto
   1.948 -qed
   1.949 -
   1.950 -lemma (in finite_product_prob_space) finite_measure_times:
   1.951 -  assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
   1.952 -  shows "\<mu>' (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu>' i (A i))"
   1.953 -  using assms
   1.954 -  unfolding \<mu>'_def M.\<mu>'_def
   1.955 -  by (subst measure_times[OF assms])
   1.956 -     (auto simp: finite_measure_eq M.finite_measure_eq setprod_ereal)
   1.957 -
   1.958 -lemma (in product_prob_space) finite_measure_infprod_emb_Pi:
   1.959 -  assumes J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> X j \<in> sets (M j)"
   1.960 -  shows "\<mu>' (emb I J (Pi\<^isub>E J X)) = (\<Prod>j\<in>J. M.\<mu>' j (X j))"
   1.961 -proof cases
   1.962 -  assume "J = {}"
   1.963 -  then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra"
   1.964 -    by (auto simp: infprod_algebra_def generator_def sigma_def emb_def)
   1.965 -  then show ?thesis using `J = {}` P.prob_space
   1.966 -    by simp
   1.967 -next
   1.968 -  assume "J \<noteq> {}"
   1.969 -  interpret J: finite_product_prob_space M J by default fact+
   1.970 -  have "(\<Prod>i\<in>J. M.\<mu>' i (X i)) = J.\<mu>' (Pi\<^isub>E J X)"
   1.971 -    using J `J \<noteq> {}` by (subst J.finite_measure_times) auto
   1.972 -  also have "\<dots> = \<mu>' (emb I J (Pi\<^isub>E J X))"
   1.973 -    using J `J \<noteq> {}` by (intro finite_measure_infprod_emb[symmetric]) auto
   1.974 -  finally show ?thesis by simp
   1.975 -qed
   1.976 -
   1.977 -lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
   1.978 +sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>M I M"
   1.979  proof
   1.980 -  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
   1.981 -    by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros)
   1.982 -qed
   1.983 -
   1.984 -lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
   1.985 -proof
   1.986 -  fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
   1.987 -    by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
   1.988 +  show "emeasure (Pi\<^isub>M I M) (space (Pi\<^isub>M I M)) = 1"
   1.989 +  proof cases
   1.990 +    assume "I = {}" then show ?thesis by (simp add: space_PiM_empty)
   1.991 +  next
   1.992 +    assume "I \<noteq> {}"
   1.993 +    then obtain i where "i \<in> I" by auto
   1.994 +    moreover then have "emb I {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i)) = (space (Pi\<^isub>M I M))"
   1.995 +      by (auto simp: prod_emb_def space_PiM)
   1.996 +    ultimately show ?thesis
   1.997 +      using emeasure_PiM_emb_not_empty[of "{i}" "\<lambda>i. space (M i)"]
   1.998 +      by (simp add: emeasure_PiM emeasure_space_1)
   1.999 +  qed
  1.1000  qed
  1.1001  
  1.1002 -lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
  1.1003 -  by (auto intro: sigma_sets.Basic)
  1.1004 -
  1.1005 -lemma (in product_prob_space) infprod_algebra_alt:
  1.1006 -  "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
  1.1007 -    sets = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i))),
  1.1008 -    measure = measure (Pi\<^isub>P I M) \<rparr>"
  1.1009 -  (is "_ = sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>")
  1.1010 -proof (rule measure_space.equality)
  1.1011 -  let ?G = "\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M)"
  1.1012 -  have "sigma_sets ?O ?M = sigma_sets ?O ?G"
  1.1013 -  proof (intro equalityI sigma_sets_mono UN_least)
  1.1014 -    fix J assume J: "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}"
  1.1015 -    have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto
  1.1016 -    also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper)
  1.1017 -    also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_superset_generator)
  1.1018 -    finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> sigma_sets ?O ?G" .
  1.1019 -    have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
  1.1020 -      by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
  1.1021 -    also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
  1.1022 -      using J M.sets_into_space
  1.1023 -      by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
  1.1024 -    also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
  1.1025 -      using J by (intro sigma_sets_mono') auto
  1.1026 -    finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
  1.1027 -      by (simp add: infprod_algebra_def generator_def)
  1.1028 -  qed
  1.1029 -  then show "sets (Pi\<^isub>P I M) = sets (sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>)"
  1.1030 -    by (simp_all add: infprod_algebra_def generator_def sets_sigma)
  1.1031 -qed simp_all
  1.1032 -
  1.1033 -lemma (in product_prob_space) infprod_algebra_alt2:
  1.1034 -  "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
  1.1035 -    sets = (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i)),
  1.1036 -    measure = measure (Pi\<^isub>P I M) \<rparr>"
  1.1037 -  (is "_ = ?S")
  1.1038 -proof (rule measure_space.equality)
  1.1039 -  let "sigma \<lparr> space = ?O, sets = ?A, \<dots> = _ \<rparr>" = ?S
  1.1040 -  let ?G = "(\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
  1.1041 -  have "sets (Pi\<^isub>P I M) = sigma_sets ?O ?G"
  1.1042 -    by (subst infprod_algebra_alt) (simp add: sets_sigma)
  1.1043 -  also have "\<dots> = sigma_sets ?O ?A"
  1.1044 -  proof (intro equalityI sigma_sets_mono subsetI)
  1.1045 -    interpret A: sigma_algebra ?S
  1.1046 -      by (rule sigma_algebra_sigma) auto
  1.1047 -    fix A assume "A \<in> ?G"
  1.1048 -    then obtain J B where "finite J" "J \<noteq> {}" "J \<subseteq> I" "A = emb I J (Pi\<^isub>E J B)"
  1.1049 -        and B: "\<And>i. i \<in> J \<Longrightarrow> B i \<in> sets (M i)"
  1.1050 -      by auto
  1.1051 -    then have A: "A = (\<Inter>j\<in>J. (\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M))"
  1.1052 -      by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
  1.1053 -    { fix j assume "j\<in>J"
  1.1054 -      with `J \<subseteq> I` have "j \<in> I" by auto
  1.1055 -      with `j \<in> J` B have "(\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M) \<in> sets ?S"
  1.1056 -        by (auto simp: sets_sigma intro: sigma_sets.Basic) }
  1.1057 -    with `finite J` `J \<noteq> {}` have "A \<in> sets ?S"
  1.1058 -      unfolding A by (intro A.finite_INT) auto
  1.1059 -    then show "A \<in> sigma_sets ?O ?A" by (simp add: sets_sigma)
  1.1060 -  next
  1.1061 -    fix A assume "A \<in> ?A"
  1.1062 -    then obtain i B where i: "i \<in> I" "B \<in> sets (M i)"
  1.1063 -        and "A = (\<lambda>x. x i) -` B \<inter> space (Pi\<^isub>P I M)"
  1.1064 -      by auto
  1.1065 -    then have "A = emb I {i} (Pi\<^isub>E {i} (\<lambda>_. B))"
  1.1066 -      by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
  1.1067 -    with i show "A \<in> sigma_sets ?O ?G"
  1.1068 -      by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto
  1.1069 -  qed
  1.1070 -  also have "\<dots> = sets ?S"
  1.1071 -    by (simp add: sets_sigma)
  1.1072 -  finally show "sets (Pi\<^isub>P I M) = sets ?S" .
  1.1073 -qed simp_all
  1.1074 -
  1.1075 -lemma (in product_prob_space) measurable_into_infprod_algebra:
  1.1076 -  assumes "sigma_algebra N"
  1.1077 -  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)"
  1.1078 -  assumes ext: "\<And>x. x \<in> space N \<Longrightarrow> f x \<in> extensional I"
  1.1079 -  shows "f \<in> measurable N (Pi\<^isub>P I M)"
  1.1080 -proof -
  1.1081 -  interpret N: sigma_algebra N by fact
  1.1082 -  have f_in: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> space N \<rightarrow> space (M i)"
  1.1083 -    using f by (auto simp: measurable_def)
  1.1084 -  { fix i A assume i: "i \<in> I" "A \<in> sets (M i)"
  1.1085 -    then have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N = (\<lambda>x. f x i) -` A \<inter> space N"
  1.1086 -      using f_in ext by (auto simp: infprod_algebra_def generator_def)
  1.1087 -    also have "\<dots> \<in> sets N"
  1.1088 -      by (rule measurable_sets f i)+
  1.1089 -    finally have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N \<in> sets N" . }
  1.1090 -  with f_in ext show ?thesis
  1.1091 -    by (subst infprod_algebra_alt2)
  1.1092 -       (auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def)
  1.1093 +lemma (in product_prob_space) emeasure_PiM_emb:
  1.1094 +  assumes X: "J \<subseteq> I" "finite J" "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
  1.1095 +  shows "emeasure (Pi\<^isub>M I M) (emb I J (Pi\<^isub>E J X)) = (\<Prod> i\<in>J. emeasure (M i) (X i))"
  1.1096 +proof cases
  1.1097 +  assume "J = {}"
  1.1098 +  moreover have "emb I {} {\<lambda>x. undefined} = space (Pi\<^isub>M I M)"
  1.1099 +    by (auto simp: space_PiM prod_emb_def)
  1.1100 +  ultimately show ?thesis
  1.1101 +    by (simp add: space_PiM_empty P.emeasure_space_1)
  1.1102 +next
  1.1103 +  assume "J \<noteq> {}" with X show ?thesis
  1.1104 +    by (subst emeasure_PiM_emb_not_empty) (auto simp: emeasure_PiM)
  1.1105  qed
  1.1106  
  1.1107 -lemma (in product_prob_space) measurable_singleton_infprod:
  1.1108 -  assumes "i \<in> I"
  1.1109 -  shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)"
  1.1110 -proof (unfold measurable_def, intro CollectI conjI ballI)
  1.1111 -  show "(\<lambda>x. x i) \<in> space (Pi\<^isub>P I M) \<rightarrow> space (M i)"
  1.1112 -    using M.sets_into_space `i \<in> I`
  1.1113 -    by (auto simp: infprod_algebra_def generator_def)
  1.1114 -  fix A assume "A \<in> sets (M i)"
  1.1115 -  have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) = emb I {i} (\<Pi>\<^isub>E _\<in>{i}. A)"
  1.1116 -    by (auto simp: infprod_algebra_def generator_def emb_def)
  1.1117 -  also have "\<dots> \<in> sets (Pi\<^isub>P I M)"
  1.1118 -    using `i \<in> I` `A \<in> sets (M i)`
  1.1119 -    by (intro emb_in_infprod_algebra product_algebraI) auto
  1.1120 -  finally show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)" .
  1.1121 -qed
  1.1122 +lemma (in product_prob_space) measure_PiM_emb:
  1.1123 +  assumes "J \<subseteq> I" "finite J" "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
  1.1124 +  shows "measure (PiM I M) (emb I J (Pi\<^isub>E J X)) = (\<Prod> i\<in>J. measure (M i) (X i))"
  1.1125 +  using emeasure_PiM_emb[OF assms]
  1.1126 +  unfolding emeasure_eq_measure M.emeasure_eq_measure by (simp add: setprod_ereal)
  1.1127  
  1.1128 -lemma (in product_prob_space) sigma_product_algebra_sigma_eq:
  1.1129 -  assumes M: "\<And>i. i \<in> I \<Longrightarrow> M i = sigma (E i)"
  1.1130 -  shows "sets (Pi\<^isub>P I M) = sigma_sets (space (Pi\<^isub>P I M)) (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (E i))"
  1.1131 -proof -
  1.1132 -  let ?E = "(\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (E i))"
  1.1133 -  let ?M = "(\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i))"
  1.1134 -  { fix i A assume "i\<in>I" "A \<in> sets (E i)"
  1.1135 -    then have "A \<in> sets (M i)" using M by auto
  1.1136 -    then have "A \<in> Pow (space (M i))" using M.sets_into_space by auto
  1.1137 -    then have "A \<in> Pow (space (E i))" using M[OF `i \<in> I`] by auto }
  1.1138 -  moreover
  1.1139 -  have "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. x i) \<in> space infprod_algebra \<rightarrow> space (E i)"
  1.1140 -    by (auto simp: M infprod_algebra_def generator_def Pi_iff)
  1.1141 -  ultimately have "sigma_sets (space (Pi\<^isub>P I M)) ?M \<subseteq> sigma_sets (space (Pi\<^isub>P I M)) ?E"
  1.1142 -    apply (intro sigma_sets_mono UN_least)
  1.1143 -    apply (simp add: sets_sigma M)
  1.1144 -    apply (subst sigma_sets_vimage[symmetric])
  1.1145 -    apply (auto intro!: sigma_sets_mono')
  1.1146 -    done
  1.1147 -  moreover have "sigma_sets (space (Pi\<^isub>P I M)) ?E \<subseteq> sigma_sets (space (Pi\<^isub>P I M)) ?M"
  1.1148 -    by (intro sigma_sets_mono') (auto simp: M)
  1.1149 -  ultimately show ?thesis
  1.1150 -    by (subst infprod_algebra_alt2) (auto simp: sets_sigma)
  1.1151 -qed
  1.1152 -
  1.1153 -lemma (in product_prob_space) Int_proj_eq_emb:
  1.1154 -  assumes "J \<noteq> {}" "J \<subseteq> I"
  1.1155 -  shows "(\<Inter>i\<in>J. (\<lambda>x. x i) -` A i \<inter> space (Pi\<^isub>P I M)) = emb I J (Pi\<^isub>E J A)"
  1.1156 -  using assms by (auto simp: infprod_algebra_def generator_def emb_def Pi_iff)
  1.1157 -
  1.1158 -lemma (in product_prob_space) emb_insert:
  1.1159 -  "i \<notin> J \<Longrightarrow> emb I J (Pi\<^isub>E J f) \<inter> ((\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) =
  1.1160 -    emb I (insert i J) (Pi\<^isub>E (insert i J) (f(i := A)))"
  1.1161 -  by (auto simp: emb_def Pi_iff infprod_algebra_def generator_def split: split_if_asm)
  1.1162 +lemma (in finite_product_prob_space) finite_measure_PiM_emb:
  1.1163 +  "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
  1.1164 +  using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets_into_space, of I A M]
  1.1165 +  by auto
  1.1166  
  1.1167  subsection {* Sequence space *}
  1.1168  
  1.1169 @@ -1003,36 +722,30 @@
  1.1170  
  1.1171  lemma (in sequence_space) infprod_in_sets[intro]:
  1.1172    fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
  1.1173 -  shows "Pi UNIV E \<in> sets (Pi\<^isub>P UNIV M)"
  1.1174 +  shows "Pi UNIV E \<in> sets (Pi\<^isub>M UNIV M)"
  1.1175  proof -
  1.1176    have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
  1.1177 -    using E E[THEN M.sets_into_space]
  1.1178 -    by (auto simp: emb_def Pi_iff extensional_def) blast
  1.1179 -  with E show ?thesis
  1.1180 -    by (auto intro: emb_in_infprod_algebra)
  1.1181 +    using E E[THEN sets_into_space]
  1.1182 +    by (auto simp: prod_emb_def Pi_iff extensional_def) blast
  1.1183 +  with E show ?thesis by auto
  1.1184  qed
  1.1185  
  1.1186 -lemma (in sequence_space) measure_infprod:
  1.1187 +lemma (in sequence_space) measure_PiM_countable:
  1.1188    fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
  1.1189 -  shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (Pi UNIV E)"
  1.1190 +  shows "(\<lambda>n. \<Prod>i\<le>n. measure (M i) (E i)) ----> measure (Pi\<^isub>M UNIV M) (Pi UNIV E)"
  1.1191  proof -
  1.1192    let ?E = "\<lambda>n. emb UNIV {..n} (Pi\<^isub>E {.. n} E)"
  1.1193 -  { fix n :: nat
  1.1194 -    interpret n: finite_product_prob_space M "{..n}" by default auto
  1.1195 -    have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"
  1.1196 -      using E by (subst n.finite_measure_times) auto
  1.1197 -    also have "\<dots> = \<mu>' (?E n)"
  1.1198 -      using E by (intro finite_measure_infprod_emb[symmetric]) auto
  1.1199 -    finally have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = \<mu>' (?E n)" . }
  1.1200 +  have "\<And>n. (\<Prod>i\<le>n. measure (M i) (E i)) = measure (Pi\<^isub>M UNIV M) (?E n)"
  1.1201 +    using E by (simp add: measure_PiM_emb)
  1.1202    moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
  1.1203 -    using E E[THEN M.sets_into_space]
  1.1204 -    by (auto simp: emb_def extensional_def Pi_iff) blast
  1.1205 -  moreover have "range ?E \<subseteq> sets (Pi\<^isub>P UNIV M)"
  1.1206 +    using E E[THEN sets_into_space]
  1.1207 +    by (auto simp: prod_emb_def extensional_def Pi_iff) blast
  1.1208 +  moreover have "range ?E \<subseteq> sets (Pi\<^isub>M UNIV M)"
  1.1209      using E by auto
  1.1210    moreover have "decseq ?E"
  1.1211 -    by (auto simp: emb_def Pi_iff decseq_def)
  1.1212 +    by (auto simp: prod_emb_def Pi_iff decseq_def)
  1.1213    ultimately show ?thesis
  1.1214 -    by (simp add: finite_continuity_from_above)
  1.1215 +    by (simp add: finite_Lim_measure_decseq)
  1.1216  qed
  1.1217  
  1.1218  end
  1.1219 \ No newline at end of file