# HG changeset patch
# User hoelzl
# Date 1353344508 -3600
# Node ID 4319691be975f2a65c06fd1055d9e42b8cb91f6d
# Parent 4161c834c2fdefd0aaf4f6d87e5611f82fea4100
tuned: use induction rule sigma_sets_induct_disjoint
diff -r 4161c834c2fd -r 4319691be975 src/HOL/Probability/Projective_Limit.thy
--- 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 "\r'. subseq r' \ (\l. (\i. ((f \ (s \ r')) i)\<^isub>F n) ----> l)" by (auto simp: o_def)
qed
-lemma (in finmap_seqs_into_compact)
- diagonal_tendsto: "\l. (\i. (f (diagseq i))\<^isub>F n) ----> l"
+lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\l. (\i. (f (diagseq i))\<^isub>F n) ----> l"
proof -
have "\i n0. (f o seqseq i) i = f (diagseq i)" unfolding diagseq_def by simp
from reducer_reduces obtain l where l: "(\i. ((f \ seqseq (Suc n)) i)\<^isub>F n) ----> l"
@@ -191,8 +190,7 @@
abbreviation "lim\<^isub>B \ (\J P. limP J (\_. borel) P)"
-lemma
- emeasure_limB_emb_not_empty:
+lemma emeasure_limB_emb_not_empty:
assumes "I \ {}"
assumes X: "J \ {}" "J \ I" "finite J" "\i\J. B i \ 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 \ P: polish_projective I "\J. PiM J (\_. borel::('a) measure)"
proof qed
-lemma (in polish_product_prob_space)
- limP_eq_PiM:
+lemma (in polish_product_prob_space) limP_eq_PiM:
"I \ {} \ lim\<^isub>P I (\_. borel) (\J. PiM J (\_. borel::('a) measure)) =
PiM I (\_. borel)"
by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb)
diff -r 4161c834c2fd -r 4319691be975 src/HOL/Probability/Regularity.thy
--- 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: "\A. closed A \ ?inner A \ ?outer A"
- proof
- fix A::"'a set" assume "closed A" hence "A \ sets borel" by (simp add: compact_imp_closed)
+ { fix A::"'a set" assume "closed A" hence "A \ sets borel" by (simp add: compact_imp_closed)
hence [simp]: "A \ 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 "\K \ A. compact K \ emeasure M A \ emeasure M K + ereal e"
by blast
qed simp
- show "?outer A"
+ have "?outer A"
proof cases
assume "A \ {}"
let ?G = "\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 \ sets M. ?inner B \ ?outer B}"
- interpret dynkin: dynkin_system "space M" ?D
- proof (rule dynkin_systemI)
- have "{U::'a set. space M \ U \ 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 "\K\{K. K \ space M \ compact K}. emeasure M (space M) \ 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 \ ?D" by (simp add: sU sb)
+ note `?inner A` `?outer A` }
+ note closed_in_D = this
+ from `B \ sets borel`
+ have "Int_stable (Collect closed)" "Collect closed \ Pow UNIV" "B \ 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 \ ?D" thus "B \ space M" by (simp add: sU)
- from `B \ ?D` have [simp]: "B \ sets M" and "?inner B" "?outer B" by auto
- hence inner: "emeasure M B = (SUP K:{K. K \ B \ compact K}. emeasure M K)"
- and outer: "emeasure M B = (INF U:{U. B \ U \ 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 \ 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 "\ = (INF K:{K. K \ B \ compact K}. M (space M) - M K)"
unfolding inner by (subst INFI_ereal_cminus) force+
@@ -315,7 +313,7 @@
also have "\ \ (INF U:{U. U \ B \ closed U}. M (space M - U))"
by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
also have "(INF U:{U. U \ B \ closed U}. M (space M - U)) =
- (INF U:{U. space M - B \ U \ open U}. emeasure M U)"
+ (INF U:{U. space M - B \ U \ open U}. emeasure M U)"
by (subst INF_image[of "\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 \ U \ open U}. emeasure M U) \ 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 "\ = (SUP U: {U. B \ U \ open U}. M (space M) - M U)"
- unfolding outer by (subst SUPR_ereal_cminus) auto
- also have "\ = (SUP U:{U. B \ U \ open U}. M (space M - U))"
- by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
- also have "\ = (SUP K:{K. K \ space M - B \ closed K}. emeasure M K)"
- by (subst SUP_image[of "\u. space M - u", symmetric])
- (rule SUP_cong, auto simp: sU)
- also have "\ = (SUP K:{K. K \ space M - B \ compact K}. emeasure M K)"
- proof (safe intro!: antisym SUP_least)
- fix K assume "closed K" "K \ space M - B"
- from closed_in_D[OF `closed K`]
- have K_inner: "emeasure M K = (SUP K:{Ka. Ka \ K \ compact Ka}. emeasure M K)" by simp
- show "emeasure M K \ (SUP K:{K. K \ space M - B \ compact K}. emeasure M K)"
- unfolding K_inner using `K \ 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 \ ?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 "\ = (SUP U: {U. B \ U \ open U}. M (space M) - M U)"
+ unfolding outer by (subst SUPR_ereal_cminus) auto
+ also have "\ = (SUP U:{U. B \ U \ open U}. M (space M - U))"
+ by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
+ also have "\ = (SUP K:{K. K \ space M - B \ closed K}. emeasure M K)"
+ by (subst SUP_image[of "\u. space M - u", symmetric])
+ (rule SUP_cong, auto simp: sU)
+ also have "\ = (SUP K:{K. K \ space M - B \ compact K}. emeasure M K)"
+ proof (safe intro!: antisym SUP_least)
+ fix K assume "closed K" "K \ space M - B"
+ from closed_in_D[OF `closed K`]
+ have K_inner: "emeasure M K = (SUP K:{Ka. Ka \ K \ compact Ka}. emeasure M K)" by simp
+ show "emeasure M K \ (SUP K:{K. K \ space M - B \ compact K}. emeasure M K)"
+ unfolding K_inner using `K \ 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 \ _"
- assume "range D \ ?D" hence "range D \ sets M" by auto
- moreover assume "disjoint_family D"
- ultimately have M[symmetric]: "(\i. M (D i)) = M (\i. D i)" by (rule suminf_emeasure)
+ case (union D)
+ then have "range D \ sets M" by (auto simp: sb borel_eq_closed)
+ with union have M[symmetric]: "(\i. M (D i)) = M (\i. D i)" by (intro suminf_emeasure)
also have "(\n. \i\{0.. (\i. M (D i))"
by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
finally have measure_LIMSEQ: "(\n. \i = 0.. measure M (\i. D i)"
by (simp add: emeasure_eq_measure)
have "(\i. D i) \ sets M" using `range D \ sets M` by auto
- moreover
- hence "?inner (\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 \ (D i) \ compact K}. emeasure M K)"
- using `range D \ ?D` by blast
+ using union by blast
from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
show "\K. K \ D i \ compact K \ emeasure M (D i) \ emeasure M K + e/(2*Suc n0)"
by (auto simp: emeasure_eq_measure)
@@ -410,8 +406,9 @@
ultimately
have "?K\(\i. D i) \ compact ?K \ emeasure M (\i. D i) \ emeasure M ?K + ereal e" by simp
thus "\K\\i. D i. compact K \ emeasure M (\i. D i) \ emeasure M K + ereal e" ..
- qed
- moreover have "?outer (\i. D i)"
+ qed fact
+ case 2
+ show ?case
proof (rule approx_outer[OF `(\i. D i) \ sets M`])
fix e::real assume "e > 0"
have "\i::nat. \U. D i \ U \ open U \ 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) \ U \ open U}. emeasure M U)"
- using `range D \ ?D` by blast
+ using union by blast
from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
show "\U. D i \ U \ open U \ e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
by (auto simp: emeasure_eq_measure)
@@ -455,20 +452,7 @@
have "(\i. D i) \ ?U \ open ?U \ emeasure M ?U \ emeasure M (\i. D i) + ereal e" by simp
thus "\B. (\i. D i) \ B \ open B \ emeasure M B \ emeasure M (\i. D i) + ereal e" ..
qed
- ultimately show "(\i. D i) \ ?D" by safe
qed
- have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
- also have "\ = dynkin (space M) (Collect closed)"
- proof (rule sigma_eq_dynkin)
- show "Collect closed \ 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 "\ \ ?D" using closed_in_D
- by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
- finally have "sets borel \ ?D" .
- moreover have "?D \ 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