summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Mon, 19 Nov 2012 18:01:48 +0100 | |

changeset 50125 | 4319691be975 |

parent 50124 | 4161c834c2fd |

child 50126 | 3dec88149176 |

tuned: use induction rule sigma_sets_induct_disjoint

src/HOL/Probability/Projective_Limit.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Probability/Regularity.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Probability/Projective_Limit.thy Mon Nov 19 16:09:11 2012 +0100 +++ b/src/HOL/Probability/Projective_Limit.thy Mon Nov 19 18:01:48 2012 +0100 @@ -157,8 +157,7 @@ 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) qed -lemma (in finmap_seqs_into_compact) - diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" +lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l" proof - have "\<And>i n0. (f o seqseq i) i = f (diagseq i)" unfolding diagseq_def by simp from reducer_reduces obtain l where l: "(\<lambda>i. ((f \<circ> seqseq (Suc n)) i)\<^isub>F n) ----> l" @@ -191,8 +190,7 @@ abbreviation "lim\<^isub>B \<equiv> (\<lambda>J P. limP J (\<lambda>_. borel) P)" -lemma - emeasure_limB_emb_not_empty: +lemma emeasure_limB_emb_not_empty: assumes "I \<noteq> {}" assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel" 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)" @@ -691,8 +689,7 @@ sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)" proof qed -lemma (in polish_product_prob_space) - limP_eq_PiM: +lemma (in polish_product_prob_space) limP_eq_PiM: "I \<noteq> {} \<Longrightarrow> lim\<^isub>P I (\<lambda>_. borel) (\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)) = PiM I (\<lambda>_. borel)" by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb)

--- a/src/HOL/Probability/Regularity.thy Mon Nov 19 16:09:11 2012 +0100 +++ b/src/HOL/Probability/Regularity.thy Mon Nov 19 18:01:48 2012 +0100 @@ -210,11 +210,9 @@ ultimately show "?thesis e " by (auto simp: sU) qed - have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A" - proof - fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed) + { fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed) hence [simp]: "A \<in> sets M" by (simp add: sb) - show "?inner A" + have "?inner A" proof (rule approx_inner) fix e::real assume "e > 0" from approx_space[OF this] obtain K where @@ -237,7 +235,7 @@ ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e" by blast qed simp - show "?outer A" + have "?outer A" proof cases assume "A \<noteq> {}" let ?G = "\<lambda>d. {x. infdist x A < d}" @@ -288,25 +286,25 @@ by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb) ultimately show ?thesis by simp qed (auto intro!: ereal_INFI) - qed - let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}" - interpret dynkin: dynkin_system "space M" ?D - proof (rule dynkin_systemI) - have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU) - hence "?outer (space M)" by (simp add: min_def INF_def) - moreover - have "?inner (space M)" - proof (rule ereal_approx_SUP) - fix e::real assume "0 < e" - thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e" - by (rule approx_space) - qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"]) - ultimately show "space M \<in> ?D" by (simp add: sU sb) + note `?inner A` `?outer A` } + note closed_in_D = this + from `B \<in> sets borel` + have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)" + by (auto simp: Int_stable_def borel_eq_closed) + then show "?inner B" "?outer B" + proof (induct B rule: sigma_sets_induct_disjoint) + case empty + { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto } + { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) } next - fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU) - from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto - hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)" - and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto + case (basic B) + { case 1 from basic closed_in_D show ?case by auto } + { case 2 from basic closed_in_D show ?case by auto } + next + case (compl B) + note inner = compl(2) and outer = compl(3) + from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed) + case 2 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)" unfolding inner by (subst INFI_ereal_cminus) force+ @@ -315,7 +313,7 @@ also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))" by (rule INF_superset_mono) (auto simp add: compact_imp_closed) also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) = - (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)" + (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)" by (subst INF_image[of "\<lambda>u. space M - u", symmetric]) (rule INF_cong, auto simp add: sU intro!: INF_cong) finally have @@ -323,41 +321,39 @@ moreover have "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)" by (auto simp: sb sU intro!: INF_greatest emeasure_mono) - ultimately have "?outer (space M - B)" by simp - moreover - { - have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) - also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" - unfolding outer by (subst SUPR_ereal_cminus) auto - also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))" - by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) - also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)" - by (subst SUP_image[of "\<lambda>u. space M - u", symmetric]) - (rule SUP_cong, auto simp: sU) - also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)" - proof (safe intro!: antisym SUP_least) - fix K assume "closed K" "K \<subseteq> space M - B" - from closed_in_D[OF `closed K`] - have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp - show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)" - unfolding K_inner using `K \<subseteq> space M - B` - by (auto intro!: SUP_upper SUP_least) - qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed) - finally have "?inner (space M - B)" . - } hence "?inner (space M - B)" . - ultimately show "space M - B \<in> ?D" by auto + ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) + + case 1 + have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) + also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" + unfolding outer by (subst SUPR_ereal_cminus) auto + also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))" + by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) + also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)" + by (subst SUP_image[of "\<lambda>u. space M - u", symmetric]) + (rule SUP_cong, auto simp: sU) + also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)" + proof (safe intro!: antisym SUP_least) + fix K assume "closed K" "K \<subseteq> space M - B" + from closed_in_D[OF `closed K`] + have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp + show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)" + unfolding K_inner using `K \<subseteq> space M - B` + by (auto intro!: SUP_upper SUP_least) + qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed) + finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) next - fix D :: "nat \<Rightarrow> _" - assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto - moreover assume "disjoint_family D" - ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure) + case (union D) + then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed) + with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure) also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))" by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg) finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure) have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto - moreover - hence "?inner (\<Union>i. D i)" + + case 1 + show ?case proof (rule approx_inner) fix e::real assume "e > 0" with measure_LIMSEQ @@ -379,7 +375,7 @@ fix i from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos) have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)" - using `range D \<subseteq> ?D` by blast + using union by blast from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this] show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)" by (auto simp: emeasure_eq_measure) @@ -410,8 +406,9 @@ ultimately have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ereal e" by simp thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" .. - qed - moreover have "?outer (\<Union>i. D i)" + qed fact + case 2 + show ?case proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`]) fix e::real assume "e > 0" have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" @@ -419,7 +416,7 @@ fix i::nat from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos) have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)" - using `range D \<subseteq> ?D` by blast + using union by blast from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this] show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" by (auto simp: emeasure_eq_measure) @@ -455,20 +452,7 @@ have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by simp thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ereal e" .. qed - ultimately show "(\<Union>i. D i) \<in> ?D" by safe qed - have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU) - also have "\<dots> = dynkin (space M) (Collect closed)" - proof (rule sigma_eq_dynkin) - show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU) - show "Int_stable (Collect closed)" by (auto simp: Int_stable_def) - qed - also have "\<dots> \<subseteq> ?D" using closed_in_D - by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb) - finally have "sets borel \<subseteq> ?D" . - moreover have "?D \<subseteq> sets borel" by (auto simp: sb) - ultimately have "sets borel = ?D" by simp - with assms show "?inner B" and "?outer B" by auto qed end