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.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.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.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.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
```