cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
authorhoelzl
Wed Oct 07 17:11:16 2015 +0200 (2015-10-07)
changeset 61359e985b52c3eb3
parent 61358 131fc8c10402
child 61360 a273bdac0934
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
src/HOL/Library/FuncSet.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Projective_Limit.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Wed Oct 07 15:31:59 2015 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Oct 07 17:11:16 2015 +0200
     1.3 @@ -184,6 +184,9 @@
     1.4  
     1.5  subsection \<open>Bounded Abstraction: @{term restrict}\<close>
     1.6  
     1.7 +lemma restrict_cong: "I = J \<Longrightarrow> (\<And>i. i \<in> J =simp=> f i = g i) \<Longrightarrow> restrict f I = restrict g J"
     1.8 +  by (auto simp: restrict_def fun_eq_iff simp_implies_def)
     1.9 +
    1.10  lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B"
    1.11    by (simp add: Pi_def restrict_def)
    1.12  
     2.1 --- a/src/HOL/Probability/Distributions.thy	Wed Oct 07 15:31:59 2015 +0200
     2.2 +++ b/src/HOL/Probability/Distributions.thy	Wed Oct 07 17:11:16 2015 +0200
     2.3 @@ -973,11 +973,7 @@
     2.4          by (intro integral_cong) auto
     2.5        finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
     2.6          exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
     2.7 -        apply (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
     2.8 -        apply (subst integral_mult_right_zero[symmetric])
     2.9 -        apply (intro integral_cong)
    2.10 -        apply simp_all
    2.11 -        done
    2.12 +        by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
    2.13        then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b"
    2.14          by (simp add: field_simps atLeastAtMost_def indicator_inter_arith)
    2.15      qed
     3.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 07 15:31:59 2015 +0200
     3.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 07 17:11:16 2015 +0200
     3.3 @@ -351,6 +351,15 @@
     3.4  lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
     3.5    using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
     3.6  
     3.7 +lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)"
     3.8 +  by (auto simp: prod_emb_def space_PiM)
     3.9 +
    3.10 +lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow>  (\<exists>i\<in>I. space (M i) = {})"
    3.11 +  by (auto simp: space_PiM PiE_eq_empty_iff)
    3.12 +
    3.13 +lemma undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)"
    3.14 +  by (auto simp: space_PiM)
    3.15 +
    3.16  lemma sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
    3.17    using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
    3.18  
    3.19 @@ -621,6 +630,20 @@
    3.20    finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
    3.21  qed (auto simp: space_pair_measure space_PiM PiE_def)
    3.22  
    3.23 +lemma measurable_fun_upd:
    3.24 +  assumes I: "I = J \<union> {i}"
    3.25 +  assumes f[measurable]: "f \<in> measurable N (PiM J M)"
    3.26 +  assumes h[measurable]: "h \<in> measurable N (M i)"
    3.27 +  shows "(\<lambda>x. (f x) (i := h x)) \<in> measurable N (PiM I M)"
    3.28 +proof (intro measurable_PiM_single')
    3.29 +  fix j assume "j \<in> I" then show "(\<lambda>\<omega>. ((f \<omega>)(i := h \<omega>)) j) \<in> measurable N (M j)"
    3.30 +    unfolding I by (cases "j = i") auto
    3.31 +next
    3.32 +  show "(\<lambda>x. (f x)(i := h x)) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
    3.33 +    using I f[THEN measurable_space] h[THEN measurable_space]
    3.34 +    by (auto simp: space_PiM PiE_iff extensional_def)
    3.35 +qed
    3.36 +
    3.37  lemma measurable_component_update:
    3.38    "x \<in> space (Pi\<^sub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^sub>M (insert i I) M)"
    3.39    by simp
    3.40 @@ -673,6 +696,25 @@
    3.41    unfolding prod_emb_def space_PiM[symmetric]
    3.42    by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
    3.43  
    3.44 +lemma merge_in_prod_emb:
    3.45 +  assumes "y \<in> space (PiM I M)" "x \<in> X" and X: "X \<in> sets (Pi\<^sub>M J M)" and "J \<subseteq> I"
    3.46 +  shows "merge J I (x, y) \<in> prod_emb I M J X"
    3.47 +  using assms sets.sets_into_space[OF X]
    3.48 +  by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff
    3.49 +           cong: if_cong restrict_cong)
    3.50 +     (simp add: extensional_def)
    3.51 +
    3.52 +lemma prod_emb_eq_emptyD:
    3.53 +  assumes J: "J \<subseteq> I" and ne: "space (PiM I M) \<noteq> {}" and X: "X \<in> sets (Pi\<^sub>M J M)"
    3.54 +    and *: "prod_emb I M J X = {}"
    3.55 +  shows "X = {}"
    3.56 +proof safe
    3.57 +  fix x assume "x \<in> X"
    3.58 +  obtain \<omega> where "\<omega> \<in> space (PiM I M)"
    3.59 +    using ne by blast
    3.60 +  from merge_in_prod_emb[OF this \<open>x\<in>X\<close> X J] * show "x \<in> {}" by auto 
    3.61 +qed
    3.62 +
    3.63  lemma sets_in_Pi_aux:
    3.64    "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
    3.65    {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
    3.66 @@ -817,6 +859,36 @@
    3.67      by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
    3.68  qed simp
    3.69  
    3.70 +lemma (in product_sigma_finite) PiM_eqI:
    3.71 +  assumes "finite I" "sets P = PiM I M"
    3.72 +  assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
    3.73 +  shows "P = PiM I M"
    3.74 +proof -
    3.75 +  interpret finite_product_sigma_finite M I
    3.76 +    proof qed fact
    3.77 +  from sigma_finite_pairs guess C .. note C = this
    3.78 +  show ?thesis
    3.79 +  proof (rule measure_eqI_generator_eq[symmetric, OF Int_stable_prod_algebra prod_algebra_sets_into_space])
    3.80 +    show "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
    3.81 +      by (rule sets_PiM)
    3.82 +    then show "sets P = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
    3.83 +      unfolding `sets P = sets (PiM I M)` by simp
    3.84 +    def A \<equiv> "\<lambda>n. \<Pi>\<^sub>E i\<in>I. C i n"
    3.85 +    show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>"
    3.86 +      using C \<open>finite I\<close>
    3.87 +      by (auto intro!: prod_algebraI_finite simp: A_def emeasure_PiM subset_eq setprod_PInf emeasure_nonneg)
    3.88 +    show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
    3.89 +      using C by (simp add: A_def space_PiM)
    3.90 +
    3.91 +    fix X assume X: "X \<in> prod_algebra I M"
    3.92 +    then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
    3.93 +      and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
    3.94 +      by (force elim!: prod_algebraE)
    3.95 +    show "emeasure (PiM I M) X = emeasure P X"
    3.96 +      unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq emeasure_PiM J \<open>finite I\<close>)
    3.97 +  qed
    3.98 +qed
    3.99 +
   3.100  lemma (in product_sigma_finite) sigma_finite: 
   3.101    assumes "finite I"
   3.102    shows "sigma_finite_measure (PiM I M)"
   3.103 @@ -843,84 +915,24 @@
   3.104    using emeasure_PiM[OF finite_index] by auto
   3.105  
   3.106  lemma (in product_sigma_finite) nn_integral_empty:
   3.107 -  assumes pos: "0 \<le> f (\<lambda>k. undefined)"
   3.108 -  shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
   3.109 -proof -
   3.110 -  interpret finite_product_sigma_finite M "{}" by standard (fact finite.emptyI)
   3.111 -  have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
   3.112 -    using assms by (subst measure_times) auto
   3.113 -  then show ?thesis
   3.114 -    unfolding nn_integral_def simple_function_def simple_integral_def[abs_def]
   3.115 -  proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
   3.116 -    show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
   3.117 -      by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
   3.118 -    show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
   3.119 -      by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm)
   3.120 -  qed
   3.121 -qed
   3.122 +  "0 \<le> f (\<lambda>k. undefined) \<Longrightarrow> integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
   3.123 +  by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2)
   3.124  
   3.125  lemma (in product_sigma_finite) distr_merge:
   3.126    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   3.127    shows "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J) = Pi\<^sub>M (I \<union> J) M"
   3.128     (is "?D = ?P")
   3.129 -proof -
   3.130 +proof (rule PiM_eqI)
   3.131    interpret I: finite_product_sigma_finite M I by standard fact
   3.132    interpret J: finite_product_sigma_finite M J by standard fact
   3.133 -  have "finite (I \<union> J)" using fin by auto
   3.134 -  interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
   3.135 -  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
   3.136 -  let ?g = "merge I J"
   3.137 -
   3.138 -  from IJ.sigma_finite_pairs obtain F where
   3.139 -    F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
   3.140 -       "incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I \<union> J. F i k)"
   3.141 -       "(\<Union>k. \<Pi>\<^sub>E i\<in>I \<union> J. F i k) = space ?P"
   3.142 -       "\<And>k. \<forall>i\<in>I\<union>J. emeasure (M i) (F i k) \<noteq> \<infinity>"
   3.143 -    by auto
   3.144 -  let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I \<union> J. F i k"
   3.145 -  
   3.146 -  show ?thesis
   3.147 -  proof (rule measure_eqI_generator_eq[symmetric])
   3.148 -    show "Int_stable (prod_algebra (I \<union> J) M)"
   3.149 -      by (rule Int_stable_prod_algebra)
   3.150 -    show "prod_algebra (I \<union> J) M \<subseteq> Pow (\<Pi>\<^sub>E i \<in> I \<union> J. space (M i))"
   3.151 -      by (rule prod_algebra_sets_into_space)
   3.152 -    show "sets ?P = sigma_sets (\<Pi>\<^sub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
   3.153 -      by (rule sets_PiM)
   3.154 -    then show "sets ?D = sigma_sets (\<Pi>\<^sub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
   3.155 -      by simp
   3.156 -
   3.157 -    show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F
   3.158 -      using fin by (auto simp: prod_algebra_eq_finite)
   3.159 -    show "(\<Union>i. \<Pi>\<^sub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^sub>E i\<in>I \<union> J. space (M i))"
   3.160 -      using F(3) by (simp add: space_PiM)
   3.161 -  next
   3.162 -    fix k
   3.163 -    from F `finite I` setprod_PInf[of "I \<union> J", OF emeasure_nonneg, of M]
   3.164 -    show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
   3.165 -  next
   3.166 -    fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
   3.167 -    with fin obtain F where A_eq: "A = (Pi\<^sub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   3.168 -      by (auto simp add: prod_algebra_eq_finite)
   3.169 -    let ?B = "Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M"
   3.170 -    let ?X = "?g -` A \<inter> space ?B"
   3.171 -    have "Pi\<^sub>E I F \<subseteq> space (Pi\<^sub>M I M)" "Pi\<^sub>E J F \<subseteq> space (Pi\<^sub>M J M)"
   3.172 -      using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+
   3.173 -    then have X: "?X = (Pi\<^sub>E I F \<times> Pi\<^sub>E J F)"
   3.174 -      unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
   3.175 -    have "emeasure ?D A = emeasure ?B ?X"
   3.176 -      using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
   3.177 -    also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
   3.178 -      using `finite J` `finite I` F unfolding X
   3.179 -      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times)
   3.180 -    also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
   3.181 -      using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod.union_inter_neutral)
   3.182 -    also have "\<dots> = emeasure ?P (Pi\<^sub>E (I \<union> J) F)"
   3.183 -      using `finite J` `finite I` F unfolding A
   3.184 -      by (intro IJ.measure_times[symmetric]) auto
   3.185 -    finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp
   3.186 -  qed
   3.187 -qed
   3.188 +  fix A assume A: "\<And>i. i \<in> I \<union> J \<Longrightarrow> A i \<in> sets (M i)"
   3.189 +  have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = PiE I A \<times> PiE J A"
   3.190 +    using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
   3.191 +  from A fin show "emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) (Pi\<^sub>E (I \<union> J) A) =
   3.192 +      (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
   3.193 +    by (subst emeasure_distr)
   3.194 +       (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times setprod.union_disjoint)
   3.195 +qed (insert fin, simp_all)
   3.196  
   3.197  lemma (in product_sigma_finite) product_nn_integral_fold:
   3.198    assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   3.199 @@ -1043,23 +1055,13 @@
   3.200  
   3.201  lemma (in product_sigma_finite) distr_component:
   3.202    "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
   3.203 -proof (intro measure_eqI[symmetric])
   3.204 -  interpret I: finite_product_sigma_finite M "{i}" by standard simp
   3.205 -
   3.206 -  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
   3.207 -    by (auto simp: extensional_def restrict_def)
   3.208 -
   3.209 -  have [measurable]: "\<And>j. j \<in> {i} \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)" by simp
   3.210 -
   3.211 -  fix A assume A: "A \<in> sets ?P"
   3.212 -  then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)" 
   3.213 -    by simp
   3.214 -  also have "\<dots> = (\<integral>\<^sup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
   3.215 -    by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
   3.216 -  also have "\<dots> = emeasure ?D A"
   3.217 -    using A by (simp add: product_nn_integral_singleton emeasure_distr)
   3.218 -  finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" .
   3.219 -qed simp
   3.220 +proof (intro PiM_eqI)
   3.221 +  fix A assume "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
   3.222 +  moreover then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
   3.223 +    by (auto dest: sets.sets_into_space)
   3.224 +  ultimately show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
   3.225 +    by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
   3.226 +qed simp_all
   3.227  
   3.228  lemma (in product_sigma_finite)
   3.229    assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
     4.1 --- a/src/HOL/Probability/Giry_Monad.thy	Wed Oct 07 15:31:59 2015 +0200
     4.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Wed Oct 07 17:11:16 2015 +0200
     4.3 @@ -1405,6 +1405,10 @@
     4.4    apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
     4.5    done
     4.6  
     4.7 +lemma bind_return_distr':
     4.8 +  "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (\<lambda>x. return N (f x)) = distr M N f"
     4.9 +  using bind_return_distr[of M f N] by (simp add: comp_def)
    4.10 +
    4.11  lemma bind_assoc:
    4.12    fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure"
    4.13    assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)"
     5.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 07 15:31:59 2015 +0200
     5.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 07 17:11:16 2015 +0200
     5.3 @@ -1263,7 +1263,7 @@
     5.4    note rv_Y = this[measurable]
     5.5      
     5.6    interpret Y: prob_space "distr M borel (Y i)" for i
     5.7 -    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
     5.8 +    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: indep_vars_def prob_space_return)
     5.9    interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
    5.10      ..
    5.11    
    5.12 @@ -1305,7 +1305,7 @@
    5.13    note int_Y = this
    5.14      
    5.15    interpret Y: prob_space "distr M borel (Y i)" for i
    5.16 -    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
    5.17 +    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: indep_vars_def prob_space_return)
    5.18    interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
    5.19      ..
    5.20    
     6.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 07 15:31:59 2015 +0200
     6.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 07 17:11:16 2015 +0200
     6.3 @@ -8,341 +8,55 @@
     6.4    imports Probability_Measure Caratheodory Projective_Family
     6.5  begin
     6.6  
     6.7 -lemma (in product_prob_space) emeasure_PiM_emb_not_empty:
     6.8 -  assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. X i \<in> sets (M i)"
     6.9 -  shows "emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = emeasure (Pi\<^sub>M J M) (Pi\<^sub>E J X)"
    6.10 -proof cases
    6.11 -  assume "finite I" with X show ?thesis by simp
    6.12 -next
    6.13 -  let ?\<Omega> = "\<Pi>\<^sub>E i\<in>I. space (M i)"
    6.14 -  let ?G = generator
    6.15 -  assume "\<not> finite I"
    6.16 -  then have I_not_empty: "I \<noteq> {}" by auto
    6.17 -  interpret G!: algebra ?\<Omega> generator by (rule algebra_generator) fact
    6.18 -  note mu_G_mono =
    6.19 -    G.additive_increasing[OF positive_mu_G[OF I_not_empty] additive_mu_G[OF I_not_empty],
    6.20 -      THEN increasingD]
    6.21 -  write mu_G  ("\<mu>G")
    6.22 -
    6.23 -  { fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> ?G"
    6.24 -
    6.25 -    from `infinite I` `finite J` obtain k where k: "k \<in> I" "k \<notin> J"
    6.26 -      by (metis rev_finite_subset subsetI)
    6.27 -    moreover from Z guess K' X' by (rule generatorE)
    6.28 -    moreover def K \<equiv> "insert k K'"
    6.29 -    moreover def X \<equiv> "emb K K' X'"
    6.30 -    ultimately have K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "X \<in> sets (Pi\<^sub>M K M)" "Z = emb I K X"
    6.31 -      "K - J \<noteq> {}" "K - J \<subseteq> I" "\<mu>G Z = emeasure (Pi\<^sub>M K M) X"
    6.32 -      by (auto simp: subset_insertI)
    6.33 -    let ?M = "\<lambda>y. (\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^sub>M (K - J) M)"
    6.34 -    { fix y assume y: "y \<in> space (Pi\<^sub>M J M)"
    6.35 -      note * = merge_emb[OF `K \<subseteq> I` `J \<subseteq> I` y, of X]
    6.36 -      moreover
    6.37 -      have **: "?M y \<in> sets (Pi\<^sub>M (K - J) M)"
    6.38 -        using J K y by (intro merge_sets) auto
    6.39 -      ultimately
    6.40 -      have ***: "((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)) \<in> ?G"
    6.41 -        using J K by (intro generatorI) auto
    6.42 -      have "\<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^sub>M I M)) = emeasure (Pi\<^sub>M (K - J) M) (?M y)"
    6.43 -        unfolding * using K J by (subst mu_G_eq[OF _ _ _ **]) auto
    6.44 -      note * ** *** this }
    6.45 -    note merge_in_G = this
    6.46 -
    6.47 -    have "finite (K - J)" using K by auto
    6.48 -
    6.49 -    interpret J: finite_product_prob_space M J by standard fact+
    6.50 -    interpret KmJ: finite_product_prob_space M "K - J" by standard fact+
    6.51 -
    6.52 -    have "\<mu>G Z = emeasure (Pi\<^sub>M (J \<union> (K - J)) M) (emb (J \<union> (K - J)) K X)"
    6.53 -      using K J by simp
    6.54 -    also have "\<dots> = (\<integral>\<^sup>+ x. emeasure (Pi\<^sub>M (K - J) M) (?M x) \<partial>Pi\<^sub>M J M)"
    6.55 -      using K J by (subst emeasure_fold_integral) auto
    6.56 -    also have "\<dots> = (\<integral>\<^sup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)) \<partial>Pi\<^sub>M J M)"
    6.57 -      (is "_ = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)")
    6.58 -    proof (intro nn_integral_cong)
    6.59 -      fix x assume x: "x \<in> space (Pi\<^sub>M J M)"
    6.60 -      with K merge_in_G(2)[OF this]
    6.61 -      show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
    6.62 -        unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst mu_G_eq) auto
    6.63 -    qed
    6.64 -    finally have fold: "\<mu>G Z = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)" .
    6.65 -
    6.66 -    { fix x assume x: "x \<in> space (Pi\<^sub>M J M)"
    6.67 -      then have "\<mu>G (?MZ x) \<le> 1"
    6.68 -        unfolding merge_in_G(4)[OF x] `Z = emb I K X`
    6.69 -        by (intro KmJ.measure_le_1 merge_in_G(2)[OF x]) }
    6.70 -    note le_1 = this
    6.71 -
    6.72 -    let ?q = "\<lambda>y. \<mu>G ((\<lambda>x. merge J (I - J) (y,x)) -` Z \<inter> space (Pi\<^sub>M I M))"
    6.73 -    have "?q \<in> borel_measurable (Pi\<^sub>M J M)"
    6.74 -      unfolding `Z = emb I K X` using J K merge_in_G(3)
    6.75 -      by (simp add: merge_in_G  mu_G_eq emeasure_fold_measurable cong: measurable_cong)
    6.76 -    note this fold le_1 merge_in_G(3) }
    6.77 -  note fold = this
    6.78 -
    6.79 -  have "\<exists>\<mu>. (\<forall>s\<in>?G. \<mu> s = \<mu>G s) \<and> measure_space ?\<Omega> (sigma_sets ?\<Omega> ?G) \<mu>"
    6.80 -  proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
    6.81 -    fix A assume "A \<in> ?G"
    6.82 -    with generatorE guess J X . note JX = this
    6.83 -    interpret JK: finite_product_prob_space M J by standard fact+ 
    6.84 -    from JX show "\<mu>G A \<noteq> \<infinity>" by simp
    6.85 -  next
    6.86 -    fix A assume A: "range A \<subseteq> ?G" "decseq A" "(\<Inter>i. A i) = {}"
    6.87 -    then have "decseq (\<lambda>i. \<mu>G (A i))"
    6.88 -      by (auto intro!: mu_G_mono simp: decseq_def)
    6.89 -    moreover
    6.90 -    have "(INF i. \<mu>G (A i)) = 0"
    6.91 -    proof (rule ccontr)
    6.92 -      assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0")
    6.93 -      moreover have "0 \<le> ?a"
    6.94 -        using A positive_mu_G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
    6.95 -      ultimately have "0 < ?a" by auto
    6.96 -
    6.97 -      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^sub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (limP J M (\<lambda>J. (Pi\<^sub>M J M))) X"
    6.98 -        using A by (intro allI generator_Ex) auto
    6.99 -      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\<^sub>M (J' n) M)"
   6.100 -        and A': "\<And>n. A n = emb I (J' n) (X' n)"
   6.101 -        unfolding choice_iff by blast
   6.102 -      moreover def J \<equiv> "\<lambda>n. (\<Union>i\<le>n. J' i)"
   6.103 -      moreover def X \<equiv> "\<lambda>n. emb (J n) (J' n) (X' n)"
   6.104 -      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\<^sub>M (J n) M)"
   6.105 -        by auto
   6.106 -      with A' have A_eq: "\<And>n. A n = emb I (J n) (X n)" "\<And>n. A n \<in> ?G"
   6.107 -        unfolding J_def X_def by (subst prod_emb_trans) (insert A, auto)
   6.108 -
   6.109 -      have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"
   6.110 -        unfolding J_def by force
   6.111 -
   6.112 -      interpret J: finite_product_prob_space M "J i" for i by standard fact+
   6.113 -
   6.114 -      have a_le_1: "?a \<le> 1"
   6.115 -        using mu_G_spec[of "J 0" "A 0" "X 0"] J A_eq
   6.116 -        by (auto intro!: INF_lower2[of 0] J.measure_le_1)
   6.117 -
   6.118 -      let ?M = "\<lambda>K Z y. (\<lambda>x. merge K (I - K) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)"
   6.119 -
   6.120 -      { fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
   6.121 -        then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
   6.122 -        fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
   6.123 -        interpret J': finite_product_prob_space M J' by standard fact+
   6.124 -
   6.125 -        let ?q = "\<lambda>n y. \<mu>G (?M J' (Z n) y)"
   6.126 -        let ?Q = "\<lambda>n. ?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^sub>M J' M)"
   6.127 -        { fix n
   6.128 -          have "?q n \<in> borel_measurable (Pi\<^sub>M J' M)"
   6.129 -            using Z J' by (intro fold(1)) auto
   6.130 -          then have "?Q n \<in> sets (Pi\<^sub>M J' M)"
   6.131 -            by (rule measurable_sets) auto }
   6.132 -        note Q_sets = this
   6.133 +lemma (in product_prob_space) distr_PiM_restrict_finite:
   6.134 +  assumes "finite J" "J \<subseteq> I"
   6.135 +  shows "distr (PiM I M) (PiM J M) (\<lambda>x. restrict x J) = PiM J M"
   6.136 +proof (rule PiM_eqI)
   6.137 +  fix X assume X: "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
   6.138 +  { fix J X assume J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" and X: "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
   6.139 +    have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
   6.140 +    proof (subst emeasure_extend_measure_Pair[OF PiM_def, where \<mu>'=lim], goal_cases)
   6.141 +      case 1 then show ?case
   6.142 +        by (simp add: M.emeasure_space_1 emeasure_PiM Pi_iff sets_PiM_I_finite emeasure_lim_emb)
   6.143 +    next
   6.144 +      case (2 J X)
   6.145 +      then have "emb I J (Pi\<^sub>E J X) \<in> sets (PiM I M)"
   6.146 +        by (intro measurable_prod_emb sets_PiM_I_finite) auto
   6.147 +      from this[THEN sets.sets_into_space] show ?case
   6.148 +        by (simp add: space_PiM)
   6.149 +    qed (insert assms J X, simp_all del: sets_lim
   6.150 +      add: M.emeasure_space_1 sets_lim[symmetric] emeasure_countably_additive emeasure_positive) }
   6.151 +  note * = this
   6.152  
   6.153 -        have "?a / 2^(k+1) \<le> (INF n. emeasure (Pi\<^sub>M J' M) (?Q n))"
   6.154 -        proof (intro INF_greatest)
   6.155 -          fix n
   6.156 -          have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
   6.157 -          also have "\<dots> \<le> (\<integral>\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^sub>M J' M)"
   6.158 -            unfolding fold(2)[OF J' `Z n \<in> ?G`]
   6.159 -          proof (intro nn_integral_mono)
   6.160 -            fix x assume x: "x \<in> space (Pi\<^sub>M J' M)"
   6.161 -            then have "?q n x \<le> 1 + 0"
   6.162 -              using J' Z fold(3) Z_sets by auto
   6.163 -            also have "\<dots> \<le> 1 + ?a / 2^(k+1)"
   6.164 -              using `0 < ?a` by (intro add_mono) auto
   6.165 -            finally have "?q n x \<le> 1 + ?a / 2^(k+1)" .
   6.166 -            with x show "?q n x \<le> indicator (?Q n) x + ?a / 2^(k+1)"
   6.167 -              by (auto split: split_indicator simp del: power_Suc)
   6.168 -          qed
   6.169 -          also have "\<dots> = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)"
   6.170 -            using `0 \<le> ?a` Q_sets J'.emeasure_space_1
   6.171 -            by (subst nn_integral_add) auto
   6.172 -          finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \<le> 1`
   6.173 -            by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"])
   6.174 -               (auto simp: field_simps)
   6.175 -        qed
   6.176 -        also have "\<dots> = emeasure (Pi\<^sub>M J' M) (\<Inter>n. ?Q n)"
   6.177 -        proof (intro INF_emeasure_decseq)
   6.178 -          show "range ?Q \<subseteq> sets (Pi\<^sub>M J' M)" using Q_sets by auto
   6.179 -          show "decseq ?Q"
   6.180 -            unfolding decseq_def
   6.181 -          proof (safe intro!: vimageI[OF refl])
   6.182 -            fix m n :: nat assume "m \<le> n"
   6.183 -            fix x assume x: "x \<in> space (Pi\<^sub>M J' M)"
   6.184 -            assume "?a / 2^(k+1) \<le> ?q n x"
   6.185 -            also have "?q n x \<le> ?q m x"
   6.186 -            proof (rule mu_G_mono)
   6.187 -              from fold(4)[OF J', OF Z_sets x]
   6.188 -              show "?M J' (Z n) x \<in> ?G" "?M J' (Z m) x \<in> ?G" by auto
   6.189 -              show "?M J' (Z n) x \<subseteq> ?M J' (Z m) x"
   6.190 -                using `decseq Z`[THEN decseqD, OF `m \<le> n`] by auto
   6.191 -            qed
   6.192 -            finally show "?a / 2^(k+1) \<le> ?q m x" .
   6.193 -          qed
   6.194 -        qed simp
   6.195 -        finally have "(\<Inter>n. ?Q n) \<noteq> {}"
   6.196 -          using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
   6.197 -        then have "\<exists>w\<in>space (Pi\<^sub>M J' M). \<forall>n. ?a / 2 ^ (k + 1) \<le> ?q n w" by auto }
   6.198 -      note Ex_w = this
   6.199 -
   6.200 -      let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"
   6.201 +  have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
   6.202 +  proof cases
   6.203 +    assume "\<not> (J \<noteq> {} \<or> I = {})"
   6.204 +    then obtain i where "J = {}" "i \<in> I" by auto
   6.205 +    moreover then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
   6.206 +      by (auto simp: space_PiM prod_emb_def)
   6.207 +    ultimately show ?thesis
   6.208 +      by (simp add: * M.emeasure_space_1)
   6.209 +  qed (simp add: *[OF _ assms X])
   6.210 +  with assms show "emeasure (distr (Pi\<^sub>M I M) (Pi\<^sub>M J M) (\<lambda>x. restrict x J)) (Pi\<^sub>E J X) = (\<Prod>i\<in>J. emeasure (M i) (X i))"
   6.211 +    by (subst emeasure_distr_restrict[OF _ refl]) (auto intro!: sets_PiM_I_finite X)
   6.212 +qed (insert assms, auto)
   6.213  
   6.214 -      let ?P = "\<lambda>w k. w \<in> space (Pi\<^sub>M (J k) M) \<and> (\<forall>n. ?a / 2 ^ (Suc k) \<le> ?q k n w)"
   6.215 -      have "\<exists>w. \<forall>k. ?P (w k) k \<and> restrict (w (Suc k)) (J k) = w k"
   6.216 -      proof (rule dependent_nat_choice)
   6.217 -        have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
   6.218 -        from Ex_w[OF A(1,2) this J(1-3), of 0] show "\<exists>w. ?P w 0" by auto
   6.219 -      next
   6.220 -        fix w k assume Suc: "?P w k"
   6.221 -        show "\<exists>w'. ?P w' (Suc k) \<and> restrict w' (J k) = w"
   6.222 -        proof cases
   6.223 -          assume [simp]: "J k = J (Suc k)"
   6.224 -          have "?a / 2 ^ (Suc (Suc k)) \<le> ?a / 2 ^ (k + 1)"
   6.225 -            using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
   6.226 -          with Suc show ?thesis
   6.227 -            by (auto intro!: exI[of _ w] simp: extensional_restrict space_PiM intro: order_trans)
   6.228 -        next
   6.229 -          assume "J k \<noteq> J (Suc k)"
   6.230 -          with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
   6.231 -          have "range (\<lambda>n. ?M (J k) (A n) w) \<subseteq> ?G" "decseq (\<lambda>n. ?M (J k) (A n) w)"
   6.232 -            "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) w)"
   6.233 -            using `decseq A` fold(4)[OF J(1-3) A_eq(2), of w k] Suc
   6.234 -            by (auto simp: decseq_def)
   6.235 -          from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
   6.236 -          obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
   6.237 -            "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) w) w')" by auto
   6.238 -          let ?w = "merge (J k) ?D (w, w')"
   6.239 -          have [simp]: "\<And>x. merge (J k) (I - J k) (w, merge ?D (I - ?D) (w', x)) =
   6.240 -            merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
   6.241 -            using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
   6.242 -            by (auto intro!: ext split: split_merge)
   6.243 -          have *: "\<And>n. ?M ?D (?M (J k) (A n) w) w' = ?M (J (Suc k)) (A n) ?w"
   6.244 -            using w'(1) J(3)[of "Suc k"]
   6.245 -            by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
   6.246 -          show ?thesis
   6.247 -            using Suc w' J_mono[of k "Suc k"] unfolding *
   6.248 -            by (intro exI[of _ ?w])
   6.249 -               (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
   6.250 -        qed
   6.251 -      qed
   6.252 -      then obtain w where w:
   6.253 -        "\<And>k. w k \<in> space (Pi\<^sub>M (J k) M)"
   6.254 -        "\<And>k n. ?a / 2 ^ (Suc k) \<le> ?q k n (w k)"
   6.255 -        "\<And>k. restrict (w (Suc k)) (J k) = w k"
   6.256 -        by metis
   6.257 -
   6.258 -      { fix k
   6.259 -        from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
   6.260 -        then have "?M (J k) (A k) (w k) \<noteq> {}"
   6.261 -          using positive_mu_G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
   6.262 -          by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
   6.263 -        then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
   6.264 -        then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
   6.265 -        then have "\<exists>x\<in>A k. restrict x (J k) = w k"
   6.266 -          using `w k \<in> space (Pi\<^sub>M (J k) M)`
   6.267 -          by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM) }
   6.268 -      note w_ext = this
   6.269 +lemma (in product_prob_space) emeasure_PiM_emb':
   6.270 +  "J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> emeasure (Pi\<^sub>M I M) (emb I J X) = PiM J M X"
   6.271 +  by (subst distr_PiM_restrict_finite[symmetric, of J])
   6.272 +     (auto intro!: emeasure_distr_restrict[symmetric])
   6.273  
   6.274 -      { fix k l i assume "k \<le> l" "i \<in> J k"
   6.275 -        { fix l have "w k i = w (k + l) i"
   6.276 -          proof (induct l)
   6.277 -            case (Suc l)
   6.278 -            from `i \<in> J k` J_mono[of k "k + l"] have "i \<in> J (k + l)" by auto
   6.279 -            with w(3)[of "k + l"]
   6.280 -            have "w (k + l) i = w (k + Suc l) i"
   6.281 -              by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
   6.282 -            with Suc show ?case by simp
   6.283 -          qed simp }
   6.284 -        from this[of "l - k"] `k \<le> l` have "w l i = w k i" by simp }
   6.285 -      note w_mono = this
   6.286 -
   6.287 -      def w' \<equiv> "\<lambda>i. if i \<in> (\<Union>k. J k) then w (LEAST k. i \<in> J k) i else if i \<in> I then (SOME x. x \<in> space (M i)) else undefined"
   6.288 -      { fix i k assume k: "i \<in> J k"
   6.289 -        have "w k i = w (LEAST k. i \<in> J k) i"
   6.290 -          by (intro w_mono Least_le k LeastI[of _ k])
   6.291 -        then have "w' i = w k i"
   6.292 -          unfolding w'_def using k by auto }
   6.293 -      note w'_eq = this
   6.294 -      have w'_simps1: "\<And>i. i \<notin> I \<Longrightarrow> w' i = undefined"
   6.295 -        using J by (auto simp: w'_def)
   6.296 -      have w'_simps2: "\<And>i. i \<notin> (\<Union>k. J k) \<Longrightarrow> i \<in> I \<Longrightarrow> w' i \<in> space (M i)"
   6.297 -        using J by (auto simp: w'_def intro!: someI_ex[OF M.not_empty[unfolded ex_in_conv[symmetric]]])
   6.298 -      { fix i assume "i \<in> I" then have "w' i \<in> space (M i)"
   6.299 -          using w(1) by (cases "i \<in> (\<Union>k. J k)") (force simp: w'_simps2 w'_eq space_PiM)+ }
   6.300 -      note w'_simps[simp] = w'_eq w'_simps1 w'_simps2 this
   6.301 -
   6.302 -      have w': "w' \<in> space (Pi\<^sub>M I M)"
   6.303 -        using w(1) by (auto simp add: Pi_iff extensional_def space_PiM)
   6.304 -
   6.305 -      { fix n
   6.306 -        have "restrict w' (J n) = w n" using w(1)[of n]
   6.307 -          by (auto simp add: fun_eq_iff space_PiM)
   6.308 -        with w_ext[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)"
   6.309 -          by auto
   6.310 -        then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
   6.311 -      then have "w' \<in> (\<Inter>i. A i)" by auto
   6.312 -      with `(\<Inter>i. A i) = {}` show False by auto
   6.313 -    qed
   6.314 -    ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
   6.315 -      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (A i)"] by simp
   6.316 -  qed fact+
   6.317 -  then guess \<mu> .. note \<mu> = this
   6.318 -  show ?thesis
   6.319 -  proof (subst emeasure_extend_measure_Pair[OF PiM_def, of I M \<mu> J X])
   6.320 -    from assms show "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
   6.321 -      by (simp add: Pi_iff)
   6.322 -  next
   6.323 -    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))"
   6.324 -    then show "emb I J (Pi\<^sub>E J X) \<in> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
   6.325 -      by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space)
   6.326 -    have "emb I J (Pi\<^sub>E J X) \<in> generator"
   6.327 -      using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
   6.328 -    then have "\<mu> (emb I J (Pi\<^sub>E J X)) = \<mu>G (emb I J (Pi\<^sub>E J X))"
   6.329 -      using \<mu> by simp
   6.330 -    also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
   6.331 -      using J  `I \<noteq> {}` by (subst mu_G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff)
   6.332 -    also have "\<dots> = (\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}.
   6.333 -      if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
   6.334 -      using J `I \<noteq> {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1)
   6.335 -    finally show "\<mu> (emb I J (Pi\<^sub>E J X)) = \<dots>" .
   6.336 -  next
   6.337 -    let ?F = "\<lambda>j. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j))"
   6.338 -    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)"
   6.339 -      using X `I \<noteq> {}` by (intro setprod.mono_neutral_right) (auto simp: M.emeasure_space_1)
   6.340 -    then show "(\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}. ?F j) =
   6.341 -      emeasure (Pi\<^sub>M J M) (Pi\<^sub>E J X)"
   6.342 -      using X by (auto simp add: emeasure_PiM) 
   6.343 -  next
   6.344 -    show "positive (sets (Pi\<^sub>M I M)) \<mu>" "countably_additive (sets (Pi\<^sub>M I M)) \<mu>"
   6.345 -      using \<mu> unfolding sets_PiM_generator by (auto simp: measure_space_def)
   6.346 -  qed
   6.347 -qed
   6.348 +lemma (in product_prob_space) emeasure_PiM_emb:
   6.349 +  "J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow> 
   6.350 +    emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod> i\<in>J. emeasure (M i) (X i))"
   6.351 +  by (subst emeasure_PiM_emb') (auto intro!: emeasure_PiM)
   6.352  
   6.353  sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^sub>M I M"
   6.354  proof
   6.355 +  have *: "emb I {} {\<lambda>x. undefined} = space (PiM I M)"
   6.356 +    by (auto simp: prod_emb_def space_PiM)
   6.357    show "emeasure (Pi\<^sub>M I M) (space (Pi\<^sub>M I M)) = 1"
   6.358 -  proof cases
   6.359 -    assume "I = {}" then show ?thesis by (simp add: space_PiM_empty)
   6.360 -  next
   6.361 -    assume "I \<noteq> {}"
   6.362 -    then obtain i where i: "i \<in> I" by auto
   6.363 -    then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
   6.364 -      by (auto simp: prod_emb_def space_PiM)
   6.365 -    with i show ?thesis
   6.366 -      using emeasure_PiM_emb_not_empty[of "{i}" "\<lambda>i. space (M i)"]
   6.367 -      by (simp add: emeasure_PiM emeasure_space_1)
   6.368 -  qed
   6.369 -qed
   6.370 -
   6.371 -lemma (in product_prob_space) emeasure_PiM_emb:
   6.372 -  assumes X: "J \<subseteq> I" "finite J" "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
   6.373 -  shows "emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod> i\<in>J. emeasure (M i) (X i))"
   6.374 -proof cases
   6.375 -  assume "J = {}"
   6.376 -  moreover have "emb I {} {\<lambda>x. undefined} = space (Pi\<^sub>M I M)"
   6.377 -    by (auto simp: space_PiM prod_emb_def)
   6.378 -  ultimately show ?thesis
   6.379 -    by (simp add: space_PiM_empty P.emeasure_space_1)
   6.380 -next
   6.381 -  assume "J \<noteq> {}" with X show ?thesis
   6.382 -    by (subst emeasure_PiM_emb_not_empty) (auto simp: emeasure_PiM)
   6.383 +    using emeasure_PiM_emb[of "{}" "\<lambda>_. {}"] by (simp add: *)
   6.384  qed
   6.385  
   6.386  lemma (in product_prob_space) emeasure_PiM_Collect:
   6.387 @@ -388,7 +102,6 @@
   6.388  qed simp
   6.389  
   6.390  lemma (in product_prob_space) PiM_eq:
   6.391 -  assumes "I \<noteq> {}"
   6.392    assumes "sets M' = sets (PiM I M)"
   6.393    assumes eq: "\<And>J F. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>j. j \<in> J \<Longrightarrow> F j \<in> sets (M j)) \<Longrightarrow>
   6.394      emeasure M' (prod_emb I M J (\<Pi>\<^sub>E j\<in>J. F j)) = (\<Prod>j\<in>J. emeasure (M j) (F j))"
   6.395 @@ -400,15 +113,15 @@
   6.396      unfolding `sets M' = sets (PiM I M)` by simp
   6.397  
   6.398    def i \<equiv> "SOME i. i \<in> I"
   6.399 -  with `I \<noteq> {}` have i: "i \<in> I"
   6.400 -    by (auto intro: someI_ex)
   6.401 +  have i: "I \<noteq> {} \<Longrightarrow> i \<in> I"
   6.402 +    unfolding i_def by (rule someI_ex) auto
   6.403  
   6.404 -  def A \<equiv> "\<lambda>n::nat. prod_emb I M {i} (\<Pi>\<^sub>E j\<in>{i}. space (M i))"
   6.405 +  def A \<equiv> "\<lambda>n::nat. if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
   6.406    then show "range A \<subseteq> prod_algebra I M"
   6.407 -    by (auto intro!: prod_algebraI i)
   6.408 +    using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i)
   6.409  
   6.410    have A_eq: "\<And>i. A i = space (PiM I M)"
   6.411 -    by (auto simp: prod_emb_def space_PiM Pi_iff A_def i)
   6.412 +    by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI)
   6.413    show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   6.414      unfolding A_eq by (auto simp: space_PiM)
   6.415    show "\<And>i. emeasure (PiM I M) (A i) \<noteq> \<infinity>"
     7.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 07 15:31:59 2015 +0200
     7.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 07 17:11:16 2015 +0200
     7.3 @@ -555,6 +555,53 @@
     7.4      unfolding ereal_minus_eq_minus_iff using finite A0 by auto
     7.5  qed
     7.6  
     7.7 +lemma emeasure_INT_decseq_subset:
     7.8 +  fixes F :: "nat \<Rightarrow> 'a set"
     7.9 +  assumes I: "I \<noteq> {}" and F: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<le> j \<Longrightarrow> F j \<subseteq> F i"
    7.10 +  assumes F_sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M"
    7.11 +    and fin: "\<And>i. i \<in> I \<Longrightarrow> emeasure M (F i) \<noteq> \<infinity>"
    7.12 +  shows "emeasure M (\<Inter>i\<in>I. F i) = (INF i:I. emeasure M (F i))"
    7.13 +proof cases
    7.14 +  assume "finite I"
    7.15 +  have "(\<Inter>i\<in>I. F i) = F (Max I)"
    7.16 +    using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F) auto
    7.17 +  moreover have "(INF i:I. emeasure M (F i)) = emeasure M (F (Max I))"
    7.18 +    using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F emeasure_mono) auto
    7.19 +  ultimately show ?thesis
    7.20 +    by simp
    7.21 +next
    7.22 +  assume "infinite I"
    7.23 +  def L \<equiv> "\<lambda>n. LEAST i. i \<in> I \<and> i \<ge> n"
    7.24 +  have L: "L n \<in> I \<and> n \<le> L n" for n
    7.25 +    unfolding L_def
    7.26 +  proof (rule LeastI_ex)
    7.27 +    show "\<exists>x. x \<in> I \<and> n \<le> x"
    7.28 +      using \<open>infinite I\<close> finite_subset[of I "{..< n}"]
    7.29 +      by (rule_tac ccontr) (auto simp: not_le)
    7.30 +  qed
    7.31 +  have L_eq[simp]: "i \<in> I \<Longrightarrow> L i = i" for i
    7.32 +    unfolding L_def by (intro Least_equality) auto
    7.33 +  have L_mono: "i \<le> j \<Longrightarrow> L i \<le> L j" for i j
    7.34 +    using L[of j] unfolding L_def by (intro Least_le) (auto simp: L_def)
    7.35 +
    7.36 +  have "emeasure M (\<Inter>i. F (L i)) = (INF i. emeasure M (F (L i)))"
    7.37 +  proof (intro INF_emeasure_decseq[symmetric])
    7.38 +    show "decseq (\<lambda>i. F (L i))"
    7.39 +      using L by (intro antimonoI F L_mono) auto
    7.40 +  qed (insert L fin, auto)
    7.41 +  also have "\<dots> = (INF i:I. emeasure M (F i))"
    7.42 +  proof (intro antisym INF_greatest)
    7.43 +    show "i \<in> I \<Longrightarrow> (INF i. emeasure M (F (L i))) \<le> emeasure M (F i)" for i
    7.44 +      by (intro INF_lower2[of i]) auto
    7.45 +  qed (insert L, auto intro: INF_lower)
    7.46 +  also have "(\<Inter>i. F (L i)) = (\<Inter>i\<in>I. F i)"
    7.47 +  proof (intro antisym INF_greatest)
    7.48 +    show "i \<in> I \<Longrightarrow> (\<Inter>i. F (L i)) \<subseteq> F i" for i
    7.49 +      by (intro INF_lower2[of i]) auto
    7.50 +  qed (insert L, auto)
    7.51 +  finally show ?thesis .
    7.52 +qed
    7.53 +
    7.54  lemma Lim_emeasure_decseq:
    7.55    assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
    7.56    shows "(\<lambda>i. emeasure M (A i)) ----> emeasure M (\<Inter>i. A i)"
     8.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Oct 07 15:31:59 2015 +0200
     8.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Oct 07 17:11:16 2015 +0200
     8.3 @@ -1511,8 +1511,10 @@
     8.4  qed
     8.5  
     8.6  lemma nn_integral_monotone_convergence_INF:
     8.7 -  assumes f: "decseq f" and [measurable]: "\<And>i. f i \<in> borel_measurable M"
     8.8 -  assumes fin: "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>"
     8.9 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
    8.10 +  assumes f: "\<And>i j x. i \<le> j \<Longrightarrow> x \<in> space M \<Longrightarrow> f j x \<le> f i x"
    8.11 +    and [measurable]: "\<And>i. f i \<in> borel_measurable M"
    8.12 +    and fin: "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>"
    8.13    shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))"
    8.14  proof -
    8.15    { fix f :: "nat \<Rightarrow> ereal" and j assume "decseq f"
    8.16 @@ -1523,28 +1525,33 @@
    8.17        done }
    8.18    note INF_shift = this
    8.19  
    8.20 -  have dec: "\<And>f::nat \<Rightarrow> 'a \<Rightarrow> ereal. decseq f \<Longrightarrow> decseq (\<lambda>j x. max 0 (f (j + i) x))"
    8.21 -    by (intro antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def)
    8.22 +  have dec: "decseq (\<lambda>j x. max 0 (restrict (f (j + i)) (space M) x))"
    8.23 +    using f by (intro antimonoI le_funI max.mono) (auto simp: decseq_def le_fun_def)
    8.24  
    8.25 -  have "(\<integral>\<^sup>+ x. max 0 (INF i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (INF i. max 0 (f i x)) \<partial>M)"
    8.26 +  have "(\<integral>\<^sup>+ x. max 0 (INF i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (INF i. max 0 (restrict (f i) (space M) x)) \<partial>M)"
    8.27      by (intro nn_integral_cong)
    8.28         (simp add: sup_ereal_def[symmetric] sup_INF del: sup_ereal_def)
    8.29 -  also have "\<dots> = (\<integral>\<^sup>+ x. (INF j. max 0 (f (j + i) x)) \<partial>M)"
    8.30 +  also have "\<dots> = (\<integral>\<^sup>+ x. (INF j. max 0 (restrict (f (j + i)) (space M) x)) \<partial>M)"
    8.31      using f by (intro nn_integral_cong INF_shift antimonoI le_funI max.mono) 
    8.32                 (auto simp: decseq_def le_fun_def)
    8.33 -  also have "\<dots> = (INF j. (\<integral>\<^sup>+ x. max 0 (f (j + i) x) \<partial>M))"
    8.34 +  also have "\<dots> = (INF j. (\<integral>\<^sup>+ x. max 0 (restrict (f (j + i)) (space M) x) \<partial>M))"
    8.35    proof (rule nn_integral_monotone_convergence_INF')
    8.36 -    show "\<And>j. (\<lambda>x. max 0 (f (j + i) x)) \<in> borel_measurable M"
    8.37 -      by measurable
    8.38 -    show "(\<integral>\<^sup>+ x. max 0 (f (0 + i) x) \<partial>M) < \<infinity>"
    8.39 -      using fin by (simp add: nn_integral_max_0)
    8.40 +    show "(\<lambda>x. max 0 (restrict (f (j + i)) (space M) x)) \<in> borel_measurable M" for j
    8.41 +      by (subst measurable_cong[where g="\<lambda>x. max 0 (f (j + i) x)"]) measurable
    8.42 +    show "(\<integral>\<^sup>+ x. max 0 (restrict (f (0 + i)) (space M) x) \<partial>M) < \<infinity>"
    8.43 +      using fin by (simp add: nn_integral_max_0 cong: nn_integral_cong)
    8.44    qed (intro max.cobounded1 dec f)+
    8.45 -  also have "\<dots> = (INF j. (\<integral>\<^sup>+ x. max 0 (f j x) \<partial>M))"
    8.46 +  also have "\<dots> = (INF j. (\<integral>\<^sup>+ x. max 0 (restrict (f j) (space M) x) \<partial>M))"
    8.47      using f by (intro INF_shift[symmetric] nn_integral_mono antimonoI le_funI max.mono) 
    8.48                 (auto simp: decseq_def le_fun_def)
    8.49 -  finally show ?thesis unfolding nn_integral_max_0 .
    8.50 +  finally show ?thesis unfolding nn_integral_max_0 by (simp cong: nn_integral_cong)
    8.51  qed
    8.52  
    8.53 +lemma nn_integral_monotone_convergence_INF_decseq:
    8.54 +  assumes f: "decseq f" and *: "\<And>i. f i \<in> borel_measurable M" "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>"
    8.55 +  shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))"
    8.56 +  using nn_integral_monotone_convergence_INF[of M f i, OF _ *] f by (auto simp: antimono_def le_fun_def)
    8.57 +
    8.58  lemma sup_continuous_nn_integral[order_continuous_intros]:
    8.59    assumes f: "\<And>y. sup_continuous (f y)"
    8.60    assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
    8.61 @@ -1771,7 +1778,7 @@
    8.62    fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume "decseq C" "\<And>i. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)"
    8.63    then show "(\<lambda>s. \<integral>\<^sup>+x. (INF i. C i) x \<partial>M s) = (INF i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))"
    8.64      unfolding INF_apply[abs_def]
    8.65 -    by (subst nn_integral_monotone_convergence_INF)
    8.66 +    by (subst nn_integral_monotone_convergence_INF_decseq)
    8.67         (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets)
    8.68  next
    8.69    show "\<And>x. g x \<le> (\<lambda>s. integral\<^sup>N (M s) (f top))"
    8.70 @@ -1782,7 +1789,7 @@
    8.71    fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C"
    8.72    with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)"
    8.73      unfolding INF_apply[abs_def]
    8.74 -    by (subst nn_integral_monotone_convergence_INF)
    8.75 +    by (subst nn_integral_monotone_convergence_INF_decseq)
    8.76         (auto cong: measurable_cong_sets intro!: borel_measurable_INF
    8.77               simp: INF_less_iff simp del: ereal_infty_less(1))
    8.78  next
     9.1 --- a/src/HOL/Probability/Probability.thy	Wed Oct 07 15:31:59 2015 +0200
     9.2 +++ b/src/HOL/Probability/Probability.thy	Wed Oct 07 17:11:16 2015 +0200
     9.3 @@ -12,9 +12,7 @@
     9.4    Probability_Mass_Function
     9.5    Stream_Space
     9.6    Embed_Measure
     9.7 -  Interval_Integral
     9.8 -  Set_Integral
     9.9 -  Giry_Monad
    9.10  begin
    9.11  
    9.12  end
    9.13 +
    10.1 --- a/src/HOL/Probability/Probability_Measure.thy	Wed Oct 07 15:31:59 2015 +0200
    10.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Wed Oct 07 17:11:16 2015 +0200
    10.3 @@ -43,6 +43,16 @@
    10.4      by (auto simp: emeasure_distr emeasure_space_1)
    10.5  qed
    10.6  
    10.7 +lemma prob_space_distrD:
    10.8 +  assumes f: "f \<in> measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M"
    10.9 +proof
   10.10 +  interpret M!: prob_space "distr M N f" by fact
   10.11 +  have "f -` space N \<inter> space M = space M"
   10.12 +    using f[THEN measurable_space] by auto
   10.13 +  then show "emeasure M (space M) = 1"
   10.14 +    using M.emeasure_space_1 by (simp add: emeasure_distr[OF f])
   10.15 +qed
   10.16 +
   10.17  lemma (in prob_space) prob_space: "prob (space M) = 1"
   10.18    using emeasure_space_1 unfolding measure_def by (simp add: one_ereal_def)
   10.19  
   10.20 @@ -1152,4 +1162,53 @@
   10.21    "finite S \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s) \<Longrightarrow> (\<Sum>s\<in>S. p s) = 1 \<Longrightarrow> prob_space (point_measure S p)"
   10.22    by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite)
   10.23  
   10.24 +lemma (in prob_space) distr_pair_fst: "distr (N \<Otimes>\<^sub>M M) N fst = N"
   10.25 +proof (intro measure_eqI)
   10.26 +  fix A assume A: "A \<in> sets (distr (N \<Otimes>\<^sub>M M) N fst)"
   10.27 +  from A have "emeasure (distr (N \<Otimes>\<^sub>M M) N fst) A = emeasure (N \<Otimes>\<^sub>M M) (A \<times> space M)"
   10.28 +    by (auto simp add: emeasure_distr space_pair_measure dest: sets.sets_into_space intro!: arg_cong2[where f=emeasure])
   10.29 +  with A show "emeasure (distr (N \<Otimes>\<^sub>M M) N fst) A = emeasure N A"
   10.30 +    by (simp add: emeasure_pair_measure_Times emeasure_space_1)
   10.31 +qed simp
   10.32 +
   10.33 +lemma (in product_prob_space) distr_reorder:
   10.34 +  assumes "inj_on t J" "t \<in> J \<rightarrow> K" "finite K"
   10.35 +  shows "distr (PiM K M) (Pi\<^sub>M J (\<lambda>x. M (t x))) (\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) = PiM J (\<lambda>x. M (t x))"
   10.36 +proof (rule product_sigma_finite.PiM_eqI)
   10.37 +  show "product_sigma_finite (\<lambda>x. M (t x))" ..
   10.38 +  have "t`J \<subseteq> K" using assms by auto
   10.39 +  then show [simp]: "finite J"
   10.40 +    by (rule finite_imageD[OF finite_subset]) fact+
   10.41 +  fix A assume A: "\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M (t i))"
   10.42 +  moreover have "((\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) -` Pi\<^sub>E J A \<inter> space (Pi\<^sub>M K M)) =
   10.43 +    (\<Pi>\<^sub>E i\<in>K. if i \<in> t`J then A (the_inv_into J t i) else space (M i))"
   10.44 +    using A A[THEN sets.sets_into_space] \<open>t \<in> J \<rightarrow> K\<close> \<open>inj_on t J\<close>
   10.45 +    by (subst prod_emb_Pi[symmetric]) (auto simp: space_PiM PiE_iff the_inv_into_f_f prod_emb_def)
   10.46 +  ultimately show "distr (Pi\<^sub>M K M) (Pi\<^sub>M J (\<lambda>x. M (t x))) (\<lambda>\<omega>. \<lambda>n\<in>J. \<omega> (t n)) (Pi\<^sub>E J A) = (\<Prod>i\<in>J. M (t i) (A i))"
   10.47 +    using assms
   10.48 +    apply (subst emeasure_distr)
   10.49 +    apply (auto intro!: sets_PiM_I_finite simp: Pi_iff)
   10.50 +    apply (subst emeasure_PiM)
   10.51 +    apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> setprod.reindex[OF \<open>inj_on t J\<close>]
   10.52 +      if_distrib[where f="emeasure (M _)"] setprod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>)
   10.53 +    done
   10.54 +qed simp
   10.55 +
   10.56 +lemma (in product_prob_space) distr_restrict:
   10.57 +  "J \<subseteq> K \<Longrightarrow> finite K \<Longrightarrow> (\<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)"
   10.58 +  using distr_reorder[of "\<lambda>x. x" J K] by (simp add: Pi_iff subset_eq)
   10.59 +
   10.60 +lemma (in product_prob_space) emeasure_prod_emb[simp]:
   10.61 +  assumes L: "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^sub>M J M)"
   10.62 +  shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X"
   10.63 +  by (subst distr_restrict[OF L])
   10.64 +     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
   10.65 +
   10.66 +lemma emeasure_distr_restrict:
   10.67 +  assumes "I \<subseteq> K" and Q[measurable_cong]: "sets Q = sets (PiM K M)" and A[measurable]: "A \<in> sets (PiM I M)"
   10.68 +  shows "emeasure (distr Q (PiM I M) (\<lambda>\<omega>. restrict \<omega> I)) A = emeasure Q (prod_emb K M I A)"
   10.69 +  using \<open>I\<subseteq>K\<close> sets_eq_imp_space_eq[OF Q]
   10.70 +  by (subst emeasure_distr)
   10.71 +     (auto simp: measurable_cong_sets[OF Q] prod_emb_def space_PiM[symmetric] intro!: measurable_restrict)
   10.72 +
   10.73  end
    11.1 --- a/src/HOL/Probability/Projective_Family.thy	Wed Oct 07 15:31:59 2015 +0200
    11.2 +++ b/src/HOL/Probability/Projective_Family.thy	Wed Oct 07 17:11:16 2015 +0200
    11.3 @@ -6,342 +6,672 @@
    11.4  section {*Projective Family*}
    11.5  
    11.6  theory Projective_Family
    11.7 -imports Finite_Product_Measure Probability_Measure
    11.8 +imports Finite_Product_Measure Giry_Monad
    11.9  begin
   11.10  
   11.11 -lemma (in product_prob_space) distr_restrict:
   11.12 -  assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
   11.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")
   11.14 -proof (rule measure_eqI_generator_eq)
   11.15 -  have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset)
   11.16 -  interpret J: finite_product_prob_space M J proof qed fact
   11.17 -  interpret K: finite_product_prob_space M K proof qed fact
   11.18 -
   11.19 -  let ?J = "{Pi\<^sub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
   11.20 -  let ?F = "\<lambda>i. \<Pi>\<^sub>E k\<in>J. space (M k)"
   11.21 -  let ?\<Omega> = "(\<Pi>\<^sub>E k\<in>J. space (M k))"
   11.22 -  show "Int_stable ?J"
   11.23 -    by (rule Int_stable_PiE)
   11.24 -  show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
   11.25 -    using `finite J` by (auto intro!: prod_algebraI_finite)
   11.26 -  { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
   11.27 -  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space)
   11.28 -  show "sets (\<Pi>\<^sub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
   11.29 -    using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
   11.30 -
   11.31 -  fix X assume "X \<in> ?J"
   11.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
   11.33 -  with `finite J` have X: "X \<in> sets (Pi\<^sub>M J M)"
   11.34 -    by simp
   11.35 -
   11.36 -  have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
   11.37 -    using E by (simp add: J.measure_times)
   11.38 -  also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))"
   11.39 -    by simp
   11.40 -  also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
   11.41 -    using `finite K` `J \<subseteq> K`
   11.42 -    by (intro setprod.mono_neutral_left) (auto simp: M.emeasure_space_1)
   11.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))"
   11.44 -    using E by (simp add: K.measure_times)
   11.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))"
   11.46 -    using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
   11.47 -  finally show "emeasure (Pi\<^sub>M J M) X = emeasure ?D X"
   11.48 -    using X `J \<subseteq> K` apply (subst emeasure_distr)
   11.49 -    by (auto intro!: measurable_restrict_subset simp: space_PiM)
   11.50 +lemma vimage_restrict_preseve_mono:
   11.51 +  assumes J: "J \<subseteq> I"
   11.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> {}"
   11.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)"
   11.54 +  shows "A \<subseteq> B"
   11.55 +proof  (intro subsetI)
   11.56 +  fix x assume "x \<in> A"
   11.57 +  from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
   11.58 +  have "J \<inter> (I - J) = {}" by auto
   11.59 +  show "x \<in> B"
   11.60 +  proof cases
   11.61 +    assume x: "x \<in> (\<Pi>\<^sub>E i\<in>J. S i)"
   11.62 +    have "merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
   11.63 +      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close>
   11.64 +      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
   11.65 +    also have "\<dots> \<subseteq> (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)" by fact
   11.66 +    finally show "x \<in> B"
   11.67 +      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> eq
   11.68 +      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
   11.69 +  qed (insert \<open>x\<in>A\<close> sets, auto)
   11.70  qed
   11.71  
   11.72 -lemma (in product_prob_space) emeasure_prod_emb[simp]:
   11.73 -  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^sub>M J M)"
   11.74 -  shows "emeasure (Pi\<^sub>M L M) (prod_emb L M J X) = emeasure (Pi\<^sub>M J M) X"
   11.75 -  by (subst distr_restrict[OF L])
   11.76 -     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)
   11.77 -
   11.78 -definition
   11.79 -  limP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
   11.80 -  "limP I M P = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i))
   11.81 -    {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
   11.82 -    (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j))
   11.83 -    (\<lambda>(J, X). emeasure (P J) (Pi\<^sub>E J X))"
   11.84 -
   11.85 -abbreviation "lim\<^sub>P \<equiv> limP"
   11.86 -
   11.87 -lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)"
   11.88 -  by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure)
   11.89 -
   11.90 -lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)"
   11.91 -  by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure)
   11.92 -
   11.93 -lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\<Pi>\<^sub>M i\<in>I. M i) M'"
   11.94 -  unfolding measurable_def by auto
   11.95 -
   11.96 -lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\<Pi>\<^sub>M i\<in>I. M i)"
   11.97 -  unfolding measurable_def by auto
   11.98 -
   11.99  locale projective_family =
  11.100 -  fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
  11.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>
  11.102 -     (P H) (prod_emb H M J X) = (P J) X"
  11.103 -  assumes proj_prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
  11.104 -  assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
  11.105 -  assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
  11.106 +  fixes I :: "'i set" and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M :: "'i \<Rightarrow> 'a measure"
  11.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)"
  11.108 +  assumes prob_space_P: "\<And>J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> prob_space (P J)"
  11.109  begin
  11.110  
  11.111 -lemma emeasure_limP:
  11.112 -  assumes "finite J"
  11.113 -  assumes "J \<subseteq> I"
  11.114 -  assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)"
  11.115 -  shows "emeasure (limP J M P) (Pi\<^sub>E J A) = emeasure (P J) (Pi\<^sub>E J A)"
  11.116 -proof -
  11.117 -  have "Pi\<^sub>E J (restrict A J) \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))"
  11.118 -    using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast
  11.119 -  hence "emeasure (limP J M P) (Pi\<^sub>E J A) =
  11.120 -    emeasure (limP J M P) (prod_emb J M J (Pi\<^sub>E J A))"
  11.121 -    using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
  11.122 -  also have "\<dots> = emeasure (P J) (Pi\<^sub>E J A)"
  11.123 -  proof (rule emeasure_extend_measure_Pair[OF limP_def])
  11.124 -    show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
  11.125 -    show "countably_additive (sets (limP J M P)) (P J)" unfolding countably_additive_def
  11.126 -      by (auto simp: suminf_emeasure proj_sets[OF `finite J`])
  11.127 -    show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))"
  11.128 -      using assms by auto
  11.129 -    fix K and X::"'i \<Rightarrow> 'a set"
  11.130 -    show "prod_emb J M K (Pi\<^sub>E K X) \<in> Pow (\<Pi>\<^sub>E i\<in>J. space (M i))"
  11.131 -      by (auto simp: prod_emb_def)
  11.132 -    assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))"
  11.133 -    thus "emeasure (P J) (prod_emb J M K (Pi\<^sub>E K X)) = emeasure (P K) (Pi\<^sub>E K X)"
  11.134 -      using assms
  11.135 -      apply (cases "J = {}")
  11.136 -      apply (simp add: prod_emb_id)
  11.137 -      apply (fastforce simp add: intro!: projective sets_PiM_I_finite)
  11.138 -      done
  11.139 -  qed
  11.140 -  finally show ?thesis .
  11.141 -qed
  11.142 +lemma sets_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (P J) = sets (PiM J M)"
  11.143 +  by (subst P[of J J]) simp_all
  11.144 +
  11.145 +lemma space_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> space (P J) = space (PiM J M)"
  11.146 +  using sets_P by (rule sets_eq_imp_space_eq)
  11.147  
  11.148 -lemma limP_finite[simp]:
  11.149 -  assumes "finite J"
  11.150 -  assumes "J \<subseteq> I"
  11.151 -  shows "limP J M P = P J" (is "?P = _")
  11.152 -proof (rule measure_eqI_generator_eq)
  11.153 -  let ?J = "{Pi\<^sub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
  11.154 -  let ?\<Omega> = "(\<Pi>\<^sub>E k\<in>J. space (M k))"
  11.155 -  interpret prob_space "P J" using proj_prob_space `finite J` by simp
  11.156 -  show "emeasure ?P (\<Pi>\<^sub>E k\<in>J. space (M k)) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
  11.157 -  show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
  11.158 -    using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
  11.159 -  fix X assume "X \<in> ?J"
  11.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
  11.161 -  with `finite J` have "X \<in> sets (limP J M P)" by simp
  11.162 -  have emb_self: "prod_emb J M J (Pi\<^sub>E J E) = Pi\<^sub>E J E"
  11.163 -    using E sets.sets_into_space
  11.164 -    by (auto intro!: prod_emb_PiE_same_index)
  11.165 -  show "emeasure (limP J M P) X = emeasure (P J) X"
  11.166 -    unfolding X using E
  11.167 -    by (intro emeasure_limP assms) simp
  11.168 -qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE)
  11.169 +lemma not_empty_M: "i \<in> I \<Longrightarrow> space (M i) \<noteq> {}"
  11.170 +  using prob_space_P[THEN prob_space.not_empty] by (auto simp: space_PiM space_P)
  11.171  
  11.172 -lemma emeasure_fun_emb[simp]:
  11.173 -  assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
  11.174 -  shows "emeasure (limP L M P) (prod_emb L M J X) = emeasure (limP J M P) X"
  11.175 -  using assms
  11.176 -  by (subst limP_finite) (auto simp: limP_finite finite_subset projective)
  11.177 +lemma not_empty: "space (PiM I M) \<noteq> {}"
  11.178 +  by (simp add: not_empty_M)
  11.179  
  11.180  abbreviation
  11.181 -  "emb L K X \<equiv> prod_emb L M K X"
  11.182 +  "emb L K \<equiv> prod_emb L M K"
  11.183  
  11.184 -lemma prod_emb_injective:
  11.185 -  assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^sub>M J M)" "Y \<in> sets (Pi\<^sub>M J M)"
  11.186 -  assumes "emb L J X = emb L J Y"
  11.187 -  shows "X = Y"
  11.188 -proof (rule injective_vimage_restrict)
  11.189 +lemma emb_preserve_mono:
  11.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)"
  11.191 +  assumes "emb L J X \<subseteq> emb L J Y"
  11.192 +  shows "X \<subseteq> Y"
  11.193 +proof (rule vimage_restrict_preseve_mono)
  11.194    show "X \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))"
  11.195      using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
  11.196 -  have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
  11.197 -  proof
  11.198 -    fix i assume "i \<in> L"
  11.199 -    interpret prob_space "P {i}" using proj_prob_space by simp
  11.200 -    from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
  11.201 -  qed
  11.202 -  from bchoice[OF this]
  11.203 -  show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
  11.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))"
  11.205 -    using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
  11.206 +  show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}"
  11.207 +    using \<open>L \<subseteq> I\<close> by (auto simp add: not_empty_M space_PiM[symmetric])
  11.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))"
  11.209 +    using `prod_emb L M J X \<subseteq> prod_emb L M J Y` by (simp add: prod_emb_def)
  11.210  qed fact
  11.211  
  11.212 -definition generator :: "('i \<Rightarrow> 'a) set set" where
  11.213 -  "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^sub>M J M))"
  11.214 +lemma emb_injective:
  11.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)"
  11.216 +  shows "emb L J X = emb L J Y \<Longrightarrow> X = Y"
  11.217 +  by (intro antisym emb_preserve_mono[OF L X Y] emb_preserve_mono[OF L Y X]) auto
  11.218 +
  11.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"
  11.220 +  by (auto intro!: emeasure_distr_restrict[symmetric] simp: P sets_P)
  11.221  
  11.222 -lemma generatorI':
  11.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"
  11.224 -  unfolding generator_def by auto
  11.225 +inductive_set generator :: "('i \<Rightarrow> 'a) set set" where
  11.226 +  "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emb I J X \<in> generator"
  11.227 +
  11.228 +lemma algebra_generator: "algebra (space (PiM I M)) generator"
  11.229 +  unfolding algebra_iff_Int
  11.230 +proof (safe elim!: generator.cases)
  11.231 +  fix J X assume J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (PiM J M)"
  11.232 +
  11.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
  11.234 +    by (auto simp: prod_emb_def space_PiM)
  11.235  
  11.236 -lemma algebra_generator:
  11.237 -  assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G")
  11.238 -  unfolding algebra_def algebra_axioms_def ring_of_sets_iff
  11.239 -proof (intro conjI ballI)
  11.240 -  let ?G = generator
  11.241 -  show "?G \<subseteq> Pow ?\<Omega>"
  11.242 -    by (auto simp: generator_def prod_emb_def)
  11.243 -  from `I \<noteq> {}` obtain i where "i \<in> I" by auto
  11.244 -  then show "{} \<in> ?G"
  11.245 -    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
  11.246 -             simp: sigma_sets.Empty generator_def prod_emb_def)
  11.247 -  from `i \<in> I` show "?\<Omega> \<in> ?G"
  11.248 -    by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^sub>E {i} (\<lambda>i. space (M i))"]
  11.249 -             simp: generator_def prod_emb_def)
  11.250 -  fix A assume "A \<in> ?G"
  11.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"
  11.252 -    by (auto simp: generator_def)
  11.253 -  fix B assume "B \<in> ?G"
  11.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"
  11.255 -    by (auto simp: generator_def)
  11.256 -  let ?RA = "emb (JA \<union> JB) JA XA"
  11.257 -  let ?RB = "emb (JA \<union> JB) JB XB"
  11.258 -  have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)"
  11.259 -    using XA A XB B by auto
  11.260 -  show "A - B \<in> ?G" "A \<union> B \<in> ?G"
  11.261 -    unfolding * using XA XB by (safe intro!: generatorI') auto
  11.262 -qed
  11.263 +  have "emb I J (space (PiM J M) - X) \<in> generator"
  11.264 +    by (intro generator.intros J sets.Diff sets.top X)
  11.265 +  with J show "space (Pi\<^sub>M I M) - emb I J X \<in> generator"
  11.266 +    by (simp add: space_PiM prod_emb_PiE)
  11.267 +  
  11.268 +  fix K Y assume K: "finite K" "K \<subseteq> I" and Y: "Y \<in> sets (PiM K M)"
  11.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"
  11.270 +    unfolding prod_emb_Int[symmetric]
  11.271 +    by (intro generator.intros sets.Int measurable_prod_emb) (auto intro!: J K X Y)
  11.272 +  with J K X Y show "emb I J X \<inter> emb I K Y \<in> generator"
  11.273 +    by simp
  11.274 +qed (force simp: generator.simps prod_emb_empty[symmetric])
  11.275  
  11.276 -lemma sets_PiM_generator:
  11.277 -  "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) generator"
  11.278 -proof cases
  11.279 -  assume "I = {}" then show ?thesis
  11.280 -    unfolding generator_def
  11.281 -    by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong)
  11.282 -next
  11.283 -  assume "I \<noteq> {}"
  11.284 -  show ?thesis
  11.285 -  proof
  11.286 -    show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) generator"
  11.287 -      unfolding sets_PiM
  11.288 -    proof (safe intro!: sigma_sets_subseteq)
  11.289 -      fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
  11.290 -        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
  11.291 -    qed
  11.292 -  qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset)
  11.293 -qed
  11.294 +interpretation generator!: algebra "space (PiM I M)" generator
  11.295 +  by (rule algebra_generator)
  11.296  
  11.297 -lemma generatorI:
  11.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"
  11.299 -  unfolding generator_def by auto
  11.300 +lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
  11.301 +proof (intro antisym sets.sigma_sets_subset)
  11.302 +  show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) generator"
  11.303 +    unfolding sets_PiM_single space_PiM[symmetric]
  11.304 +  proof (intro sigma_sets_mono', safe)
  11.305 +    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
  11.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)"
  11.307 +      by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def)
  11.308 +    with \<open>i\<in>I\<close> A show "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} \<in> generator"
  11.309 +      by (auto intro!: generator.intros sets_PiM_I_finite)
  11.310 +  qed
  11.311 +qed (auto elim!: generator.cases)
  11.312  
  11.313  definition mu_G ("\<mu>G") where
  11.314 -  "\<mu>G A =
  11.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))"
  11.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))"
  11.317 +
  11.318 +definition lim :: "('i \<Rightarrow> 'a) measure" where
  11.319 +  "lim = extend_measure (space (PiM I M)) generator (\<lambda>x. x) \<mu>G"
  11.320 +
  11.321 +lemma space_lim[simp]: "space lim = space (PiM I M)"
  11.322 +  using generator.space_closed
  11.323 +  unfolding lim_def by (intro space_extend_measure) simp
  11.324 +
  11.325 +lemma sets_lim[simp, measurable]: "sets lim = sets (PiM I M)"
  11.326 +  using generator.space_closed by (simp add: lim_def sets_PiM_generator sets_extend_measure)
  11.327  
  11.328  lemma mu_G_spec:
  11.329 -  assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^sub>M J M)"
  11.330 -  shows "\<mu>G A = emeasure (limP J M P) X"
  11.331 +  assumes J: "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)"
  11.332 +  shows "\<mu>G (emb I J X) = emeasure (P J) X"
  11.333    unfolding mu_G_def
  11.334  proof (intro the_equality allI impI ballI)
  11.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)"
  11.336 -  have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)"
  11.337 -    using K J by (simp del: limP_finite)
  11.338 +  fix K Y assume K: "finite K" "K \<subseteq> I" "Y \<in> sets (Pi\<^sub>M K M)"
  11.339 +    and [simp]: "emb I J X = emb I K Y"
  11.340 +  have "emeasure (P K) Y = emeasure (P (K \<union> J)) (emb (K \<union> J) K Y)"
  11.341 +    using K J by (simp add: emeasure_P)
  11.342    also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
  11.343 -    using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
  11.344 -  also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X"
  11.345 -    using K J by (simp del: limP_finite)
  11.346 -  finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" ..
  11.347 +    using K J by (simp add: emb_injective[of "K \<union> J" I])
  11.348 +  also have "emeasure (P (K \<union> J)) (emb (K \<union> J) J X) = emeasure (P J) X"
  11.349 +    using K J by (subst emeasure_P) simp_all
  11.350 +  finally show "emeasure (P J) X = emeasure (P K) Y" ..
  11.351  qed (insert J, force)
  11.352  
  11.353 -lemma mu_G_eq:
  11.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"
  11.355 -  by (intro mu_G_spec) auto
  11.356 +lemma positive_mu_G: "positive generator \<mu>G"
  11.357 +proof -
  11.358 +  show ?thesis
  11.359 +  proof (safe intro!: positive_def[THEN iffD2])
  11.360 +    obtain J where "finite J" "J \<subseteq> I" by auto
  11.361 +    then have "\<mu>G (emb I J {}) = 0"
  11.362 +      by (subst mu_G_spec) auto
  11.363 +    then show "\<mu>G {} = 0" by simp
  11.364 +  qed (auto simp: mu_G_spec elim!: generator.cases)
  11.365 +qed
  11.366  
  11.367 -lemma generator_Ex:
  11.368 -  assumes *: "A \<in> generator"
  11.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"
  11.370 -proof -
  11.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)"
  11.372 -    unfolding generator_def by auto
  11.373 -  with mu_G_spec[OF this] show ?thesis by (auto simp del: limP_finite)
  11.374 +lemma additive_mu_G: "additive generator \<mu>G"
  11.375 +proof (safe intro!: additive_def[THEN iffD2] elim!: generator.cases)
  11.376 +  fix J X K Y assume J: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
  11.377 +    and K: "finite K" "K \<subseteq> I" "Y \<in> sets (PiM K M)"
  11.378 +    and "emb I J X \<inter> emb I K Y = {}"
  11.379 +  then have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
  11.380 +    by (intro emb_injective[of "J \<union> K" I _ "{}"]) (auto simp: sets.Int prod_emb_Int)
  11.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))"
  11.382 +    using J K by simp
  11.383 +  also have "\<dots> = emeasure (P (J \<union> K)) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
  11.384 +    using J K by (simp add: mu_G_spec sets.Un del: prod_emb_Un)
  11.385 +  also have "\<dots> = \<mu>G (emb I J X) + \<mu>G (emb I K Y)"
  11.386 +    using J K JK_disj by (simp add: plus_emeasure[symmetric] mu_G_spec emeasure_P sets_P)
  11.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)" .
  11.388  qed
  11.389  
  11.390 -lemma generatorE:
  11.391 -  assumes A: "A \<in> generator"
  11.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"
  11.393 -  using generator_Ex[OF A] by atomize_elim auto
  11.394 -
  11.395 -lemma merge_sets:
  11.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)"
  11.397 -  by simp
  11.398 -
  11.399 -lemma merge_emb:
  11.400 -  assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^sub>M J M)"
  11.401 -  shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^sub>M I M)) =
  11.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))"
  11.403 +lemma emeasure_lim:
  11.404 +  assumes JX: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
  11.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>
  11.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> {}"
  11.407 +  shows "emeasure lim (emb I J X) = P J X"
  11.408  proof -
  11.409 -  have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)"
  11.410 -    by (auto simp: restrict_def merge_def)
  11.411 -  have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)"
  11.412 -    by (auto simp: restrict_def merge_def)
  11.413 -  have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto
  11.414 -  have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
  11.415 -  have [simp]: "(K - J) \<inter> K = K - J" by auto
  11.416 -  from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
  11.417 -    by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
  11.418 -       auto
  11.419 -qed
  11.420 -
  11.421 -lemma positive_mu_G:
  11.422 -  assumes "I \<noteq> {}"
  11.423 -  shows "positive generator \<mu>G"
  11.424 -proof -
  11.425 -  interpret G!: algebra "\<Pi>\<^sub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
  11.426 +  have "\<exists>\<mu>. (\<forall>s\<in>generator. \<mu> s = \<mu>G s) \<and>
  11.427 +    measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \<mu>"
  11.428 +  proof (rule generator.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
  11.429 +    show "\<And>A. A \<in> generator \<Longrightarrow> \<mu>G A \<noteq> \<infinity>"
  11.430 +    proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI)
  11.431 +      fix J assume "finite J" "J \<subseteq> I"
  11.432 +      then interpret prob_space "P J" by (rule prob_space_P)
  11.433 +      show "\<And>X. X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emeasure (P J) X \<noteq> \<infinity>"
  11.434 +        by simp
  11.435 +    qed
  11.436 +  next
  11.437 +    fix A assume "range A \<subseteq> generator" and "decseq A" "(\<Inter>i. A i) = {}"
  11.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)"
  11.439 +      unfolding image_subset_iff generator.simps by blast
  11.440 +    then obtain J X where A: "\<And>i. A i = emb I (J i) (X i)"
  11.441 +      and *: "\<And>i. finite (J i)" "\<And>i. J i \<subseteq> I" "\<And>i. X i \<in> sets (PiM (J i) M)"
  11.442 +      by metis
  11.443 +    have "(INF i. P (J i) (X i)) = 0"
  11.444 +    proof (rule ccontr)
  11.445 +      assume INF_P: "(INF i. P (J i) (X i)) \<noteq> 0"
  11.446 +      have "(\<Inter>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i))) \<noteq> {}"
  11.447 +      proof (rule cont)
  11.448 +        show "decseq (\<lambda>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))"
  11.449 +          using * \<open>decseq A\<close> by (subst prod_emb_trans) (auto simp: A[abs_def])
  11.450 +        show "0 < (INF i. P (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))"
  11.451 +           using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest)
  11.452 +        show "incseq (\<lambda>i. \<Union>n\<le>i. J n)"
  11.453 +          by (force simp: incseq_def)
  11.454 +      qed (insert *, auto)
  11.455 +      with \<open>(\<Inter>i. A i) = {}\<close> * show False
  11.456 +        by (subst (asm) prod_emb_trans) (auto simp: A[abs_def])
  11.457 +    qed
  11.458 +    moreover have "(\<lambda>i. P (J i) (X i)) ----> (INF i. P (J i) (X i))"
  11.459 +    proof (intro LIMSEQ_INF antimonoI)
  11.460 +      fix x y :: nat assume "x \<le> y"
  11.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))"
  11.462 +        using \<open>decseq A\<close>[THEN decseqD, OF \<open>x\<le>y\<close>] *
  11.463 +        by (auto simp: A sets_P del: subsetI intro!: emeasure_mono  \<open>x \<le> y\<close>
  11.464 +              emb_preserve_mono[of "J y \<union> J x" I, where X="emb (J y \<union> J x) (J y) (X y)"])
  11.465 +      then show "P (J y) (X y) \<le> P (J x) (X x)"
  11.466 +        using * by (simp add: emeasure_P)
  11.467 +    qed
  11.468 +    ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
  11.469 +      by (auto simp: A[abs_def] mu_G_spec *)
  11.470 +  qed
  11.471 +  then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s"
  11.472 +    and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \<mu>"
  11.473 +    by (metis sets_PiM_generator)
  11.474    show ?thesis
  11.475 -  proof (intro positive_def[THEN iffD2] conjI ballI)
  11.476 -    from generatorE[OF G.empty_sets] guess J X . note this[simp]
  11.477 -    have "X = {}"
  11.478 -      by (rule prod_emb_injective[of J I]) simp_all
  11.479 -    then show "\<mu>G {} = 0" by simp
  11.480 -  next
  11.481 -    fix A assume "A \<in> generator"
  11.482 -    from generatorE[OF this] guess J X . note this[simp]
  11.483 -    show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
  11.484 -  qed
  11.485 -qed
  11.486 -
  11.487 -lemma additive_mu_G:
  11.488 -  assumes "I \<noteq> {}"
  11.489 -  shows "additive generator \<mu>G"
  11.490 -proof -
  11.491 -  interpret G!: algebra "\<Pi>\<^sub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact
  11.492 -  show ?thesis
  11.493 -  proof (intro additive_def[THEN iffD2] ballI impI)
  11.494 -    fix A assume "A \<in> generator" with generatorE guess J X . note J = this
  11.495 -    fix B assume "B \<in> generator" with generatorE guess K Y . note K = this
  11.496 -    assume "A \<inter> B = {}"
  11.497 -    have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
  11.498 -      using J K by auto
  11.499 -    have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
  11.500 -      apply (rule prod_emb_injective[of "J \<union> K" I])
  11.501 -      apply (insert `A \<inter> B = {}` JK J K)
  11.502 -      apply (simp_all add: sets.Int prod_emb_Int)
  11.503 -      done
  11.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)"
  11.505 -      using J K by simp_all
  11.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))"
  11.507 -      by simp
  11.508 -    also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
  11.509 -      using JK J(1, 4) K(1, 4) by (simp add: mu_G_eq sets.Un del: prod_emb_Un)
  11.510 -    also have "\<dots> = \<mu>G A + \<mu>G B"
  11.511 -      using J K JK_disj by (simp add: plus_emeasure[symmetric] del: limP_finite)
  11.512 -    finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
  11.513 +  proof (subst emeasure_extend_measure[OF lim_def])
  11.514 +    show "A \<in> generator \<Longrightarrow> \<mu> A = \<mu>G A" for A
  11.515 +      using eq by simp
  11.516 +    show "positive (sets lim) \<mu>" "countably_additive (sets lim) \<mu>"
  11.517 +      using ms by (auto simp add: measure_space_def)
  11.518 +    show "(\<lambda>x. x) ` generator \<subseteq> Pow (space (Pi\<^sub>M I M))"
  11.519 +      using generator.space_closed by simp
  11.520 +    show "emb I J X \<in> generator" "\<mu>G (emb I J X) = emeasure (P J) X"
  11.521 +      using JX by (auto intro: generator.intros simp: mu_G_spec)
  11.522    qed
  11.523  qed
  11.524  
  11.525  end
  11.526  
  11.527  sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
  11.528 -proof (simp add: projective_family_def, safe)
  11.529 -  fix J::"'i set" assume [simp]: "finite J"
  11.530 -  interpret f: finite_product_prob_space M J proof qed fact
  11.531 -  show "prob_space (Pi\<^sub>M J M)"
  11.532 -  proof
  11.533 -    show "emeasure (Pi\<^sub>M J M) (space (Pi\<^sub>M J M)) = 1"
  11.534 -      by (simp add: space_PiM emeasure_PiM emeasure_space_1)
  11.535 +  unfolding projective_family_def
  11.536 +proof (intro conjI allI impI distr_restrict)
  11.537 +  show "\<And>J. finite J \<Longrightarrow> prob_space (Pi\<^sub>M J M)"
  11.538 +    by (intro prob_spaceI) (simp add: space_PiM emeasure_PiM emeasure_space_1)
  11.539 +qed auto
  11.540 +
  11.541 +
  11.542 +txt \<open> Proof due to Ionescu Tulcea. \<close>
  11.543 +
  11.544 +locale Ionescu_Tulcea =
  11.545 +  fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a measure" and M :: "nat \<Rightarrow> 'a measure"
  11.546 +  assumes P[measurable]: "\<And>i. P i \<in> measurable (PiM {0..<i} M) (subprob_algebra (M i))"
  11.547 +  assumes prob_space_P: "\<And>i x. x \<in> space (PiM {0..<i} M) \<Longrightarrow> prob_space (P i x)"
  11.548 +begin
  11.549 +
  11.550 +lemma non_empty[simp]: "space (M i) \<noteq> {}"
  11.551 +proof (induction i rule: less_induct)
  11.552 +  case (less i)
  11.553 +  then obtain x where "\<And>j. j < i \<Longrightarrow> x j \<in> space (M j)"
  11.554 +    unfolding ex_in_conv[symmetric] by metis
  11.555 +  then have *: "restrict x {0..<i} \<in> space (PiM {0..<i} M)"
  11.556 +    by (auto simp: space_PiM PiE_iff)
  11.557 +  then interpret prob_space "P i (restrict x {0..<i})"
  11.558 +    by (rule prob_space_P)
  11.559 +  show ?case
  11.560 +    using not_empty subprob_measurableD(1)[OF P, OF *] by simp
  11.561 +qed
  11.562 +
  11.563 +lemma space_PiM_not_empty[simp]: "space (PiM UNIV M) \<noteq> {}"
  11.564 +  unfolding space_PiM_empty_iff by auto
  11.565 +
  11.566 +lemma space_P: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (P n x) = space (M n)"
  11.567 +  by (simp add: P[THEN subprob_measurableD(1)])
  11.568 +
  11.569 +lemma sets_P[measurable_cong]: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (P n x) = sets (M n)"
  11.570 +  by (simp add: P[THEN subprob_measurableD(2)])
  11.571 +
  11.572 +definition eP :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
  11.573 +  "eP n \<omega> = distr (P n \<omega>) (PiM {0..<Suc n} M) (fun_upd \<omega> n)"
  11.574 +
  11.575 +lemma measurable_eP[measurable]:
  11.576 +  "eP n \<in> measurable (PiM {0..< n} M) (subprob_algebra (PiM {0..<Suc n} M))"
  11.577 +  by (auto simp: eP_def[abs_def] measurable_split_conv
  11.578 +           intro!: measurable_fun_upd[where J="{0..<n}"] measurable_distr2[OF _ P])
  11.579 +
  11.580 +lemma space_eP:
  11.581 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (eP n x) = space (PiM {0..<Suc n} M)"
  11.582 +  by (simp add: measurable_eP[THEN subprob_measurableD(1)])
  11.583 +
  11.584 +lemma sets_eP[measurable]:
  11.585 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (eP n x) = sets (PiM {0..<Suc n} M)"
  11.586 +  by (simp add: measurable_eP[THEN subprob_measurableD(2)])
  11.587 +
  11.588 +lemma prob_space_eP: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (eP n x)"
  11.589 +  unfolding eP_def
  11.590 +  by (intro prob_space.prob_space_distr prob_space_P measurable_fun_upd[where J="{0..<n}"]) auto
  11.591 +
  11.592 +lemma nn_integral_eP:
  11.593 +  "\<omega> \<in> space (PiM {0..<n} M) \<Longrightarrow> f \<in> borel_measurable (PiM {0..<Suc n} M) \<Longrightarrow>
  11.594 +    (\<integral>\<^sup>+x. f x \<partial>eP n \<omega>) = (\<integral>\<^sup>+x. f (\<omega>(n := x)) \<partial>P n \<omega>)"
  11.595 +  unfolding eP_def
  11.596 +  by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..<n}"] simp: space_PiM PiE_iff)
  11.597 +
  11.598 +lemma emeasure_eP:
  11.599 +  assumes \<omega>[simp]: "\<omega> \<in> space (PiM {0..<n} M)" and A[measurable]: "A \<in> sets (PiM {0..<Suc n} M)"
  11.600 +  shows "eP n \<omega> A = P n \<omega> ((\<lambda>x. \<omega>(n := x)) -` A \<inter> space (M n))"
  11.601 +  using nn_integral_eP[of \<omega> n "indicator A"]
  11.602 +  apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator)
  11.603 +  apply (subst nn_integral_indicator[symmetric])
  11.604 +  using measurable_sets[OF measurable_fun_upd[OF _ measurable_const[OF \<omega>] measurable_id] A, of n]
  11.605 +  apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator
  11.606 +     intro!: nn_integral_cong split: split_indicator)
  11.607 +  done
  11.608 +  
  11.609 +
  11.610 +primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
  11.611 +  "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>"
  11.612 +| "C n (Suc m) \<omega> = C n m \<omega> \<guillemotright>= eP (n + m)"
  11.613 +
  11.614 +lemma measurable_C[measurable]:
  11.615 +  "C n m \<in> measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))"
  11.616 +  by (induction m) auto
  11.617 +
  11.618 +lemma space_C:
  11.619 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (C n m x) = space (PiM {0..<n + m} M)"
  11.620 +  by (simp add: measurable_C[THEN subprob_measurableD(1)])
  11.621 +
  11.622 +lemma sets_C[measurable_cong]:
  11.623 +  "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (C n m x) = sets (PiM {0..<n + m} M)"
  11.624 +  by (simp add: measurable_C[THEN subprob_measurableD(2)])
  11.625 +
  11.626 +lemma prob_space_C: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (C n m x)"
  11.627 +proof (induction m)
  11.628 +  case (Suc m) then show ?case
  11.629 +    by (auto intro!: prob_space.prob_space_bind[where S="PiM {0..<Suc (n + m)} M"]
  11.630 +             simp: space_C prob_space_eP)
  11.631 +qed (auto intro!: prob_space_return simp: space_PiM)
  11.632 +
  11.633 +lemma split_C:
  11.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>"
  11.635 +proof (induction l)
  11.636 +  case 0
  11.637 +  with \<omega> show ?case
  11.638 +    by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty]
  11.639 +                  distr_cong[OF refl sets_C[symmetric, OF \<omega>]])
  11.640 +next
  11.641 +  case (Suc l) with \<omega> show ?case
  11.642 +    by (simp add: bind_assoc[symmetric, OF _ measurable_eP]) (simp add: ac_simps)
  11.643 +qed
  11.644 +
  11.645 +lemma nn_integral_C:
  11.646 +  assumes "m \<le> m'" and f[measurable]: "f \<in> borel_measurable (PiM {0..<n+m} M)"
  11.647 +    and nonneg: "\<And>x. x \<in> space (PiM {0..<n+m} M) \<Longrightarrow> 0 \<le> f x"
  11.648 +    and x: "x \<in> space (PiM {0..<n} M)"
  11.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)"
  11.650 +  using \<open>m \<le> m'\<close>
  11.651 +proof (induction rule: dec_induct)
  11.652 +  case (step i)
  11.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"
  11.654 +  from \<open>m\<le>i\<close> x have "?C i ?E = ?C (Suc i) ?E"
  11.655 +    by (auto simp: nn_integral_bind[where B="PiM {0 ..< Suc (n + i)} M"] space_C nn_integral_eP
  11.656 +             intro!: nn_integral_cong)
  11.657 +       (simp add: space_PiM PiE_iff  nonneg prob_space.emeasure_space_1[OF prob_space_P])
  11.658 +  with step show ?case by (simp del: restrict_apply)
  11.659 +qed (auto simp: space_PiM space_C[OF x] simp del: restrict_apply intro!: nn_integral_cong)
  11.660 +
  11.661 +lemma emeasure_C:
  11.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)"
  11.663 +  shows "emeasure (C n m' x) (prod_emb {0..<n + m'} M {0..<n+m} A) = emeasure (C n m x) A"
  11.664 +  using assms
  11.665 +  by (subst (1 2) nn_integral_indicator[symmetric])
  11.666 +     (auto intro!: nn_integral_cong split: split_indicator simp del: nn_integral_indicator
  11.667 +           simp: nn_integral_C[of m m' _ n] prod_emb_iff space_PiM PiE_iff sets_C space_C)
  11.668 +
  11.669 +lemma distr_C:
  11.670 +  assumes "m \<le> m'" and [simp]: "x \<in> space (PiM {0..<n} M)"
  11.671 +  shows "C n m x = distr (C n m' x) (PiM {0..<n+m} M) (\<lambda>x. restrict x {0..<n+m})"
  11.672 +proof (rule measure_eqI)
  11.673 +  fix A assume "A \<in> sets (C n m x)"
  11.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"
  11.675 +    by (subst emeasure_C[symmetric, OF \<open>m \<le> m'\<close>]) (auto intro!: emeasure_distr_restrict[symmetric] simp: sets_C)
  11.676 +qed (simp add: sets_C)
  11.677 +
  11.678 +definition up_to :: "nat set \<Rightarrow> nat" where
  11.679 +  "up_to J = (LEAST n. \<forall>i\<ge>n. i \<notin> J)"
  11.680 +
  11.681 +lemma up_to_less: "finite J \<Longrightarrow> i \<in> J \<Longrightarrow> i < up_to J"
  11.682 +  unfolding up_to_def
  11.683 +  by (rule LeastI2[of _ "Suc (Max J)"]) (auto simp: Suc_le_eq not_le[symmetric])
  11.684 +
  11.685 +lemma up_to_iff: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> (\<forall>i\<in>J. i < n)"
  11.686 +proof safe
  11.687 +  show "finite J \<Longrightarrow> up_to J \<le> n \<Longrightarrow> i \<in> J \<Longrightarrow> i < n" for i
  11.688 +    using up_to_less[of J i] by auto
  11.689 +qed (auto simp: up_to_def intro!: Least_le)
  11.690 +
  11.691 +lemma up_to_iff_Ico: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> J \<subseteq> {0..<n}"
  11.692 +  by (auto simp: up_to_iff)
  11.693 +
  11.694 +lemma up_to: "finite J \<Longrightarrow> J \<subseteq> {0..< up_to J}"
  11.695 +  by (auto simp: up_to_less)
  11.696 +
  11.697 +lemma up_to_mono: "J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> up_to J \<le> up_to H"
  11.698 +  by (auto simp add: up_to_iff finite_subset up_to_less)
  11.699 +
  11.700 +definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
  11.701 +  "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)"
  11.702 +
  11.703 +sublocale PF!: projective_family UNIV CI
  11.704 +  unfolding projective_family_def
  11.705 +proof safe
  11.706 +  show "finite J \<Longrightarrow> prob_space (CI J)" for J
  11.707 +    using up_to[of J] unfolding CI_def
  11.708 +    by (intro prob_space.prob_space_distr prob_space_C measurable_restrict) auto
  11.709 +  note measurable_cong_sets[OF sets_C, simp]
  11.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
  11.711 +    by (auto intro!: measurable_restrict)
  11.712 +
  11.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
  11.714 +    by (simp add: CI_def distr_C[OF up_to_mono[of J H]] up_to up_to_mono distr_distr comp_def
  11.715 +                  inf.absorb2 finite_subset)
  11.716 +qed
  11.717 +
  11.718 +lemma emeasure_CI':
  11.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)"
  11.720 +  unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C)
  11.721 +
  11.722 +lemma emeasure_CI:
  11.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)"
  11.724 +  apply (subst emeasure_CI', simp_all add: finite_subset)
  11.725 +  apply (subst emeasure_C[symmetric, of "up_to J" n])
  11.726 +  apply (auto simp: finite_subset up_to_iff_Ico up_to_less)
  11.727 +  apply (subst prod_emb_trans)
  11.728 +  apply (auto simp: up_to_less finite_subset up_to_iff_Ico)
  11.729 +  done
  11.730 +
  11.731 +lemma lim:
  11.732 +  assumes J: "finite J" and X: "X \<in> sets (PiM J M)"
  11.733 +  shows "emeasure PF.lim (PF.emb UNIV J X) = emeasure (CI J) X"
  11.734 +proof (rule PF.emeasure_lim[OF J subset_UNIV X])
  11.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)"
  11.736 +    and dec: "decseq (\<lambda>i. PF.emb UNIV (J i) (X' i))"
  11.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)"
  11.738 +
  11.739 +  have sets_X[measurable]: "X n \<in> sets (PiM {0..<n} M)" for n
  11.740 +    by (cases "{i. J i \<subseteq> {0..< n}} = {}")
  11.741 +       (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int)
  11.742 +  
  11.743 +  have dec_X: "n \<le> m \<Longrightarrow> X m \<subseteq> PF.emb {0..<m} {0..<n} (X n)" for n m
  11.744 +    unfolding X_def using ivl_subset[of 0 n 0 m]
  11.745 +    by (cases "{i. J i \<subseteq> {0..< n}} = {}")
  11.746 +       (auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset)
  11.747 +
  11.748 +  have dec_X': "PF.emb {0..<n} (J j) (X' j) \<subseteq> PF.emb {0..<n} (J i) (X' i)"
  11.749 +    if [simp]: "J i \<subseteq> {0..<n}" "J j \<subseteq> {0..<n}" "i \<le> j" for n i j
  11.750 +    by (rule PF.emb_preserve_mono[of "{0..<n}" UNIV]) (auto del: subsetI intro: dec[THEN antimonoD])
  11.751 +
  11.752 +  assume "0 < (INF i. CI (J i) (X' i))"
  11.753 +  also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))"
  11.754 +  proof (intro INF_greatest)
  11.755 +    fix n
  11.756 +    interpret C!: prob_space "C 0 n (\<lambda>x. undefined)"
  11.757 +      by (rule prob_space_C) simp
  11.758 +    show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)"
  11.759 +    proof cases
  11.760 +      assume "{i. J i \<subseteq> {0..< n}} = {}" with C.emeasure_space_1  show ?thesis
  11.761 +        by (auto simp add: X_def space_C intro!: INF_lower2[of 0] prob_space.measure_le_1 PF.prob_space_P)
  11.762 +    next
  11.763 +      assume *: "{i. J i \<subseteq> {0..< n}} \<noteq> {}"
  11.764 +      have "(INF i. CI (J i) (X' i)) \<le>
  11.765 +          (INF i:{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
  11.766 +        by (intro INF_superset_mono) (auto simp: emeasure_CI)
  11.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)))"
  11.768 +        using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
  11.769 +      also have "\<dots> = C 0 n (\<lambda>_. undefined) (X n)"
  11.770 +        using * by (auto simp add: X_def INT_extend_simps)
  11.771 +      finally show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>_. undefined) (X n)" .
  11.772 +    qed
  11.773    qed
  11.774 +  finally have pos: "0 < (INF i. C 0 i (\<lambda>x. undefined) (X i))" .
  11.775 +  from less_INF_D[OF this, of 0] have "X 0 \<noteq> {}"
  11.776 +    by auto
  11.777 +
  11.778 +  { fix \<omega> n assume \<omega>: "\<omega> \<in> space (PiM {0..<n} M)"
  11.779 +    let ?C = "\<lambda>i. emeasure (C n i \<omega>) (X (n + i))"
  11.780 +    let ?C' = "\<lambda>i x. emeasure (C (Suc n) i (\<omega>(n:=x))) (X (Suc n + i))"
  11.781 +    have M: "\<And>i. ?C' i \<in> borel_measurable (P n \<omega>)"
  11.782 +      using \<omega>[measurable, simp] measurable_fun_upd[where J="{0..<n}"] by measurable auto
  11.783 +
  11.784 +    assume "0 < (INF i. ?C i)"
  11.785 +    also have "\<dots> \<le> (INF i. emeasure (C n (1 + i) \<omega>) (X (n + (1 + i))))"
  11.786 +      by (intro INF_greatest INF_lower) auto
  11.787 +    also have "\<dots> = (INF i. \<integral>\<^sup>+x. ?C' i x \<partial>P n \<omega>)"
  11.788 +      using \<omega> measurable_C[of "Suc n"]
  11.789 +      apply (intro INF_cong refl)
  11.790 +      apply (subst split_C[symmetric, OF \<omega>])
  11.791 +      apply (subst emeasure_bind[OF _ _ sets_X])
  11.792 +      apply (simp_all del: C.simps add: space_C)
  11.793 +      apply measurable
  11.794 +      apply simp
  11.795 +      apply (simp add: bind_return[OF measurable_eP] nn_integral_eP)
  11.796 +      done
  11.797 +    also have "\<dots> = (\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>)"
  11.798 +    proof (rule nn_integral_monotone_convergence_INF[symmetric])
  11.799 +      have "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) \<le> (\<integral>\<^sup>+x. 1 \<partial>P n \<omega>)"
  11.800 +        by (intro nn_integral_mono) (auto split: split_indicator)
  11.801 +      also have "\<dots> < \<infinity>"
  11.802 +        using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp
  11.803 +      finally show "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) < \<infinity>" .
  11.804 +    next
  11.805 +      fix i j :: nat and x assume "i \<le> j" "x \<in> space (P n \<omega>)"
  11.806 +      with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)"
  11.807 +        by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
  11.808 +      show "?C' j x \<le> ?C' i x"
  11.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>')
  11.810 +    qed fact
  11.811 +    finally have "(\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>) \<noteq> 0"
  11.812 +      by simp
  11.813 +    then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). 0 < (INF i. ?C' i x)"
  11.814 +       using M by (subst (asm) nn_integral_0_iff_AE)
  11.815 +         (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le)
  11.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)"
  11.817 +      by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>)
  11.818 +    then obtain x where "x \<in> space (M n)" "0 < (INF i. ?C' i x)"
  11.819 +      by (auto dest: frequently_ex)
  11.820 +    from this(2)[THEN less_INF_D, of 0] this(2)
  11.821 +    have "\<exists>x. \<omega>(n := x) \<in> X (Suc n) \<and> 0 < (INF i. ?C' i x)"
  11.822 +      by (intro exI[of _ x]) (simp split: split_indicator_asm) }
  11.823 +  note step = this
  11.824 +
  11.825 +  let ?\<omega> = "\<lambda>\<omega> n x. (restrict \<omega> {0..<n})(n := x)"
  11.826 +  let ?L = "\<lambda>\<omega> n r. INF i. emeasure (C (Suc n) i (?\<omega> \<omega> n r)) (X (Suc n + i))"
  11.827 +  have *: "(\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i)) \<Longrightarrow>
  11.828 +    restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" for \<omega> n
  11.829 +    using sets.sets_into_space[OF sets_X, of n]
  11.830 +    by (cases n) (auto simp: atLeastLessThanSuc restrict_def[of _ "{}"])
  11.831 +  have "\<exists>\<omega>. \<forall>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n) \<and> 0 < ?L \<omega> n (\<omega> n)"
  11.832 +  proof (rule dependent_wellorder_choice)
  11.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)"
  11.834 +    show "\<exists>r. ?\<omega> \<omega> n r \<in> X (Suc n) \<and> 0 < ?L \<omega> n r"
  11.835 +    proof (rule step)
  11.836 +      show "restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)"
  11.837 +        using IH[THEN conjunct1] by (rule *)
  11.838 +      show "0 < (INF i. emeasure (C n i (restrict \<omega> {0..<n})) (X (n + i)))"
  11.839 +      proof (cases n)
  11.840 +        case 0 with pos show ?thesis
  11.841 +          by (simp add: CI_def restrict_def)
  11.842 +      next
  11.843 +        case (Suc i) then show ?thesis
  11.844 +          using IH[of i, THEN conjunct2] by (simp add: atLeastLessThanSuc)
  11.845 +      qed
  11.846 +    qed
  11.847 +  qed (simp cong: restrict_cong)
  11.848 +  then obtain \<omega> where \<omega>: "\<And>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n)"
  11.849 +    by auto
  11.850 +  from this[THEN *] have \<omega>_space: "\<omega> \<in> space (PiM UNIV M)"
  11.851 +    by (auto simp: space_PiM PiE_iff Ball_def)
  11.852 +  have *: "\<omega> \<in> PF.emb UNIV {0..<n} (X n)" for n
  11.853 +  proof (cases n)
  11.854 +    case 0 with \<omega>_space \<open>X 0 \<noteq> {}\<close> sets.sets_into_space[OF sets_X, of 0] show ?thesis
  11.855 +      by (auto simp add: space_PiM prod_emb_def restrict_def PiE_iff)
  11.856 +  next
  11.857 +    case (Suc i) then show ?thesis
  11.858 +      using \<omega>[of i] \<omega>_space by (auto simp: prod_emb_def space_PiM PiE_iff atLeastLessThanSuc)
  11.859 +  qed
  11.860 +  have **: "{i. J i \<subseteq> {0..<up_to (J n)}} \<noteq> {}" for n
  11.861 +    by (auto intro!: exI[of _ n] up_to J)
  11.862 +  have "\<omega> \<in> PF.emb UNIV (J n) (X' n)" for n
  11.863 +    using *[of "up_to (J n)"] up_to[of "J n"] by (simp add: X_def prod_emb_Int prod_emb_INT[OF **])
  11.864 +  then show "(\<Inter>i. PF.emb UNIV (J i) (X' i)) \<noteq> {}"
  11.865 +    by auto
  11.866 +qed
  11.867 +
  11.868 +lemma distr_lim: assumes J[simp]: "finite J" shows "distr PF.lim (PiM J M) (\<lambda>x. restrict x J) = CI J"
  11.869 +  apply (rule measure_eqI)
  11.870 +  apply (simp add: CI_def)
  11.871 +  apply (simp add: emeasure_distr measurable_cong_sets[OF PF.sets_lim] lim[symmetric] prod_emb_def space_PiM)
  11.872 +  done
  11.873 +
  11.874 +end
  11.875 +
  11.876 +lemma (in product_prob_space) emeasure_lim_emb:
  11.877 +  assumes *: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)"
  11.878 +  shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X"
  11.879 +proof (rule emeasure_lim[OF *], goal_cases)
  11.880 +  case (1 J X)
  11.881 +  
  11.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)"
  11.883 +  proof cases
  11.884 +    assume "finite (\<Union>i. J i)"
  11.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
  11.886 +      by (intro distr_restrict[symmetric]) auto
  11.887 +    then show ?thesis
  11.888 +      by auto
  11.889 +  next
  11.890 +    assume inf: "infinite (\<Union>i. J i)"
  11.891 +    moreover have count: "countable (\<Union>i. J i)"
  11.892 +      using 1(3) by (auto intro: countable_finite)
  11.893 +    def f \<equiv> "from_nat_into (\<Union>i. J i)" and t \<equiv> "to_nat_on (\<Union>i. J i)"
  11.894 +    have ft[simp]: "x \<in> J i \<Longrightarrow> f (t x) = x" for x i
  11.895 +      unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto
  11.896 +    have tf[simp]: "t (f i) = i" for i
  11.897 +      unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count)
  11.898 +    have inj_t: "inj_on t (\<Union>i. J i)"
  11.899 +      using count by (auto simp: t_def)
  11.900 +    then have inj_t_J: "inj_on t (J i)" for i
  11.901 +      by (rule subset_inj_on) auto
  11.902 +    interpret IT!: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
  11.903 +      by standard auto
  11.904 +    interpret Mf!: product_prob_space "\<lambda>x. M (f x)" UNIV
  11.905 +      by standard
  11.906 +    have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n
  11.907 +    proof (induction n)
  11.908 +      case 0 then show ?case
  11.909 +        by (auto simp: PiM_empty intro!: measure_eqI dest!: subset_singletonD)
  11.910 +    next
  11.911 +      case (Suc n) then show ?case
  11.912 +        apply (auto intro!: measure_eqI simp: sets_bind[OF IT.sets_eP] emeasure_bind[OF _ IT.measurable_eP])
  11.913 +        apply (auto simp: Mf.product_nn_integral_insert nn_integral_indicator[symmetric] atLeastLessThanSuc IT.emeasure_eP space_PiM
  11.914 +                    split: split_indicator simp del: nn_integral_indicator intro!: nn_integral_cong)
  11.915 +        done
  11.916 +    qed
  11.917 +    have CI_eq_PiM: "IT.CI X = PiM X (\<lambda>x. M (f x))" if X: "finite X" for X
  11.918 +      by (auto simp: IT.up_to_less X  IT.CI_def C_eq_PiM intro!: Mf.distr_restrict[symmetric])
  11.919 +
  11.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))"
  11.921 +    { fix i
  11.922 +      have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = 
  11.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)))"
  11.924 +      proof (subst distr_distr)
  11.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
  11.926 +          using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp
  11.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)"
  11.928 +          by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
  11.929 +      qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
  11.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))"
  11.931 +      proof (intro distr_distr[symmetric])
  11.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
  11.933 +          using measurable_component_singleton[of "t x" "t`J i" "\<lambda>x. M (f x)"] x unfolding ft[OF x] by auto
  11.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)"
  11.935 +          by (auto intro!: measurable_restrict)
  11.936 +      qed (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
  11.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))"
  11.938 +        using \<open>finite (J i)\<close> by (subst IT.distr_lim) (auto simp: CI_eq_PiM)
  11.939 +      also have "\<dots> = Pi\<^sub>M (J i) M"
  11.940 +        using Mf.distr_reorder[of t "J i"] by (simp add: 1 inj_t_J cong: PiM_cong)
  11.941 +      finally have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" . }
  11.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"
  11.943 +      by (intro exI[of _ ?Q]) auto
  11.944 +  qed
  11.945 +  then obtain Q where sets_Q: "sets Q = PiM (\<Union>i. J i) M"
  11.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
  11.947 +
  11.948 +  from 1 interpret Q: prob_space Q
  11.949 +    by (intro prob_space_distrD[of "\<lambda>x. restrict x (J 0)" Q "PiM (J 0) M"])
  11.950 +       (auto simp: Q measurable_cong_sets[OF sets_Q]
  11.951 +                intro!: prob_space_P measurable_restrict measurable_component_singleton)
  11.952 +
  11.953 +  have "0 < (INF i. emeasure (Pi\<^sub>M (J i) M) (X i))" by fact
  11.954 +  also have "\<dots> = (INF i. emeasure Q (emb (\<Union>i. J i) (J i) (X i)))"
  11.955 +    by (simp add: emeasure_distr_restrict[OF _ sets_Q 1(4), symmetric] SUP_upper Q)
  11.956 +  also have "\<dots> = emeasure Q (\<Inter>i. emb (\<Union>i. J i) (J i) (X i))"
  11.957 +  proof (rule INF_emeasure_decseq)
  11.958 +    from 1 show "decseq (\<lambda>n. emb (\<Union>i. J i) (J n) (X n))"
  11.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]
  11.960 +         measurable_prod_emb)
  11.961 +         (auto simp: SUP_least SUP_upper antimono_def)
  11.962 +  qed (insert 1, auto simp: sets_Q)
  11.963 +  finally have "(\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) \<noteq> {}"
  11.964 +    by auto
  11.965 +  moreover have "(\<Inter>i. emb I (J i) (X i)) = {} \<Longrightarrow> (\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) = {}"
  11.966 +    using 1 by (intro emb_injective[of "\<Union>i. J i" I _ "{}"] sets.countable_INT) (auto simp: SUP_least SUP_upper)
  11.967 +  ultimately show ?case by auto
  11.968  qed
  11.969  
  11.970  end
    12.1 --- a/src/HOL/Probability/Projective_Limit.thy	Wed Oct 07 15:31:59 2015 +0200
    12.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Wed Oct 07 17:11:16 2015 +0200
    12.3 @@ -101,440 +101,361 @@
    12.4    for I::"'i set" and P
    12.5  begin
    12.6  
    12.7 -abbreviation "lim\<^sub>B \<equiv> (\<lambda>J P. limP J (\<lambda>_. borel) P)"
    12.8 +lemma emeasure_lim_emb:
    12.9 +  assumes X: "J \<subseteq> I" "finite J" "X \<in> sets (\<Pi>\<^sub>M i\<in>J. borel)"
   12.10 +  shows "lim (emb I J X) = P J X"
   12.11 +proof (rule emeasure_lim)
   12.12 +  write mu_G ("\<mu>G")
   12.13 +  interpret generator: algebra "space (PiM I (\<lambda>i. borel))" generator
   12.14 +    by (rule algebra_generator)
   12.15 +
   12.16 +  fix J and B :: "nat \<Rightarrow> ('i \<Rightarrow> 'a) set"
   12.17 +  assume J: "\<And>n. finite (J n)" "\<And>n. J n \<subseteq> I" "\<And>n. B n \<in> sets (\<Pi>\<^sub>M i\<in>J n. borel)" "incseq J"
   12.18 +    and B: "decseq (\<lambda>n. emb I (J n) (B n))"
   12.19 +    and "0 < (INF i. P (J i) (B i))" (is "0 < ?a")
   12.20 +  moreover have "?a \<le> 1"
   12.21 +    using J by (auto intro!: INF_lower2[of 0] prob_space_P[THEN prob_space.measure_le_1])
   12.22 +  ultimately obtain r where r: "?a = ereal r" "0 < r" "r \<le> 1"
   12.23 +    by (cases "?a") auto
   12.24 +  def Z \<equiv> "\<lambda>n. emb I (J n) (B n)"
   12.25 +  have Z_mono: "n \<le> m \<Longrightarrow> Z m \<subseteq> Z n" for n m
   12.26 +    unfolding Z_def using B[THEN antimonoD, of n m] .
   12.27 +  have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"
   12.28 +    using \<open>incseq J\<close> by (force simp: incseq_def)
   12.29 +  note [simp] = \<open>\<And>n. finite (J n)\<close>
   12.30 +  interpret prob_space "P (J i)" for i using J prob_space_P by simp
   12.31 +
   12.32 +  have P_eq[simp]:
   12.33 +      "sets (P (J i)) = sets (\<Pi>\<^sub>M i\<in>J i. borel)" "space (P (J i)) = space (\<Pi>\<^sub>M i\<in>J i. borel)" for i
   12.34 +    using J by (auto simp: sets_P space_P)
   12.35 +
   12.36 +  have "Z i \<in> generator" for i
   12.37 +    unfolding Z_def by (auto intro!: generator.intros J)
   12.38  
   12.39 -lemma emeasure_limB_emb_not_empty:
   12.40 -  assumes "I \<noteq> {}"
   12.41 -  assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
   12.42 -  shows "emeasure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = emeasure (lim\<^sub>B J P) (Pi\<^sub>E J B)"
   12.43 -proof -
   12.44 -  let ?\<Omega> = "\<Pi>\<^sub>E i\<in>I. space borel"
   12.45 -  let ?G = generator
   12.46 -  interpret G!: algebra ?\<Omega> generator by (intro  algebra_generator) fact
   12.47 -  note mu_G_mono =
   12.48 -    G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`],
   12.49 -      THEN increasingD]
   12.50 -  write mu_G  ("\<mu>G")
   12.51 -
   12.52 -  have "\<exists>\<mu>. (\<forall>s\<in>?G. \<mu> s = \<mu>G s) \<and> measure_space ?\<Omega> (sigma_sets ?\<Omega> ?G) \<mu>"
   12.53 -  proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G,
   12.54 -      OF `I \<noteq> {}`, OF `I \<noteq> {}`])
   12.55 -    fix A assume "A \<in> ?G"
   12.56 -    with generatorE guess J X . note JX = this
   12.57 -    interpret prob_space "P J" using proj_prob_space[OF `finite J`] .
   12.58 -    show "\<mu>G A \<noteq> \<infinity>" using JX by (simp add: limP_finite)
   12.59 -  next
   12.60 -    fix Z assume Z: "range Z \<subseteq> ?G" "decseq Z" "(\<Inter>i. Z i) = {}"
   12.61 -    then have "decseq (\<lambda>i. \<mu>G (Z i))"
   12.62 -      by (auto intro!: mu_G_mono simp: decseq_def)
   12.63 -    moreover
   12.64 -    have "(INF i. \<mu>G (Z i)) = 0"
   12.65 +  have countable_UN_J: "countable (\<Union>n. J n)" by (simp add: countable_finite)
   12.66 +  def Utn \<equiv> "to_nat_on (\<Union>n. J n)"
   12.67 +  interpret function_to_finmap "J n" Utn "from_nat_into (\<Union>n. J n)" for n
   12.68 +    by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J])
   12.69 +  have inj_on_Utn: "inj_on Utn (\<Union>n. J n)"
   12.70 +    unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on)
   12.71 +  hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule subset_inj_on) auto
   12.72 +  def P' \<equiv> "\<lambda>n. mapmeasure n (P (J n)) (\<lambda>_. borel)"
   12.73 +  interpret P': prob_space "P' n" for n
   12.74 +    unfolding P'_def mapmeasure_def using J
   12.75 +    by (auto intro!: prob_space_distr fm_measurable simp: measurable_cong_sets[OF sets_P])
   12.76 +  
   12.77 +  let ?SUP = "\<lambda>n. SUP K : {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"
   12.78 +  { fix n
   12.79 +    have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))"
   12.80 +      using J by (auto simp: P'_def mapmeasure_PiM space_P sets_P)
   12.81 +    also
   12.82 +    have "\<dots> = ?SUP n"
   12.83 +    proof (rule inner_regular)
   12.84 +      show "sets (P' n) = sets borel" by (simp add: borel_eq_PiF_borel P'_def)
   12.85 +    next
   12.86 +      show "fm n ` B n \<in> sets borel"
   12.87 +        unfolding borel_eq_PiF_borel by (auto simp: P'_def fm_image_measurable_finite sets_P J(3))
   12.88 +    qed simp
   12.89 +    finally have "emeasure (P (J n)) (B n) = ?SUP n" "?SUP n \<noteq> \<infinity>" "?SUP n \<noteq> - \<infinity>" by auto
   12.90 +  } note R = this
   12.91 +  have "\<forall>n. \<exists>K. emeasure (P (J n)) (B n) - emeasure (P' n) K \<le> 2 powr (-n) * ?a \<and> compact K \<and> K \<subseteq> fm n ` B n"
   12.92 +  proof
   12.93 +    fix n show "\<exists>K. emeasure (P (J n)) (B n) - emeasure (P' n) K \<le> ereal (2 powr - real n) * ?a \<and>
   12.94 +        compact K \<and> K \<subseteq> fm n ` B n"
   12.95 +      unfolding R[of n]
   12.96      proof (rule ccontr)
   12.97 -      assume "(INF i. \<mu>G (Z i)) \<noteq> 0" (is "?a \<noteq> 0")
   12.98 -      moreover have "0 \<le> ?a"
   12.99 -        using Z positive_mu_G[OF `I \<noteq> {}`] by (auto intro!: INF_greatest simp: positive_def)
  12.100 -      ultimately have "0 < ?a" by auto
  12.101 -      hence "?a \<noteq> -\<infinity>" by auto
  12.102 -      have "\<forall>n. \<exists>J B. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> B \<in> sets (Pi\<^sub>M J (\<lambda>_. borel)) \<and>
  12.103 -        Z n = emb I J B \<and> \<mu>G (Z n) = emeasure (lim\<^sub>B J P) B"
  12.104 -        using Z by (intro allI generator_Ex) auto
  12.105 -      then obtain J' B' where J': "\<And>n. J' n \<noteq> {}" "\<And>n. finite (J' n)" "\<And>n. J' n \<subseteq> I"
  12.106 -          "\<And>n. B' n \<in> sets (\<Pi>\<^sub>M i\<in>J' n. borel)"
  12.107 -        and Z_emb: "\<And>n. Z n = emb I (J' n) (B' n)"
  12.108 -        unfolding choice_iff by blast
  12.109 -      moreover def J \<equiv> "\<lambda>n. (\<Union>i\<le>n. J' i)"
  12.110 -      moreover def B \<equiv> "\<lambda>n. emb (J n) (J' n) (B' n)"
  12.111 -      ultimately have J: "\<And>n. J n \<noteq> {}" "\<And>n. finite (J n)" "\<And>n. J n \<subseteq> I"
  12.112 -        "\<And>n. B n \<in> sets (\<Pi>\<^sub>M i\<in>J n. borel)"
  12.113 -        by auto
  12.114 -      have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"
  12.115 -        unfolding J_def by force
  12.116 -      have "\<forall>n. \<exists>j. j \<in> J n" using J by blast
  12.117 -      then obtain j where j: "\<And>n. j n \<in> J n"
  12.118 -        unfolding choice_iff by blast
  12.119 -      note [simp] = `\<And>n. finite (J n)`
  12.120 -      from J  Z_emb have Z_eq: "\<And>n. Z n = emb I (J n) (B n)" "\<And>n. Z n \<in> ?G"
  12.121 -        unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto)
  12.122 -      interpret prob_space "P (J i)" for i using proj_prob_space by simp
  12.123 -      have "?a \<le> \<mu>G (Z 0)" by (auto intro: INF_lower)
  12.124 -      also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq mu_G_eq limP_finite proj_sets)
  12.125 -      finally have "?a \<noteq> \<infinity>" by simp
  12.126 -      have "\<And>n. \<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>" unfolding Z_eq using J J_mono
  12.127 -        by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
  12.128 +      assume H: "\<not> (\<exists>K'. ?SUP n - emeasure (P' n) K' \<le> ereal (2 powr - real n)  * ?a \<and>
  12.129 +        compact K' \<and> K' \<subseteq> fm n ` B n)"
  12.130 +      have "?SUP n \<le> ?SUP n - 2 powr (-n) * ?a"
  12.131 +      proof (intro SUP_least)
  12.132 +        fix K
  12.133 +        assume "K \<in> {K. K \<subseteq> fm n ` B n \<and> compact K}"
  12.134 +        with H have "\<not> ?SUP n - emeasure (P' n) K \<le> 2 powr (-n) * ?a"
  12.135 +          by auto
  12.136 +        hence "?SUP n - emeasure (P' n) K > 2 powr (-n) * ?a"
  12.137 +          unfolding not_less[symmetric] by simp
  12.138 +        hence "?SUP n - 2 powr (-n) * ?a > emeasure (P' n) K"
  12.139 +          using `0 < ?a` by (auto simp add: ereal_less_minus_iff ac_simps)
  12.140 +        thus "?SUP n - 2 powr (-n) * ?a \<ge> emeasure (P' n) K" by simp
  12.141 +      qed
  12.142 +      hence "?SUP n + 0 \<le> ?SUP n - (2 powr (-n) * ?a)" using `0 < ?a` by simp
  12.143 +      hence "?SUP n + 0 \<le> ?SUP n + - (2 powr (-n) * ?a)" unfolding minus_ereal_def .
  12.144 +      hence "0 \<le> - (2 powr (-n) * ?a)"
  12.145 +        using `?SUP n \<noteq> \<infinity>` `?SUP n \<noteq> - \<infinity>`
  12.146 +        by (subst (asm) ereal_add_le_add_iff) (auto simp:)
  12.147 +      moreover have "ereal (2 powr - real n) * ?a > 0" using `0 < ?a`
  12.148 +        by (auto simp: ereal_zero_less_0_iff)
  12.149 +      ultimately show False by simp
  12.150 +    qed
  12.151 +  qed
  12.152 +  then obtain K' where K':
  12.153 +    "\<And>n. emeasure (P (J n)) (B n) - emeasure (P' n) (K' n) \<le> ereal (2 powr - real n) * ?a"
  12.154 +    "\<And>n. compact (K' n)" "\<And>n. K' n \<subseteq> fm n ` B n"
  12.155 +    unfolding choice_iff by blast
  12.156 +  def K \<equiv> "\<lambda>n. fm n -` K' n \<inter> space (Pi\<^sub>M (J n) (\<lambda>_. borel))"
  12.157 +  have K_sets: "\<And>n. K n \<in> sets (Pi\<^sub>M (J n) (\<lambda>_. borel))"
  12.158 +    unfolding K_def
  12.159 +    using compact_imp_closed[OF `compact (K' _)`]
  12.160 +    by (intro measurable_sets[OF fm_measurable, of _ "Collect finite"])
  12.161 +       (auto simp: borel_eq_PiF_borel[symmetric])
  12.162 +  have K_B: "\<And>n. K n \<subseteq> B n"
  12.163 +  proof
  12.164 +    fix x n assume "x \<in> K n"
  12.165 +    then have fm_in: "fm n x \<in> fm n ` B n"
  12.166 +      using K' by (force simp: K_def)
  12.167 +    show "x \<in> B n"
  12.168 +      using `x \<in> K n` K_sets sets.sets_into_space J(1,2,3)[of n]
  12.169 +      by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\<lambda>_. borel"]) auto
  12.170 +  qed
  12.171 +  def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"
  12.172 +  have Z': "\<And>n. Z' n \<subseteq> Z n"
  12.173 +    unfolding Z'_def Z_def
  12.174 +  proof (rule prod_emb_mono, safe)
  12.175 +    fix n x assume "x \<in> K n"
  12.176 +    hence "fm n x \<in> K' n" "x \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))"
  12.177 +      by (simp_all add: K_def space_P)
  12.178 +    note this(1)
  12.179 +    also have "K' n \<subseteq> fm n ` B n" by (simp add: K')
  12.180 +    finally have "fm n x \<in> fm n ` B n" .
  12.181 +    thus "x \<in> B n"
  12.182 +    proof safe
  12.183 +      fix y assume y: "y \<in> B n"
  12.184 +      hence "y \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
  12.185 +        by (auto simp add: space_P sets_P)
  12.186 +      assume "fm n x = fm n y"
  12.187 +      note inj_onD[OF inj_on_fm[OF space_borel],
  12.188 +        OF `fm n x = fm n y` `x \<in> space _` `y \<in> space _`]
  12.189 +      with y show "x \<in> B n" by simp
  12.190 +    qed
  12.191 +  qed
  12.192 +  have "\<And>n. Z' n \<in> generator" using J K'(2) unfolding Z'_def
  12.193 +    by (auto intro!: generator.intros measurable_sets[OF fm_measurable[of _ "Collect finite"]]
  12.194 +             simp: K_def borel_eq_PiF_borel[symmetric] compact_imp_closed)
  12.195 +  def Y \<equiv> "\<lambda>n. \<Inter>i\<in>{1..n}. Z' i"
  12.196 +  hence "\<And>n k. Y (n + k) \<subseteq> Y n" by (induct_tac k) (auto simp: Y_def)
  12.197 +  hence Y_mono: "\<And>n m. n \<le> m \<Longrightarrow> Y m \<subseteq> Y n" by (auto simp: le_iff_add)
  12.198 +  have Y_Z': "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z' n" by (auto simp: Y_def)
  12.199 +  hence Y_Z: "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z n" using Z' by auto
  12.200  
  12.201 -      have countable_UN_J: "countable (\<Union>n. J n)" by (simp add: countable_finite)
  12.202 -      def Utn \<equiv> "to_nat_on (\<Union>n. J n)"
  12.203 -      interpret function_to_finmap "J n" Utn "from_nat_into (\<Union>n. J n)" for n
  12.204 -        by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J])
  12.205 -      have inj_on_Utn: "inj_on Utn (\<Union>n. J n)"
  12.206 -        unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on)
  12.207 -      hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule subset_inj_on) auto
  12.208 -      def P' \<equiv> "\<lambda>n. mapmeasure n (P (J n)) (\<lambda>_. borel)"
  12.209 -      let ?SUP = "\<lambda>n. SUP K : {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"
  12.210 -      {
  12.211 -        fix n
  12.212 -        interpret finite_measure "P (J n)" by unfold_locales
  12.213 -        have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))"
  12.214 -          using J by (auto simp: P'_def mapmeasure_PiM proj_space proj_sets)
  12.215 -        also
  12.216 -        have "\<dots> = ?SUP n"
  12.217 -        proof (rule inner_regular)
  12.218 -          show "emeasure (P' n) (space (P' n)) \<noteq> \<infinity>"
  12.219 -            unfolding P'_def
  12.220 -            by (auto simp: P'_def mapmeasure_PiF fm_measurable proj_space proj_sets)
  12.221 -          show "sets (P' n) = sets borel" by (simp add: borel_eq_PiF_borel P'_def)
  12.222 -        next
  12.223 -          show "fm n ` B n \<in> sets borel"
  12.224 -            unfolding borel_eq_PiF_borel
  12.225 -            by (auto simp del: J(2) simp: P'_def fm_image_measurable_finite proj_sets J)
  12.226 -        qed
  12.227 -        finally
  12.228 -        have "emeasure (P (J n)) (B n) = ?SUP n" "?SUP n \<noteq> \<infinity>" "?SUP n \<noteq> - \<infinity>" by auto
  12.229 -      } note R = this
  12.230 -      have "\<forall>n. \<exists>K. emeasure (P (J n)) (B n) - emeasure (P' n) K \<le> 2 powr (-n) * ?a
  12.231 -        \<and> compact K \<and> K \<subseteq> fm n ` B n"
  12.232 -      proof
  12.233 -        fix n
  12.234 -        have "emeasure (P' n) (space (P' n)) \<noteq> \<infinity>"
  12.235 -          by (simp add: mapmeasure_PiF P'_def proj_space proj_sets)
  12.236 -        then interpret finite_measure "P' n" ..
  12.237 -        show "\<exists>K. emeasure (P (J n)) (B n) - emeasure (P' n) K \<le> ereal (2 powr - real n) * ?a \<and>
  12.238 -            compact K \<and> K \<subseteq> fm n ` B n"
  12.239 -          unfolding R
  12.240 -        proof (rule ccontr)
  12.241 -          assume H: "\<not> (\<exists>K'. ?SUP n - emeasure (P' n) K' \<le> ereal (2 powr - real n)  * ?a \<and>
  12.242 -            compact K' \<and> K' \<subseteq> fm n ` B n)"
  12.243 -          have "?SUP n \<le> ?SUP n - 2 powr (-n) * ?a"
  12.244 -          proof (intro SUP_least)
  12.245 -            fix K
  12.246 -            assume "K \<in> {K. K \<subseteq> fm n ` B n \<and> compact K}"
  12.247 -            with H have "\<not> ?SUP n - emeasure (P' n) K \<le> 2 powr (-n) * ?a"
  12.248 -              by auto
  12.249 -            hence "?SUP n - emeasure (P' n) K > 2 powr (-n) * ?a"
  12.250 -              unfolding not_less[symmetric] by simp
  12.251 -            hence "?SUP n - 2 powr (-n) * ?a > emeasure (P' n) K"
  12.252 -              using `0 < ?a` by (auto simp add: ereal_less_minus_iff ac_simps)
  12.253 -            thus "?SUP n - 2 powr (-n) * ?a \<ge> emeasure (P' n) K" by simp
  12.254 -          qed
  12.255 -          hence "?SUP n + 0 \<le> ?SUP n - (2 powr (-n) * ?a)" using `0 < ?a` by simp
  12.256 -          hence "?SUP n + 0 \<le> ?SUP n + - (2 powr (-n) * ?a)" unfolding minus_ereal_def .
  12.257 -          hence "0 \<le> - (2 powr (-n) * ?a)"
  12.258 -            using `?SUP _ \<noteq> \<infinity>` `?SUP _ \<noteq> - \<infinity>`
  12.259 -            by (subst (asm) ereal_add_le_add_iff) (auto simp:)
  12.260 -          moreover have "ereal (2 powr - real n) * ?a > 0" using `0 < ?a`
  12.261 -            by (auto simp: ereal_zero_less_0_iff)
  12.262 -          ultimately show False by simp
  12.263 -        qed
  12.264 -      qed
  12.265 -      then obtain K' where K':
  12.266 -        "\<And>n. emeasure (P (J n)) (B n) - emeasure (P' n) (K' n) \<le> ereal (2 powr - real n) * ?a"
  12.267 -        "\<And>n. compact (K' n)" "\<And>n. K' n \<subseteq> fm n ` B n"
  12.268 -        unfolding choice_iff by blast
  12.269 -      def K \<equiv> "\<lambda>n. fm n -` K' n \<inter> space (Pi\<^sub>M (J n) (\<lambda>_. borel))"
  12.270 -      have K_sets: "\<And>n. K n \<in> sets (Pi\<^sub>M (J n) (\<lambda>_. borel))"
  12.271 -        unfolding K_def
  12.272 -        using compact_imp_closed[OF `compact (K' _)`]
  12.273 -        by (intro measurable_sets[OF fm_measurable, of _ "Collect finite"])
  12.274 -           (auto simp: borel_eq_PiF_borel[symmetric])
  12.275 -      have K_B: "\<And>n. K n \<subseteq> B n"
  12.276 -      proof
  12.277 -        fix x n
  12.278 -        assume "x \<in> K n" hence fm_in: "fm n x \<in> fm n ` B n"
  12.279 -          using K' by (force simp: K_def)
  12.280 -        show "x \<in> B n"
  12.281 -          using `x \<in> K n` K_sets sets.sets_into_space J[of n]
  12.282 -          by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\<lambda>_. borel"]) auto
  12.283 -      qed
  12.284 -      def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"
  12.285 -      have Z': "\<And>n. Z' n \<subseteq> Z n"
  12.286 -        unfolding Z_eq unfolding Z'_def
  12.287 -      proof (rule prod_emb_mono, safe)
  12.288 -        fix n x assume "x \<in> K n"
  12.289 -        hence "fm n x \<in> K' n" "x \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))"
  12.290 -          by (simp_all add: K_def proj_space)
  12.291 -        note this(1)
  12.292 -        also have "K' n \<subseteq> fm n ` B n" by (simp add: K')
  12.293 -        finally have "fm n x \<in> fm n ` B n" .
  12.294 -        thus "x \<in> B n"
  12.295 -        proof safe
  12.296 -          fix y assume y: "y \<in> B n"
  12.297 -          hence "y \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
  12.298 -            by (auto simp add: proj_space proj_sets)
  12.299 -          assume "fm n x = fm n y"
  12.300 -          note inj_onD[OF inj_on_fm[OF space_borel],
  12.301 -            OF `fm n x = fm n y` `x \<in> space _` `y \<in> space _`]
  12.302 -          with y show "x \<in> B n" by simp
  12.303 +  have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}"
  12.304 +  proof -
  12.305 +    fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact
  12.306 +    have "Y n = (\<Inter>i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
  12.307 +      by (auto simp: Y_def Z'_def)
  12.308 +    also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. emb (J n) (J i) (K i))"
  12.309 +      using `n \<ge> 1`
  12.310 +      by (subst prod_emb_INT) auto
  12.311 +    finally
  12.312 +    have Y_emb:
  12.313 +      "Y n = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
  12.314 +    hence "Y n \<in> generator" using J J_mono K_sets `n \<ge> 1`
  12.315 +      by (auto simp del: prod_emb_INT intro!: generator.intros)
  12.316 +    have *: "\<mu>G (Z n) = P (J n) (B n)"
  12.317 +      unfolding Z_def using J by (intro mu_G_spec) auto
  12.318 +    then have "\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>" by auto
  12.319 +    note *
  12.320 +    moreover have *: "\<mu>G (Y n) = P (J n) (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))"
  12.321 +      unfolding Y_emb using J J_mono K_sets `n \<ge> 1` by (subst mu_G_spec) auto
  12.322 +    then have "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" by auto
  12.323 +    note *
  12.324 +    moreover have "\<mu>G (Z n - Y n) =
  12.325 +        P (J n) (B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"
  12.326 +      unfolding Z_def Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`
  12.327 +      by (subst mu_G_spec) (auto intro!: sets.Diff)
  12.328 +    ultimately
  12.329 +    have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
  12.330 +      using J J_mono K_sets `n \<ge> 1`
  12.331 +      by (simp only: emeasure_eq_measure Z_def)
  12.332 +        (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] set_mp[OF K_B]
  12.333 +          simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P)
  12.334 +    also have subs: "Z n - Y n \<subseteq> (\<Union>i\<in>{1..n}. (Z i - Z' i))"
  12.335 +      using `n \<ge> 1` unfolding Y_def UN_extend_simps(7) by (intro UN_mono Diff_mono Z_mono order_refl) auto
  12.336 +    have "Z n - Y n \<in> generator" "(\<Union>i\<in>{1..n}. (Z i - Z' i)) \<in> generator"
  12.337 +      using `Z' _ \<in> generator` `Z _ \<in> generator` `Y _ \<in> generator` by auto
  12.338 +    hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union>i\<in>{1..n}. (Z i - Z' i))"
  12.339 +      using subs generator.additive_increasing[OF positive_mu_G additive_mu_G]
  12.340 +      unfolding increasing_def by auto
  12.341 +    also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using `Z _ \<in> generator` `Z' _ \<in> generator`
  12.342 +      by (intro generator.subadditive[OF positive_mu_G additive_mu_G]) auto
  12.343 +    also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr -real i * ?a)"
  12.344 +    proof (rule setsum_mono)
  12.345 +      fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp
  12.346 +      have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))"
  12.347 +        unfolding Z'_def Z_def by simp
  12.348 +      also have "\<dots> = P (J i) (B i - K i)"
  12.349 +        using J K_sets by (subst mu_G_spec) auto
  12.350 +      also have "\<dots> = P (J i) (B i) - P (J i) (K i)"
  12.351 +        using K_sets J `K _ \<subseteq> B _` by (simp add: emeasure_Diff)
  12.352 +      also have "\<dots> = P (J i) (B i) - P' i (K' i)"
  12.353 +        unfolding K_def P'_def
  12.354 +        by (auto simp: mapmeasure_PiF borel_eq_PiF_borel[symmetric]
  12.355 +          compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def)
  12.356 +      also have "\<dots> \<le> ereal (2 powr - real i) * ?a" using K'(1)[of i] .
  12.357 +      finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" .
  12.358 +    qed
  12.359 +    also have "\<dots> = ereal ((\<Sum> i\<in>{1..n}. (2 powr -real i)) * real ?a)"
  12.360 +      by (simp add: setsum_left_distrib r)
  12.361 +    also have "\<dots> < ereal (1 * real ?a)" unfolding less_ereal.simps
  12.362 +    proof (rule mult_strict_right_mono)
  12.363 +      have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)"
  12.364 +        by (rule setsum.cong) (auto simp: powr_realpow powr_divide powr_minus_divide)  
  12.365 +      also have "{1..<Suc n} = {..<Suc n} - {0}" by auto
  12.366 +      also have "setsum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) =
  12.367 +        setsum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: setsum_diff1)
  12.368 +      also have "\<dots> < 1" by (subst geometric_sum) auto
  12.369 +      finally show "(\<Sum>i = 1..n. 2 powr - real i) < 1" .
  12.370 +    qed (auto simp: r ereal_less_real_iff zero_ereal_def[symmetric])
  12.371 +    also have "\<dots> = ?a" by (auto simp: r)
  12.372 +    also have "\<dots> \<le> \<mu>G (Z n)"
  12.373 +      using J by (auto intro: INF_lower simp: Z_def mu_G_spec)
  12.374 +    finally have "\<mu>G (Z n) - \<mu>G (Y n) < \<mu>G (Z n)" .
  12.375 +    hence R: "\<mu>G (Z n) < \<mu>G (Z n) + \<mu>G (Y n)"
  12.376 +      using `\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>` by (simp add: ereal_minus_less)
  12.377 +    have "0 \<le> (- \<mu>G (Z n)) + \<mu>G (Z n)" using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto
  12.378 +    also have "\<dots> < (- \<mu>G (Z n)) + (\<mu>G (Z n) + \<mu>G (Y n))"
  12.379 +      apply (rule ereal_less_add[OF _ R]) using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto
  12.380 +    finally have "\<mu>G (Y n) > 0"
  12.381 +      using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by (auto simp: ac_simps zero_ereal_def[symmetric])
  12.382 +    thus "Y n \<noteq> {}" using positive_mu_G by (auto simp add: positive_def)
  12.383 +  qed
  12.384 +  hence "\<forall>n\<in>{1..}. \<exists>y. y \<in> Y n" by auto
  12.385 +  then obtain y where y: "\<And>n. n \<ge> 1 \<Longrightarrow> y n \<in> Y n" unfolding bchoice_iff by force
  12.386 +  {
  12.387 +    fix t and n m::nat
  12.388 +    assume "1 \<le> n" "n \<le> m" hence "1 \<le> m" by simp
  12.389 +    from Y_mono[OF `m \<ge> n`] y[OF `1 \<le> m`] have "y m \<in> Y n" by auto
  12.390 +    also have "\<dots> \<subseteq> Z' n" using Y_Z'[OF `1 \<le> n`] .
  12.391 +    finally
  12.392 +    have "fm n (restrict (y m) (J n)) \<in> K' n"
  12.393 +      unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)
  12.394 +    moreover have "finmap_of (J n) (restrict (y m) (J n)) = finmap_of (J n) (y m)"
  12.395 +      using J by (simp add: fm_def)
  12.396 +    ultimately have "fm n (y m) \<in> K' n" by simp
  12.397 +  } note fm_in_K' = this
  12.398 +  interpret finmap_seqs_into_compact "\<lambda>n. K' (Suc n)" "\<lambda>k. fm (Suc k) (y (Suc k))" borel
  12.399 +  proof
  12.400 +    fix n show "compact (K' n)" by fact
  12.401 +  next
  12.402 +    fix n
  12.403 +    from Y_mono[of n "Suc n"] y[of "Suc n"] have "y (Suc n) \<in> Y (Suc n)" by auto
  12.404 +    also have "\<dots> \<subseteq> Z' (Suc n)" using Y_Z' by auto
  12.405 +    finally
  12.406 +    have "fm (Suc n) (restrict (y (Suc n)) (J (Suc n))) \<in> K' (Suc n)"
  12.407 +      unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)
  12.408 +    thus "K' (Suc n) \<noteq> {}" by auto
  12.409 +    fix k
  12.410 +    assume "k \<in> K' (Suc n)"
  12.411 +    with K'[of "Suc n"] sets.sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
  12.412 +    then obtain b where "k = fm (Suc n) b" by auto
  12.413 +    thus "domain k = domain (fm (Suc n) (y (Suc n)))"
  12.414 +      by (simp_all add: fm_def)
  12.415 +  next
  12.416 +    fix t and n m::nat
  12.417 +    assume "n \<le> m" hence "Suc n \<le> Suc m" by simp
  12.418 +    assume "t \<in> domain (fm (Suc n) (y (Suc n)))"
  12.419 +    then obtain j where j: "t = Utn j" "j \<in> J (Suc n)" by auto
  12.420 +    hence "j \<in> J (Suc m)" using J_mono[OF `Suc n \<le> Suc m`] by auto
  12.421 +    have img: "fm (Suc n) (y (Suc m)) \<in> K' (Suc n)" using `n \<le> m`
  12.422 +      by (intro fm_in_K') simp_all
  12.423 +    show "(fm (Suc m) (y (Suc m)))\<^sub>F t \<in> (\<lambda>k. (k)\<^sub>F t) ` K' (Suc n)"
  12.424 +      apply (rule image_eqI[OF _ img])
  12.425 +      using `j \<in> J (Suc n)` `j \<in> J (Suc m)`
  12.426 +      unfolding j by (subst proj_fm, auto)+
  12.427 +  qed
  12.428 +  have "\<forall>t. \<exists>z. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z"
  12.429 +    using diagonal_tendsto ..
  12.430 +  then obtain z where z:
  12.431 +    "\<And>t. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z t"
  12.432 +    unfolding choice_iff by blast
  12.433 +  {
  12.434 +    fix n :: nat assume "n \<ge> 1"
  12.435 +    have "\<And>i. domain (fm n (y (Suc (diagseq i)))) = domain (finmap_of (Utn ` J n) z)"
  12.436 +      by simp
  12.437 +    moreover
  12.438 +    {
  12.439 +      fix t
  12.440 +      assume t: "t \<in> domain (finmap_of (Utn ` J n) z)"
  12.441 +      hence "t \<in> Utn ` J n" by simp
  12.442 +      then obtain j where j: "t = Utn j" "j \<in> J n" by auto
  12.443 +      have "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> z t"
  12.444 +        apply (subst (2) tendsto_iff, subst eventually_sequentially)
  12.445 +      proof safe
  12.446 +        fix e :: real assume "0 < e"
  12.447 +        { fix i and x :: "'i \<Rightarrow> 'a" assume i: "i \<ge> n"
  12.448 +          assume "t \<in> domain (fm n x)"
  12.449 +          hence "t \<in> domain (fm i x)" using J_mono[OF `i \<ge> n`] by auto
  12.450 +          with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
  12.451 +            using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn])
  12.452 +        } note index_shift = this
  12.453 +        have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n"
  12.454 +          apply (rule le_SucI)
  12.455 +          apply (rule order_trans) apply simp
  12.456 +          apply (rule seq_suble[OF subseq_diagseq])
  12.457 +          done
  12.458 +        from z
  12.459 +        have "\<exists>N. \<forall>i\<ge>N. dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e"
  12.460 +          unfolding tendsto_iff eventually_sequentially using `0 < e` by auto
  12.461 +        then obtain N where N: "\<And>i. i \<ge> N \<Longrightarrow>
  12.462 +          dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" by auto
  12.463 +        show "\<exists>N. \<forall>na\<ge>N. dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e "
  12.464 +        proof (rule exI[where x="max N n"], safe)
  12.465 +          fix na assume "max N n \<le> na"
  12.466 +          hence  "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) =
  12.467 +                  dist ((fm (Suc (diagseq na)) (y (Suc (diagseq na))))\<^sub>F t) (z t)" using t
  12.468 +            by (subst index_shift[OF I]) auto
  12.469 +          also have "\<dots> < e" using `max N n \<le> na` by (intro N) simp
  12.470 +          finally show "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e" .
  12.471          qed
  12.472        qed
  12.473 -      { fix n
  12.474 -        have "Z' n \<in> ?G" using K' unfolding Z'_def
  12.475 -          apply (intro generatorI'[OF J(1-3)])
  12.476 -          unfolding K_def proj_space
  12.477 -          apply (rule measurable_sets[OF fm_measurable[of _ "Collect finite"]])
  12.478 -          apply (auto simp add: P'_def borel_eq_PiF_borel[symmetric] compact_imp_closed)
  12.479 -          done
  12.480 -      }
  12.481 -      def Y \<equiv> "\<lambda>n. \<Inter>i\<in>{1..n}. Z' i"
  12.482 -      hence "\<And>n k. Y (n + k) \<subseteq> Y n" by (induct_tac k) (auto simp: Y_def)
  12.483 -      hence Y_mono: "\<And>n m. n \<le> m \<Longrightarrow> Y m \<subseteq> Y n" by (auto simp: le_iff_add)
  12.484 -      have Y_Z': "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z' n" by (auto simp: Y_def)
  12.485 -      hence Y_Z: "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z n" using Z' by auto
  12.486 -      have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}"
  12.487 -      proof -
  12.488 -        fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact
  12.489 -        have "Y n = (\<Inter>i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
  12.490 -          by (auto simp: Y_def Z'_def)
  12.491 -        also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. emb (J n) (J i) (K i))"
  12.492 -          using `n \<ge> 1`
  12.493 -          by (subst prod_emb_INT) auto
  12.494 -        finally
  12.495 -        have Y_emb:
  12.496 -          "Y n = prod_emb I (\<lambda>_. borel) (J n)
  12.497 -            (\<Inter>i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
  12.498 -        hence "Y n \<in> ?G" using J J_mono K_sets `n \<ge> 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto
  12.499 -        hence "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" unfolding Y_emb using J J_mono K_sets `n \<ge> 1`
  12.500 -          by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
  12.501 -        interpret finite_measure "(limP (J n) (\<lambda>_. borel) P)"
  12.502 -        proof
  12.503 -          have "emeasure (limP (J n) (\<lambda>_. borel) P) (J n \<rightarrow>\<^sub>E space borel) \<noteq> \<infinity>"
  12.504 -            using J by (subst emeasure_limP) auto
  12.505 -          thus  "emeasure (limP (J n) (\<lambda>_. borel) P) (space (limP (J n) (\<lambda>_. borel) P)) \<noteq> \<infinity>"
  12.506 -             by (simp add: space_PiM)
  12.507 -        qed
  12.508 -        have "\<mu>G (Z n) = limP (J n) (\<lambda>_. borel) P (B n)"
  12.509 -          unfolding Z_eq using J by (auto simp: mu_G_eq)
  12.510 -        moreover have "\<mu>G (Y n) =
  12.511 -          limP (J n) (\<lambda>_. borel) P (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))"
  12.512 -          unfolding Y_emb using J J_mono K_sets `n \<ge> 1` by (subst mu_G_eq) auto
  12.513 -        moreover have "\<mu>G (Z n - Y n) = limP (J n) (\<lambda>_. borel) P
  12.514 -          (B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"
  12.515 -          unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`
  12.516 -          by (subst mu_G_eq) (auto intro!: sets.Diff)
  12.517 -        ultimately
  12.518 -        have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
  12.519 -          using J J_mono K_sets `n \<ge> 1`
  12.520 -          by (simp only: emeasure_eq_measure)
  12.521 -            (auto dest!: bspec[where x=n]
  12.522 -            simp: extensional_restrict emeasure_eq_measure prod_emb_iff simp del: limP_finite
  12.523 -            intro!: measure_Diff[symmetric] set_mp[OF K_B])
  12.524 -        also have subs: "Z n - Y n \<subseteq> (\<Union>i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
  12.525 -          unfolding Y_def by (force simp: decseq_def)
  12.526 -        have "Z n - Y n \<in> ?G" "(\<Union>i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
  12.527 -          using `Z' _ \<in> ?G` `Z _ \<in> ?G` `Y _ \<in> ?G` by auto
  12.528 -        hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union>i\<in>{1..n}. (Z i - Z' i))"
  12.529 -          using subs G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`]]
  12.530 -          unfolding increasing_def by auto
  12.531 -        also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using `Z _ \<in> ?G` `Z' _ \<in> ?G`
  12.532 -          by (intro G.subadditive[OF positive_mu_G additive_mu_G, OF `I \<noteq> {}` `I \<noteq> {}`]) auto
  12.533 -        also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr -real i * ?a)"
  12.534 -        proof (rule setsum_mono)
  12.535 -          fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp
  12.536 -          have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))"
  12.537 -            unfolding Z'_def Z_eq by simp
  12.538 -          also have "\<dots> = P (J i) (B i - K i)"
  12.539 -            using J K_sets by (subst mu_G_eq) auto
  12.540 -          also have "\<dots> = P (J i) (B i) - P (J i) (K i)"
  12.541 -            apply (subst emeasure_Diff) using K_sets J `K _ \<subseteq> B _` apply (auto simp: proj_sets)
  12.542 -            done
  12.543 -          also have "\<dots> = P (J i) (B i) - P' i (K' i)"
  12.544 -            unfolding K_def P'_def
  12.545 -            by (auto simp: mapmeasure_PiF proj_space proj_sets borel_eq_PiF_borel[symmetric]
  12.546 -              compact_imp_closed[OF `compact (K' _)`] space_PiM PiE_def)
  12.547 -          also have "\<dots> \<le> ereal (2 powr - real i) * ?a" using K'(1)[of i] .
  12.548 -          finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" .
  12.549 -        qed
  12.550 -        also have "\<dots> = (\<Sum> i\<in>{1..n}. ereal (2 powr -real i) * ereal(real ?a))"
  12.551 -          using `?a \<noteq> \<infinity>` `?a \<noteq> - \<infinity>` by (subst ereal_real') auto
  12.552 -        also have "\<dots> = ereal (\<Sum> i\<in>{1..n}. (2 powr -real i) * (real ?a))" by simp
  12.553 -        also have "\<dots> = ereal ((\<Sum> i\<in>{1..n}. (2 powr -real i)) * real ?a)"
  12.554 -          by (simp add: setsum_left_distrib)
  12.555 -        also have "\<dots> < ereal (1 * real ?a)" unfolding less_ereal.simps
  12.556 -        proof (rule mult_strict_right_mono)
  12.557 -          have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)"
  12.558 -            by (rule setsum.cong) (auto simp: powr_realpow powr_divide powr_minus_divide)  
  12.559 -          also have "{1..<Suc n} = {..<Suc n} - {0}" by auto
  12.560 -          also have "setsum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) =
  12.561 -            setsum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: setsum_diff1)
  12.562 -          also have "\<dots> < 1" by (subst geometric_sum) auto
  12.563 -          finally show "(\<Sum>i = 1..n. 2 powr - real i) < 1" .
  12.564 -        qed (auto simp:
  12.565 -          `0 < ?a` `?a \<noteq> \<infinity>` `?a \<noteq> - \<infinity>` ereal_less_real_iff zero_ereal_def[symmetric])
  12.566 -        also have "\<dots> = ?a" using `0 < ?a` `?a \<noteq> \<infinity>` by (auto simp: ereal_real')
  12.567 -        also have "\<dots> \<le> \<mu>G (Z n)" by (auto intro: INF_lower)
  12.568 -        finally have "\<mu>G (Z n) - \<mu>G (Y n) < \<mu>G (Z n)" .
  12.569 -        hence R: "\<mu>G (Z n) < \<mu>G (Z n) + \<mu>G (Y n)"
  12.570 -          using `\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>` by (simp add: ereal_minus_less)
  12.571 -        have "0 \<le> (- \<mu>G (Z n)) + \<mu>G (Z n)" using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto
  12.572 -        also have "\<dots> < (- \<mu>G (Z n)) + (\<mu>G (Z n) + \<mu>G (Y n))"
  12.573 -          apply (rule ereal_less_add[OF _ R]) using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto
  12.574 -        finally have "\<mu>G (Y n) > 0"
  12.575 -          using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by (auto simp: ac_simps zero_ereal_def[symmetric])
  12.576 -        thus "Y n \<noteq> {}" using positive_mu_G `I \<noteq> {}` by (auto simp add: positive_def)
  12.577 -      qed
  12.578 -      hence "\<forall>n\<in>{1..}. \<exists>y. y \<in> Y n" by auto
  12.579 -      then obtain y where y: "\<And>n. n \<ge> 1 \<Longrightarrow> y n \<in> Y n" unfolding bchoice_iff by force
  12.580 -      {
  12.581 -        fix t and n m::nat
  12.582 -        assume "1 \<le> n" "n \<le> m" hence "1 \<le> m" by simp
  12.583 -        from Y_mono[OF `m \<ge> n`] y[OF `1 \<le> m`] have "y m \<in> Y n" by auto
  12.584 -        also have "\<dots> \<subseteq> Z' n" using Y_Z'[OF `1 \<le> n`] .
  12.585 -        finally
  12.586 -        have "fm n (restrict (y m) (J n)) \<in> K' n"
  12.587 -          unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)
  12.588 -        moreover have "finmap_of (J n) (restrict (y m) (J n)) = finmap_of (J n) (y m)"
  12.589 -          using J by (simp add: fm_def)
  12.590 -        ultimately have "fm n (y m) \<in> K' n" by simp
  12.591 -      } note fm_in_K' = this
  12.592 -      interpret finmap_seqs_into_compact "\<lambda>n. K' (Suc n)" "\<lambda>k. fm (Suc k) (y (Suc k))" borel
  12.593 -      proof
  12.594 -        fix n show "compact (K' n)" by fact
  12.595 -      next
  12.596 -        fix n
  12.597 -        from Y_mono[of n "Suc n"] y[of "Suc n"] have "y (Suc n) \<in> Y (Suc n)" by auto
  12.598 -        also have "\<dots> \<subseteq> Z' (Suc n)" using Y_Z' by auto
  12.599 -        finally
  12.600 -        have "fm (Suc n) (restrict (y (Suc n)) (J (Suc n))) \<in> K' (Suc n)"
  12.601 -          unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)
  12.602 -        thus "K' (Suc n) \<noteq> {}" by auto
  12.603 -        fix k
  12.604 -        assume "k \<in> K' (Suc n)"
  12.605 -        with K'[of "Suc n"] sets.sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
  12.606 -        then obtain b where "k = fm (Suc n) b" by auto
  12.607 -        thus "domain k = domain (fm (Suc n) (y (Suc n)))"
  12.608 -          by (simp_all add: fm_def)
  12.609 -      next
  12.610 -        fix t and n m::nat
  12.611 -        assume "n \<le> m" hence "Suc n \<le> Suc m" by simp
  12.612 -        assume "t \<in> domain (fm (Suc n) (y (Suc n)))"
  12.613 -        then obtain j where j: "t = Utn j" "j \<in> J (Suc n)" by auto
  12.614 -        hence "j \<in> J (Suc m)" using J_mono[OF `Suc n \<le> Suc m`] by auto
  12.615 -        have img: "fm (Suc n) (y (Suc m)) \<in> K' (Suc n)" using `n \<le> m`
  12.616 -          by (intro fm_in_K') simp_all
  12.617 -        show "(fm (Suc m) (y (Suc m)))\<^sub>F t \<in> (\<lambda>k. (k)\<^sub>F t) ` K' (Suc n)"
  12.618 -          apply (rule image_eqI[OF _ img])
  12.619 -          using `j \<in> J (Suc n)` `j \<in> J (Suc m)`
  12.620 -          unfolding j by (subst proj_fm, auto)+
  12.621 -      qed
  12.622 -      have "\<forall>t. \<exists>z. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z"
  12.623 -        using diagonal_tendsto ..
  12.624 -      then obtain z where z:
  12.625 -        "\<And>t. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) ----> z t"
  12.626 -        unfolding choice_iff by blast
  12.627 -      {
  12.628 -        fix n :: nat assume "n \<ge> 1"
  12.629 -        have "\<And>i. domain (fm n (y (Suc (diagseq i)))) = domain (finmap_of (Utn ` J n) z)"
  12.630 -          by simp
  12.631 -        moreover
  12.632 -        {
  12.633 -          fix t
  12.634 -          assume t: "t \<in> domain (finmap_of (Utn ` J n) z)"
  12.635 -          hence "t \<in> Utn ` J n" by simp
  12.636 -          then obtain j where j: "t = Utn j" "j \<in> J n" by auto
  12.637 -          have "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> z t"
  12.638 -            apply (subst (2) tendsto_iff, subst eventually_sequentially)
  12.639 -          proof safe
  12.640 -            fix e :: real assume "0 < e"
  12.641 -            { fix i x
  12.642 -              assume i: "i \<ge> n"
  12.643 -              assume "t \<in> domain (fm n x)"
  12.644 -              hence "t \<in> domain (fm i x)" using J_mono[OF `i \<ge> n`] by auto
  12.645 -              with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
  12.646 -                using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn])
  12.647 -            } note index_shift = this
  12.648 -            have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n"
  12.649 -              apply (rule le_SucI)
  12.650 -              apply (rule order_trans) apply simp
  12.651 -              apply (rule seq_suble[OF subseq_diagseq])
  12.652 -              done
  12.653 -            from z
  12.654 -            have "\<exists>N. \<forall>i\<ge>N. dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e"
  12.655 -              unfolding tendsto_iff eventually_sequentially using `0 < e` by auto
  12.656 -            then obtain N where N: "\<And>i. i \<ge> N \<Longrightarrow>
  12.657 -              dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" by auto
  12.658 -            show "\<exists>N. \<forall>na\<ge>N. dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e "
  12.659 -            proof (rule exI[where x="max N n"], safe)
  12.660 -              fix na assume "max N n \<le> na"
  12.661 -              hence  "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) =
  12.662 -                      dist ((fm (Suc (diagseq na)) (y (Suc (diagseq na))))\<^sub>F t) (z t)" using t
  12.663 -                by (subst index_shift[OF I]) auto
  12.664 -              also have "\<dots> < e" using `max N n \<le> na` by (intro N) simp
  12.665 -              finally show "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e" .
  12.666 -            qed
  12.667 -          qed
  12.668 -          hence "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> (finmap_of (Utn ` J n) z)\<^sub>F t"
  12.669 -            by (simp add: tendsto_intros)
  12.670 -        } ultimately
  12.671 -        have "(\<lambda>i. fm n (y (Suc (diagseq i)))) ----> finmap_of (Utn ` J n) z"
  12.672 -          by (rule tendsto_finmap)
  12.673 -        hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) ----> finmap_of (Utn ` J n) z"
  12.674 -          by (intro lim_subseq) (simp add: subseq_def)
  12.675 -        moreover
  12.676 -        have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
  12.677 -          apply (auto simp add: o_def intro!: fm_in_K' `1 \<le> n` le_SucI)
  12.678 -          apply (rule le_trans)
  12.679 -          apply (rule le_add2)
  12.680 -          using seq_suble[OF subseq_diagseq]
  12.681 -          apply auto
  12.682 -          done
  12.683 -        moreover
  12.684 -        from `compact (K' n)` have "closed (K' n)" by (rule compact_imp_closed)
  12.685 -        ultimately
  12.686 -        have "finmap_of (Utn ` J n) z \<in> K' n"
  12.687 -          unfolding closed_sequential_limits by blast
  12.688 -        also have "finmap_of (Utn ` J n) z  = fm n (\<lambda>i. z (Utn i))"
  12.689 -          unfolding finmap_eq_iff
  12.690 -        proof clarsimp
  12.691 -          fix i assume i: "i \<in> J n"
  12.692 -          hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
  12.693 -            unfolding Utn_def
  12.694 -            by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto
  12.695 -          with i show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
  12.696 -            by (simp add: finmap_eq_iff fm_def compose_def)
  12.697 -        qed
  12.698 -        finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" .
  12.699 -        moreover
  12.700 -        let ?J = "\<Union>n. J n"
  12.701 -        have "(?J \<inter> J n) = J n" by auto
  12.702 -        ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n"
  12.703 -          unfolding K_def by (auto simp: proj_space space_PiM)
  12.704 -        hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def
  12.705 -          using J by (auto simp: prod_emb_def PiE_def extensional_def)
  12.706 -        also have "\<dots> \<subseteq> Z n" using Z' by simp
  12.707 -        finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" .
  12.708 -      } note in_Z = this
  12.709 -      hence "(\<Inter>i\<in>{1..}. Z i) \<noteq> {}" by auto
  12.710 -      hence "(\<Inter>i. Z i) \<noteq> {}" using Z INT_decseq_offset[OF `decseq Z`] by simp
  12.711 -      thus False using Z by simp
  12.712 +      hence "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) ----> (finmap_of (Utn ` J n) z)\<^sub>F t"
  12.713 +        by (simp add: tendsto_intros)
  12.714 +    } ultimately
  12.715 +    have "(\<lambda>i. fm n (y (Suc (diagseq i)))) ----> finmap_of (Utn ` J n) z"
  12.716 +      by (rule tendsto_finmap)
  12.717 +    hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) ----> finmap_of (Utn ` J n) z"
  12.718 +      by (intro lim_subseq) (simp add: subseq_def)
  12.719 +    moreover
  12.720 +    have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
  12.721 +      apply (auto simp add: o_def intro!: fm_in_K' `1 \<le> n` le_SucI)
  12.722 +      apply (rule le_trans)
  12.723 +      apply (rule le_add2)
  12.724 +      using seq_suble[OF subseq_diagseq]
  12.725 +      apply auto
  12.726 +      done
  12.727 +    moreover
  12.728 +    from `compact (K' n)` have "closed (K' n)" by (rule compact_imp_closed)
  12.729 +    ultimately
  12.730 +    have "finmap_of (Utn ` J n) z \<in> K' n"
  12.731 +      unfolding closed_sequential_limits by blast
  12.732 +    also have "finmap_of (Utn ` J n) z  = fm n (\<lambda>i. z (Utn i))"
  12.733 +      unfolding finmap_eq_iff
  12.734 +    proof clarsimp
  12.735 +      fix i assume i: "i \<in> J n"
  12.736 +      hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
  12.737 +        unfolding Utn_def
  12.738 +        by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto
  12.739 +      with i show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
  12.740 +        by (simp add: finmap_eq_iff fm_def compose_def)
  12.741      qed
  12.742 -    ultimately show "(\<lambda>i. \<mu>G (Z i)) ----> 0"
  12.743 -      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (Z i)"] by simp
  12.744 -  qed
  12.745 -  then guess \<mu> .. note \<mu> = this
  12.746 -  def f \<equiv> "finmap_of J B"
  12.747 -  show "emeasure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = emeasure (lim\<^sub>B J P) (Pi\<^sub>E J B)"
  12.748 -  proof (subst emeasure_extend_measure_Pair[OF limP_def, of I "\<lambda>_. borel" \<mu>])
  12.749 -    show "positive (sets (lim\<^sub>B I P)) \<mu>" "countably_additive (sets (lim\<^sub>B I P)) \<mu>"
  12.750 -      using \<mu> unfolding sets_limP sets_PiM_generator by (auto simp: measure_space_def)
  12.751 -  next
  12.752 -    show "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> B \<in> J \<rightarrow> sets borel"
  12.753 -      using assms by (auto simp: f_def)
  12.754 -  next
  12.755 -    fix J and X::"'i \<Rightarrow> 'a set"
  12.756 -    show "prod_emb I (\<lambda>_. borel) J (Pi\<^sub>E J X) \<in> Pow (I \<rightarrow>\<^sub>E space borel)"
  12.757 -      by (auto simp: prod_emb_def)
  12.758 -    assume JX: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> J \<rightarrow> sets borel"
  12.759 -    hence "emb I J (Pi\<^sub>E J X) \<in> generator" using assms
  12.760 -      by (intro generatorI[where J=J and X="Pi\<^sub>E J X"]) (auto intro: sets_PiM_I_finite)
  12.761 -    hence "\<mu> (emb I J (Pi\<^sub>E J X)) = \<mu>G (emb I J (Pi\<^sub>E J X))" using \<mu> by simp
  12.762 -    also have "\<dots> = emeasure (P J) (Pi\<^sub>E J X)"
  12.763 -      using JX assms proj_sets
  12.764 -      by (subst mu_G_eq) (auto simp: mu_G_eq limP_finite intro: sets_PiM_I_finite)
  12.765 -    finally show "\<mu> (emb I J (Pi\<^sub>E J X)) = emeasure (P J) (Pi\<^sub>E J X)" .
  12.766 -  next
  12.767 -    show "emeasure (P J) (Pi\<^sub>E J B) = emeasure (limP J (\<lambda>_. borel) P) (Pi\<^sub>E J B)"
  12.768 -      using assms by (simp add: f_def limP_finite Pi_def)
  12.769 -  qed
  12.770 -qed
  12.771 +    finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" .
  12.772 +    moreover
  12.773 +    let ?J = "\<Union>n. J n"
  12.774 +    have "(?J \<inter> J n) = J n" by auto
  12.775 +    ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n"
  12.776 +      unfolding K_def by (auto simp: space_P space_PiM)
  12.777 +    hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def
  12.778 +      using J by (auto simp: prod_emb_def PiE_def extensional_def)
  12.779 +    also have "\<dots> \<subseteq> Z n" using Z' by simp
  12.780 +    finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" .
  12.781 +  } note in_Z = this
  12.782 +  hence "(\<Inter>i\<in>{1..}. Z i) \<noteq> {}" by auto
  12.783 +  thus "(\<Inter>i. Z i) \<noteq> {}"
  12.784 +    using INT_decseq_offset[OF antimonoI[OF Z_mono]] by simp
  12.785 +qed fact+
  12.786 +
  12.787 +lemma measure_lim_emb:
  12.788 +  "J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> X \<in> sets (\<Pi>\<^sub>M i\<in>J. borel) \<Longrightarrow> measure lim (emb I J X) = measure (P J) X"
  12.789 +  unfolding measure_def by (subst emeasure_lim_emb) auto
  12.790  
  12.791  end
  12.792  
  12.793 @@ -548,70 +469,24 @@
  12.794  hide_const (open) domain
  12.795  hide_const (open) basis_finmap
  12.796  
  12.797 -sublocale polish_projective \<subseteq> P!: prob_space "(lim\<^sub>B I P)"
  12.798 +sublocale polish_projective \<subseteq> P!: prob_space lim
  12.799  proof
  12.800 -  show "emeasure (lim\<^sub>B I P) (space (lim\<^sub>B I P)) = 1"
  12.801 -  proof cases
  12.802 -    assume "I = {}"
  12.803 -    interpret prob_space "P {}" using proj_prob_space by simp
  12.804 -    show ?thesis
  12.805 -      by (simp add: space_PiM_empty limP_finite emeasure_space_1 `I = {}`)
  12.806 -  next
  12.807 -    assume "I \<noteq> {}"
  12.808 -    then obtain i where "i \<in> I" by auto
  12.809 -    interpret prob_space "P {i}" using proj_prob_space by simp
  12.810 -    have R: "(space (lim\<^sub>B I P)) = (emb I {i} (Pi\<^sub>E {i} (\<lambda>_. space borel)))"
  12.811 -      by (auto simp: prod_emb_def space_PiM)
  12.812 -    moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM PiE_def)
  12.813 -    ultimately show ?thesis using `i \<in> I`
  12.814 -      apply (subst R)
  12.815 -      apply (subst emeasure_limB_emb_not_empty)
  12.816 -      apply (auto simp: limP_finite emeasure_space_1 PiE_def)
  12.817 -      done
  12.818 -  qed
  12.819 +  have *: "emb I {} {\<lambda>x. undefined} = space (\<Pi>\<^sub>M i\<in>I. borel)"
  12.820 +    by (auto simp: prod_emb_def space_PiM)
  12.821 +  interpret prob_space "P {}" 
  12.822 +    using prob_space_P by simp
  12.823 +  show "emeasure lim (space lim) = 1"
  12.824 +    using emeasure_lim_emb[of "{}" "{\<lambda>x. undefined}"] emeasure_space_1
  12.825 +    by (simp add: * PiM_empty space_P)
  12.826  qed
  12.827  
  12.828 -context polish_projective begin
  12.829 -
  12.830 -lemma emeasure_limB_emb:
  12.831 -  assumes X: "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
  12.832 -  shows "emeasure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = emeasure (P J) (Pi\<^sub>E J B)"
  12.833 -proof cases
  12.834 -  interpret prob_space "P {}" using proj_prob_space by simp
  12.835 -  assume "J = {}"
  12.836 -  moreover have "emb I {} {\<lambda>x. undefined} = space (lim\<^sub>B I P)"
  12.837 -    by (auto simp: space_PiM prod_emb_def)
  12.838 -  moreover have "{\<lambda>x. undefined} = space (lim\<^sub>B {} P)"
  12.839 -    by (auto simp: space_PiM prod_emb_def simp del: limP_finite)
  12.840 -  ultimately show ?thesis
  12.841 -    by (simp add: P.emeasure_space_1 limP_finite emeasure_space_1 del: space_limP)
  12.842 -next
  12.843 -  assume "J \<noteq> {}" with X show ?thesis
  12.844 -    by (subst emeasure_limB_emb_not_empty) (auto simp: limP_finite)
  12.845 -qed
  12.846 -
  12.847 -lemma measure_limB_emb:
  12.848 -  assumes "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
  12.849 -  shows "measure (lim\<^sub>B I P) (emb I J (Pi\<^sub>E J B)) = measure (P J) (Pi\<^sub>E J B)"
  12.850 -proof -
  12.851 -  interpret prob_space "P J" using proj_prob_space assms by simp
  12.852 -  show ?thesis
  12.853 -    using emeasure_limB_emb[OF assms]
  12.854 -    unfolding emeasure_eq_measure limP_finite[OF `finite J` `J \<subseteq> I`] P.emeasure_eq_measure
  12.855 -    by simp
  12.856 -qed
  12.857 -
  12.858 -end
  12.859 -
  12.860  locale polish_product_prob_space =
  12.861    product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set"
  12.862  
  12.863  sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)"
  12.864  proof qed
  12.865  
  12.866 -lemma (in polish_product_prob_space) limP_eq_PiM:
  12.867 -  "I \<noteq> {} \<Longrightarrow> lim\<^sub>P I (\<lambda>_. borel) (\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)) =
  12.868 -    PiM I (\<lambda>_. borel)"
  12.869 -  by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb)
  12.870 +lemma (in polish_product_prob_space) limP_eq_PiM: "lim = PiM I (\<lambda>_. borel)"
  12.871 +  by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb)
  12.872  
  12.873  end