50091

1 
(* Title: HOL/Probability/Projective_Limit.thy

50088

2 
Author: Fabian Immler, TU München


3 
*)


4 


5 
header {* Projective Limit *}


6 


7 
theory Projective_Limit


8 
imports


9 
Caratheodory


10 
Fin_Map


11 
Regularity


12 
Projective_Family


13 
Infinite_Product_Measure


14 
begin


15 


16 
subsection {* Enumeration of Countable Union of Finite Sets *}


17 


18 
locale finite_set_sequence =


19 
fixes Js::"nat \<Rightarrow> 'a set"


20 
assumes finite_seq[simp]: "finite (Js n)"


21 
begin


22 


23 
text {* Enumerate finite set *}


24 


25 
definition "enum_finite_max J = (SOME n. \<exists> f. J = f ` {i. i < n} \<and> inj_on f {i. i < n})"


26 


27 
definition enum_finite where


28 
"enum_finite J =


29 
(SOME f. J = f ` {i::nat. i < enum_finite_max J} \<and> inj_on f {i. i < enum_finite_max J})"


30 


31 
lemma enum_finite_max:


32 
assumes "finite J"


33 
shows "\<exists>f::nat\<Rightarrow>_. J = f ` {i. i < enum_finite_max J} \<and> inj_on f {i. i < enum_finite_max J}"


34 
unfolding enum_finite_max_def


35 
by (rule someI_ex) (rule finite_imp_nat_seg_image_inj_on[OF `finite J`])


36 


37 
lemma enum_finite:


38 
assumes "finite J"


39 
shows "J = enum_finite J ` {i::nat. i < enum_finite_max J} \<and>


40 
inj_on (enum_finite J) {i::nat. i < enum_finite_max J}"


41 
unfolding enum_finite_def


42 
by (rule someI_ex[of "\<lambda>f. J = f ` {i::nat. i < enum_finite_max J} \<and>


43 
inj_on f {i. i < enum_finite_max J}"]) (rule enum_finite_max[OF `finite J`])


44 


45 
lemma in_set_enum_exist:


46 
assumes "finite A"


47 
assumes "y \<in> A"


48 
shows "\<exists>i. y = enum_finite A i"


49 
using assms enum_finite by auto


50 


51 
definition set_of_Un where "set_of_Un j = (LEAST n. j \<in> Js n)"


52 


53 
definition index_in_set where "index_in_set J j = (SOME n. j = enum_finite J n)"


54 


55 
definition Un_to_nat where


56 
"Un_to_nat j = to_nat (set_of_Un j, index_in_set (Js (set_of_Un j)) j)"


57 


58 
lemma inj_on_Un_to_nat:


59 
shows "inj_on Un_to_nat (\<Union>n::nat. Js n)"


60 
proof (rule inj_onI)


61 
fix x y


62 
assume "x \<in> (\<Union>n. Js n)" "y \<in> (\<Union>n. Js n)"


63 
then obtain ix iy where ix: "x \<in> Js ix" and iy: "y \<in> Js iy" by blast


64 
assume "Un_to_nat x = Un_to_nat y"


65 
hence "set_of_Un x = set_of_Un y"


66 
"index_in_set (Js (set_of_Un y)) y = index_in_set (Js (set_of_Un x)) x"


67 
by (auto simp: Un_to_nat_def)


68 
moreover


69 
{


70 
fix x assume "x \<in> Js (set_of_Un x)"


71 
have "x = enum_finite (Js (set_of_Un x)) (index_in_set (Js (set_of_Un x)) x)"


72 
unfolding index_in_set_def


73 
apply (rule someI_ex)


74 
using `x \<in> Js (set_of_Un x)` finite_seq


75 
apply (auto intro!: in_set_enum_exist)


76 
done


77 
} note H = this


78 
moreover


79 
have "y \<in> Js (set_of_Un y)" unfolding set_of_Un_def using iy by (rule LeastI)


80 
note H[OF this]


81 
moreover


82 
have "x \<in> Js (set_of_Un x)" unfolding set_of_Un_def using ix by (rule LeastI)


83 
note H[OF this]


84 
ultimately show "x = y" by simp


85 
qed


86 


87 
lemma inj_Un[simp]:


88 
shows "inj_on (Un_to_nat) (Js n)"


89 
by (intro subset_inj_on[OF inj_on_Un_to_nat]) (auto simp: assms)


90 


91 
lemma Un_to_nat_injectiveD:


92 
assumes "Un_to_nat x = Un_to_nat y"


93 
assumes "x \<in> Js i" "y \<in> Js j"


94 
shows "x = y"


95 
using assms


96 
by (intro inj_onD[OF inj_on_Un_to_nat]) auto


97 


98 
end


99 


100 
subsection {* Sequences of Finite Maps in Compact Sets *}


101 


102 
locale finmap_seqs_into_compact =


103 
fixes K::"nat \<Rightarrow> (nat \<Rightarrow>\<^isub>F 'a::metric_space) set" and f::"nat \<Rightarrow> (nat \<Rightarrow>\<^isub>F 'a)" and M


104 
assumes compact: "\<And>n. compact (K n)"


105 
assumes f_in_K: "\<And>n. K n \<noteq> {}"


106 
assumes domain_K: "\<And>n. k \<in> K n \<Longrightarrow> domain k = domain (f n)"


107 
assumes proj_in_K:


108 
"\<And>t n m. m \<ge> n \<Longrightarrow> t \<in> domain (f n) \<Longrightarrow> (f m)\<^isub>F t \<in> (\<lambda>k. (k)\<^isub>F t) ` K n"


109 
begin


110 


111 
lemma proj_in_K': "(\<exists>n. \<forall>m \<ge> n. (f m)\<^isub>F t \<in> (\<lambda>k. (k)\<^isub>F t) ` K n)"


112 
using proj_in_K f_in_K


113 
proof cases


114 
obtain k where "k \<in> K (Suc 0)" using f_in_K by auto


115 
assume "\<forall>n. t \<notin> domain (f n)"


116 
thus ?thesis


117 
by (auto intro!: exI[where x=1] image_eqI[OF _ `k \<in> K (Suc 0)`]


118 
simp: domain_K[OF `k \<in> K (Suc 0)`])


119 
qed blast


120 


121 
lemma proj_in_KE:


122 
obtains n where "\<And>m. m \<ge> n \<Longrightarrow> (f m)\<^isub>F t \<in> (\<lambda>k. (k)\<^isub>F t) ` K n"


123 
using proj_in_K' by blast


124 


125 
lemma compact_projset:


126 
shows "compact ((\<lambda>k. (k)\<^isub>F i) ` K n)"


127 
using continuous_proj compact by (rule compact_continuous_image)


128 


129 
end


130 


131 
lemma compactE':


132 
assumes "compact S" "\<forall>n\<ge>m. f n \<in> S"


133 
obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) > l) sequentially"


134 
proof atomize_elim


135 
have "subseq (op + m)" by (simp add: subseq_def)


136 
have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto


137 
from compactE[OF `compact S` this] guess l r .


138 
hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) > l"


139 
using subseq_o[OF `subseq (op + m)` `subseq r`] by (auto simp: o_def)


140 
thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) > l" by blast


141 
qed


142 


143 
sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^isub>F n) > l)"


144 
proof


145 
fix n s


146 
assume "subseq s"


147 
from proj_in_KE[of n] guess n0 . note n0 = this


148 
have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^isub>F n \<in> (\<lambda>k. (k)\<^isub>F n) ` K n0"


149 
proof safe


150 
fix i assume "n0 \<le> i"


151 
also have "\<dots> \<le> s i" by (rule seq_suble) fact


152 
finally have "n0 \<le> s i" .


153 
with n0 show "((f \<circ> s) i)\<^isub>F n \<in> (\<lambda>k. (k)\<^isub>F n) ` K n0 "


154 
by auto


155 
qed


156 
from compactE'[OF compact_projset this] guess ls rs .


157 
thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^isub>F n) > l)" by (auto simp: o_def)


158 
qed


159 


160 
lemma (in finmap_seqs_into_compact)


161 
diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) > l"


162 
proof 


163 
have "\<And>i n0. (f o seqseq i) i = f (diagseq i)" unfolding diagseq_def by simp


164 
from reducer_reduces obtain l where l: "(\<lambda>i. ((f \<circ> seqseq (Suc n)) i)\<^isub>F n) > l"


165 
unfolding seqseq_reducer


166 
by auto


167 
have "(\<lambda>i. (f (diagseq (i + Suc n)))\<^isub>F n) =


168 
(\<lambda>i. ((f o (diagseq o (op + (Suc n)))) i)\<^isub>F n)" by (simp add: add_commute)


169 
also have "\<dots> =


170 
(\<lambda>i. ((f o ((seqseq (Suc n) o (\<lambda>x. fold_reduce (Suc n) x (Suc n + x))))) i)\<^isub>F n)"


171 
unfolding diagseq_seqseq by simp


172 
also have "\<dots> = (\<lambda>i. ((f o ((seqseq (Suc n)))) i)\<^isub>F n) o (\<lambda>x. fold_reduce (Suc n) x (Suc n + x))"


173 
by (simp add: o_def)


174 
also have "\<dots> > l"


175 
proof (rule LIMSEQ_subseq_LIMSEQ[OF _ subseq_diagonal_rest], rule tendstoI)


176 
fix e::real assume "0 < e"


177 
from tendstoD[OF l `0 < e`]


178 
show "eventually (\<lambda>x. dist (((f \<circ> seqseq (Suc n)) x)\<^isub>F n) l < e)


179 
sequentially" .


180 
qed


181 
finally show ?thesis by (intro exI) (rule LIMSEQ_offset)


182 
qed


183 


184 
subsection {* DaniellKolmogorov Theorem *}


185 


186 
text {* Existence of Projective Limit *}


187 


188 
locale polish_projective = projective_family I P "\<lambda>_. borel::'a::polish_space measure"


189 
for I::"'i set" and P


190 
begin


191 


192 
abbreviation "PiB \<equiv> (\<lambda>J P. PiP J (\<lambda>_. borel) P)"


193 


194 
lemma


195 
emeasure_PiB_emb_not_empty:


196 
assumes "I \<noteq> {}"


197 
assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"


198 
shows "emeasure (PiB I P) (emb I J (Pi\<^isub>E J B)) = emeasure (PiB J P) (Pi\<^isub>E J B)"


199 
proof 


200 
let ?\<Omega> = "\<Pi>\<^isub>E i\<in>I. space borel"


201 
let ?G = generator


202 
interpret G!: algebra ?\<Omega> generator by (intro algebra_generator) fact


203 
note \<mu>G_mono =


204 
G.additive_increasing[OF positive_\<mu>G[OF `I \<noteq> {}`] additive_\<mu>G[OF `I \<noteq> {}`], THEN increasingD]


205 
have "\<exists>\<mu>. (\<forall>s\<in>?G. \<mu> s = \<mu>G s) \<and> measure_space ?\<Omega> (sigma_sets ?\<Omega> ?G) \<mu>"


206 
proof (rule G.caratheodory_empty_continuous[OF positive_\<mu>G additive_\<mu>G,


207 
OF `I \<noteq> {}`, OF `I \<noteq> {}`])


208 
fix A assume "A \<in> ?G"


209 
with generatorE guess J X . note JX = this


210 
interpret prob_space "P J" using prob_space[OF `finite J`] .


211 
show "\<mu>G A \<noteq> \<infinity>" using JX by (simp add: PiP_finite)


212 
next


213 
fix Z assume Z: "range Z \<subseteq> ?G" "decseq Z" "(\<Inter>i. Z i) = {}"


214 
then have "decseq (\<lambda>i. \<mu>G (Z i))"


215 
by (auto intro!: \<mu>G_mono simp: decseq_def)


216 
moreover


217 
have "(INF i. \<mu>G (Z i)) = 0"


218 
proof (rule ccontr)


219 
assume "(INF i. \<mu>G (Z i)) \<noteq> 0" (is "?a \<noteq> 0")


220 
moreover have "0 \<le> ?a"


221 
using Z positive_\<mu>G[OF `I \<noteq> {}`] by (auto intro!: INF_greatest simp: positive_def)


222 
ultimately have "0 < ?a" by auto


223 
hence "?a \<noteq> \<infinity>" by auto


224 
have "\<forall>n. \<exists>J B. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> B \<in> sets (Pi\<^isub>M J (\<lambda>_. borel)) \<and>


225 
Z n = emb I J B \<and> \<mu>G (Z n) = emeasure (PiB J P) B"


226 
using Z by (intro allI generator_Ex) auto


227 
then obtain J' B' where J': "\<And>n. J' n \<noteq> {}" "\<And>n. finite (J' n)" "\<And>n. J' n \<subseteq> I"


228 
"\<And>n. B' n \<in> sets (\<Pi>\<^isub>M i\<in>J' n. borel)"


229 
and Z_emb: "\<And>n. Z n = emb I (J' n) (B' n)"


230 
unfolding choice_iff by blast


231 
moreover def J \<equiv> "\<lambda>n. (\<Union>i\<le>n. J' i)"


232 
moreover def B \<equiv> "\<lambda>n. emb (J n) (J' n) (B' n)"


233 
ultimately have J: "\<And>n. J n \<noteq> {}" "\<And>n. finite (J n)" "\<And>n. J n \<subseteq> I"


234 
"\<And>n. B n \<in> sets (\<Pi>\<^isub>M i\<in>J n. borel)"


235 
by auto


236 
have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"


237 
unfolding J_def by force


238 
have "\<forall>n. \<exists>j. j \<in> J n" using J by blast


239 
then obtain j where j: "\<And>n. j n \<in> J n"


240 
unfolding choice_iff by blast


241 
note [simp] = `\<And>n. finite (J n)`


242 
from J Z_emb have Z_eq: "\<And>n. Z n = emb I (J n) (B n)" "\<And>n. Z n \<in> ?G"


243 
unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto)


244 
interpret prob_space "P (J i)" for i using prob_space by simp


245 
have "?a \<le> \<mu>G (Z 0)" by (auto intro: INF_lower)


246 
also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq \<mu>G_eq PiP_finite proj_sets)


247 
finally have "?a \<noteq> \<infinity>" by simp


248 
have "\<And>n. \<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>" unfolding Z_eq using J J_mono


249 
by (subst \<mu>G_eq) (auto simp: PiP_finite proj_sets \<mu>G_eq)


250 


251 
interpret finite_set_sequence J by unfold_locales simp


252 
def Utn \<equiv> Un_to_nat


253 
interpret function_to_finmap "J n" Utn "inv_into (J n) Utn" for n


254 
by unfold_locales (auto simp: Utn_def)


255 
def P' \<equiv> "\<lambda>n. mapmeasure n (P (J n)) (\<lambda>_. borel)"


256 
let ?SUP = "\<lambda>n. SUP K : {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"


257 
{


258 
fix n


259 
interpret finite_measure "P (J n)" by unfold_locales


260 
have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))"


261 
using J by (auto simp: P'_def mapmeasure_PiM proj_space proj_sets)


262 
also


263 
have "\<dots> = ?SUP n"


264 
proof (rule inner_regular)


265 
show "emeasure (P' n) (space (P' n)) \<noteq> \<infinity>"


266 
unfolding P'_def


267 
by (auto simp: P'_def mapmeasure_PiF fm_measurable proj_space proj_sets)


268 
show "sets (P' n) = sets borel" by (simp add: borel_eq_PiF_borel P'_def)


269 
next


270 
show "fm n ` B n \<in> sets borel"


271 
unfolding borel_eq_PiF_borel


272 
by (auto simp del: J(2) simp: P'_def fm_image_measurable_finite proj_sets J)


273 
qed


274 
finally


275 
have "emeasure (P (J n)) (B n) = ?SUP n" "?SUP n \<noteq> \<infinity>" "?SUP n \<noteq>  \<infinity>" by auto


276 
} note R = this


277 
have "\<forall>n. \<exists>K. emeasure (P (J n)) (B n)  emeasure (P' n) K \<le> 2 powr (n) * ?a


278 
\<and> compact K \<and> K \<subseteq> fm n ` B n"


279 
proof


280 
fix n


281 
have "emeasure (P' n) (space (P' n)) \<noteq> \<infinity>"


282 
by (simp add: mapmeasure_PiF P'_def proj_space proj_sets)


283 
then interpret finite_measure "P' n" ..


284 
show "\<exists>K. emeasure (P (J n)) (B n)  emeasure (P' n) K \<le> ereal (2 powr  real n) * ?a \<and>


285 
compact K \<and> K \<subseteq> fm n ` B n"


286 
unfolding R


287 
proof (rule ccontr)


288 
assume H: "\<not> (\<exists>K'. ?SUP n  emeasure (P' n) K' \<le> ereal (2 powr  real n) * ?a \<and>


289 
compact K' \<and> K' \<subseteq> fm n ` B n)"


290 
have "?SUP n \<le> ?SUP n  2 powr (n) * ?a"


291 
proof (intro SUP_least)


292 
fix K


293 
assume "K \<in> {K. K \<subseteq> fm n ` B n \<and> compact K}"


294 
with H have "\<not> ?SUP n  emeasure (P' n) K \<le> 2 powr (n) * ?a"


295 
by auto


296 
hence "?SUP n  emeasure (P' n) K > 2 powr (n) * ?a"


297 
unfolding not_less[symmetric] by simp


298 
hence "?SUP n  2 powr (n) * ?a > emeasure (P' n) K"


299 
using `0 < ?a` by (auto simp add: ereal_less_minus_iff ac_simps)


300 
thus "?SUP n  2 powr (n) * ?a \<ge> emeasure (P' n) K" by simp


301 
qed


302 
hence "?SUP n + 0 \<le> ?SUP n  (2 powr (n) * ?a)" using `0 < ?a` by simp


303 
hence "?SUP n + 0 \<le> ?SUP n +  (2 powr (n) * ?a)" unfolding minus_ereal_def .


304 
hence "0 \<le>  (2 powr (n) * ?a)"


305 
using `?SUP _ \<noteq> \<infinity>` `?SUP _ \<noteq>  \<infinity>`


306 
by (subst (asm) ereal_add_le_add_iff) (auto simp:)


307 
moreover have "ereal (2 powr  real n) * ?a > 0" using `0 < ?a`


308 
by (auto simp: ereal_zero_less_0_iff)


309 
ultimately show False by simp


310 
qed


311 
qed


312 
then obtain K' where K':


313 
"\<And>n. emeasure (P (J n)) (B n)  emeasure (P' n) (K' n) \<le> ereal (2 powr  real n) * ?a"


314 
"\<And>n. compact (K' n)" "\<And>n. K' n \<subseteq> fm n ` B n"


315 
unfolding choice_iff by blast


316 
def K \<equiv> "\<lambda>n. fm n ` K' n \<inter> space (Pi\<^isub>M (J n) (\<lambda>_. borel))"


317 
have K_sets: "\<And>n. K n \<in> sets (Pi\<^isub>M (J n) (\<lambda>_. borel))"


318 
unfolding K_def


319 
using compact_imp_closed[OF `compact (K' _)`]


320 
by (intro measurable_sets[OF fm_measurable, of _ "Collect finite"])


321 
(auto simp: borel_eq_PiF_borel[symmetric])


322 
have K_B: "\<And>n. K n \<subseteq> B n"


323 
proof


324 
fix x n


325 
assume "x \<in> K n" hence fm_in: "fm n x \<in> fm n ` B n"


326 
using K' by (force simp: K_def)


327 
show "x \<in> B n"


328 
apply (rule inj_on_image_mem_iff[OF inj_on_fm _ fm_in])


329 
using `x \<in> K n` K_sets J[of n] sets_into_space


330 
apply (auto simp: proj_space)


331 
using J[of n] sets_into_space apply auto


332 
done


333 
qed


334 
def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"


335 
have Z': "\<And>n. Z' n \<subseteq> Z n"


336 
unfolding Z_eq unfolding Z'_def


337 
proof (rule prod_emb_mono, safe)


338 
fix n x assume "x \<in> K n"


339 
hence "fm n x \<in> K' n" "x \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))"


340 
by (simp_all add: K_def proj_space)


341 
note this(1)


342 
also have "K' n \<subseteq> fm n ` B n" by (simp add: K')


343 
finally have "fm n x \<in> fm n ` B n" .


344 
thus "x \<in> B n"


345 
proof safe


346 
fix y assume "y \<in> B n"


347 
moreover


348 
hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets_into_space[of "B n" "P (J n)"]


349 
by (auto simp add: proj_space proj_sets)


350 
assume "fm n x = fm n y"


351 
note inj_onD[OF inj_on_fm[OF space_borel],


352 
OF `fm n x = fm n y` `x \<in> space _` `y \<in> space _`]


353 
ultimately show "x \<in> B n" by simp


354 
qed


355 
qed


356 
{ fix n


357 
have "Z' n \<in> ?G" using K' unfolding Z'_def


358 
apply (intro generatorI'[OF J(13)])


359 
unfolding K_def proj_space


360 
apply (rule measurable_sets[OF fm_measurable[of _ "Collect finite"]])


361 
apply (auto simp add: P'_def borel_eq_PiF_borel[symmetric] compact_imp_closed)


362 
done


363 
}


364 
def Y \<equiv> "\<lambda>n. \<Inter>i\<in>{1..n}. Z' i"


365 
hence "\<And>n k. Y (n + k) \<subseteq> Y n" by (induct_tac k) (auto simp: Y_def)


366 
hence Y_mono: "\<And>n m. n \<le> m \<Longrightarrow> Y m \<subseteq> Y n" by (auto simp: le_iff_add)


367 
have Y_Z': "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z' n" by (auto simp: Y_def)


368 
hence Y_Z: "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z n" using Z' by auto


369 
have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}"


370 
proof 


371 
fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact


372 
have "Y n = (\<Inter> i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono


373 
by (auto simp: Y_def Z'_def)


374 
also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter> i\<in>{1..n}. emb (J n) (J i) (K i))"


375 
using `n \<ge> 1`


376 
by (subst prod_emb_INT) auto


377 
finally


378 
have Y_emb:


379 
"Y n = prod_emb I (\<lambda>_. borel) (J n)


380 
(\<Inter> i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .


381 
hence "Y n \<in> ?G" using J J_mono K_sets `n \<ge> 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto


382 
hence "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" unfolding Y_emb using J J_mono K_sets `n \<ge> 1`


383 
by (subst \<mu>G_eq) (auto simp: PiP_finite proj_sets \<mu>G_eq)


384 
interpret finite_measure "(PiP (J n) (\<lambda>_. borel) P)"


385 
proof


386 
have "emeasure (PiP (J n) (\<lambda>_. borel) P) (J n \<rightarrow>\<^isub>E space borel) \<noteq> \<infinity>"


387 
using J by (subst emeasure_PiP) auto


388 
thus "emeasure (PiP (J n) (\<lambda>_. borel) P) (space (PiP (J n) (\<lambda>_. borel) P)) \<noteq> \<infinity>"


389 
by (simp add: space_PiM)


390 
qed


391 
have "\<mu>G (Z n) = PiP (J n) (\<lambda>_. borel) P (B n)"


392 
unfolding Z_eq using J by (auto simp: \<mu>G_eq)


393 
moreover have "\<mu>G (Y n) =


394 
PiP (J n) (\<lambda>_. borel) P (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))"


395 
unfolding Y_emb using J J_mono K_sets `n \<ge> 1` by (subst \<mu>G_eq) auto


396 
moreover have "\<mu>G (Z n  Y n) = PiP (J n) (\<lambda>_. borel) P


397 
(B n  (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"


398 
unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`


399 
by (subst \<mu>G_eq) (auto intro!: Diff)


400 
ultimately


401 
have "\<mu>G (Z n)  \<mu>G (Y n) = \<mu>G (Z n  Y n)"


402 
using J J_mono K_sets `n \<ge> 1`


403 
by (simp only: emeasure_eq_measure)


404 
(auto dest!: bspec[where x=n]


405 
simp: extensional_restrict emeasure_eq_measure prod_emb_iff


406 
intro!: measure_Diff[symmetric] set_mp[OF K_B])


407 
also have subs: "Z n  Y n \<subseteq> (\<Union> i\<in>{1..n}. (Z i  Z' i))" using Z' Z `n \<ge> 1`


408 
unfolding Y_def by (force simp: decseq_def)


409 
have "Z n  Y n \<in> ?G" "(\<Union> i\<in>{1..n}. (Z i  Z' i)) \<in> ?G"


410 
using `Z' _ \<in> ?G` `Z _ \<in> ?G` `Y _ \<in> ?G` by auto


411 
hence "\<mu>G (Z n  Y n) \<le> \<mu>G (\<Union> i\<in>{1..n}. (Z i  Z' i))"


412 
using subs G.additive_increasing[OF positive_\<mu>G[OF `I \<noteq> {}`] additive_\<mu>G[OF `I \<noteq> {}`]]


413 
unfolding increasing_def by auto


414 
also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i  Z' i))" using `Z _ \<in> ?G` `Z' _ \<in> ?G`


415 
by (intro G.subadditive[OF positive_\<mu>G additive_\<mu>G, OF `I \<noteq> {}` `I \<noteq> {}`]) auto


416 
also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr real i * ?a)"


417 
proof (rule setsum_mono)


418 
fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp


419 
have "\<mu>G (Z i  Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i  K i))"


420 
unfolding Z'_def Z_eq by simp


421 
also have "\<dots> = P (J i) (B i  K i)"


422 
apply (subst \<mu>G_eq) using J K_sets apply auto


423 
apply (subst PiP_finite) apply auto


424 
done


425 
also have "\<dots> = P (J i) (B i)  P (J i) (K i)"


426 
apply (subst emeasure_Diff) using K_sets J `K _ \<subseteq> B _` apply (auto simp: proj_sets)


427 
done


428 
also have "\<dots> = P (J i) (B i)  P' i (K' i)"


429 
unfolding K_def P'_def


430 
by (auto simp: mapmeasure_PiF proj_space proj_sets borel_eq_PiF_borel[symmetric]


431 
compact_imp_closed[OF `compact (K' _)`] space_PiM)


432 
also have "\<dots> \<le> ereal (2 powr  real i) * ?a" using K'(1)[of i] .


433 
finally show "\<mu>G (Z i  Z' i) \<le> (2 powr  real i) * ?a" .


434 
qed


435 
also have "\<dots> = (\<Sum> i\<in>{1..n}. ereal (2 powr real i) * ereal(real ?a))"


436 
using `?a \<noteq> \<infinity>` `?a \<noteq>  \<infinity>` by (subst ereal_real') auto


437 
also have "\<dots> = ereal (\<Sum> i\<in>{1..n}. (2 powr real i) * (real ?a))" by simp


438 
also have "\<dots> = ereal ((\<Sum> i\<in>{1..n}. (2 powr real i)) * real ?a)"


439 
by (simp add: setsum_left_distrib)


440 
also have "\<dots> < ereal (1 * real ?a)" unfolding less_ereal.simps


441 
proof (rule mult_strict_right_mono)


442 
have "(\<Sum>i\<in>{1..n}. 2 powr  real i) = (\<Sum>i\<in>{1..<Suc n}. (1/2) ^ i)"


443 
by (rule setsum_cong)


444 
(auto simp: powr_realpow[symmetric] powr_minus powr_divide inverse_eq_divide)


445 
also have "{1..<Suc n} = {0..<Suc n}  {0}" by auto


446 
also have "setsum (op ^ (1 / 2::real)) ({0..<Suc n}  {0}) =


447 
setsum (op ^ (1 / 2)) ({0..<Suc n})  1" by (auto simp: setsum_diff1)


448 
also have "\<dots> < 1" by (subst sumr_geometric) auto


449 
finally show "(\<Sum>i = 1..n. 2 powr  real i) < 1" .


450 
qed (auto simp:


451 
`0 < ?a` `?a \<noteq> \<infinity>` `?a \<noteq>  \<infinity>` ereal_less_real_iff zero_ereal_def[symmetric])


452 
also have "\<dots> = ?a" using `0 < ?a` `?a \<noteq> \<infinity>` by (auto simp: ereal_real')


453 
also have "\<dots> \<le> \<mu>G (Z n)" by (auto intro: INF_lower)


454 
finally have "\<mu>G (Z n)  \<mu>G (Y n) < \<mu>G (Z n)" .


455 
hence R: "\<mu>G (Z n) < \<mu>G (Z n) + \<mu>G (Y n)"


456 
using `\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>` by (simp add: ereal_minus_less)


457 
have "0 \<le> ( \<mu>G (Z n)) + \<mu>G (Z n)" using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto


458 
also have "\<dots> < ( \<mu>G (Z n)) + (\<mu>G (Z n) + \<mu>G (Y n))"


459 
apply (rule ereal_less_add[OF _ R]) using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto


460 
finally have "\<mu>G (Y n) > 0"


461 
using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by (auto simp: ac_simps zero_ereal_def[symmetric])


462 
thus "Y n \<noteq> {}" using positive_\<mu>G `I \<noteq> {}` by (auto simp add: positive_def)


463 
qed


464 
hence "\<forall>n\<in>{1..}. \<exists>y. y \<in> Y n" by auto


465 
then obtain y where y: "\<And>n. n \<ge> 1 \<Longrightarrow> y n \<in> Y n" unfolding bchoice_iff by force


466 
{


467 
fix t and n m::nat


468 
assume "1 \<le> n" "n \<le> m" hence "1 \<le> m" by simp


469 
from Y_mono[OF `m \<ge> n`] y[OF `1 \<le> m`] have "y m \<in> Y n" by auto


470 
also have "\<dots> \<subseteq> Z' n" using Y_Z'[OF `1 \<le> n`] .


471 
finally


472 
have "fm n (restrict (y m) (J n)) \<in> K' n"


473 
unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)


474 
moreover have "finmap_of (J n) (restrict (y m) (J n)) = finmap_of (J n) (y m)"


475 
using J by (simp add: fm_def)


476 
ultimately have "fm n (y m) \<in> K' n" by simp


477 
} note fm_in_K' = this


478 
interpret finmap_seqs_into_compact "\<lambda>n. K' (Suc n)" "\<lambda>k. fm (Suc k) (y (Suc k))" borel


479 
proof


480 
fix n show "compact (K' n)" by fact


481 
next


482 
fix n


483 
from Y_mono[of n "Suc n"] y[of "Suc n"] have "y (Suc n) \<in> Y (Suc n)" by auto


484 
also have "\<dots> \<subseteq> Z' (Suc n)" using Y_Z' by auto


485 
finally


486 
have "fm (Suc n) (restrict (y (Suc n)) (J (Suc n))) \<in> K' (Suc n)"


487 
unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff)


488 
thus "K' (Suc n) \<noteq> {}" by auto


489 
fix k


490 
assume "k \<in> K' (Suc n)"


491 
with K'[of "Suc n"] sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto


492 
then obtain b where "k = fm (Suc n) b" by auto


493 
thus "domain k = domain (fm (Suc n) (y (Suc n)))"


494 
by (simp_all add: fm_def)


495 
next


496 
fix t and n m::nat


497 
assume "n \<le> m" hence "Suc n \<le> Suc m" by simp


498 
assume "t \<in> domain (fm (Suc n) (y (Suc n)))"


499 
then obtain j where j: "t = Utn j" "j \<in> J (Suc n)" by auto


500 
hence "j \<in> J (Suc m)" using J_mono[OF `Suc n \<le> Suc m`] by auto


501 
have img: "fm (Suc n) (y (Suc m)) \<in> K' (Suc n)" using `n \<le> m`


502 
by (intro fm_in_K') simp_all


503 
show "(fm (Suc m) (y (Suc m)))\<^isub>F t \<in> (\<lambda>k. (k)\<^isub>F t) ` K' (Suc n)"


504 
apply (rule image_eqI[OF _ img])


505 
using `j \<in> J (Suc n)` `j \<in> J (Suc m)`


506 
unfolding j by (subst proj_fm, auto)+


507 
qed


508 
have "\<forall>t. \<exists>z. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^isub>F t) > z"


509 
using diagonal_tendsto ..


510 
then obtain z where z:


511 
"\<And>t. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^isub>F t) > z t"


512 
unfolding choice_iff by blast


513 
{


514 
fix n :: nat assume "n \<ge> 1"


515 
have "\<And>i. domain (fm n (y (Suc (diagseq i)))) = domain (finmap_of (Utn ` J n) z)"


516 
by simp


517 
moreover


518 
{


519 
fix t


520 
assume t: "t \<in> domain (finmap_of (Utn ` J n) z)"


521 
hence "t \<in> Utn ` J n" by simp


522 
then obtain j where j: "t = Utn j" "j \<in> J n" by auto


523 
have "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^isub>F t) > z t"


524 
apply (subst (2) tendsto_iff, subst eventually_sequentially)


525 
proof safe


526 
fix e :: real assume "0 < e"


527 
{ fix i x assume "i \<ge> n" "t \<in> domain (fm n x)"


528 
moreover


529 
hence "t \<in> domain (fm i x)" using J_mono[OF `i \<ge> n`] by auto


530 
ultimately have "(fm i x)\<^isub>F t = (fm n x)\<^isub>F t"


531 
using j by (auto simp: proj_fm dest!:


532 
Un_to_nat_injectiveD[simplified Utn_def[symmetric]])


533 
} note index_shift = this


534 
have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n"


535 
apply (rule le_SucI)


536 
apply (rule order_trans) apply simp


537 
apply (rule seq_suble[OF subseq_diagseq])


538 
done


539 
from z


540 
have "\<exists>N. \<forall>i\<ge>N. dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^isub>F t) (z t) < e"


541 
unfolding tendsto_iff eventually_sequentially using `0 < e` by auto


542 
then obtain N where N: "\<And>i. i \<ge> N \<Longrightarrow>


543 
dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^isub>F t) (z t) < e" by auto


544 
show "\<exists>N. \<forall>na\<ge>N. dist ((fm n (y (Suc (diagseq na))))\<^isub>F t) (z t) < e "


545 
proof (rule exI[where x="max N n"], safe)


546 
fix na assume "max N n \<le> na"


547 
hence "dist ((fm n (y (Suc (diagseq na))))\<^isub>F t) (z t) =


548 
dist ((fm (Suc (diagseq na)) (y (Suc (diagseq na))))\<^isub>F t) (z t)" using t


549 
by (subst index_shift[OF I]) auto


550 
also have "\<dots> < e" using `max N n \<le> na` by (intro N) simp


551 
finally show "dist ((fm n (y (Suc (diagseq na))))\<^isub>F t) (z t) < e" .


552 
qed


553 
qed


554 
hence "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^isub>F t) > (finmap_of (Utn ` J n) z)\<^isub>F t"


555 
by (simp add: tendsto_intros)


556 
} ultimately


557 
have "(\<lambda>i. fm n (y (Suc (diagseq i)))) > finmap_of (Utn ` J n) z"


558 
by (rule tendsto_finmap)


559 
hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) > finmap_of (Utn ` J n) z"


560 
by (intro lim_subseq) (simp add: subseq_def)


561 
moreover


562 
have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"


563 
apply (auto simp add: o_def intro!: fm_in_K' `1 \<le> n` le_SucI)


564 
apply (rule le_trans)


565 
apply (rule le_add2)


566 
using seq_suble[OF subseq_diagseq]


567 
apply auto


568 
done


569 
moreover


570 
from `compact (K' n)` have "closed (K' n)" by (rule compact_imp_closed)


571 
ultimately


572 
have "finmap_of (Utn ` J n) z \<in> K' n"


573 
unfolding closed_sequential_limits by blast


574 
also have "finmap_of (Utn ` J n) z = fm n (\<lambda>i. z (Utn i))"


575 
by (auto simp: finmap_eq_iff fm_def compose_def f_inv_into_f)


576 
finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" .


577 
moreover


578 
let ?J = "\<Union>n. J n"


579 
have "(?J \<inter> J n) = J n" by auto


580 
ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n"


581 
unfolding K_def by (auto simp: proj_space space_PiM)


582 
hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def


583 
using J by (auto simp: prod_emb_def extensional_def)


584 
also have "\<dots> \<subseteq> Z n" using Z' by simp


585 
finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" .


586 
} note in_Z = this


587 
hence "(\<Inter>i\<in>{1..}. Z i) \<noteq> {}" by auto


588 
hence "(\<Inter>i. Z i) \<noteq> {}" using Z INT_decseq_offset[OF `decseq Z`] by simp


589 
thus False using Z by simp


590 
qed


591 
ultimately show "(\<lambda>i. \<mu>G (Z i)) > 0"


592 
using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (Z i)"] by simp


593 
qed


594 
then guess \<mu> .. note \<mu> = this


595 
def f \<equiv> "finmap_of J B"


596 
show "emeasure (PiB I P) (emb I J (Pi\<^isub>E J B)) = emeasure (PiB J P) (Pi\<^isub>E J B)"


597 
proof (subst emeasure_extend_measure_Pair[OF PiP_def, of I "\<lambda>_. borel" \<mu>])


598 
show "positive (sets (PiB I P)) \<mu>" "countably_additive (sets (PiB I P)) \<mu>"


599 
using \<mu> unfolding sets_PiP sets_PiM_generator by (auto simp: measure_space_def)


600 
next


601 
show "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> B \<in> J \<rightarrow> sets borel"


602 
using assms by (auto simp: f_def)


603 
next


604 
fix J and X::"'i \<Rightarrow> 'a set"


605 
show "prod_emb I (\<lambda>_. borel) J (Pi\<^isub>E J X) \<in> Pow ((I \<rightarrow> space borel) \<inter> extensional I)"


606 
by (auto simp: prod_emb_def)


607 
assume JX: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> J \<rightarrow> sets borel"


608 
hence "emb I J (Pi\<^isub>E J X) \<in> generator" using assms


609 
by (intro generatorI[where J=J and X="Pi\<^isub>E J X"]) (auto intro: sets_PiM_I_finite)


610 
hence "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))" using \<mu> by simp


611 
also have "\<dots> = emeasure (P J) (Pi\<^isub>E J X)"


612 
using JX assms proj_sets


613 
by (subst \<mu>G_eq) (auto simp: \<mu>G_eq PiP_finite intro: sets_PiM_I_finite)


614 
finally show "\<mu> (emb I J (Pi\<^isub>E J X)) = emeasure (P J) (Pi\<^isub>E J X)" .


615 
next


616 
show "emeasure (P J) (Pi\<^isub>E J B) = emeasure (PiP J (\<lambda>_. borel) P) (Pi\<^isub>E J B)"


617 
using assms by (simp add: f_def PiP_finite Pi_def)


618 
qed


619 
qed


620 


621 
end


622 

50090

623 
hide_const (open) PiF


624 
hide_const (open) Pi\<^isub>F


625 
hide_const (open) Pi'


626 
hide_const (open) Abs_finmap


627 
hide_const (open) Rep_finmap


628 
hide_const (open) finmap_of


629 
hide_const (open) finmapset


630 
hide_const (open) proj


631 
hide_const (open) domain


632 
hide_const (open) enum_basis_finmap


633 

50088

634 
sublocale polish_projective \<subseteq> P!: prob_space "(PiB I P)"


635 
proof


636 
show "emeasure (PiB I P) (space (PiB I P)) = 1"


637 
proof cases


638 
assume "I = {}"


639 
interpret prob_space "P {}" using prob_space by simp


640 
show ?thesis


641 
by (simp add: space_PiM_empty PiP_finite emeasure_space_1 `I = {}`)


642 
next


643 
assume "I \<noteq> {}"


644 
then obtain i where "i \<in> I" by auto


645 
interpret prob_space "P {i}" using prob_space by simp


646 
have R: "(space (PiB I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"


647 
by (auto simp: prod_emb_def space_PiM)


648 
moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)


649 
ultimately show ?thesis using `i \<in> I`


650 
apply (subst R)


651 
apply (subst emeasure_PiB_emb_not_empty)


652 
apply (auto simp: PiP_finite emeasure_space_1)


653 
done


654 
qed


655 
qed


656 


657 
context polish_projective begin


658 


659 
lemma emeasure_PiB_emb:


660 
assumes X: "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"


661 
shows "emeasure (PiB I P) (emb I J (Pi\<^isub>E J B)) = emeasure (P J) (Pi\<^isub>E J B)"


662 
proof cases


663 
interpret prob_space "P {}" using prob_space by simp


664 
assume "J = {}"


665 
moreover have "emb I {} {\<lambda>x. undefined} = space (PiB I P)"


666 
by (auto simp: space_PiM prod_emb_def)


667 
moreover have "{\<lambda>x. undefined} = space (PiB {} P)"


668 
by (auto simp: space_PiM prod_emb_def)


669 
ultimately show ?thesis


670 
by (simp add: P.emeasure_space_1 PiP_finite emeasure_space_1 del: space_PiP)


671 
next


672 
assume "J \<noteq> {}" with X show ?thesis


673 
by (subst emeasure_PiB_emb_not_empty) (auto simp: PiP_finite)


674 
qed


675 


676 
lemma measure_PiB_emb:


677 
assumes "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"


678 
shows "measure (PiB I P) (emb I J (Pi\<^isub>E J B)) = measure (P J) (Pi\<^isub>E J B)"


679 
proof 


680 
interpret prob_space "P J" using prob_space assms by simp


681 
show ?thesis


682 
using emeasure_PiB_emb[OF assms]


683 
unfolding emeasure_eq_measure PiP_finite[OF `finite J` `J \<subseteq> I`] P.emeasure_eq_measure


684 
by simp


685 
qed


686 


687 
end


688 


689 
locale polish_product_prob_space =


690 
product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set"


691 


692 
sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)"


693 
proof qed


694 


695 
lemma (in polish_product_prob_space)


696 
PiP_eq_PiM:


697 
"I \<noteq> {} \<Longrightarrow> PiP I (\<lambda>_. borel) (\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)) =


698 
PiM I (\<lambda>_. borel)"


699 
by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_PiB_emb)


700 


701 
end
