1(* Title: HOL/Probability/Projective_Limit.thy 2 Author: Fabian Immler, TU M��nchen 3*) 4 5section \<open>Projective Limit\<close> 6 7theory Projective_Limit 8imports 9 Fin_Map 10 Infinite_Product_Measure 11 "HOL-Library.Diagonal_Subsequence" 12begin 13 14subsection \<open>Sequences of Finite Maps in Compact Sets\<close> 15 16locale finmap_seqs_into_compact = 17 fixes K::"nat \<Rightarrow> (nat \<Rightarrow>\<^sub>F 'a::metric_space) set" and f::"nat \<Rightarrow> (nat \<Rightarrow>\<^sub>F 'a)" and M 18 assumes compact: "\<And>n. compact (K n)" 19 assumes f_in_K: "\<And>n. K n \<noteq> {}" 20 assumes domain_K: "\<And>n. k \<in> K n \<Longrightarrow> domain k = domain (f n)" 21 assumes proj_in_K: 22 "\<And>t n m. m \<ge> n \<Longrightarrow> t \<in> domain (f n) \<Longrightarrow> (f m)\<^sub>F t \<in> (\<lambda>k. (k)\<^sub>F t) ` K n" 23begin 24 25lemma proj_in_K': "(\<exists>n. \<forall>m \<ge> n. (f m)\<^sub>F t \<in> (\<lambda>k. (k)\<^sub>F t) ` K n)" 26 using proj_in_K f_in_K 27proof cases 28 obtain k where "k \<in> K (Suc 0)" using f_in_K by auto 29 assume "\<forall>n. t \<notin> domain (f n)" 30 thus ?thesis 31 by (auto intro!: exI[where x=1] image_eqI[OF _ \<open>k \<in> K (Suc 0)\<close>] 32 simp: domain_K[OF \<open>k \<in> K (Suc 0)\<close>]) 33qed blast 34 35lemma proj_in_KE: 36 obtains n where "\<And>m. m \<ge> n \<Longrightarrow> (f m)\<^sub>F t \<in> (\<lambda>k. (k)\<^sub>F t) ` K n" 37 using proj_in_K' by blast 38 39lemma compact_projset: 40 shows "compact ((\<lambda>k. (k)\<^sub>F i) ` K n)" 41 using continuous_proj compact by (rule compact_continuous_image) 42 43end 44 45lemma compactE': 46 fixes S :: "'a :: metric_space set" 47 assumes "compact S" "\<forall>n\<ge>m. f n \<in> S" 48 obtains l r where "l \<in> S" "strict_mono (r::nat\<Rightarrow>nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially" 49proof atomize_elim 50 have "strict_mono ((+) m)" by (simp add: strict_mono_def) 51 have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto 52 from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r . 53 hence "l \<in> S" "strict_mono ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l" 54 using strict_mono_o[OF \<open>strict_mono ((+) m)\<close> \<open>strict_mono r\<close>] by (auto simp: o_def) 55 thus "\<exists>l r. l \<in> S \<and> strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast 56qed 57 58sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^sub>F n) \<longlonglongrightarrow> l)" 59proof 60 fix n and s :: "nat \<Rightarrow> nat" 61 assume "strict_mono s" 62 from proj_in_KE[of n] guess n0 . note n0 = this 63 have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0" 64 proof safe 65 fix i assume "n0 \<le> i" 66 also have "\<dots> \<le> s i" by (rule seq_suble) fact 67 finally have "n0 \<le> s i" . 68 with n0 show "((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0 " 69 by auto 70 qed 71 from compactE'[OF compact_projset this] guess ls rs . 72 thus "\<exists>r'. strict_mono r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def) 73qed 74 75lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l" 76proof - 77 obtain l where "(\<lambda>i. ((f o (diagseq o (+) (Suc n))) i)\<^sub>F n) \<longlonglongrightarrow> l" 78 proof (atomize_elim, rule diagseq_holds) 79 fix r s n 80 assume "strict_mono (r :: nat \<Rightarrow> nat)" 81 assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<longlonglongrightarrow> l" 82 then obtain l where "((\<lambda>i. (f i)\<^sub>F n) o s) \<longlonglongrightarrow> l" 83 by (auto simp: o_def) 84 hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>strict_mono r\<close> 85 by (rule LIMSEQ_subseq_LIMSEQ) 86 thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^sub>F n) \<longlonglongrightarrow> l" by (auto simp add: o_def) 87 qed 88 hence "(\<lambda>i. ((f (diagseq (i + Suc n))))\<^sub>F n) \<longlonglongrightarrow> l" by (simp add: ac_simps) 89 hence "(\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l" by (rule LIMSEQ_offset) 90 thus ?thesis .. 91qed 92 93subsection \<open>Daniell-Kolmogorov Theorem\<close> 94 95text \<open>Existence of Projective Limit\<close> 96 97locale polish_projective = projective_family I P "\<lambda>_. borel::'a::polish_space measure" 98 for I::"'i set" and P 99begin 100 101lemma emeasure_lim_emb: 102 assumes X: "J \<subseteq> I" "finite J" "X \<in> sets (\<Pi>\<^sub>M i\<in>J. borel)" 103 shows "lim (emb I J X) = P J X" 104proof (rule emeasure_lim) 105 write mu_G ("\<mu>G") 106 interpret generator: algebra "space (PiM I (\<lambda>i. borel))" generator 107 by (rule algebra_generator) 108 109 fix J and B :: "nat \<Rightarrow> ('i \<Rightarrow> 'a) set" 110 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" 111 and B: "decseq (\<lambda>n. emb I (J n) (B n))" 112 and "0 < (INF i. P (J i) (B i))" (is "0 < ?a") 113 moreover have "?a \<le> 1" 114 using J by (auto intro!: INF_lower2[of 0] prob_space_P[THEN prob_space.measure_le_1]) 115 ultimately obtain r where r: "?a = ennreal r" "0 < r" "r \<le> 1" 116 by (cases "?a") (auto simp: top_unique) 117 define Z where "Z n = emb I (J n) (B n)" for n 118 have Z_mono: "n \<le> m \<Longrightarrow> Z m \<subseteq> Z n" for n m 119 unfolding Z_def using B[THEN antimonoD, of n m] . 120 have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m" 121 using \<open>incseq J\<close> by (force simp: incseq_def) 122 note [simp] = \<open>\<And>n. finite (J n)\<close> 123 interpret prob_space "P (J i)" for i using J prob_space_P by simp 124 125 have P_eq[simp]: 126 "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 127 using J by (auto simp: sets_P space_P) 128 129 have "Z i \<in> generator" for i 130 unfolding Z_def by (auto intro!: generator.intros J) 131 132 have countable_UN_J: "countable (\<Union>n. J n)" by (simp add: countable_finite) 133 define Utn where "Utn = to_nat_on (\<Union>n. J n)" 134 interpret function_to_finmap "J n" Utn "from_nat_into (\<Union>n. J n)" for n 135 by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J]) 136 have inj_on_Utn: "inj_on Utn (\<Union>n. J n)" 137 unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on) 138 hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule subset_inj_on) auto 139 define P' where "P' n = mapmeasure n (P (J n)) (\<lambda>_. borel)" for n 140 interpret P': prob_space "P' n" for n 141 unfolding P'_def mapmeasure_def using J 142 by (auto intro!: prob_space_distr fm_measurable simp: measurable_cong_sets[OF sets_P]) 143 144 let ?SUP = "\<lambda>n. SUP K \<in> {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K" 145 { fix n 146 have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))" 147 using J by (auto simp: P'_def mapmeasure_PiM space_P sets_P) 148 also 149 have "\<dots> = ?SUP n" 150 proof (rule inner_regular) 151 show "sets (P' n) = sets borel" by (simp add: borel_eq_PiF_borel P'_def) 152 next 153 show "fm n ` B n \<in> sets borel" 154 unfolding borel_eq_PiF_borel by (auto simp: P'_def fm_image_measurable_finite sets_P J(3)) 155 qed simp 156 finally have *: "emeasure (P (J n)) (B n) = ?SUP n" . 157 have "?SUP n \<noteq> \<infinity>" 158 unfolding *[symmetric] by simp 159 note * this 160 } note R = this 161 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" 162 proof 163 fix n show "\<exists>K. emeasure (P (J n)) (B n) - emeasure (P' n) K \<le> ennreal (2 powr - real n) * ?a \<and> 164 compact K \<and> K \<subseteq> fm n ` B n" 165 unfolding R[of n] 166 proof (rule ccontr) 167 assume H: "\<nexists>K'. ?SUP n - emeasure (P' n) K' \<le> ennreal (2 powr - real n) * ?a \<and> 168 compact K' \<and> K' \<subseteq> fm n ` B n" 169 have "?SUP n + 0 < ?SUP n + 2 powr (-n) * ?a" 170 using R[of n] unfolding ennreal_add_left_cancel_less ennreal_zero_less_mult_iff 171 by (auto intro: \<open>0 < ?a\<close>) 172 also have "\<dots> = (SUP K\<in>{K. K \<subseteq> fm n ` B n \<and> compact K}. emeasure (P' n) K + 2 powr (-n) * ?a)" 173 by (rule ennreal_SUP_add_left[symmetric]) auto 174 also have "\<dots> \<le> ?SUP n" 175 proof (intro SUP_least) 176 fix K assume "K \<in> {K. K \<subseteq> fm n ` B n \<and> compact K}" 177 with H have "2 powr (-n) * ?a < ?SUP n - emeasure (P' n) K" 178 by auto 179 then show "emeasure (P' n) K + (2 powr (-n)) * ?a \<le> ?SUP n" 180 by (subst (asm) less_diff_eq_ennreal) (auto simp: less_top[symmetric] R(1)[symmetric] ac_simps) 181 qed 182 finally show False by simp 183 qed 184 qed 185 then obtain K' where K': 186 "\<And>n. emeasure (P (J n)) (B n) - emeasure (P' n) (K' n) \<le> ennreal (2 powr - real n) * ?a" 187 "\<And>n. compact (K' n)" "\<And>n. K' n \<subseteq> fm n ` B n" 188 unfolding choice_iff by blast 189 define K where "K n = fm n -` K' n \<inter> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" for n 190 have K_sets: "\<And>n. K n \<in> sets (Pi\<^sub>M (J n) (\<lambda>_. borel))" 191 unfolding K_def 192 using compact_imp_closed[OF \<open>compact (K' _)\<close>] 193 by (intro measurable_sets[OF fm_measurable, of _ "Collect finite"]) 194 (auto simp: borel_eq_PiF_borel[symmetric]) 195 have K_B: "\<And>n. K n \<subseteq> B n" 196 proof 197 fix x n assume "x \<in> K n" 198 then have fm_in: "fm n x \<in> fm n ` B n" 199 using K' by (force simp: K_def) 200 show "x \<in> B n" 201 using \<open>x \<in> K n\<close> K_sets sets.sets_into_space J(1,2,3)[of n] inj_on_image_mem_iff[OF inj_on_fm] 202 by (metis (no_types) Int_iff K_def fm_in space_borel) 203 qed 204 define Z' where "Z' n = emb I (J n) (K n)" for n 205 have Z': "\<And>n. Z' n \<subseteq> Z n" 206 unfolding Z'_def Z_def 207 proof (rule prod_emb_mono, safe) 208 fix n x assume "x \<in> K n" 209 hence "fm n x \<in> K' n" "x \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" 210 by (simp_all add: K_def space_P) 211 note this(1) 212 also have "K' n \<subseteq> fm n ` B n" by (simp add: K') 213 finally have "fm n x \<in> fm n ` B n" . 214 thus "x \<in> B n" 215 proof safe 216 fix y assume y: "y \<in> B n" 217 hence "y \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"] 218 by (auto simp add: space_P sets_P) 219 assume "fm n x = fm n y" 220 note inj_onD[OF inj_on_fm[OF space_borel], 221 OF \<open>fm n x = fm n y\<close> \<open>x \<in> space _\<close> \<open>y \<in> space _\<close>] 222 with y show "x \<in> B n" by simp 223 qed 224 qed 225 have "\<And>n. Z' n \<in> generator" using J K'(2) unfolding Z'_def 226 by (auto intro!: generator.intros measurable_sets[OF fm_measurable[of _ "Collect finite"]] 227 simp: K_def borel_eq_PiF_borel[symmetric] compact_imp_closed) 228 define Y where "Y n = (\<Inter>i\<in>{1..n}. Z' i)" for n 229 hence "\<And>n k. Y (n + k) \<subseteq> Y n" by (induct_tac k) (auto simp: Y_def) 230 hence Y_mono: "\<And>n m. n \<le> m \<Longrightarrow> Y m \<subseteq> Y n" by (auto simp: le_iff_add) 231 have Y_Z': "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z' n" by (auto simp: Y_def) 232 hence Y_Z: "\<And>n. n \<ge> 1 \<Longrightarrow> Y n \<subseteq> Z n" using Z' by auto 233 234 have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}" 235 proof - 236 fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact 237 have "Y n = (\<Inter>i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono 238 by (auto simp: Y_def Z'_def) 239 also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. emb (J n) (J i) (K i))" 240 using \<open>n \<ge> 1\<close> 241 by (subst prod_emb_INT) auto 242 finally 243 have Y_emb: 244 "Y n = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" . 245 hence "Y n \<in> generator" using J J_mono K_sets \<open>n \<ge> 1\<close> 246 by (auto simp del: prod_emb_INT intro!: generator.intros) 247 have *: "\<mu>G (Z n) = P (J n) (B n)" 248 unfolding Z_def using J by (intro mu_G_spec) auto 249 then have "\<mu>G (Z n) \<noteq> \<infinity>" by auto 250 note * 251 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))" 252 unfolding Y_emb using J J_mono K_sets \<open>n \<ge> 1\<close> by (subst mu_G_spec) auto 253 then have "\<mu>G (Y n) \<noteq> \<infinity>" by auto 254 note * 255 moreover have "\<mu>G (Z n - Y n) = 256 P (J n) (B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))" 257 unfolding Z_def Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets \<open>n \<ge> 1\<close> 258 by (subst mu_G_spec) (auto intro!: sets.Diff) 259 ultimately 260 have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)" 261 using J J_mono K_sets \<open>n \<ge> 1\<close> 262 by (simp only: emeasure_eq_measure Z_def) 263 (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] subsetD[OF K_B] 264 intro!: arg_cong[where f=ennreal] 265 simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P 266 ennreal_minus measure_nonneg) 267 also have subs: "Z n - Y n \<subseteq> (\<Union>i\<in>{1..n}. (Z i - Z' i))" 268 using \<open>n \<ge> 1\<close> unfolding Y_def UN_extend_simps(7) by (intro UN_mono Diff_mono Z_mono order_refl) auto 269 have "Z n - Y n \<in> generator" "(\<Union>i\<in>{1..n}. (Z i - Z' i)) \<in> generator" 270 using \<open>Z' _ \<in> generator\<close> \<open>Z _ \<in> generator\<close> \<open>Y _ \<in> generator\<close> by auto 271 hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union>i\<in>{1..n}. (Z i - Z' i))" 272 using subs generator.additive_increasing[OF positive_mu_G additive_mu_G] 273 unfolding increasing_def by auto 274 also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using \<open>Z _ \<in> generator\<close> \<open>Z' _ \<in> generator\<close> 275 by (intro generator.subadditive[OF positive_mu_G additive_mu_G]) auto 276 also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr -real i * ?a)" 277 proof (rule sum_mono) 278 fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp 279 have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))" 280 unfolding Z'_def Z_def by simp 281 also have "\<dots> = P (J i) (B i - K i)" 282 using J K_sets by (subst mu_G_spec) auto 283 also have "\<dots> = P (J i) (B i) - P (J i) (K i)" 284 using K_sets J \<open>K _ \<subseteq> B _\<close> by (simp add: emeasure_Diff) 285 also have "\<dots> = P (J i) (B i) - P' i (K' i)" 286 unfolding K_def P'_def 287 by (auto simp: mapmeasure_PiF borel_eq_PiF_borel[symmetric] 288 compact_imp_closed[OF \<open>compact (K' _)\<close>] space_PiM PiE_def) 289 also have "\<dots> \<le> ennreal (2 powr - real i) * ?a" using K'(1)[of i] . 290 finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" . 291 qed 292 also have "\<dots> = ennreal ((\<Sum> i\<in>{1..n}. (2 powr -enn2real i)) * enn2real ?a)" 293 using r by (simp add: sum_distrib_right ennreal_mult[symmetric]) 294 also have "\<dots> < ennreal (1 * enn2real ?a)" 295 proof (intro ennreal_lessI mult_strict_right_mono) 296 have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)" 297 by (rule sum.cong) (auto simp: powr_realpow powr_divide power_divide powr_minus_divide) 298 also have "{1..<Suc n} = {..<Suc n} - {0}" by auto 299 also have "sum ((^) (1 / 2::real)) ({..<Suc n} - {0}) = 300 sum ((^) (1 / 2)) ({..<Suc n}) - 1" by (auto simp: sum_diff1) 301 also have "\<dots> < 1" by (subst geometric_sum) auto 302 finally show "(\<Sum>i = 1..n. 2 powr - enn2real i) < 1" by simp 303 qed (auto simp: r enn2real_positive_iff) 304 also have "\<dots> = ?a" by (auto simp: r) 305 also have "\<dots> \<le> \<mu>G (Z n)" 306 using J by (auto intro: INF_lower simp: Z_def mu_G_spec) 307 finally have "\<mu>G (Z n) - \<mu>G (Y n) < \<mu>G (Z n)" . 308 hence R: "\<mu>G (Z n) < \<mu>G (Z n) + \<mu>G (Y n)" 309 using \<open>\<mu>G (Y n) \<noteq> \<infinity>\<close> by (auto simp: zero_less_iff_neq_zero) 310 then have "\<mu>G (Y n) > 0" 311 by simp 312 thus "Y n \<noteq> {}" using positive_mu_G by (auto simp add: positive_def) 313 qed 314 hence "\<forall>n\<in>{1..}. \<exists>y. y \<in> Y n" by auto 315 then obtain y where y: "\<And>n. n \<ge> 1 \<Longrightarrow> y n \<in> Y n" unfolding bchoice_iff by force 316 { 317 fix t and n m::nat 318 assume "1 \<le> n" "n \<le> m" hence "1 \<le> m" by simp 319 from Y_mono[OF \<open>m \<ge> n\<close>] y[OF \<open>1 \<le> m\<close>] have "y m \<in> Y n" by auto 320 also have "\<dots> \<subseteq> Z' n" using Y_Z'[OF \<open>1 \<le> n\<close>] . 321 finally 322 have "fm n (restrict (y m) (J n)) \<in> K' n" 323 unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff) 324 moreover have "finmap_of (J n) (restrict (y m) (J n)) = finmap_of (J n) (y m)" 325 using J by (simp add: fm_def) 326 ultimately have "fm n (y m) \<in> K' n" by simp 327 } note fm_in_K' = this 328 interpret finmap_seqs_into_compact "\<lambda>n. K' (Suc n)" "\<lambda>k. fm (Suc k) (y (Suc k))" borel 329 proof 330 fix n show "compact (K' n)" by fact 331 next 332 fix n 333 from Y_mono[of n "Suc n"] y[of "Suc n"] have "y (Suc n) \<in> Y (Suc n)" by auto 334 also have "\<dots> \<subseteq> Z' (Suc n)" using Y_Z' by auto 335 finally 336 have "fm (Suc n) (restrict (y (Suc n)) (J (Suc n))) \<in> K' (Suc n)" 337 unfolding Z'_def K_def prod_emb_iff by (simp add: Z'_def K_def prod_emb_iff) 338 thus "K' (Suc n) \<noteq> {}" by auto 339 fix k 340 assume "k \<in> K' (Suc n)" 341 with K'[of "Suc n"] sets.sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto 342 then obtain b where "k = fm (Suc n) b" by auto 343 thus "domain k = domain (fm (Suc n) (y (Suc n)))" 344 by (simp_all add: fm_def) 345 next 346 fix t and n m::nat 347 assume "n \<le> m" hence "Suc n \<le> Suc m" by simp 348 assume "t \<in> domain (fm (Suc n) (y (Suc n)))" 349 then obtain j where j: "t = Utn j" "j \<in> J (Suc n)" by auto 350 hence "j \<in> J (Suc m)" using J_mono[OF \<open>Suc n \<le> Suc m\<close>] by auto 351 have img: "fm (Suc n) (y (Suc m)) \<in> K' (Suc n)" using \<open>n \<le> m\<close> 352 by (intro fm_in_K') simp_all 353 show "(fm (Suc m) (y (Suc m)))\<^sub>F t \<in> (\<lambda>k. (k)\<^sub>F t) ` K' (Suc n)" 354 apply (rule image_eqI[OF _ img]) 355 using \<open>j \<in> J (Suc n)\<close> \<open>j \<in> J (Suc m)\<close> 356 unfolding j by (subst proj_fm, auto)+ 357 qed 358 have "\<forall>t. \<exists>z. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> z" 359 using diagonal_tendsto .. 360 then obtain z where z: 361 "\<And>t. (\<lambda>i. (fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> z t" 362 unfolding choice_iff by blast 363 { 364 fix n :: nat assume "n \<ge> 1" 365 have "\<And>i. domain (fm n (y (Suc (diagseq i)))) = domain (finmap_of (Utn ` J n) z)" 366 by simp 367 moreover 368 { 369 fix t 370 assume t: "t \<in> domain (finmap_of (Utn ` J n) z)" 371 hence "t \<in> Utn ` J n" by simp 372 then obtain j where j: "t = Utn j" "j \<in> J n" by auto 373 have "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> z t" 374 apply (subst (2) tendsto_iff, subst eventually_sequentially) 375 proof safe 376 fix e :: real assume "0 < e" 377 { fix i and x :: "'i \<Rightarrow> 'a" assume i: "i \<ge> n" 378 assume "t \<in> domain (fm n x)" 379 hence "t \<in> domain (fm i x)" using J_mono[OF \<open>i \<ge> n\<close>] by auto 380 with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t" 381 using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn]) 382 } note index_shift = this 383 have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n" 384 apply (rule le_SucI) 385 apply (rule order_trans) apply simp 386 apply (rule seq_suble[OF subseq_diagseq]) 387 done 388 from z 389 have "\<exists>N. \<forall>i\<ge>N. dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" 390 unfolding tendsto_iff eventually_sequentially using \<open>0 < e\<close> by auto 391 then obtain N where N: "\<And>i. i \<ge> N \<Longrightarrow> 392 dist ((fm (Suc (diagseq i)) (y (Suc (diagseq i))))\<^sub>F t) (z t) < e" by auto 393 show "\<exists>N. \<forall>na\<ge>N. dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e " 394 proof (rule exI[where x="max N n"], safe) 395 fix na assume "max N n \<le> na" 396 hence "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) = 397 dist ((fm (Suc (diagseq na)) (y (Suc (diagseq na))))\<^sub>F t) (z t)" using t 398 by (subst index_shift[OF I]) auto 399 also have "\<dots> < e" using \<open>max N n \<le> na\<close> by (intro N) simp 400 finally show "dist ((fm n (y (Suc (diagseq na))))\<^sub>F t) (z t) < e" . 401 qed 402 qed 403 hence "(\<lambda>i. (fm n (y (Suc (diagseq i))))\<^sub>F t) \<longlonglongrightarrow> (finmap_of (Utn ` J n) z)\<^sub>F t" 404 by (simp add: tendsto_intros) 405 } ultimately 406 have "(\<lambda>i. fm n (y (Suc (diagseq i)))) \<longlonglongrightarrow> finmap_of (Utn ` J n) z" 407 by (rule tendsto_finmap) 408 hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) \<longlonglongrightarrow> finmap_of (Utn ` J n) z" 409 by (rule LIMSEQ_subseq_LIMSEQ) (simp add: strict_mono_def) 410 moreover 411 have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)" 412 apply (auto simp add: o_def intro!: fm_in_K' \<open>1 \<le> n\<close> le_SucI) 413 apply (rule le_trans) 414 apply (rule le_add2) 415 using seq_suble[OF subseq_diagseq] 416 apply auto 417 done 418 moreover 419 from \<open>compact (K' n)\<close> have "closed (K' n)" by (rule compact_imp_closed) 420 ultimately 421 have "finmap_of (Utn ` J n) z \<in> K' n" 422 unfolding closed_sequential_limits by blast 423 also have "finmap_of (Utn ` J n) z = fm n (\<lambda>i. z (Utn i))" 424 unfolding finmap_eq_iff 425 proof clarsimp 426 fix i assume i: "i \<in> J n" 427 hence "from_nat_into (\<Union>n. J n) (Utn i) = i" 428 unfolding Utn_def 429 by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto 430 with i show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)" 431 by (simp add: finmap_eq_iff fm_def compose_def) 432 qed 433 finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" . 434 moreover 435 let ?J = "\<Union>n. J n" 436 have "(?J \<inter> J n) = J n" by auto 437 ultimately have "restrict (\<lambda>i. z (Utn i)) (?J \<inter> J n) \<in> K n" 438 unfolding K_def by (auto simp: space_P space_PiM) 439 hence "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z' n" unfolding Z'_def 440 using J by (auto simp: prod_emb_def PiE_def extensional_def) 441 also have "\<dots> \<subseteq> Z n" using Z' by simp 442 finally have "restrict (\<lambda>i. z (Utn i)) ?J \<in> Z n" . 443 } note in_Z = this 444 hence "(\<Inter>i\<in>{1..}. Z i) \<noteq> {}" by auto 445 thus "(\<Inter>i. Z i) \<noteq> {}" 446 using INT_decseq_offset[OF antimonoI[OF Z_mono]] by simp 447qed fact+ 448 449lemma measure_lim_emb: 450 "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" 451 unfolding measure_def by (subst emeasure_lim_emb) auto 452 453end 454 455hide_const (open) PiF 456hide_const (open) Pi\<^sub>F 457hide_const (open) Pi' 458hide_const (open) finmap_of 459hide_const (open) proj 460hide_const (open) domain 461hide_const (open) basis_finmap 462 463sublocale polish_projective \<subseteq> P: prob_space lim 464proof 465 have *: "emb I {} {\<lambda>x. undefined} = space (\<Pi>\<^sub>M i\<in>I. borel)" 466 by (auto simp: prod_emb_def space_PiM) 467 interpret prob_space "P {}" 468 using prob_space_P by simp 469 show "emeasure lim (space lim) = 1" 470 using emeasure_lim_emb[of "{}" "{\<lambda>x. undefined}"] emeasure_space_1 471 by (simp add: * PiM_empty space_P) 472qed 473 474locale polish_product_prob_space = 475 product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set" 476 477sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)" 478 .. 479 480lemma (in polish_product_prob_space) limP_eq_PiM: "lim = PiM I (\<lambda>_. borel)" 481 by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb) 482 483end 484