1(* Title: HOL/Probability/Projective_Family.thy 2 Author: Fabian Immler, TU M��nchen 3 Author: Johannes H��lzl, TU M��nchen 4*) 5 6section \<open>Projective Family\<close> 7 8theory Projective_Family 9imports Giry_Monad 10begin 11 12lemma vimage_restrict_preseve_mono: 13 assumes J: "J \<subseteq> I" 14 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> {}" 15 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)" 16 shows "A \<subseteq> B" 17proof (intro subsetI) 18 fix x assume "x \<in> A" 19 from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto 20 have "J \<inter> (I - J) = {}" by auto 21 show "x \<in> B" 22 proof cases 23 assume x: "x \<in> (\<Pi>\<^sub>E i\<in>J. S i)" 24 have "merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i)" 25 using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> 26 by (auto simp del: PiE_cancel_merge simp add: Un_absorb1) 27 also have "\<dots> \<subseteq> (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)" by fact 28 finally show "x \<in> B" 29 using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S] \<open>x\<in>A\<close> eq 30 by (auto simp del: PiE_cancel_merge simp add: Un_absorb1) 31 qed (insert \<open>x\<in>A\<close> sets, auto) 32qed 33 34locale projective_family = 35 fixes I :: "'i set" and P :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M :: "'i \<Rightarrow> 'a measure" 36 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)" 37 assumes prob_space_P: "\<And>J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> prob_space (P J)" 38begin 39 40lemma sets_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (P J) = sets (PiM J M)" 41 by (subst P[of J J]) simp_all 42 43lemma space_P: "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> space (P J) = space (PiM J M)" 44 using sets_P by (rule sets_eq_imp_space_eq) 45 46lemma not_empty_M: "i \<in> I \<Longrightarrow> space (M i) \<noteq> {}" 47 using prob_space_P[THEN prob_space.not_empty] by (auto simp: space_PiM space_P) 48 49lemma not_empty: "space (PiM I M) \<noteq> {}" 50 by (simp add: not_empty_M) 51 52abbreviation 53 "emb L K \<equiv> prod_emb L M K" 54 55lemma emb_preserve_mono: 56 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)" 57 assumes "emb L J X \<subseteq> emb L J Y" 58 shows "X \<subseteq> Y" 59proof (rule vimage_restrict_preseve_mono) 60 show "X \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^sub>E i\<in>J. space (M i))" 61 using sets[THEN sets.sets_into_space] by (auto simp: space_PiM) 62 show "(\<Pi>\<^sub>E i\<in>L. space (M i)) \<noteq> {}" 63 using \<open>L \<subseteq> I\<close> by (auto simp add: not_empty_M space_PiM[symmetric]) 64 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))" 65 using \<open>prod_emb L M J X \<subseteq> prod_emb L M J Y\<close> by (simp add: prod_emb_def) 66qed fact 67 68lemma emb_injective: 69 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)" 70 shows "emb L J X = emb L J Y \<Longrightarrow> X = Y" 71 by (intro antisym emb_preserve_mono[OF L X Y] emb_preserve_mono[OF L Y X]) auto 72 73lemma 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" 74 by (auto intro!: emeasure_distr_restrict[symmetric] simp: P sets_P) 75 76inductive_set generator :: "('i \<Rightarrow> 'a) set set" where 77 "finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emb I J X \<in> generator" 78 79lemma algebra_generator: "algebra (space (PiM I M)) generator" 80 unfolding algebra_iff_Int 81proof (safe elim!: generator.cases) 82 fix J X assume J: "finite J" "J \<subseteq> I" and X: "X \<in> sets (PiM J M)" 83 84 from X[THEN sets.sets_into_space] J show "x \<in> emb I J X \<Longrightarrow> x \<in> space (PiM I M)" for x 85 by (auto simp: prod_emb_def space_PiM) 86 87 have "emb I J (space (PiM J M) - X) \<in> generator" 88 by (intro generator.intros J sets.Diff sets.top X) 89 with J show "space (Pi\<^sub>M I M) - emb I J X \<in> generator" 90 by (simp add: space_PiM prod_emb_PiE) 91 92 fix K Y assume K: "finite K" "K \<subseteq> I" and Y: "Y \<in> sets (PiM K M)" 93 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" 94 unfolding prod_emb_Int[symmetric] 95 by (intro generator.intros sets.Int measurable_prod_emb) (auto intro!: J K X Y) 96 with J K X Y show "emb I J X \<inter> emb I K Y \<in> generator" 97 by simp 98qed (force simp: generator.simps prod_emb_empty[symmetric]) 99 100interpretation generator: algebra "space (PiM I M)" generator 101 by (rule algebra_generator) 102 103lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator" 104proof (intro antisym sets.sigma_sets_subset) 105 show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) generator" 106 unfolding sets_PiM_single space_PiM[symmetric] 107 proof (intro sigma_sets_mono', safe) 108 fix i A assume "i \<in> I" and A: "A \<in> sets (M i)" 109 then have "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} = emb I {i} (\<Pi>\<^sub>E j\<in>{i}. A)" 110 by (auto simp: prod_emb_def space_PiM restrict_def Pi_iff PiE_iff extensional_def) 111 with \<open>i\<in>I\<close> A show "{f \<in> space (Pi\<^sub>M I M). f i \<in> A} \<in> generator" 112 by (auto intro!: generator.intros sets_PiM_I_finite) 113 qed 114qed (auto elim!: generator.cases) 115 116definition mu_G ("\<mu>G") where 117 "\<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))" 118 119definition lim :: "('i \<Rightarrow> 'a) measure" where 120 "lim = extend_measure (space (PiM I M)) generator (\<lambda>x. x) \<mu>G" 121 122lemma space_lim[simp]: "space lim = space (PiM I M)" 123 using generator.space_closed 124 unfolding lim_def by (intro space_extend_measure) simp 125 126lemma sets_lim[simp, measurable]: "sets lim = sets (PiM I M)" 127 using generator.space_closed by (simp add: lim_def sets_PiM_generator sets_extend_measure) 128 129lemma mu_G_spec: 130 assumes J: "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)" 131 shows "\<mu>G (emb I J X) = emeasure (P J) X" 132 unfolding mu_G_def 133proof (intro the_equality allI impI ballI) 134 fix K Y assume K: "finite K" "K \<subseteq> I" "Y \<in> sets (Pi\<^sub>M K M)" 135 and [simp]: "emb I J X = emb I K Y" 136 have "emeasure (P K) Y = emeasure (P (K \<union> J)) (emb (K \<union> J) K Y)" 137 using K J by (simp add: emeasure_P) 138 also have "emb (K \<union> J) K Y = emb (K \<union> J) J X" 139 using K J by (simp add: emb_injective[of "K \<union> J" I]) 140 also have "emeasure (P (K \<union> J)) (emb (K \<union> J) J X) = emeasure (P J) X" 141 using K J by (subst emeasure_P) simp_all 142 finally show "emeasure (P J) X = emeasure (P K) Y" .. 143qed (insert J, force) 144 145lemma positive_mu_G: "positive generator \<mu>G" 146proof - 147 show ?thesis 148 proof (safe intro!: positive_def[THEN iffD2]) 149 obtain J where "finite J" "J \<subseteq> I" by auto 150 then have "\<mu>G (emb I J {}) = 0" 151 by (subst mu_G_spec) auto 152 then show "\<mu>G {} = 0" by simp 153 qed 154qed 155 156lemma additive_mu_G: "additive generator \<mu>G" 157proof (safe intro!: additive_def[THEN iffD2] elim!: generator.cases) 158 fix J X K Y assume J: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)" 159 and K: "finite K" "K \<subseteq> I" "Y \<in> sets (PiM K M)" 160 and "emb I J X \<inter> emb I K Y = {}" 161 then have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}" 162 by (intro emb_injective[of "J \<union> K" I _ "{}"]) (auto simp: sets.Int prod_emb_Int) 163 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))" 164 using J K by simp 165 also have "\<dots> = emeasure (P (J \<union> K)) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)" 166 using J K by (simp add: mu_G_spec sets.Un del: prod_emb_Un) 167 also have "\<dots> = \<mu>G (emb I J X) + \<mu>G (emb I K Y)" 168 using J K JK_disj by (simp add: plus_emeasure[symmetric] mu_G_spec emeasure_P sets_P) 169 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)" . 170qed 171 172lemma emeasure_lim: 173 assumes JX: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)" 174 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> 175 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> {}" 176 shows "emeasure lim (emb I J X) = P J X" 177proof - 178 have "\<exists>\<mu>. (\<forall>s\<in>generator. \<mu> s = \<mu>G s) \<and> 179 measure_space (space (PiM I M)) (sigma_sets (space (PiM I M)) generator) \<mu>" 180 proof (rule generator.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G]) 181 show "\<And>A. A \<in> generator \<Longrightarrow> \<mu>G A \<noteq> \<infinity>" 182 proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI) 183 fix J assume "finite J" "J \<subseteq> I" 184 then interpret prob_space "P J" by (rule prob_space_P) 185 show "\<And>X. X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emeasure (P J) X \<noteq> top" 186 by simp 187 qed 188 next 189 fix A assume "range A \<subseteq> generator" and "decseq A" "(\<Inter>i. A i) = {}" 190 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)" 191 unfolding image_subset_iff generator.simps by blast 192 then obtain J X where A: "\<And>i. A i = emb I (J i) (X i)" 193 and *: "\<And>i. finite (J i)" "\<And>i. J i \<subseteq> I" "\<And>i. X i \<in> sets (PiM (J i) M)" 194 by metis 195 have "(INF i. P (J i) (X i)) = 0" 196 proof (rule ccontr) 197 assume INF_P: "(INF i. P (J i) (X i)) \<noteq> 0" 198 have "(\<Inter>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i))) \<noteq> {}" 199 proof (rule cont) 200 show "decseq (\<lambda>i. emb I (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))" 201 using * \<open>decseq A\<close> by (subst prod_emb_trans) (auto simp: A[abs_def]) 202 show "0 < (INF i. P (\<Union>n\<le>i. J n) (emb (\<Union>n\<le>i. J n) (J i) (X i)))" 203 using * INF_P by (subst emeasure_P) (auto simp: less_le intro!: INF_greatest) 204 show "incseq (\<lambda>i. \<Union>n\<le>i. J n)" 205 by (force simp: incseq_def) 206 qed (insert *, auto) 207 with \<open>(\<Inter>i. A i) = {}\<close> * show False 208 by (subst (asm) prod_emb_trans) (auto simp: A[abs_def]) 209 qed 210 moreover have "(\<lambda>i. P (J i) (X i)) \<longlonglongrightarrow> (INF i. P (J i) (X i))" 211 proof (intro LIMSEQ_INF antimonoI) 212 fix x y :: nat assume "x \<le> y" 213 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))" 214 using \<open>decseq A\<close>[THEN decseqD, OF \<open>x\<le>y\<close>] * 215 by (auto simp: A sets_P del: subsetI intro!: emeasure_mono \<open>x \<le> y\<close> 216 emb_preserve_mono[of "J y \<union> J x" I, where X="emb (J y \<union> J x) (J y) (X y)"]) 217 then show "P (J y) (X y) \<le> P (J x) (X x)" 218 using * by (simp add: emeasure_P) 219 qed 220 ultimately show "(\<lambda>i. \<mu>G (A i)) \<longlonglongrightarrow> 0" 221 by (auto simp: A[abs_def] mu_G_spec *) 222 qed 223 then obtain \<mu> where eq: "\<forall>s\<in>generator. \<mu> s = \<mu>G s" 224 and ms: "measure_space (space (PiM I M)) (sets (PiM I M)) \<mu>" 225 by (metis sets_PiM_generator) 226 show ?thesis 227 proof (subst emeasure_extend_measure[OF lim_def]) 228 show "A \<in> generator \<Longrightarrow> \<mu> A = \<mu>G A" for A 229 using eq by simp 230 show "positive (sets lim) \<mu>" "countably_additive (sets lim) \<mu>" 231 using ms by (auto simp add: measure_space_def) 232 show "(\<lambda>x. x) ` generator \<subseteq> Pow (space (Pi\<^sub>M I M))" 233 using generator.space_closed by simp 234 show "emb I J X \<in> generator" "\<mu>G (emb I J X) = emeasure (P J) X" 235 using JX by (auto intro: generator.intros simp: mu_G_spec) 236 qed 237qed 238 239end 240 241sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M 242 unfolding projective_family_def 243proof (intro conjI allI impI distr_restrict) 244 show "\<And>J. finite J \<Longrightarrow> prob_space (Pi\<^sub>M J M)" 245 by (intro prob_spaceI) (simp add: space_PiM emeasure_PiM emeasure_space_1) 246qed auto 247 248 249txt \<open> Proof due to Ionescu Tulcea. \<close> 250 251locale Ionescu_Tulcea = 252 fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a measure" and M :: "nat \<Rightarrow> 'a measure" 253 assumes P[measurable]: "\<And>i. P i \<in> measurable (PiM {0..<i} M) (subprob_algebra (M i))" 254 assumes prob_space_P: "\<And>i x. x \<in> space (PiM {0..<i} M) \<Longrightarrow> prob_space (P i x)" 255begin 256 257lemma non_empty[simp]: "space (M i) \<noteq> {}" 258proof (induction i rule: less_induct) 259 case (less i) 260 then obtain x where "\<And>j. j < i \<Longrightarrow> x j \<in> space (M j)" 261 unfolding ex_in_conv[symmetric] by metis 262 then have *: "restrict x {0..<i} \<in> space (PiM {0..<i} M)" 263 by (auto simp: space_PiM PiE_iff) 264 then interpret prob_space "P i (restrict x {0..<i})" 265 by (rule prob_space_P) 266 show ?case 267 using not_empty subprob_measurableD(1)[OF P, OF *] by simp 268qed 269 270lemma space_PiM_not_empty[simp]: "space (PiM UNIV M) \<noteq> {}" 271 unfolding space_PiM_empty_iff by auto 272 273lemma space_P: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (P n x) = space (M n)" 274 by (simp add: P[THEN subprob_measurableD(1)]) 275 276lemma sets_P[measurable_cong]: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (P n x) = sets (M n)" 277 by (simp add: P[THEN subprob_measurableD(2)]) 278 279definition eP :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where 280 "eP n \<omega> = distr (P n \<omega>) (PiM {0..<Suc n} M) (fun_upd \<omega> n)" 281 282lemma measurable_eP[measurable]: 283 "eP n \<in> measurable (PiM {0..< n} M) (subprob_algebra (PiM {0..<Suc n} M))" 284 by (auto simp: eP_def[abs_def] measurable_split_conv 285 intro!: measurable_fun_upd[where J="{0..<n}"] measurable_distr2[OF _ P]) 286 287lemma space_eP: 288 "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (eP n x) = space (PiM {0..<Suc n} M)" 289 by (simp add: measurable_eP[THEN subprob_measurableD(1)]) 290 291lemma sets_eP[measurable]: 292 "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (eP n x) = sets (PiM {0..<Suc n} M)" 293 by (simp add: measurable_eP[THEN subprob_measurableD(2)]) 294 295lemma prob_space_eP: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (eP n x)" 296 unfolding eP_def 297 by (intro prob_space.prob_space_distr prob_space_P measurable_fun_upd[where J="{0..<n}"]) auto 298 299lemma nn_integral_eP: 300 "\<omega> \<in> space (PiM {0..<n} M) \<Longrightarrow> f \<in> borel_measurable (PiM {0..<Suc n} M) \<Longrightarrow> 301 (\<integral>\<^sup>+x. f x \<partial>eP n \<omega>) = (\<integral>\<^sup>+x. f (\<omega>(n := x)) \<partial>P n \<omega>)" 302 unfolding eP_def 303 by (subst nn_integral_distr) (auto intro!: measurable_fun_upd[where J="{0..<n}"] simp: space_PiM PiE_iff) 304 305lemma emeasure_eP: 306 assumes \<omega>[simp]: "\<omega> \<in> space (PiM {0..<n} M)" and A[measurable]: "A \<in> sets (PiM {0..<Suc n} M)" 307 shows "eP n \<omega> A = P n \<omega> ((\<lambda>x. \<omega>(n := x)) -` A \<inter> space (M n))" 308 using nn_integral_eP[of \<omega> n "indicator A"] 309 apply (simp add: sets_eP nn_integral_indicator[symmetric] sets_P del: nn_integral_indicator) 310 apply (subst nn_integral_indicator[symmetric]) 311 using measurable_sets[OF measurable_fun_upd[OF _ measurable_const[OF \<omega>] measurable_id] A, of n] 312 apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator 313 intro!: nn_integral_cong split: split_indicator) 314 done 315 316 317primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where 318 "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>" 319| "C n (Suc m) \<omega> = C n m \<omega> \<bind> eP (n + m)" 320 321lemma measurable_C[measurable]: 322 "C n m \<in> measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))" 323 by (induction m) auto 324 325lemma space_C: 326 "x \<in> space (PiM {0..<n} M) \<Longrightarrow> space (C n m x) = space (PiM {0..<n + m} M)" 327 by (simp add: measurable_C[THEN subprob_measurableD(1)]) 328 329lemma sets_C[measurable_cong]: 330 "x \<in> space (PiM {0..<n} M) \<Longrightarrow> sets (C n m x) = sets (PiM {0..<n + m} M)" 331 by (simp add: measurable_C[THEN subprob_measurableD(2)]) 332 333lemma prob_space_C: "x \<in> space (PiM {0..<n} M) \<Longrightarrow> prob_space (C n m x)" 334proof (induction m) 335 case (Suc m) then show ?case 336 by (auto intro!: prob_space.prob_space_bind[where S="PiM {0..<Suc (n + m)} M"] 337 simp: space_C prob_space_eP) 338qed (auto intro!: prob_space_return simp: space_PiM) 339 340lemma split_C: 341 assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<bind> C (n + m) l) = C n (m + l) \<omega>" 342proof (induction l) 343 case 0 344 with \<omega> show ?case 345 by (simp add: bind_return_distr' prob_space_C[THEN prob_space.not_empty] 346 distr_cong[OF refl sets_C[symmetric, OF \<omega>]]) 347next 348 case (Suc l) with \<omega> show ?case 349 by (simp add: bind_assoc[symmetric, OF _ measurable_eP]) (simp add: ac_simps) 350qed 351 352lemma nn_integral_C: 353 assumes "m \<le> m'" and f[measurable]: "f \<in> borel_measurable (PiM {0..<n+m} M)" 354 and nonneg: "\<And>x. x \<in> space (PiM {0..<n+m} M) \<Longrightarrow> 0 \<le> f x" 355 and x: "x \<in> space (PiM {0..<n} M)" 356 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)" 357 using \<open>m \<le> m'\<close> 358proof (induction rule: dec_induct) 359 case (step i) 360 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" 361 from \<open>m\<le>i\<close> x have "?C i ?E = ?C (Suc i) ?E" 362 by (auto simp: nn_integral_bind[where B="PiM {0 ..< Suc (n + i)} M"] space_C nn_integral_eP 363 intro!: nn_integral_cong) 364 (simp add: space_PiM PiE_iff nonneg prob_space.emeasure_space_1[OF prob_space_P]) 365 with step show ?case by (simp del: restrict_apply) 366qed (auto simp: space_PiM space_C[OF x] simp del: restrict_apply intro!: nn_integral_cong) 367 368lemma emeasure_C: 369 assumes "m \<le> m'" and A[measurable]: "A \<in> sets (PiM {0..<n+m} M)" and [simp]: "x \<in> space (PiM {0..<n} M)" 370 shows "emeasure (C n m' x) (prod_emb {0..<n + m'} M {0..<n+m} A) = emeasure (C n m x) A" 371 using assms 372 by (subst (1 2) nn_integral_indicator[symmetric]) 373 (auto intro!: nn_integral_cong split: split_indicator simp del: nn_integral_indicator 374 simp: nn_integral_C[of m m' _ n] prod_emb_iff space_PiM PiE_iff sets_C space_C) 375 376lemma distr_C: 377 assumes "m \<le> m'" and [simp]: "x \<in> space (PiM {0..<n} M)" 378 shows "C n m x = distr (C n m' x) (PiM {0..<n+m} M) (\<lambda>x. restrict x {0..<n+m})" 379proof (rule measure_eqI) 380 fix A assume "A \<in> sets (C n m x)" 381 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" 382 by (subst emeasure_C[symmetric, OF \<open>m \<le> m'\<close>]) (auto intro!: emeasure_distr_restrict[symmetric] simp: sets_C) 383qed (simp add: sets_C) 384 385definition up_to :: "nat set \<Rightarrow> nat" where 386 "up_to J = (LEAST n. \<forall>i\<ge>n. i \<notin> J)" 387 388lemma up_to_less: "finite J \<Longrightarrow> i \<in> J \<Longrightarrow> i < up_to J" 389 unfolding up_to_def 390 by (rule LeastI2[of _ "Suc (Max J)"]) (auto simp: Suc_le_eq not_le[symmetric]) 391 392lemma up_to_iff: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> (\<forall>i\<in>J. i < n)" 393proof safe 394 show "finite J \<Longrightarrow> up_to J \<le> n \<Longrightarrow> i \<in> J \<Longrightarrow> i < n" for i 395 using up_to_less[of J i] by auto 396qed (auto simp: up_to_def intro!: Least_le) 397 398lemma up_to_iff_Ico: "finite J \<Longrightarrow> up_to J \<le> n \<longleftrightarrow> J \<subseteq> {0..<n}" 399 by (auto simp: up_to_iff) 400 401lemma up_to: "finite J \<Longrightarrow> J \<subseteq> {0..< up_to J}" 402 by (auto simp: up_to_less) 403 404lemma up_to_mono: "J \<subseteq> H \<Longrightarrow> finite H \<Longrightarrow> up_to J \<le> up_to H" 405 by (auto simp add: up_to_iff finite_subset up_to_less) 406 407definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where 408 "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)" 409 410sublocale PF: projective_family UNIV CI 411 unfolding projective_family_def 412proof safe 413 show "finite J \<Longrightarrow> prob_space (CI J)" for J 414 using up_to[of J] unfolding CI_def 415 by (intro prob_space.prob_space_distr prob_space_C measurable_restrict) auto 416 note measurable_cong_sets[OF sets_C, simp] 417 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 418 by (auto intro!: measurable_restrict) 419 420 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 421 by (simp add: CI_def distr_C[OF up_to_mono[of J H]] up_to up_to_mono distr_distr comp_def 422 inf.absorb2 finite_subset) 423qed 424 425lemma emeasure_CI': 426 "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)" 427 unfolding CI_def using up_to[of J] by (rule emeasure_distr_restrict) (auto simp: sets_C) 428 429lemma emeasure_CI: 430 "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)" 431 apply (subst emeasure_CI', simp_all add: finite_subset) 432 apply (subst emeasure_C[symmetric, of "up_to J" n]) 433 apply (auto simp: finite_subset up_to_iff_Ico up_to_less) 434 apply (subst prod_emb_trans) 435 apply (auto simp: up_to_less finite_subset up_to_iff_Ico) 436 done 437 438lemma lim: 439 assumes J: "finite J" and X: "X \<in> sets (PiM J M)" 440 shows "emeasure PF.lim (PF.emb UNIV J X) = emeasure (CI J) X" 441proof (rule PF.emeasure_lim[OF J subset_UNIV X]) 442 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)" 443 and dec: "decseq (\<lambda>i. PF.emb UNIV (J i) (X' i))" 444 define X where "X n = 445 (\<Inter>i\<in>{i. J i \<subseteq> {0..< n}}. PF.emb {0..<n} (J i) (X' i)) \<inter> space (PiM {0..<n} M)" for n 446 447 have sets_X[measurable]: "X n \<in> sets (PiM {0..<n} M)" for n 448 by (cases "{i. J i \<subseteq> {0..< n}} = {}") 449 (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int) 450 451 have dec_X: "n \<le> m \<Longrightarrow> X m \<subseteq> PF.emb {0..<m} {0..<n} (X n)" for n m 452 unfolding X_def using ivl_subset[of 0 n 0 m] 453 by (cases "{i. J i \<subseteq> {0..< n}} = {}") 454 (auto simp add: prod_emb_Int prod_emb_PiE space_PiM simp del: ivl_subset) 455 456 have dec_X': "PF.emb {0..<n} (J j) (X' j) \<subseteq> PF.emb {0..<n} (J i) (X' i)" 457 if [simp]: "J i \<subseteq> {0..<n}" "J j \<subseteq> {0..<n}" "i \<le> j" for n i j 458 by (rule PF.emb_preserve_mono[of "{0..<n}" UNIV]) (auto del: subsetI intro: dec[THEN antimonoD]) 459 460 assume "0 < (INF i. CI (J i) (X' i))" 461 also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))" 462 proof (intro INF_greatest) 463 fix n 464 interpret C: prob_space "C 0 n (\<lambda>x. undefined)" 465 by (rule prob_space_C) simp 466 show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)" 467 proof cases 468 assume "{i. J i \<subseteq> {0..< n}} = {}" with C.emeasure_space_1 show ?thesis 469 by (auto simp add: X_def space_C intro!: INF_lower2[of 0] prob_space.measure_le_1 PF.prob_space_P) 470 next 471 assume *: "{i. J i \<subseteq> {0..< n}} \<noteq> {}" 472 have "(INF i. CI (J i) (X' i)) \<le> 473 (INF i\<in>{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))" 474 by (intro INF_superset_mono) (auto simp: emeasure_CI) 475 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)))" 476 using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C) 477 also have "\<dots> = C 0 n (\<lambda>_. undefined) (X n)" 478 using * by (auto simp add: X_def INT_extend_simps) 479 finally show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>_. undefined) (X n)" . 480 qed 481 qed 482 finally have pos: "0 < (INF i. C 0 i (\<lambda>x. undefined) (X i))" . 483 from less_INF_D[OF this, of 0] have "X 0 \<noteq> {}" 484 by auto 485 486 { fix \<omega> n assume \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" 487 let ?C = "\<lambda>i. emeasure (C n i \<omega>) (X (n + i))" 488 let ?C' = "\<lambda>i x. emeasure (C (Suc n) i (\<omega>(n:=x))) (X (Suc n + i))" 489 have M: "\<And>i. ?C' i \<in> borel_measurable (P n \<omega>)" 490 using \<omega>[measurable, simp] measurable_fun_upd[where J="{0..<n}"] by measurable auto 491 492 assume "0 < (INF i. ?C i)" 493 also have "\<dots> \<le> (INF i. emeasure (C n (1 + i) \<omega>) (X (n + (1 + i))))" 494 by (intro INF_greatest INF_lower) auto 495 also have "\<dots> = (INF i. \<integral>\<^sup>+x. ?C' i x \<partial>P n \<omega>)" 496 using \<omega> measurable_C[of "Suc n"] 497 apply (intro INF_cong refl) 498 apply (subst split_C[symmetric, OF \<omega>]) 499 apply (subst emeasure_bind[OF _ _ sets_X]) 500 apply (simp_all del: C.simps add: space_C) 501 apply measurable 502 apply simp 503 apply (simp add: bind_return[OF measurable_eP] nn_integral_eP) 504 done 505 also have "\<dots> = (\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>)" 506 proof (rule nn_integral_monotone_convergence_INF_AE[symmetric]) 507 have "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) \<le> (\<integral>\<^sup>+x. 1 \<partial>P n \<omega>)" 508 by (intro nn_integral_mono) (auto split: split_indicator) 509 also have "\<dots> < \<infinity>" 510 using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp 511 finally show "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) < \<infinity>" . 512 next 513 show "AE x in P n \<omega>. ?C' (Suc i) x \<le> ?C' i x" for i 514 proof (rule AE_I2) 515 fix x assume "x \<in> space (P n \<omega>)" 516 with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)" 517 by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def) 518 with \<omega> show "?C' (Suc i) x \<le> ?C' i x" 519 apply (subst emeasure_C[symmetric, of i "Suc i"]) 520 apply (auto intro!: emeasure_mono[OF dec_X] del: subsetI 521 simp: sets_C space_P) 522 apply (subst sets_bind[OF sets_eP]) 523 apply (simp_all add: space_C space_P) 524 done 525 qed 526 qed fact 527 finally have "(\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>) \<noteq> 0" 528 by simp 529 with M have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). 0 < (INF i. ?C' i x)" 530 by (subst (asm) nn_integral_0_iff_AE) 531 (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le zero_less_iff_neq_zero) 532 then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). x \<in> space (M n) \<and> 0 < (INF i. ?C' i x)" 533 by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>) 534 then obtain x where "x \<in> space (M n)" "0 < (INF i. ?C' i x)" 535 by (auto dest: frequently_ex) 536 from this(2)[THEN less_INF_D, of 0] this(2) 537 have "\<exists>x. \<omega>(n := x) \<in> X (Suc n) \<and> 0 < (INF i. ?C' i x)" 538 by (intro exI[of _ x]) (simp split: split_indicator_asm) } 539 note step = this 540 541 let ?\<omega> = "\<lambda>\<omega> n x. (restrict \<omega> {0..<n})(n := x)" 542 let ?L = "\<lambda>\<omega> n r. INF i. emeasure (C (Suc n) i (?\<omega> \<omega> n r)) (X (Suc n + i))" 543 have *: "(\<And>i. i < n \<Longrightarrow> ?\<omega> \<omega> i (\<omega> i) \<in> X (Suc i)) \<Longrightarrow> 544 restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" for \<omega> n 545 using sets.sets_into_space[OF sets_X, of n] 546 by (cases n) (auto simp: atLeastLessThanSuc restrict_def[of _ "{}"]) 547 have "\<exists>\<omega>. \<forall>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n) \<and> 0 < ?L \<omega> n (\<omega> n)" 548 proof (rule dependent_wellorder_choice) 549 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)" 550 show "\<exists>r. ?\<omega> \<omega> n r \<in> X (Suc n) \<and> 0 < ?L \<omega> n r" 551 proof (rule step) 552 show "restrict \<omega> {0..<n} \<in> space (Pi\<^sub>M {0..<n} M)" 553 using IH[THEN conjunct1] by (rule *) 554 show "0 < (INF i. emeasure (C n i (restrict \<omega> {0..<n})) (X (n + i)))" 555 proof (cases n) 556 case 0 with pos show ?thesis 557 by (simp add: CI_def restrict_def) 558 next 559 case (Suc i) then show ?thesis 560 using IH[of i, THEN conjunct2] by (simp add: atLeastLessThanSuc) 561 qed 562 qed 563 qed (simp cong: restrict_cong) 564 then obtain \<omega> where \<omega>: "\<And>n. ?\<omega> \<omega> n (\<omega> n) \<in> X (Suc n)" 565 by auto 566 from this[THEN *] have \<omega>_space: "\<omega> \<in> space (PiM UNIV M)" 567 by (auto simp: space_PiM PiE_iff Ball_def) 568 have *: "\<omega> \<in> PF.emb UNIV {0..<n} (X n)" for n 569 proof (cases n) 570 case 0 with \<omega>_space \<open>X 0 \<noteq> {}\<close> sets.sets_into_space[OF sets_X, of 0] show ?thesis 571 by (auto simp add: space_PiM prod_emb_def restrict_def PiE_iff) 572 next 573 case (Suc i) then show ?thesis 574 using \<omega>[of i] \<omega>_space by (auto simp: prod_emb_def space_PiM PiE_iff atLeastLessThanSuc) 575 qed 576 have **: "{i. J i \<subseteq> {0..<up_to (J n)}} \<noteq> {}" for n 577 by (auto intro!: exI[of _ n] up_to J) 578 have "\<omega> \<in> PF.emb UNIV (J n) (X' n)" for n 579 using *[of "up_to (J n)"] up_to[of "J n"] by (simp add: X_def prod_emb_Int prod_emb_INT[OF **]) 580 then show "(\<Inter>i. PF.emb UNIV (J i) (X' i)) \<noteq> {}" 581 by auto 582qed 583 584lemma distr_lim: assumes J[simp]: "finite J" shows "distr PF.lim (PiM J M) (\<lambda>x. restrict x J) = CI J" 585 apply (rule measure_eqI) 586 apply (simp add: CI_def) 587 apply (simp add: emeasure_distr measurable_cong_sets[OF PF.sets_lim] lim[symmetric] prod_emb_def space_PiM) 588 done 589 590end 591 592lemma (in product_prob_space) emeasure_lim_emb: 593 assumes *: "finite J" "J \<subseteq> I" "X \<in> sets (PiM J M)" 594 shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X" 595proof (rule emeasure_lim[OF *], goal_cases) 596 case (1 J X) 597 598 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)" 599 proof cases 600 assume "finite (\<Union>i. J i)" 601 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 602 by (intro distr_restrict[symmetric]) auto 603 then show ?thesis 604 by auto 605 next 606 assume inf: "infinite (\<Union>i. J i)" 607 moreover have count: "countable (\<Union>i. J i)" 608 using 1(3) by (auto intro: countable_finite) 609 define f where "f = from_nat_into (\<Union>i. J i)" 610 define t where "t = to_nat_on (\<Union>i. J i)" 611 have ft[simp]: "x \<in> J i \<Longrightarrow> f (t x) = x" for x i 612 unfolding f_def t_def using inf count by (intro from_nat_into_to_nat_on) auto 613 have tf[simp]: "t (f i) = i" for i 614 unfolding t_def f_def by (intro to_nat_on_from_nat_into_infinite inf count) 615 have inj_t: "inj_on t (\<Union>i. J i)" 616 using count by (auto simp: t_def) 617 then have inj_t_J: "inj_on t (J i)" for i 618 by (rule subset_inj_on) auto 619 interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)" 620 by standard auto 621 interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV 622 by standard 623 have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n 624 proof (induction n) 625 case 0 then show ?case 626 by (auto simp: PiM_empty intro!: measure_eqI dest!: subset_singletonD) 627 next 628 case (Suc n) then show ?case 629 apply (auto intro!: measure_eqI simp: sets_bind[OF IT.sets_eP] emeasure_bind[OF _ IT.measurable_eP]) 630 apply (auto simp: Mf.product_nn_integral_insert nn_integral_indicator[symmetric] atLeastLessThanSuc IT.emeasure_eP space_PiM 631 split: split_indicator simp del: nn_integral_indicator intro!: nn_integral_cong) 632 done 633 qed 634 have CI_eq_PiM: "IT.CI X = PiM X (\<lambda>x. M (f x))" if X: "finite X" for X 635 by (auto simp: IT.up_to_less X IT.CI_def C_eq_PiM intro!: Mf.distr_restrict[symmetric]) 636 637 let ?Q = "distr IT.PF.lim (PiM (\<Union>i. J i) M) (\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x))" 638 { fix i 639 have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = 640 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)))" 641 proof (subst distr_distr) 642 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 643 using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp 644 then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (\<Union>(J ` UNIV)) M)" 645 by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl]) 646 qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton) 647 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))" 648 proof (intro distr_distr[symmetric]) 649 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 650 using measurable_component_singleton[of "t x" "t`J i" "\<lambda>x. M (f x)"] x unfolding ft[OF x] by auto 651 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)" 652 by (auto intro!: measurable_restrict) 653 qed (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl]) 654 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))" 655 using \<open>finite (J i)\<close> by (subst IT.distr_lim) (auto simp: CI_eq_PiM) 656 also have "\<dots> = Pi\<^sub>M (J i) M" 657 using Mf.distr_reorder[of t "J i"] by (simp add: 1 inj_t_J cong: PiM_cong) 658 finally have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" . } 659 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" 660 by (intro exI[of _ ?Q]) auto 661 qed 662 then obtain Q where sets_Q: "sets Q = PiM (\<Union>i. J i) M" 663 and Q: "\<And>i. distr Q (PiM (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M" by blast 664 665 from 1 interpret Q: prob_space Q 666 by (intro prob_space_distrD[of "\<lambda>x. restrict x (J 0)" Q "PiM (J 0) M"]) 667 (auto simp: Q measurable_cong_sets[OF sets_Q] 668 intro!: prob_space_P measurable_restrict measurable_component_singleton) 669 670 have "0 < (INF i. emeasure (Pi\<^sub>M (J i) M) (X i))" by fact 671 also have "\<dots> = (INF i. emeasure Q (emb (\<Union>i. J i) (J i) (X i)))" 672 by (simp add: emeasure_distr_restrict[OF _ sets_Q 1(4), symmetric] SUP_upper Q) 673 also have "\<dots> = emeasure Q (\<Inter>i. emb (\<Union>i. J i) (J i) (X i))" 674 proof (rule INF_emeasure_decseq) 675 from 1 show "decseq (\<lambda>n. emb (\<Union>i. J i) (J n) (X n))" 676 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] 677 measurable_prod_emb) 678 (auto simp: SUP_least SUP_upper antimono_def) 679 qed (insert 1, auto simp: sets_Q) 680 finally have "(\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) \<noteq> {}" 681 by auto 682 moreover have "(\<Inter>i. emb I (J i) (X i)) = {} \<Longrightarrow> (\<Inter>i. emb (\<Union>i. J i) (J i) (X i)) = {}" 683 using 1 by (intro emb_injective[of "\<Union>i. J i" I _ "{}"] sets.countable_INT) (auto simp: SUP_least SUP_upper) 684 ultimately show ?case by auto 685qed 686 687end 688