# HG changeset patch # User hoelzl # Date 1349863943 -7200 # Node ID 5e5b2da42a69909304c5ad16aaf5a77adeb9383a # Parent 38b84d1802ed70e464094c7e7f7fcad3cf569e02 remove incseq assumption from measure_eqI_generator_eq diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 @@ -385,7 +385,7 @@ then show "sets ?D = sigma_sets (space ?P) ?E" by simp next - show "range F \ ?E" "incseq F" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" + show "range F \ ?E" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" using F by (auto simp: space_pair_measure) next fix X assume "X \ ?E" diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 @@ -751,7 +751,6 @@ show "range ?F \ prod_algebra (I \ J) M" using F using fin by (auto simp: prod_algebra_eq_finite) - show "incseq ?F" by fact show "(\i. \\<^isub>E ia\I \ J. F ia i) = (\\<^isub>E i\I \ J. space (M i))" using F(3) by (simp add: space_PiM) next diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Independent_Family.thy --- a/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Independent_Family.thy Wed Oct 10 12:12:23 2012 +0200 @@ -23,13 +23,6 @@ qed auto definition (in prob_space) - "indep_events A I \ (A`I \ events) \ - (\J\I. J \ {} \ finite J \ prob (\j\J. A j) = (\j\J. prob (A j)))" - -definition (in prob_space) - "indep_event A B \ indep_events (bool_case A B) UNIV" - -definition (in prob_space) "indep_sets F I \ (\i\I. F i \ events) \ (\J\I. J \ {} \ finite J \ (\A\Pi J F. prob (\j\J. A j) = (\j\J. prob (A j))))" @@ -37,6 +30,24 @@ "indep_set A B \ indep_sets (bool_case A B) UNIV" definition (in prob_space) + indep_events_def_alt: "indep_events A I \ indep_sets (\i. {A i}) I" + +lemma image_subset_iff_funcset: "F ` A \ B \ F \ A \ B" + by auto + +lemma (in prob_space) indep_events_def: + "indep_events A I \ (A`I \ events) \ + (\J\I. J \ {} \ finite J \ prob (\j\J. A j) = (\j\J. prob (A j)))" + unfolding indep_events_def_alt indep_sets_def + apply (simp add: Ball_def Pi_iff image_subset_iff_funcset) + apply (intro conj_cong refl arg_cong[where f=All] ext imp_cong) + apply auto + done + +definition (in prob_space) + "indep_event A B \ indep_events (bool_case A B) UNIV" + +definition (in prob_space) "indep_vars M' X I \ (\i\I. random_variable (M' i) (X i)) \ indep_sets (\i. sigma_sets (space M) { X i -` A \ space M | A. A \ sets (M' i)}) I" @@ -48,11 +59,6 @@ "I = J \ (\i. i \ I \ F i = G i) \ indep_sets F I \ indep_sets G J" by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+ -lemma (in prob_space) indep_sets_singleton_iff_indep_events: - "indep_sets (\i. {F i}) I \ indep_events F I" - unfolding indep_sets_def indep_events_def - by (simp, intro conj_cong ball_cong all_cong imp_cong) (auto simp: Pi_iff) - lemma (in prob_space) indep_events_finite_index_events: "indep_events F I \ (\J\I. J \ {} \ finite J \ indep_events F J)" by (auto simp: indep_events_def) @@ -660,7 +666,7 @@ show "indep_sets (\i. sigma_sets (space M) {F i}) UNIV" proof (rule indep_sets_sigma) show "indep_sets (\i. {F i}) UNIV" - unfolding indep_sets_singleton_iff_indep_events by fact + unfolding indep_events_def_alt[symmetric] by fact fix i show "Int_stable {F i}" unfolding Int_stable_def by simp qed @@ -892,7 +898,7 @@ show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')" by (simp add: sets_PiM space_PiM cong: prod_algebra_cong) let ?A = "\i. \\<^isub>E i\I. space (M' i)" - show "range ?A \ prod_algebra I M'" "incseq ?A" "(\i. ?A i) = space (Pi\<^isub>M I M')" + show "range ?A \ prod_algebra I M'" "(\i. ?A i) = space (Pi\<^isub>M I M')" by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong) { fix i show "emeasure ?D (\\<^isub>E i\I. space (M' i)) \ \" by auto } next @@ -1042,7 +1048,7 @@ then show "sets M = sigma_sets (space ?P) ?E" using sets[symmetric] by simp next - show "range F \ ?E" "incseq F" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" + show "range F \ ?E" "(\i. F i) = space ?P" "\i. emeasure ?P (F i) \ \" using F by (auto simp: space_pair_measure) next fix X assume "X \ ?E" diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:23 2012 +0200 @@ -87,7 +87,7 @@ let ?\ = "(\\<^isub>E k\J. space (M k))" show "Int_stable ?J" by (rule Int_stable_PiE) - show "range ?F \ ?J" "incseq ?F" "(\i. ?F i) = ?\" + show "range ?F \ ?J" "(\i. ?F i) = ?\" using `finite J` by (auto intro!: prod_algebraI_finite) { fix i show "emeasure ?P (?F i) \ \" by simp } show "?J \ Pow ?\" by (auto simp: Pi_iff dest: sets_into_space) diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Oct 10 12:12:23 2012 +0200 @@ -569,7 +569,6 @@ by (simp_all add: borel_eq_atLeastAtMost sets_eq) show "range cube \ ?E" unfolding cube_def [abs_def] by auto - show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI) { fix x :: 'a have "\n. x \ cube n" using mem_big_cube[of x] by fastforce } then show "(\i. cube i :: 'a set) = UNIV" by auto diff -r 38b84d1802ed -r 5e5b2da42a69 src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Wed Oct 10 12:12:23 2012 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Wed Oct 10 12:12:23 2012 +0200 @@ -628,7 +628,7 @@ and eq: "\X. X \ E \ emeasure M X = emeasure N X" and M: "sets M = sigma_sets \ E" and N: "sets N = sigma_sets \ E" - and A: "range A \ E" "incseq A" "(\i. A i) = \" "\i. emeasure M (A i) \ \" + and A: "range A \ E" "(\i. A i) = \" "\i. emeasure M (A i) \ \" shows "M = N" proof - let ?\ = "emeasure M" and ?\ = "emeasure N" @@ -673,25 +673,38 @@ have *: "sigma_sets \ E = ?D" using `F \ E` `Int_stable E` by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq) - have "\D. D \ sigma_sets \ E \ ?\ (F \ D) = ?\ (F \ D)" - by (subst (asm) *) auto } + have "\D. D \ sets M \ emeasure M (F \ D) = emeasure N (F \ D)" + unfolding M by (subst (asm) *) auto } note * = this show "M = N" proof (rule measure_eqI) show "sets M = sets N" using M N by simp + have [simp, intro]: "\i. A i \ sets M" + using A(1) by (auto simp: subset_eq M) fix F assume "F \ sets M" - then have "F \ sigma_sets \ E" - using M by simp - let ?A = "\i. A i \ F" - have "range ?A \ sigma_sets \ E" "incseq ?A" - using A(1,2) `F \ sigma_sets \ E` by (auto simp: incseq_def) - moreover - { fix i have "?\ (?A i) = ?\ (?A i)" - using *[of "A i" F] `F \ sigma_sets \ E` A finite by auto } - ultimately show "?\ F = ?\ F" - using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `F \ sigma_sets \ E` - by (auto simp: M N SUP_emeasure_incseq) + let ?D = "disjointed (\i. F \ A i)" + have "space M = \" + using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \ E` by blast + then have F_eq: "F = (\i. ?D i)" + using `F \ sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq) + have [simp, intro]: "\i. ?D i \ sets M" + using range_disjointed_sets[of "\i. F \ A i" M] `F \ sets M` + by (auto simp: subset_eq) + have "disjoint_family ?D" + by (auto simp: disjoint_family_disjointed) + moreover + { fix i + have "A i \ ?D i = ?D i" + by (auto simp: disjointed_def) + then have "emeasure M (?D i) = emeasure N (?D i)" + using *[of "A i" "?D i", OF _ A(3)] A(1) by auto } + ultimately show "emeasure M F = emeasure N F" + using N M + apply (subst (1 2) F_eq) + apply (subst (1 2) suminf_emeasure[symmetric]) + apply auto + done qed qed