src/HOL/Probability/Projective_Family.thy
changeset 61359 e985b52c3eb3
parent 58876 1888e3cb8048
child 61605 1bf7b186542e
     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Wed Oct 07 15:31:59 2015 +0200
     1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Wed Oct 07 17:11:16 2015 +0200
     1.3 @@ -6,342 +6,672 @@
     1.4  section {*Projective Family*}
     1.5  
     1.6  theory Projective_Family
     1.7 -imports Finite_Product_Measure Probability_Measure
     1.8 +imports Finite_Product_Measure Giry_Monad
     1.9  begin
    1.10  
    1.11 -lemma (in product_prob_space) distr_restrict:
    1.12 -  assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
    1.13 -  shows "(\<Pi>\<^sub>M i\<in>J. M i) = distr (\<Pi>\<^sub>M i\<in>K. M i) (\<Pi>\<^sub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D")
    1.14 -proof (rule measure_eqI_generator_eq)
    1.15 -  have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
    1.16 -  interpret J: finite_product_prob_space M J proof qed fact
    1.17 -  interpret K: finite_product_prob_space M K proof qed fact
    1.18 -
    1.19 -  let ?J = "{Pi\<^sub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
    1.20 -  let ?F = "\<lambda>i. \<Pi>\<^sub>E k\<in>J. space (M k)"
    1.21 -  let ?\<Omega> = "(\<Pi>\<^sub>E k\<in>J. space (M k))"
    1.22 -  show "Int_stable ?J"
    1.23 -    by (rule Int_stable_PiE)
    1.24 -  show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
    1.25 -    using `finite J` by (auto intro!: prod_algebraI_finite)
    1.26 -  { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
    1.27 -  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space)
    1.28 -  show "sets (\<Pi>\<^sub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
    1.29 -    using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
    1.30 -
    1.31 -  fix X assume "X \<in> ?J"
    1.32 -  then obtain E where [simp]: "X = Pi\<^sub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
    1.33 -  with `finite J` have X: "X \<in> sets (Pi\<^sub>M J M)"
    1.34 -    by simp
    1.35 -
    1.36 -  have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
    1.37 -    using E by (simp add: J.measure_times)
    1.38 -  also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
    1.39 -    by simp
    1.40 -  also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
    1.41 -    using `finite K` `J \<subseteq> K`
    1.42 -    by (intro setprod.mono_neutral_left) (auto simp: M.emeasure_space_1)
    1.43 -  also have "\<dots> = emeasure (Pi\<^sub>M K M) (\<Pi>\<^sub>E i\<in>K. if i \<in> J then E i else space (M i))"
    1.44 -    using E by (simp add: K.measure_times)
    1.45 -  also have "(\<Pi>\<^sub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^sub>E J E \<inter> (\<Pi>\<^sub>E i\<in>K. space (M i))"
    1.46 -    using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
    1.47 -  finally show "emeasure (Pi\<^sub>M J M) X = emeasure ?D X"
    1.48 -    using X `J \<subseteq> K` apply (subst emeasure_distr)
    1.49 -    by (auto intro!: measurable_restrict_subset simp: space_PiM)
    1.50 +lemma vimage_restrict_preseve_mono:
    1.51 +  assumes J: "J \<subseteq> I"
    1.52 +  and sets: "A \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" and ne: "(\<Pi>\<^sub>E i\<in>I. S i) \<noteq> {}"
    1.53 +  and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i) \<subseteq> (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
    1.54 +  shows "A \<subseteq> B"
    1.55 +proof  (intro subsetI)
    1.56 +  fix x assume "x \<in> A"
    1.57 +  from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
    1.58 +  have "J \<inter> (I - J) = {}" by auto
    1.59 +  show "x \<in> B"
    1.60 +  proof cases
    1.61 +    assume x: "x \<in> (\<Pi>\<^sub>E i\<in>J. S i)"
    1.62 +    have "merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
    1.63 +      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close>
    1.64 +      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
    1.65 +    also have "\<dots> \<subseteq> (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)" by fact
    1.66 +    finally show "x \<in> B"
    1.67 +      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> eq
    1.68 +      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
    1.69 +  qed (insert \<open>x\<in>A\<close> sets, auto)
    1.70  qed
    1.71  
    1.72 -lemma (in product_prob_space) emeasure_prod_emb[simp]:
    1.73 -  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^sub>M J M)"
    1.74 -  shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X"
    1.75 -  by (subst distr_restrict[OF L])
    1.76 -     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
    1.77 -
    1.78 -definition
    1.79 -  limP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
    1.80 -  "limP I M P = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i))
    1.81 -    {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
    1.82 -    (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j))
    1.83 -    (\<lambda>(J, X). emeasure (P J) (Pi\<^sub>E J X))"
    1.84 -
    1.85 -abbreviation "lim\<^sub>P \<equiv> limP"
    1.86 -
    1.87 -lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)"
    1.88 -  by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure)
    1.89 -
    1.90 -lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)"
    1.91 -  by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure)
    1.92 -
    1.93 -lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\<Pi>\<^sub>M i\<in>I. M i) M'"
    1.94 -  unfolding measurable_def by auto
    1.95 -
    1.96 -lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\<Pi>\<^sub>M i\<in>I. M i)"
    1.97 -  unfolding measurable_def by auto
    1.98 -
    1.99  locale projective_family =
   1.100 -  fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
   1.101 -  assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow>
   1.102 -     (P H) (prod_emb H M J X) = (P J) X"
   1.103 -  assumes proj_prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
   1.104 -  assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
   1.105 -  assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
   1.106 +  fixes I :: "'i set" and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M :: "'i \<Rightarrow> 'a measure"
   1.107 +  assumes P: "\<And>J H. J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> P J = distr (P H) (PiM J M) (\<lambda>f. restrict f J)"
   1.108 +  assumes prob_space_P: "\<And>J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> prob_space (P J)"
   1.109  begin
   1.110  
   1.111 -lemma emeasure_limP:
   1.112 -  assumes "finite J"
   1.113 -  assumes "J \<subseteq> I"
   1.114 -  assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)"
   1.115 -  shows "emeasure (limP J M P) (Pi\<^sub>E J A) = emeasure (P J) (Pi\<^sub>E J A)"
   1.116 -proof -
   1.117 -  have "Pi\<^sub>E J (restrict A J) \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))"
   1.118 -    using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast
   1.119 -  hence "emeasure (limP J M P) (Pi\<^sub>E J A) =
   1.120 -    emeasure (limP J M P) (prod_emb J M J (Pi\<^sub>E J A))"
   1.121 -    using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
   1.122 -  also have "\<dots> = emeasure (P J) (Pi\<^sub>E J A)"
   1.123 -  proof (rule emeasure_extend_measure_Pair[OF limP_def])
   1.124 -    show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
   1.125 -    show "countably_additive (sets (limP J M P)) (P J)" unfolding countably_additive_def
   1.126 -      by (auto simp: suminf_emeasure proj_sets[OF `finite J`])
   1.127 -    show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))"
   1.128 -      using assms by auto
   1.129 -    fix K and X::"'i \<Rightarrow> 'a set"
   1.130 -    show "prod_emb J M K (Pi\<^sub>E K X) \<in> Pow (\<Pi>\<^sub>E i\<in>J. space (M i))"
   1.131 -      by (auto simp: prod_emb_def)
   1.132 -    assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))"
   1.133 -    thus "emeasure (P J) (prod_emb J M K (Pi\<^sub>E K X)) = emeasure (P K) (Pi\<^sub>E K X)"
   1.134 -      using assms
   1.135 -      apply (cases "J = {}")
   1.136 -      apply (simp add: prod_emb_id)
   1.137 -      apply (fastforce simp add: intro!: projective sets_PiM_I_finite)
   1.138 -      done
   1.139 -  qed
   1.140 -  finally show ?thesis .
   1.141 -qed
   1.142 +lemma sets_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (P J) = sets (PiM J M)"
   1.143 +  by (subst P[of J J]) simp_all
   1.144 +
   1.145 +lemma space_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> space (P J) = space (PiM J M)"
   1.146 +  using sets_P by (rule sets_eq_imp_space_eq)
   1.147  
   1.148 -lemma limP_finite[simp]:
   1.149 -  assumes "finite J"
   1.150 -  assumes "J \<subseteq> I"
   1.151 -  shows "limP J M P = P J" (is "?P = _")
   1.152 -proof (rule measure_eqI_generator_eq)
   1.153 -  let ?J = "{Pi\<^sub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
   1.154 -  let ?\<Omega> = "(\<Pi>\<^sub>E k\<in>J. space (M k))"
   1.155 -  interpret prob_space "P J" using proj_prob_space `finite J` by simp
   1.156 -  show "emeasure ?P (\<Pi>\<^sub>E k\<in>J. space (M k)) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
   1.157 -  show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
   1.158 -    using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
   1.159 -  fix X assume "X \<in> ?J"
   1.160 -  then obtain E where X: "X = Pi\<^sub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
   1.161 -  with `finite J` have "X \<in> sets (limP J M P)" by simp
   1.162 -  have emb_self: "prod_emb J M J (Pi\<^sub>E J E) = Pi\<^sub>E J E"
   1.163 -    using E sets.sets_into_space
   1.164 -    by (auto intro!: prod_emb_PiE_same_index)
   1.165 -  show "emeasure (limP J M P) X = emeasure (P J) X"
   1.166 -    unfolding X using E
   1.167 -    by (intro emeasure_limP assms) simp
   1.168 -qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE)
   1.169 +lemma not_empty_M: "i \<in> I \<Longrightarrow> space (M i) \<noteq> {}"
   1.170 +  using prob_space_P[THEN prob_space.not_empty] by (auto simp: space_PiM space_P)
   1.171  
   1.172 -lemma emeasure_fun_emb[simp]:
   1.173 -  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
   1.174 -  shows "emeasure (limP L M P) (prod_emb L M J X) = emeasure (limP J M P) X"
   1.175 -  using assms
   1.176 -  by (subst limP_finite) (auto simp: limP_finite finite_subset projective)
   1.177 +lemma not_empty: "space (PiM I M) \<noteq> {}"
   1.178 +  by (simp add: not_empty_M)
   1.179  
   1.180  abbreviation
   1.181 -  "emb L K X \<equiv> prod_emb L M K X"
   1.182 +  "emb L K \<equiv> prod_emb L M K"
   1.183  
   1.184 -lemma prod_emb_injective:
   1.185 -  assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^sub>M J M)" "Y \<in> sets (Pi\<^sub>M J M)"
   1.186 -  assumes "emb L J X = emb L J Y"
   1.187 -  shows "X = Y"
   1.188 -proof (rule injective_vimage_restrict)
   1.189 +lemma emb_preserve_mono:
   1.190 +  assumes "J \<subseteq> L" "L \<subseteq> I" and sets: "X \<in> sets (Pi\<^sub>M J M)" "Y \<in> sets (Pi\<^sub>M J M)"
   1.191 +  assumes "emb L J X \<subseteq> emb L J Y"
   1.192 +  shows "X \<subseteq> Y"
   1.193 +proof (rule vimage_restrict_preseve_mono)
   1.194    show "X \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))"
   1.195      using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
   1.196 -  have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
   1.197 -  proof
   1.198 -    fix i assume "i \<in> L"
   1.199 -    interpret prob_space "P {i}" using proj_prob_space by simp
   1.200 -    from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
   1.201 -  qed
   1.202 -  from bchoice[OF this]
   1.203 -  show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
   1.204 -  show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i))"
   1.205 -    using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
   1.206 +  show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}"
   1.207 +    using \<open>L \<subseteq> I\<close> by (auto simp add: not_empty_M space_PiM[symmetric])
   1.208 +  show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<subseteq> (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^sub>E i\<in>L. space (M i))"
   1.209 +    using `prod_emb L M J X \<subseteq> prod_emb L M J Y` by (simp add: prod_emb_def)
   1.210  qed fact
   1.211  
   1.212 -definition generator :: "('i \<Rightarrow> 'a) set set" where
   1.213 -  "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^sub>M J M))"
   1.214 +lemma emb_injective:
   1.215 +  assumes L: "J \<subseteq> L" "L \<subseteq> I" and X: "X \<in> sets (Pi\<^sub>M J M)" and Y: "Y \<in> sets (Pi\<^sub>M J M)"
   1.216 +  shows "emb L J X = emb L J Y \<Longrightarrow> X = Y"
   1.217 +  by (intro antisym emb_preserve_mono[OF L X Y] emb_preserve_mono[OF L Y X]) auto
   1.218 +
   1.219 +lemma emeasure_P: "J \<subseteq> K \<Longrightarrow> finite K \<Longrightarrow> K \<subseteq> I \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> P K (emb K J X) = P J X"
   1.220 +  by (auto intro!: emeasure_distr_restrict[symmetric] simp: P sets_P)
   1.221  
   1.222 -lemma generatorI':
   1.223 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emb I J X \<in> generator"
   1.224 -  unfolding generator_def by auto
   1.225 +inductive_set generator :: "('i \<Rightarrow> 'a) set set" where
   1.226 +  "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emb I J X \<in> generator"
   1.227 +
   1.228 +lemma algebra_generator: "algebra (space (PiM I M)) generator"
   1.229 +  unfolding algebra_iff_Int
   1.230 +proof (safe elim!: generator.cases)
   1.231 +  fix J X assume J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (PiM J M)"
   1.232 +
   1.233 +  from X[THEN sets.sets_into_space] J show "x \<in> emb I J X \<Longrightarrow> x \<in> space (PiM I M)" for x
   1.234 +    by (auto simp: prod_emb_def space_PiM)
   1.235  
   1.236 -lemma algebra_generator:
   1.237 -  assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
   1.238 -  unfolding algebra_def algebra_axioms_def ring_of_sets_iff
   1.239 -proof (intro conjI ballI)
   1.240 -  let ?G = generator
   1.241 -  show "?G \<subseteq> Pow ?\<Omega>"
   1.242 -    by (auto simp: generator_def prod_emb_def)
   1.243 -  from `I \<noteq> {}` obtain i where "i \<in> I" by auto
   1.244 -  then show "{} \<in> ?G"
   1.245 -    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
   1.246 -             simp: sigma_sets.Empty generator_def prod_emb_def)
   1.247 -  from `i \<in> I` show "?\<Omega> \<in> ?G"
   1.248 -    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^sub>E {i} (\<lambda>i. space (M i))"]
   1.249 -             simp: generator_def prod_emb_def)
   1.250 -  fix A assume "A \<in> ?G"
   1.251 -  then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^sub>M JA M)" and A: "A = emb I JA XA"
   1.252 -    by (auto simp: generator_def)
   1.253 -  fix B assume "B \<in> ?G"
   1.254 -  then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^sub>M JB M)" and B: "B = emb I JB XB"
   1.255 -    by (auto simp: generator_def)
   1.256 -  let ?RA = "emb (JA \<union> JB) JA XA"
   1.257 -  let ?RB = "emb (JA \<union> JB) JB XB"
   1.258 -  have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
   1.259 -    using XA A XB B by auto
   1.260 -  show "A - B \<in> ?G" "A \<union> B \<in> ?G"
   1.261 -    unfolding * using XA XB by (safe intro!: generatorI') auto
   1.262 -qed
   1.263 +  have "emb I J (space (PiM J M) - X) \<in> generator"
   1.264 +    by (intro generator.intros J sets.Diff sets.top X)
   1.265 +  with J show "space (Pi\<^sub>M I M) - emb I J X \<in> generator"
   1.266 +    by (simp add: space_PiM prod_emb_PiE)
   1.267 +  
   1.268 +  fix K Y assume K: "finite K" "K \<subseteq> I" and Y: "Y \<in> sets (PiM K M)"
   1.269 +  have "emb I (J \<union> K) (emb (J \<union> K) J X) \<inter> emb I (J \<union> K) (emb (J \<union> K) K Y) \<in> generator"
   1.270 +    unfolding prod_emb_Int[symmetric]
   1.271 +    by (intro generator.intros sets.Int measurable_prod_emb) (auto intro!: J K X Y)
   1.272 +  with J K X Y show "emb I J X \<inter> emb I K Y \<in> generator"
   1.273 +    by simp
   1.274 +qed (force simp: generator.simps prod_emb_empty[symmetric])
   1.275  
   1.276 -lemma sets_PiM_generator:
   1.277 -  "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) generator"
   1.278 -proof cases
   1.279 -  assume "I = {}" then show ?thesis
   1.280 -    unfolding generator_def
   1.281 -    by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
   1.282 -next
   1.283 -  assume "I \<noteq> {}"
   1.284 -  show ?thesis
   1.285 -  proof
   1.286 -    show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) generator"
   1.287 -      unfolding sets_PiM
   1.288 -    proof (safe intro!: sigma_sets_subseteq)
   1.289 -      fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
   1.290 -        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
   1.291 -    qed
   1.292 -  qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset)
   1.293 -qed
   1.294 +interpretation generator!: algebra "space (PiM I M)" generator
   1.295 +  by (rule algebra_generator)
   1.296  
   1.297 -lemma generatorI:
   1.298 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
   1.299 -  unfolding generator_def by auto
   1.300 +lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
   1.301 +proof (intro antisym sets.sigma_sets_subset)
   1.302 +  show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) generator"
   1.303 +    unfolding sets_PiM_single space_PiM[symmetric]
   1.304 +  proof (intro sigma_sets_mono', safe)
   1.305 +    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
   1.306 +    then have "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} = emb I {i} (\<Pi>\<^sub>E j\<in>{i}. A)"
   1.307 +      by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def)
   1.308 +    with \<open>i\<in>I\<close> A show "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} \<in> generator"
   1.309 +      by (auto intro!: generator.intros sets_PiM_I_finite)
   1.310 +  qed
   1.311 +qed (auto elim!: generator.cases)
   1.312  
   1.313  definition mu_G ("\<mu>G") where
   1.314 -  "\<mu>G A =
   1.315 -    (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^sub>M J M). A = emb I J X \<longrightarrow> x = emeasure (limP J M P) X))"
   1.316 +  "\<mu>G A = (THE x. \<forall>J\<subseteq>I. finite J \<longrightarrow> (\<forall>X\<in>sets (Pi\<^sub>M J M). A = emb I J X \<longrightarrow> x = emeasure (P J) X))"
   1.317 +
   1.318 +definition lim :: "('i \<Rightarrow> 'a) measure" where
   1.319 +  "lim = extend_measure (space (PiM I M)) generator (\<lambda>x. x) \<mu>G"
   1.320 +
   1.321 +lemma space_lim[simp]: "space lim = space (PiM I M)"
   1.322 +  using generator.space_closed
   1.323 +  unfolding lim_def by (intro space_extend_measure) simp
   1.324 +
   1.325 +lemma sets_lim[simp, measurable]: "sets lim = sets (PiM I M)"
   1.326 +  using generator.space_closed by (simp add: lim_def sets_PiM_generator sets_extend_measure)
   1.327  
   1.328  lemma mu_G_spec:
   1.329 -  assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^sub>M J M)"
   1.330 -  shows "\<mu>G A = emeasure (limP J M P) X"
   1.331 +  assumes J: "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)"
   1.332 +  shows "\<mu>G (emb I J X) = emeasure (P J) X"
   1.333    unfolding mu_G_def
   1.334  proof (intro the_equality allI impI ballI)
   1.335 -  fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^sub>M K M)"
   1.336 -  have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)"
   1.337 -    using K J by (simp del: limP_finite)
   1.338 +  fix K Y assume K: "finite K" "K \<subseteq> I" "Y \<in> sets (Pi\<^sub>M K M)"
   1.339 +    and [simp]: "emb I J X = emb I K Y"
   1.340 +  have "emeasure (P K) Y = emeasure (P (K \<union> J)) (emb (K \<union> J) K Y)"
   1.341 +    using K J by (simp add: emeasure_P)
   1.342    also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
   1.343 -    using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
   1.344 -  also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X"
   1.345 -    using K J by (simp del: limP_finite)
   1.346 -  finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" ..
   1.347 +    using K J by (simp add: emb_injective[of "K \<union> J" I])
   1.348 +  also have "emeasure (P (K \<union> J)) (emb (K \<union> J) J X) = emeasure (P J) X"
   1.349 +    using K J by (subst emeasure_P) simp_all
   1.350 +  finally show "emeasure (P J) X = emeasure (P K) Y" ..
   1.351  qed (insert J, force)
   1.352  
   1.353 -lemma mu_G_eq:
   1.354 -  "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (limP J M P) X"
   1.355 -  by (intro mu_G_spec) auto
   1.356 +lemma positive_mu_G: "positive generator \<mu>G"
   1.357 +proof -
   1.358 +  show ?thesis
   1.359 +  proof (safe intro!: positive_def[THEN iffD2])
   1.360 +    obtain J where "finite J" "J \<subseteq> I" by auto
   1.361 +    then have "\<mu>G (emb I J {}) = 0"
   1.362 +      by (subst mu_G_spec) auto
   1.363 +    then show "\<mu>G {} = 0" by simp
   1.364 +  qed (auto simp: mu_G_spec elim!: generator.cases)
   1.365 +qed
   1.366  
   1.367 -lemma generator_Ex:
   1.368 -  assumes *: "A \<in> generator"
   1.369 -  shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^sub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (limP J M P) X"
   1.370 -proof -
   1.371 -  from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^sub>M J M)"
   1.372 -    unfolding generator_def by auto
   1.373 -  with mu_G_spec[OF this] show ?thesis by (auto simp del: limP_finite)
   1.374 +lemma additive_mu_G: "additive generator \<mu>G"
   1.375 +proof (safe intro!: additive_def[THEN iffD2] elim!: generator.cases)
   1.376 +  fix J X K Y assume J: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
   1.377 +    and K: "finite K" "K \<subseteq> I" "Y \<in> sets (PiM K M)"
   1.378 +    and "emb I J X \<inter> emb I K Y = {}"
   1.379 +  then have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
   1.380 +    by (intro emb_injective[of "J \<union> K" I _ "{}"]) (auto simp: sets.Int prod_emb_Int)
   1.381 +  have "\<mu>G (emb I J X \<union> emb I K Y) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
   1.382 +    using J K by simp
   1.383 +  also have "\<dots> = emeasure (P (J \<union> K)) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   1.384 +    using J K by (simp add: mu_G_spec sets.Un del: prod_emb_Un)
   1.385 +  also have "\<dots> = \<mu>G (emb I J X) + \<mu>G (emb I K Y)"
   1.386 +    using J K JK_disj by (simp add: plus_emeasure[symmetric] mu_G_spec emeasure_P sets_P)
   1.387 +  finally show "\<mu>G (emb I J X \<union> emb I K Y) = \<mu>G (emb I J X) + \<mu>G (emb I K Y)" .
   1.388  qed
   1.389  
   1.390 -lemma generatorE:
   1.391 -  assumes A: "A \<in> generator"
   1.392 -  obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (limP J M P) X"
   1.393 -  using generator_Ex[OF A] by atomize_elim auto
   1.394 -
   1.395 -lemma merge_sets:
   1.396 -  "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^sub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^sub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^sub>M K M) \<in> sets (Pi\<^sub>M K M)"
   1.397 -  by simp
   1.398 -
   1.399 -lemma merge_emb:
   1.400 -  assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^sub>M J M)"
   1.401 -  shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^sub>M I M)) =
   1.402 -    emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^sub>M (K - J) M))"
   1.403 +lemma emeasure_lim:
   1.404 +  assumes JX: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
   1.405 +  assumes cont: "\<And>J X. (\<And>i. J i \<subseteq> I) \<Longrightarrow> incseq J \<Longrightarrow> (\<And>i. finite (J i)) \<Longrightarrow> (\<And>i. X i \<in> sets (PiM (J i) M)) \<Longrightarrow>
   1.406 +    decseq (\<lambda>i. emb I (J i) (X i)) \<Longrightarrow> 0 < (INF i. P (J i) (X i)) \<Longrightarrow> (\<Inter>i. emb I (J i) (X i)) \<noteq> {}"
   1.407 +  shows "emeasure lim (emb I J X) = P J X"
   1.408  proof -
   1.409 -  have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
   1.410 -    by (auto simp: restrict_def merge_def)
   1.411 -  have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
   1.412 -    by (auto simp: restrict_def merge_def)
   1.413 -  have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
   1.414 -  have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
   1.415 -  have [simp]: "(K - J) \<inter> K = K - J" by auto
   1.416 -  from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
   1.417 -    by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
   1.418 -       auto
   1.419 -qed
   1.420 -
   1.421 -lemma positive_mu_G:
   1.422 -  assumes "I \<noteq> {}"
   1.423 -  shows "positive generator \<mu>G"
   1.424 -proof -
   1.425 -  interpret G!: algebra "\<Pi>\<^sub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
   1.426 +  have "\<exists>\<mu>. (\<forall>s\<in>generator. \<mu> s = \<mu>G s) \<and>
   1.427 +    measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \<mu>"
   1.428 +  proof (rule generator.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
   1.429 +    show "\<And>A. A \<in> generator \<Longrightarrow> \<mu>G A \<noteq> \<infinity>"
   1.430 +    proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI)
   1.431 +      fix J assume "finite J" "J \<subseteq> I"
   1.432 +      then interpret prob_space "P J" by (rule prob_space_P)
   1.433 +      show "\<And>X. X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emeasure (P J) X \<noteq> \<infinity>"
   1.434 +        by simp
   1.435 +    qed
   1.436 +  next
   1.437 +    fix A assume "range A \<subseteq> generator" and "decseq A" "(\<Inter>i. A i) = {}"
   1.438 +    then have "\<forall>i. \<exists>J X. A i = emb I J X \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (PiM J M)"
   1.439 +      unfolding image_subset_iff generator.simps by blast
   1.440 +    then obtain J X where A: "\<And>i. A i = emb I (J i) (X i)"
   1.441 +      and *: "\<And>i. finite (J i)" "\<And>i. J i \<subseteq> I" "\<And>i. X i \<in> sets (PiM (J i) M)"
   1.442 +      by metis
   1.443 +    have "(INF i. P (J i) (X i)) = 0"
   1.444 +    proof (rule ccontr)
   1.445 +      assume INF_P: "(INF i. P (J i) (X i)) \<noteq> 0"
   1.446 +      have "(\<Inter>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i))) \<noteq> {}"
   1.447 +      proof (rule cont)
   1.448 +        show "decseq (\<lambda>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))"
   1.449 +          using * \<open>decseq A\<close> by (subst prod_emb_trans) (auto simp: A[abs_def])
   1.450 +        show "0 < (INF i. P (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))"
   1.451 +           using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest)
   1.452 +        show "incseq (\<lambda>i. \<Union>n\<le>i. J n)"
   1.453 +          by (force simp: incseq_def)
   1.454 +      qed (insert *, auto)
   1.455 +      with \<open>(\<Inter>i. A i) = {}\<close> * show False
   1.456 +        by (subst (asm) prod_emb_trans) (auto simp: A[abs_def])
   1.457 +    qed
   1.458 +    moreover have "(\<lambda>i. P (J i) (X i)) ----> (INF i. P (J i) (X i))"
   1.459 +    proof (intro LIMSEQ_INF antimonoI)
   1.460 +      fix x y :: nat assume "x \<le> y"
   1.461 +      have "P (J y \<union> J x) (emb (J y \<union> J x) (J y) (X y)) \<le> P (J y \<union> J x) (emb (J y \<union> J x) (J x) (X x))"
   1.462 +        using \<open>decseq A\<close>[THEN decseqD, OF \<open>x\<le>y\<close>] *
   1.463 +        by (auto simp: A sets_P del: subsetI intro!: emeasure_mono  \<open>x \<le> y\<close>
   1.464 +              emb_preserve_mono[of "J y \<union> J x" I, where X="emb (J y \<union> J x) (J y) (X y)"])
   1.465 +      then show "P (J y) (X y) \<le> P (J x) (X x)"
   1.466 +        using * by (simp add: emeasure_P)
   1.467 +    qed
   1.468 +    ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
   1.469 +      by (auto simp: A[abs_def] mu_G_spec *)
   1.470 +  qed
   1.471 +  then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s"
   1.472 +    and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \<mu>"
   1.473 +    by (metis sets_PiM_generator)
   1.474    show ?thesis
   1.475 -  proof (intro positive_def[THEN iffD2] conjI ballI)
   1.476 -    from generatorE[OF G.empty_sets] guess J X . note this[simp]
   1.477 -    have "X = {}"
   1.478 -      by (rule prod_emb_injective[of J I]) simp_all
   1.479 -    then show "\<mu>G {} = 0" by simp
   1.480 -  next
   1.481 -    fix A assume "A \<in> generator"
   1.482 -    from generatorE[OF this] guess J X . note this[simp]
   1.483 -    show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
   1.484 -  qed
   1.485 -qed
   1.486 -
   1.487 -lemma additive_mu_G:
   1.488 -  assumes "I \<noteq> {}"
   1.489 -  shows "additive generator \<mu>G"
   1.490 -proof -
   1.491 -  interpret G!: algebra "\<Pi>\<^sub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
   1.492 -  show ?thesis
   1.493 -  proof (intro additive_def[THEN iffD2] ballI impI)
   1.494 -    fix A assume "A \<in> generator" with generatorE guess J X . note J = this
   1.495 -    fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
   1.496 -    assume "A \<inter> B = {}"
   1.497 -    have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
   1.498 -      using J K by auto
   1.499 -    have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
   1.500 -      apply (rule prod_emb_injective[of "J \<union> K" I])
   1.501 -      apply (insert `A \<inter> B = {}` JK J K)
   1.502 -      apply (simp_all add: sets.Int prod_emb_Int)
   1.503 -      done
   1.504 -    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.505 -      using J K by simp_all
   1.506 -    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.507 -      by simp
   1.508 -    also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
   1.509 -      using JK J(1, 4) K(1, 4) by (simp add: mu_G_eq sets.Un del: prod_emb_Un)
   1.510 -    also have "\<dots> = \<mu>G A + \<mu>G B"
   1.511 -      using J K JK_disj by (simp add: plus_emeasure[symmetric] del: limP_finite)
   1.512 -    finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
   1.513 +  proof (subst emeasure_extend_measure[OF lim_def])
   1.514 +    show "A \<in> generator \<Longrightarrow> \<mu> A = \<mu>G A" for A
   1.515 +      using eq by simp
   1.516 +    show "positive (sets lim) \<mu>" "countably_additive (sets lim) \<mu>"
   1.517 +      using ms by (auto simp add: measure_space_def)
   1.518 +    show "(\<lambda>x. x) ` generator \<subseteq> Pow (space (Pi\<^sub>M I M))"
   1.519 +      using generator.space_closed by simp
   1.520 +    show "emb I J X \<in> generator" "\<mu>G (emb I J X) = emeasure (P J) X"
   1.521 +      using JX by (auto intro: generator.intros simp: mu_G_spec)
   1.522    qed
   1.523  qed
   1.524  
   1.525  end
   1.526  
   1.527  sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
   1.528 -proof (simp add: projective_family_def, safe)
   1.529 -  fix J::"'i set" assume [simp]: "finite J"
   1.530 -  interpret f: finite_product_prob_space M J proof qed fact
   1.531 -  show "prob_space (Pi\<^sub>M J M)"
   1.532 -  proof
   1.533 -    show "emeasure (Pi\<^sub>M J M) (space (Pi\<^sub>M J M)) = 1"
   1.534 -      by (simp add: space_PiM emeasure_PiM emeasure_space_1)
   1.535 +  unfolding projective_family_def
   1.536 +proof (intro conjI allI impI distr_restrict)
   1.537 +  show "\<And>J. finite J \<Longrightarrow> prob_space (Pi\<^sub>M J M)"
   1.538 +    by (intro prob_spaceI) (simp add: space_PiM emeasure_PiM emeasure_space_1)
   1.539 +qed auto
   1.540 +
   1.541 +
   1.542 +txt \<open> Proof due to Ionescu Tulcea. \<close>
   1.543 +
   1.544 +locale Ionescu_Tulcea =
   1.545 +  fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a measure" and M :: "nat \<Rightarrow> 'a measure"
   1.546 +  assumes P[measurable]: "\<And>i. P i \<in> measurable (PiM {0..<i} M) (subprob_algebra (M i))"
   1.547 +  assumes prob_space_P: "\<And>i x. x \<in> space (PiM {0..<i} M) \<Longrightarrow> prob_space (P i x)"
   1.548 +begin
   1.549 +
   1.550 +lemma non_empty[simp]: "space (M i) \<noteq> {}"
   1.551 +proof (induction i rule: less_induct)
   1.552 +  case (less i)
   1.553 +  then obtain x where "\<And>j. j < i \<Longrightarrow> x j \<in> space (M j)"
   1.554 +    unfolding ex_in_conv[symmetric] by metis
   1.555 +  then have *: "restrict x {0..<i} \<in> space (PiM {0..<i} M)"
   1.556 +    by (auto simp: space_PiM PiE_iff)
   1.557 +  then interpret prob_space "P i (restrict x {0..<i})"
   1.558 +    by (rule prob_space_P)
   1.559 +  show ?case
   1.560 +    using not_empty subprob_measurableD(1)[OF P, OF *] by simp
   1.561 +qed
   1.562 +
   1.563 +lemma space_PiM_not_empty[simp]: "space (PiM UNIV M) \<noteq> {}"
   1.564 +  unfolding space_PiM_empty_iff by auto
   1.565 +
   1.566 +lemma space_P: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (P n x) = space (M n)"
   1.567 +  by (simp add: P[THEN subprob_measurableD(1)])
   1.568 +
   1.569 +lemma sets_P[measurable_cong]: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (P n x) = sets (M n)"
   1.570 +  by (simp add: P[THEN subprob_measurableD(2)])
   1.571 +
   1.572 +definition eP :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   1.573 +  "eP n \<omega> = distr (P n \<omega>) (PiM {0..<Suc n} M) (fun_upd \<omega> n)"
   1.574 +
   1.575 +lemma measurable_eP[measurable]:
   1.576 +  "eP n \<in> measurable (PiM {0..< n} M) (subprob_algebra (PiM {0..<Suc n} M))"
   1.577 +  by (auto simp: eP_def[abs_def] measurable_split_conv
   1.578 +           intro!: measurable_fun_upd[where J="{0..<n}"] measurable_distr2[OF _ P])
   1.579 +
   1.580 +lemma space_eP:
   1.581 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (eP n x) = space (PiM {0..<Suc n} M)"
   1.582 +  by (simp add: measurable_eP[THEN subprob_measurableD(1)])
   1.583 +
   1.584 +lemma sets_eP[measurable]:
   1.585 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (eP n x) = sets (PiM {0..<Suc n} M)"
   1.586 +  by (simp add: measurable_eP[THEN subprob_measurableD(2)])
   1.587 +
   1.588 +lemma prob_space_eP: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (eP n x)"
   1.589 +  unfolding eP_def
   1.590 +  by (intro prob_space.prob_space_distr prob_space_P measurable_fun_upd[where J="{0..<n}"]) auto
   1.591 +
   1.592 +lemma nn_integral_eP:
   1.593 +  "\<omega> \<in> space (PiM {0..<n} M) \<Longrightarrow> f \<in> borel_measurable (PiM {0..<Suc n} M) \<Longrightarrow>
   1.594 +    (\<integral>\<^sup>+x. f x \<partial>eP n \<omega>) = (\<integral>\<^sup>+x. f (\<omega>(n := x)) \<partial>P n \<omega>)"
   1.595 +  unfolding eP_def
   1.596 +  by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..<n}"] simp: space_PiM PiE_iff)
   1.597 +
   1.598 +lemma emeasure_eP:
   1.599 +  assumes \<omega>[simp]: "\<omega> \<in> space (PiM {0..<n} M)" and A[measurable]: "A \<in> sets (PiM {0..<Suc n} M)"
   1.600 +  shows "eP n \<omega> A = P n \<omega> ((\<lambda>x. \<omega>(n := x)) -` A \<inter> space (M n))"
   1.601 +  using nn_integral_eP[of \<omega> n "indicator A"]
   1.602 +  apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator)
   1.603 +  apply (subst nn_integral_indicator[symmetric])
   1.604 +  using measurable_sets[OF measurable_fun_upd[OF _ measurable_const[OF \<omega>] measurable_id] A, of n]
   1.605 +  apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator
   1.606 +     intro!: nn_integral_cong split: split_indicator)
   1.607 +  done
   1.608 +  
   1.609 +
   1.610 +primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   1.611 +  "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>"
   1.612 +| "C n (Suc m) \<omega> = C n m \<omega> \<guillemotright>= eP (n + m)"
   1.613 +
   1.614 +lemma measurable_C[measurable]:
   1.615 +  "C n m \<in> measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))"
   1.616 +  by (induction m) auto
   1.617 +
   1.618 +lemma space_C:
   1.619 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (C n m x) = space (PiM {0..<n + m} M)"
   1.620 +  by (simp add: measurable_C[THEN subprob_measurableD(1)])
   1.621 +
   1.622 +lemma sets_C[measurable_cong]:
   1.623 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (C n m x) = sets (PiM {0..<n + m} M)"
   1.624 +  by (simp add: measurable_C[THEN subprob_measurableD(2)])
   1.625 +
   1.626 +lemma prob_space_C: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (C n m x)"
   1.627 +proof (induction m)
   1.628 +  case (Suc m) then show ?case
   1.629 +    by (auto intro!: prob_space.prob_space_bind[where S="PiM {0..<Suc (n + m)} M"]
   1.630 +             simp: space_C prob_space_eP)
   1.631 +qed (auto intro!: prob_space_return simp: space_PiM)
   1.632 +
   1.633 +lemma split_C:
   1.634 +  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<guillemotright>= C (n + m) l) = C n (m + l) \<omega>"
   1.635 +proof (induction l)
   1.636 +  case 0
   1.637 +  with \<omega> show ?case
   1.638 +    by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty]
   1.639 +                  distr_cong[OF refl sets_C[symmetric, OF \<omega>]])
   1.640 +next
   1.641 +  case (Suc l) with \<omega> show ?case
   1.642 +    by (simp add: bind_assoc[symmetric, OF _ measurable_eP]) (simp add: ac_simps)
   1.643 +qed
   1.644 +
   1.645 +lemma nn_integral_C:
   1.646 +  assumes "m \<le> m'" and f[measurable]: "f \<in> borel_measurable (PiM {0..<n+m} M)"
   1.647 +    and nonneg: "\<And>x. x \<in> space (PiM {0..<n+m} M) \<Longrightarrow> 0 \<le> f x"
   1.648 +    and x: "x \<in> space (PiM {0..<n} M)"
   1.649 +  shows "(\<integral>\<^sup>+x. f x \<partial>C n m x) = (\<integral>\<^sup>+x. f (restrict x {0..<n+m}) \<partial>C n m' x)"
   1.650 +  using \<open>m \<le> m'\<close>
   1.651 +proof (induction rule: dec_induct)
   1.652 +  case (step i)
   1.653 +  let ?E = "\<lambda>x. f (restrict x {0..<n + m})" and ?C = "\<lambda>i f. \<integral>\<^sup>+x. f x \<partial>C n i x"
   1.654 +  from \<open>m\<le>i\<close> x have "?C i ?E = ?C (Suc i) ?E"
   1.655 +    by (auto simp: nn_integral_bind[where B="PiM {0 ..< Suc (n + i)} M"] space_C nn_integral_eP
   1.656 +             intro!: nn_integral_cong)
   1.657 +       (simp add: space_PiM PiE_iff  nonneg prob_space.emeasure_space_1[OF prob_space_P])
   1.658 +  with step show ?case by (simp del: restrict_apply)
   1.659 +qed (auto simp: space_PiM space_C[OF x] simp del: restrict_apply intro!: nn_integral_cong)
   1.660 +
   1.661 +lemma emeasure_C:
   1.662 +  assumes "m \<le> m'" and A[measurable]: "A \<in> sets (PiM {0..<n+m} M)" and [simp]: "x \<in> space (PiM {0..<n} M)"
   1.663 +  shows "emeasure (C n m' x) (prod_emb {0..<n + m'} M {0..<n+m} A) = emeasure (C n m x) A"
   1.664 +  using assms
   1.665 +  by (subst (1 2) nn_integral_indicator[symmetric])
   1.666 +     (auto intro!: nn_integral_cong split: split_indicator simp del: nn_integral_indicator
   1.667 +           simp: nn_integral_C[of m m' _ n] prod_emb_iff space_PiM PiE_iff sets_C space_C)
   1.668 +
   1.669 +lemma distr_C:
   1.670 +  assumes "m \<le> m'" and [simp]: "x \<in> space (PiM {0..<n} M)"
   1.671 +  shows "C n m x = distr (C n m' x) (PiM {0..<n+m} M) (\<lambda>x. restrict x {0..<n+m})"
   1.672 +proof (rule measure_eqI)
   1.673 +  fix A assume "A \<in> sets (C n m x)"
   1.674 +  with \<open>m \<le> m'\<close> show "emeasure (C n m x) A = emeasure (distr (C n m' x) (Pi\<^sub>M {0..<n + m} M) (\<lambda>x. restrict x {0..<n + m})) A"
   1.675 +    by (subst emeasure_C[symmetric, OF \<open>m \<le> m'\<close>]) (auto intro!: emeasure_distr_restrict[symmetric] simp: sets_C)
   1.676 +qed (simp add: sets_C)
   1.677 +
   1.678 +definition up_to :: "nat set \<Rightarrow> nat" where
   1.679 +  "up_to J = (LEAST n. \<forall>i\<ge>n. i \<notin> J)"
   1.680 +
   1.681 +lemma up_to_less: "finite J \<Longrightarrow> i \<in> J \<Longrightarrow> i < up_to J"
   1.682 +  unfolding up_to_def
   1.683 +  by (rule LeastI2[of _ "Suc (Max J)"]) (auto simp: Suc_le_eq not_le[symmetric])
   1.684 +
   1.685 +lemma up_to_iff: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> (\<forall>i\<in>J. i < n)"
   1.686 +proof safe
   1.687 +  show "finite J \<Longrightarrow> up_to J \<le> n \<Longrightarrow> i \<in> J \<Longrightarrow> i < n" for i
   1.688 +    using up_to_less[of J i] by auto
   1.689 +qed (auto simp: up_to_def intro!: Least_le)
   1.690 +
   1.691 +lemma up_to_iff_Ico: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> J \<subseteq> {0..<n}"
   1.692 +  by (auto simp: up_to_iff)
   1.693 +
   1.694 +lemma up_to: "finite J \<Longrightarrow> J \<subseteq> {0..< up_to J}"
   1.695 +  by (auto simp: up_to_less)
   1.696 +
   1.697 +lemma up_to_mono: "J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> up_to J \<le> up_to H"
   1.698 +  by (auto simp add: up_to_iff finite_subset up_to_less)
   1.699 +
   1.700 +definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   1.701 +  "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)"
   1.702 +
   1.703 +sublocale PF!: projective_family UNIV CI
   1.704 +  unfolding projective_family_def
   1.705 +proof safe
   1.706 +  show "finite J \<Longrightarrow> prob_space (CI J)" for J
   1.707 +    using up_to[of J] unfolding CI_def
   1.708 +    by (intro prob_space.prob_space_distr prob_space_C measurable_restrict) auto
   1.709 +  note measurable_cong_sets[OF sets_C, simp]
   1.710 +  have [simp]: "J \<subseteq> H \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M H M) (Pi\<^sub>M J M)" for H J
   1.711 +    by (auto intro!: measurable_restrict)
   1.712 +
   1.713 +  show "J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> CI J = distr (CI H) (Pi\<^sub>M J M) (\<lambda>f. restrict f J)" for J H
   1.714 +    by (simp add: CI_def distr_C[OF up_to_mono[of J H]] up_to up_to_mono distr_distr comp_def
   1.715 +                  inf.absorb2 finite_subset)
   1.716 +qed
   1.717 +
   1.718 +lemma emeasure_CI':
   1.719 +  "finite J \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> CI J X = C 0 (up_to J) (\<lambda>_. undefined) (PF.emb {0..<up_to J} J X)"
   1.720 +  unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C)
   1.721 +
   1.722 +lemma emeasure_CI:
   1.723 +  "J \<subseteq> {0..<n} \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> CI J X = C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} J X)"
   1.724 +  apply (subst emeasure_CI', simp_all add: finite_subset)
   1.725 +  apply (subst emeasure_C[symmetric, of "up_to J" n])
   1.726 +  apply (auto simp: finite_subset up_to_iff_Ico up_to_less)
   1.727 +  apply (subst prod_emb_trans)
   1.728 +  apply (auto simp: up_to_less finite_subset up_to_iff_Ico)
   1.729 +  done
   1.730 +
   1.731 +lemma lim:
   1.732 +  assumes J: "finite J" and X: "X \<in> sets (PiM J M)"
   1.733 +  shows "emeasure PF.lim (PF.emb UNIV J X) = emeasure (CI J) X"
   1.734 +proof (rule PF.emeasure_lim[OF J subset_UNIV X])
   1.735 +  fix J X' assume J[simp]: "\<And>i. finite (J i)" and X'[measurable]: "\<And>i. X' i \<in> sets (Pi\<^sub>M (J i) M)"
   1.736 +    and dec: "decseq (\<lambda>i. PF.emb UNIV (J i) (X' i))"
   1.737 +  def X \<equiv> "\<lambda>n. (\<Inter>i\<in>{i. J i \<subseteq> {0..< n}}. PF.emb {0..<n} (J i) (X' i)) \<inter> space (PiM {0..<n} M)"
   1.738 +
   1.739 +  have sets_X[measurable]: "X n \<in> sets (PiM {0..<n} M)" for n
   1.740 +    by (cases "{i. J i \<subseteq> {0..< n}} = {}")
   1.741 +       (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int)
   1.742 +  
   1.743 +  have dec_X: "n \<le> m \<Longrightarrow> X m \<subseteq> PF.emb {0..<m} {0..<n} (X n)" for n m
   1.744 +    unfolding X_def using ivl_subset[of 0 n 0 m]
   1.745 +    by (cases "{i. J i \<subseteq> {0..< n}} = {}")
   1.746 +       (auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset)
   1.747 +
   1.748 +  have dec_X': "PF.emb {0..<n} (J j) (X' j) \<subseteq> PF.emb {0..<n} (J i) (X' i)"
   1.749 +    if [simp]: "J i \<subseteq> {0..<n}" "J j \<subseteq> {0..<n}" "i \<le> j" for n i j
   1.750 +    by (rule PF.emb_preserve_mono[of "{0..<n}" UNIV]) (auto del: subsetI intro: dec[THEN antimonoD])
   1.751 +
   1.752 +  assume "0 < (INF i. CI (J i) (X' i))"
   1.753 +  also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))"
   1.754 +  proof (intro INF_greatest)
   1.755 +    fix n
   1.756 +    interpret C!: prob_space "C 0 n (\<lambda>x. undefined)"
   1.757 +      by (rule prob_space_C) simp
   1.758 +    show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)"
   1.759 +    proof cases
   1.760 +      assume "{i. J i \<subseteq> {0..< n}} = {}" with C.emeasure_space_1  show ?thesis
   1.761 +        by (auto simp add: X_def space_C intro!: INF_lower2[of 0] prob_space.measure_le_1 PF.prob_space_P)
   1.762 +    next
   1.763 +      assume *: "{i. J i \<subseteq> {0..< n}} \<noteq> {}"
   1.764 +      have "(INF i. CI (J i) (X' i)) \<le>
   1.765 +          (INF i:{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
   1.766 +        by (intro INF_superset_mono) (auto simp: emeasure_CI)
   1.767 +      also have "\<dots> = C 0 n (\<lambda>_. undefined) (\<Inter>i\<in>{i. J i \<subseteq> {0..<n}}. (PF.emb {0..<n} (J i) (X' i)))"
   1.768 +        using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
   1.769 +      also have "\<dots> = C 0 n (\<lambda>_. undefined) (X n)"
   1.770 +        using * by (auto simp add: X_def INT_extend_simps)
   1.771 +      finally show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>_. undefined) (X n)" .
   1.772 +    qed
   1.773    qed
   1.774 +  finally have pos: "0 < (INF i. C 0 i (\<lambda>x. undefined) (X i))" .
   1.775 +  from less_INF_D[OF this, of 0] have "X 0 \<noteq> {}"
   1.776 +    by auto
   1.777 +
   1.778 +  { fix \<omega> n assume \<omega>: "\<omega> \<in> space (PiM {0..<n} M)"
   1.779 +    let ?C = "\<lambda>i. emeasure (C n i \<omega>) (X (n + i))"
   1.780 +    let ?C' = "\<lambda>i x. emeasure (C (Suc n) i (\<omega>(n:=x))) (X (Suc n + i))"
   1.781 +    have M: "\<And>i. ?C' i \<in> borel_measurable (P n \<omega>)"
   1.782 +      using \<omega>[measurable, simp] measurable_fun_upd[where J="{0..<n}"] by measurable auto
   1.783 +
   1.784 +    assume "0 < (INF i. ?C i)"
   1.785 +    also have "\<dots> \<le> (INF i. emeasure (C n (1 + i) \<omega>) (X (n + (1 + i))))"
   1.786 +      by (intro INF_greatest INF_lower) auto
   1.787 +    also have "\<dots> = (INF i. \<integral>\<^sup>+x. ?C' i x \<partial>P n \<omega>)"
   1.788 +      using \<omega> measurable_C[of "Suc n"]
   1.789 +      apply (intro INF_cong refl)
   1.790 +      apply (subst split_C[symmetric, OF \<omega>])
   1.791 +      apply (subst emeasure_bind[OF _ _ sets_X])
   1.792 +      apply (simp_all del: C.simps add: space_C)
   1.793 +      apply measurable
   1.794 +      apply simp
   1.795 +      apply (simp add: bind_return[OF measurable_eP] nn_integral_eP)
   1.796 +      done
   1.797 +    also have "\<dots> = (\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>)"
   1.798 +    proof (rule nn_integral_monotone_convergence_INF[symmetric])
   1.799 +      have "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) \<le> (\<integral>\<^sup>+x. 1 \<partial>P n \<omega>)"
   1.800 +        by (intro nn_integral_mono) (auto split: split_indicator)
   1.801 +      also have "\<dots> < \<infinity>"
   1.802 +        using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp
   1.803 +      finally show "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) < \<infinity>" .
   1.804 +    next
   1.805 +      fix i j :: nat and x assume "i \<le> j" "x \<in> space (P n \<omega>)"
   1.806 +      with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)"
   1.807 +        by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
   1.808 +      show "?C' j x \<le> ?C' i x"
   1.809 +        using \<open>i \<le> j\<close> by (subst emeasure_C[symmetric, of i]) (auto intro!: emeasure_mono dec_X del: subsetI simp: sets_C space_P \<omega> \<omega>')
   1.810 +    qed fact
   1.811 +    finally have "(\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>) \<noteq> 0"
   1.812 +      by simp
   1.813 +    then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). 0 < (INF i. ?C' i x)"
   1.814 +       using M by (subst (asm) nn_integral_0_iff_AE)
   1.815 +         (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le)
   1.816 +    then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). x \<in> space (M n) \<and> 0 < (INF i. ?C' i x)"
   1.817 +      by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>)
   1.818 +    then obtain x where "x \<in> space (M n)" "0 < (INF i. ?C' i x)"
   1.819 +      by (auto dest: frequently_ex)
   1.820 +    from this(2)[THEN less_INF_D, of 0] this(2)
   1.821 +    have "\<exists>x. \<omega>(n := x) \<in> X (Suc n) \<and> 0 < (INF i. ?C' i x)"
   1.822 +      by (intro exI[of _ x]) (simp split: split_indicator_asm) }
   1.823 +  note step = this
   1.824 +
   1.825 +  let ?\<omega> = "\<lambda>\<omega> n x. (restrict \<omega> {0..<n})(n := x)"
   1.826 +  let ?L = "\<lambda>\<omega> n r. INF i. emeasure (C (Suc n) i (?\<omega> \<omega> n r)) (X (Suc n + i))"
   1.827 +  have *: "(\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i)) \<Longrightarrow>
   1.828 +    restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" for \<omega> n
   1.829 +    using sets.sets_into_space[OF sets_X, of n]
   1.830 +    by (cases n) (auto simp: atLeastLessThanSuc restrict_def[of _ "{}"])
   1.831 +  have "\<exists>\<omega>. \<forall>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n) \<and> 0 < ?L \<omega> n (\<omega> n)"
   1.832 +  proof (rule dependent_wellorder_choice)
   1.833 +    fix n \<omega> assume IH: "\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i) \<and> 0 < ?L \<omega> i (\<omega> i)"
   1.834 +    show "\<exists>r. ?\<omega> \<omega> n r \<in> X (Suc n) \<and> 0 < ?L \<omega> n r"
   1.835 +    proof (rule step)
   1.836 +      show "restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)"
   1.837 +        using IH[THEN conjunct1] by (rule *)
   1.838 +      show "0 < (INF i. emeasure (C n i (restrict \<omega> {0..<n})) (X (n + i)))"
   1.839 +      proof (cases n)
   1.840 +        case 0 with pos show ?thesis
   1.841 +          by (simp add: CI_def restrict_def)
   1.842 +      next
   1.843 +        case (Suc i) then show ?thesis
   1.844 +          using IH[of i, THEN conjunct2] by (simp add: atLeastLessThanSuc)
   1.845 +      qed
   1.846 +    qed
   1.847 +  qed (simp cong: restrict_cong)
   1.848 +  then obtain \<omega> where \<omega>: "\<And>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n)"
   1.849 +    by auto
   1.850 +  from this[THEN *] have \<omega>_space: "\<omega> \<in> space (PiM UNIV M)"
   1.851 +    by (auto simp: space_PiM PiE_iff Ball_def)
   1.852 +  have *: "\<omega> \<in> PF.emb UNIV {0..<n} (X n)" for n
   1.853 +  proof (cases n)
   1.854 +    case 0 with \<omega>_space \<open>X 0 \<noteq> {}\<close> sets.sets_into_space[OF sets_X, of 0] show ?thesis
   1.855 +      by (auto simp add: space_PiM prod_emb_def restrict_def PiE_iff)
   1.856 +  next
   1.857 +    case (Suc i) then show ?thesis
   1.858 +      using \<omega>[of i] \<omega>_space by (auto simp: prod_emb_def space_PiM PiE_iff atLeastLessThanSuc)
   1.859 +  qed
   1.860 +  have **: "{i. J i \<subseteq> {0..<up_to (J n)}} \<noteq> {}" for n
   1.861 +    by (auto intro!: exI[of _ n] up_to J)
   1.862 +  have "\<omega> \<in> PF.emb UNIV (J n) (X' n)" for n
   1.863 +    using *[of "up_to (J n)"] up_to[of "J n"] by (simp add: X_def prod_emb_Int prod_emb_INT[OF **])
   1.864 +  then show "(\<Inter>i. PF.emb UNIV (J i) (X' i)) \<noteq> {}"
   1.865 +    by auto
   1.866 +qed
   1.867 +
   1.868 +lemma distr_lim: assumes J[simp]: "finite J" shows "distr PF.lim (PiM J M) (\<lambda>x. restrict x J) = CI J"
   1.869 +  apply (rule measure_eqI)
   1.870 +  apply (simp add: CI_def)
   1.871 +  apply (simp add: emeasure_distr measurable_cong_sets[OF PF.sets_lim] lim[symmetric] prod_emb_def space_PiM)
   1.872 +  done
   1.873 +
   1.874 +end
   1.875 +
   1.876 +lemma (in product_prob_space) emeasure_lim_emb:
   1.877 +  assumes *: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
   1.878 +  shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X"
   1.879 +proof (rule emeasure_lim[OF *], goal_cases)
   1.880 +  case (1 J X)
   1.881 +  
   1.882 +  have "\<exists>Q. (\<forall>i. sets Q = PiM (\<Union>i. J i) M \<and> distr Q (PiM (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M)"
   1.883 +  proof cases
   1.884 +    assume "finite (\<Union>i. J i)"
   1.885 +    then have "distr (PiM (\<Union>i. J i) M) (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" for i
   1.886 +      by (intro distr_restrict[symmetric]) auto
   1.887 +    then show ?thesis
   1.888 +      by auto
   1.889 +  next
   1.890 +    assume inf: "infinite (\<Union>i. J i)"
   1.891 +    moreover have count: "countable (\<Union>i. J i)"
   1.892 +      using 1(3) by (auto intro: countable_finite)
   1.893 +    def f \<equiv> "from_nat_into (\<Union>i. J i)" and t \<equiv> "to_nat_on (\<Union>i. J i)"
   1.894 +    have ft[simp]: "x \<in> J i \<Longrightarrow> f (t x) = x" for x i
   1.895 +      unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto
   1.896 +    have tf[simp]: "t (f i) = i" for i
   1.897 +      unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count)
   1.898 +    have inj_t: "inj_on t (\<Union>i. J i)"
   1.899 +      using count by (auto simp: t_def)
   1.900 +    then have inj_t_J: "inj_on t (J i)" for i
   1.901 +      by (rule subset_inj_on) auto
   1.902 +    interpret IT!: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
   1.903 +      by standard auto
   1.904 +    interpret Mf!: product_prob_space "\<lambda>x. M (f x)" UNIV
   1.905 +      by standard
   1.906 +    have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n
   1.907 +    proof (induction n)
   1.908 +      case 0 then show ?case
   1.909 +        by (auto simp: PiM_empty intro!: measure_eqI dest!: subset_singletonD)
   1.910 +    next
   1.911 +      case (Suc n) then show ?case
   1.912 +        apply (auto intro!: measure_eqI simp: sets_bind[OF IT.sets_eP] emeasure_bind[OF _ IT.measurable_eP])
   1.913 +        apply (auto simp: Mf.product_nn_integral_insert nn_integral_indicator[symmetric] atLeastLessThanSuc IT.emeasure_eP space_PiM
   1.914 +                    split: split_indicator simp del: nn_integral_indicator intro!: nn_integral_cong)
   1.915 +        done
   1.916 +    qed
   1.917 +    have CI_eq_PiM: "IT.CI X = PiM X (\<lambda>x. M (f x))" if X: "finite X" for X
   1.918 +      by (auto simp: IT.up_to_less X  IT.CI_def C_eq_PiM intro!: Mf.distr_restrict[symmetric])
   1.919 +
   1.920 +    let ?Q = "distr IT.PF.lim (PiM (\<Union>i. J i) M) (\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x))"
   1.921 +    { fix i
   1.922 +      have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = 
   1.923 +        distr IT.PF.lim (Pi\<^sub>M (J i) M) ((\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<circ> (\<lambda>\<omega>. restrict \<omega> (t`J i)))"
   1.924 +      proof (subst distr_distr)
   1.925 +        have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M UNIV (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x i
   1.926 +          using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp
   1.927 +        then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (UNION UNIV J) M)"
   1.928 +          by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
   1.929 +      qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
   1.930 +      also have "\<dots> = distr (distr IT.PF.lim (PiM (t`J i) (\<lambda>x. M (f x))) (\<lambda>\<omega>. restrict \<omega> (t`J i))) (Pi\<^sub>M (J i) M) (\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n))"
   1.931 +      proof (intro distr_distr[symmetric])
   1.932 +        have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M (t`J i) (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x
   1.933 +          using measurable_component_singleton[of "t x" "t`J i" "\<lambda>x. M (f x)"] x unfolding ft[OF x] by auto
   1.934 +        then show "(\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<in> measurable (Pi\<^sub>M (t ` J i) (\<lambda>x. M (f x))) (Pi\<^sub>M (J i) M)"
   1.935 +          by (auto intro!: measurable_restrict)
   1.936 +      qed (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
   1.937 +      also have "\<dots> = distr (PiM (t`J i) (\<lambda>x. M (f x))) (Pi\<^sub>M (J i) M) (\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n))"
   1.938 +        using \<open>finite (J i)\<close> by (subst IT.distr_lim) (auto simp: CI_eq_PiM)
   1.939 +      also have "\<dots> = Pi\<^sub>M (J i) M"
   1.940 +        using Mf.distr_reorder[of t "J i"] by (simp add: 1 inj_t_J cong: PiM_cong)
   1.941 +      finally have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" . }
   1.942 +    then show "\<exists>Q. \<forall>i. sets Q = PiM (\<Union>i. J i) M \<and> distr Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M"
   1.943 +      by (intro exI[of _ ?Q]) auto
   1.944 +  qed
   1.945 +  then obtain Q where sets_Q: "sets Q = PiM (\<Union>i. J i) M"
   1.946 +    and Q: "\<And>i. distr Q (PiM (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" by blast
   1.947 +
   1.948 +  from 1 interpret Q: prob_space Q
   1.949 +    by (intro prob_space_distrD[of "\<lambda>x. restrict x (J 0)" Q "PiM (J 0) M"])
   1.950 +       (auto simp: Q measurable_cong_sets[OF sets_Q]
   1.951 +                intro!: prob_space_P measurable_restrict measurable_component_singleton)
   1.952 +
   1.953 +  have "0 < (INF i. emeasure (Pi\<^sub>M (J i) M) (X i))" by fact
   1.954 +  also have "\<dots> = (INF i. emeasure Q (emb (\<Union>i. J i) (J i) (X i)))"
   1.955 +    by (simp add: emeasure_distr_restrict[OF _ sets_Q 1(4), symmetric] SUP_upper Q)
   1.956 +  also have "\<dots> = emeasure Q (\<Inter>i. emb (\<Union>i. J i) (J i) (X i))"
   1.957 +  proof (rule INF_emeasure_decseq)
   1.958 +    from 1 show "decseq (\<lambda>n. emb (\<Union>i. J i) (J n) (X n))"
   1.959 +      by (intro antimonoI emb_preserve_mono[where X="emb (\<Union>i. J i) (J n) (X n)" and L=I and J="\<Union>i. J i" for n]
   1.960 +         measurable_prod_emb)
   1.961 +         (auto simp: SUP_least SUP_upper antimono_def)
   1.962 +  qed (insert 1, auto simp: sets_Q)
   1.963 +  finally have "(\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) \<noteq> {}"
   1.964 +    by auto
   1.965 +  moreover have "(\<Inter>i. emb I (J i) (X i)) = {} \<Longrightarrow> (\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) = {}"
   1.966 +    using 1 by (intro emb_injective[of "\<Union>i. J i" I _ "{}"] sets.countable_INT) (auto simp: SUP_least SUP_upper)
   1.967 +  ultimately show ?case by auto
   1.968  qed
   1.969  
   1.970  end