equal
deleted
inserted
replaced
155 qed |
155 qed |
156 from compactE'[OF compact_projset this] guess ls rs . |
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) |
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 |
158 qed |
159 |
159 |
160 lemma (in finmap_seqs_into_compact) |
160 lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" |
161 diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" |
|
162 proof - |
161 proof - |
163 have "\<And>i n0. (f o seqseq i) i = f (diagseq i)" unfolding diagseq_def by simp |
162 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" |
163 from reducer_reduces obtain l where l: "(\<lambda>i. ((f \<circ> seqseq (Suc n)) i)\<^isub>F n) ----> l" |
165 unfolding seqseq_reducer |
164 unfolding seqseq_reducer |
166 by auto |
165 by auto |
189 for I::"'i set" and P |
188 for I::"'i set" and P |
190 begin |
189 begin |
191 |
190 |
192 abbreviation "lim\<^isub>B \<equiv> (\<lambda>J P. limP J (\<lambda>_. borel) P)" |
191 abbreviation "lim\<^isub>B \<equiv> (\<lambda>J P. limP J (\<lambda>_. borel) P)" |
193 |
192 |
194 lemma |
193 lemma emeasure_limB_emb_not_empty: |
195 emeasure_limB_emb_not_empty: |
|
196 assumes "I \<noteq> {}" |
194 assumes "I \<noteq> {}" |
197 assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel" |
195 assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel" |
198 shows "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (lim\<^isub>B J P) (Pi\<^isub>E J B)" |
196 shows "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (lim\<^isub>B J P) (Pi\<^isub>E J B)" |
199 proof - |
197 proof - |
200 let ?\<Omega> = "\<Pi>\<^isub>E i\<in>I. space borel" |
198 let ?\<Omega> = "\<Pi>\<^isub>E i\<in>I. space borel" |
689 product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set" |
687 product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set" |
690 |
688 |
691 sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)" |
689 sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)" |
692 proof qed |
690 proof qed |
693 |
691 |
694 lemma (in polish_product_prob_space) |
692 lemma (in polish_product_prob_space) limP_eq_PiM: |
695 limP_eq_PiM: |
|
696 "I \<noteq> {} \<Longrightarrow> lim\<^isub>P I (\<lambda>_. borel) (\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)) = |
693 "I \<noteq> {} \<Longrightarrow> lim\<^isub>P I (\<lambda>_. borel) (\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)) = |
697 PiM I (\<lambda>_. borel)" |
694 PiM I (\<lambda>_. borel)" |
698 by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb) |
695 by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb) |
699 |
696 |
700 end |
697 end |