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

author | hoelzl |

Wed, 07 Dec 2011 15:10:29 +0100 | |

changeset 45777 | c36637603821 |

parent 45776 | 714100f5fda4 |

child 45778 | df6e210fb44c |

remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

--- a/src/HOL/Probability/Binary_Product_Measure.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Wed Dec 07 15:10:29 2011 +0100 @@ -315,12 +315,9 @@ subsection {* Binary products of $\sigma$-finite measure spaces *} -locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 +locale pair_sigma_finite = pair_sigma_algebra M1 M2 + M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" -sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 - by default - lemma (in pair_sigma_finite) measure_cut_measurable_fst: assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") proof - @@ -919,10 +916,7 @@ show "a \<in> A" and "b \<in> B" by auto qed -locale pair_finite_sigma_algebra = M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2 - for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" - -sublocale pair_finite_sigma_algebra \<subseteq> pair_sigma_algebra by default +locale pair_finite_sigma_algebra = pair_sigma_algebra M1 M2 + M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2 for M1 M2 lemma (in pair_finite_sigma_algebra) finite_pair_sigma_algebra: shows "P = \<lparr> space = space M1 \<times> space M2, sets = Pow (space M1 \<times> space M2), \<dots> = algebra.more P \<rparr>" @@ -933,20 +927,16 @@ qed sublocale pair_finite_sigma_algebra \<subseteq> finite_sigma_algebra P - apply default - using M1.finite_space M2.finite_space - apply (subst finite_pair_sigma_algebra) apply simp - apply (subst (1 2) finite_pair_sigma_algebra) apply simp - done +proof + show "finite (space P)" + using M1.finite_space M2.finite_space + by (subst finite_pair_sigma_algebra) simp + show "sets P = Pow (space P)" + by (subst (1 2) finite_pair_sigma_algebra) simp +qed -locale pair_finite_space = M1: finite_measure_space M1 + M2: finite_measure_space M2 - for M1 M2 - -sublocale pair_finite_space \<subseteq> pair_finite_sigma_algebra - by default - -sublocale pair_finite_space \<subseteq> pair_sigma_finite - by default +locale pair_finite_space = pair_sigma_finite M1 M2 + pair_finite_sigma_algebra M1 M2 + + M1: finite_measure_space M1 + M2: finite_measure_space M2 for M1 M2 lemma (in pair_finite_space) pair_measure_Pair[simp]: assumes "a \<in> space M1" "b \<in> space M2" @@ -964,6 +954,10 @@ using pair_measure_Pair assms by (cases x) auto sublocale pair_finite_space \<subseteq> finite_measure_space P - by default (auto simp: space_pair_measure) +proof unfold_locales + show "measure P (space P) \<noteq> \<infinity>" + by (subst (2) finite_pair_sigma_algebra) + (simp add: pair_measure_times) +qed end \ No newline at end of file

--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Dec 07 15:10:29 2011 +0100 @@ -240,7 +240,7 @@ locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" + fixes I :: "'i set" - assumes finite_index: "finite I" + assumes finite_index[simp, intro]: "finite I" definition "product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)), @@ -508,22 +508,15 @@ finally show "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M \<in> sets M" . qed -locale product_sigma_finite = - fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +locale product_sigma_finite = product_sigma_algebra M + for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" + assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)" -locale finite_product_sigma_finite = product_sigma_finite M - for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" + - fixes I :: "'i set" assumes finite_index'[intro]: "finite I" - sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i by (rule sigma_finite_measures) -sublocale product_sigma_finite \<subseteq> product_sigma_algebra - by default - -sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra - by default (fact finite_index') +locale finite_product_sigma_finite = finite_product_sigma_algebra M I + product_sigma_finite M + for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set" lemma (in finite_product_sigma_finite) product_algebra_generator_measure: assumes "Pi\<^isub>E I F \<in> sets G"

--- a/src/HOL/Probability/Independent_Family.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Independent_Family.thy Wed Dec 07 15:10:29 2011 +0100 @@ -845,8 +845,8 @@ moreover have "D.prob A = P.prob A" proof (rule prob_space_unique_Int_stable) - show "prob_space ?D'" by default - show "prob_space (Pi\<^isub>M I ?M)" by default + show "prob_space ?D'" by unfold_locales + show "prob_space (Pi\<^isub>M I ?M)" by unfold_locales show "Int_stable P.G" using M'.Int by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def) show "space P.G \<in> sets P.G" @@ -963,13 +963,13 @@ unfolding space_pair_measure[simplified pair_measure_def space_sigma] using X.top Y.top by (auto intro!: pair_measure_generatorI) - show "prob_space ?J" by default + show "prob_space ?J" by unfold_locales show "space ?J = space ?P" by (simp add: pair_measure_generator_def space_pair_measure) show "sets ?J = sets (sigma ?P)" by (simp add: pair_measure_def) - show "prob_space XY.P" by default + show "prob_space XY.P" by unfold_locales show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)" by (simp_all add: pair_measure_generator_def pair_measure_def)

--- a/src/HOL/Probability/Infinite_Product_Measure.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Dec 07 15:10:29 2011 +0100 @@ -41,36 +41,11 @@ qed qed -locale product_prob_space = - fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set" - assumes prob_spaces: "\<And>i. prob_space (M i)" - and I_not_empty: "I \<noteq> {}" - -locale finite_product_prob_space = product_prob_space M I - for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set" + - assumes finite_index'[intro]: "finite I" - -sublocale product_prob_space \<subseteq> M: prob_space "M i" for i - by (rule prob_spaces) - -sublocale product_prob_space \<subseteq> product_sigma_finite - by default - -sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite - by default (fact finite_index') - -sublocale finite_product_prob_space \<subseteq> prob_space "Pi\<^isub>M I M" -proof - show "measure P (space P) = 1" - by (simp add: measure_times measure_space_1 setprod_1) -qed - lemma (in product_prob_space) measure_preserving_restrict: assumes "J \<noteq> {}" "J \<subseteq> K" "finite K" shows "(\<lambda>f. restrict f J) \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i)" (is "?R \<in> _") proof - - interpret K: finite_product_prob_space M K - by default (insert assms, auto) + interpret K: finite_product_prob_space M K by default fact have J: "J \<noteq> {}" "finite J" using assms by (auto simp add: finite_subset) interpret J: finite_product_prob_space M J by default (insert J, auto) @@ -297,7 +272,7 @@ definition (in product_prob_space) infprod_algebra :: "('i \<Rightarrow> 'a) measure_space" where "infprod_algebra = sigma generator \<lparr> measure := (SOME \<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and> - measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>" + prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>" syntax "_PiP" :: "[pttrn, 'i set, ('b, 'd) measure_space_scheme] => ('i => 'b, 'd) measure_space_scheme" ("(3PIP _:_./ _)" 10) @@ -314,13 +289,13 @@ translations "PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)" -sublocale product_prob_space \<subseteq> G!: algebra generator +lemma (in product_prob_space) algebra_generator: + assumes "I \<noteq> {}" shows "algebra generator" proof let ?G = generator show "sets ?G \<subseteq> Pow (space ?G)" by (auto simp: generator_def emb_def) - from I_not_empty - obtain i where "i \<in> I" by auto + from `I \<noteq> {}` obtain i where "i \<in> I" by auto then show "{} \<in> sets ?G" by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"] simp: product_algebra_def sigma_def sigma_sets.Empty generator_def emb_def) @@ -343,42 +318,54 @@ using XA XB by (auto intro!: generatorI') qed -lemma (in product_prob_space) positive_\<mu>G: "positive generator \<mu>G" -proof (intro positive_def[THEN iffD2] conjI ballI) - from generatorE[OF G.empty_sets] guess J X . note this[simp] - interpret J: finite_product_sigma_finite M J by default fact - have "X = {}" - by (rule emb_injective[of J I]) simp_all - then show "\<mu>G {} = 0" by simp -next - fix A assume "A \<in> sets generator" - from generatorE[OF this] guess J X . note this[simp] - interpret J: finite_product_sigma_finite M J by default fact - show "0 \<le> \<mu>G A" by simp +lemma (in product_prob_space) positive_\<mu>G: + assumes "I \<noteq> {}" + shows "positive generator \<mu>G" +proof - + interpret G!: algebra generator by (rule algebra_generator) fact + show ?thesis + proof (intro positive_def[THEN iffD2] conjI ballI) + from generatorE[OF G.empty_sets] guess J X . note this[simp] + interpret J: finite_product_sigma_finite M J by default fact + have "X = {}" + by (rule emb_injective[of J I]) simp_all + then show "\<mu>G {} = 0" by simp + next + fix A assume "A \<in> sets generator" + from generatorE[OF this] guess J X . note this[simp] + interpret J: finite_product_sigma_finite M J by default fact + show "0 \<le> \<mu>G A" by simp + qed qed -lemma (in product_prob_space) additive_\<mu>G: "additive generator \<mu>G" -proof (intro additive_def[THEN iffD2] ballI impI) - fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this - fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this - assume "A \<inter> B = {}" - have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)" - using J K by auto - interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact - have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}" - apply (rule emb_injective[of "J \<union> K" I]) - apply (insert `A \<inter> B = {}` JK J K) - apply (simp_all add: JK.Int emb_simps) - done - have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)" - using J K by simp_all - then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))" - by (simp add: emb_simps) - also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)" - using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un) - also have "\<dots> = \<mu>G A + \<mu>G B" - using J K JK_disj by (simp add: JK.measure_additive[symmetric]) - finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" . +lemma (in product_prob_space) additive_\<mu>G: + assumes "I \<noteq> {}" + shows "additive generator \<mu>G" +proof - + interpret G!: algebra generator by (rule algebra_generator) fact + show ?thesis + proof (intro additive_def[THEN iffD2] ballI impI) + fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this + fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this + assume "A \<inter> B = {}" + have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)" + using J K by auto + interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact + have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}" + apply (rule emb_injective[of "J \<union> K" I]) + apply (insert `A \<inter> B = {}` JK J K) + apply (simp_all add: JK.Int emb_simps) + done + have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)" + using J K by simp_all + then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))" + by (simp add: emb_simps) + also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)" + using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un) + also have "\<dots> = \<mu>G A + \<mu>G B" + using J K JK_disj by (simp add: JK.measure_additive[symmetric]) + finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" . + qed qed lemma (in product_prob_space) finite_index_eq_finite_product: @@ -386,7 +373,7 @@ shows "sets (sigma generator) = sets (Pi\<^isub>M I M)" proof safe interpret I: finite_product_sigma_algebra M I by default fact - have [simp]: "space generator = space (Pi\<^isub>M I M)" + have space_generator[simp]: "space generator = space (Pi\<^isub>M I M)" by (simp add: generator_def product_algebra_def) { fix A assume "A \<in> sets (sigma generator)" then show "A \<in> sets I.P" unfolding sets_sigma @@ -396,19 +383,32 @@ with `finite I` have "emb I J X \<in> sets I.P" by auto with `emb I J X = A` show "A \<in> sets I.P" by simp qed auto } - { fix A assume "A \<in> sets I.P" - moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto - ultimately show "A \<in> sets (sigma generator)" - using `finite I` I_not_empty unfolding sets_sigma - by (intro sigma_sets.Basic generatorI[of I A]) auto } + { fix A assume A: "A \<in> sets I.P" + show "A \<in> sets (sigma generator)" + proof cases + assume "I = {}" + with I.P_empty[OF this] A + have "A = space generator \<or> A = {}" + unfolding space_generator by auto + then show ?thesis + by (auto simp: sets_sigma simp del: space_generator + intro: sigma_sets.Empty sigma_sets_top) + next + assume "I \<noteq> {}" + note A this + moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto + ultimately show "A \<in> sets (sigma generator)" + using `finite I` unfolding sets_sigma + by (intro sigma_sets.Basic generatorI[of I A]) auto + qed } qed lemma (in product_prob_space) extend_\<mu>G: "\<exists>\<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and> - measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>" + prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>" proof cases assume "finite I" - interpret I: finite_product_sigma_finite M I by default fact + interpret I: finite_product_prob_space M I by default fact show ?thesis proof (intro exI[of _ "measure (Pi\<^isub>M I M)"] ballI conjI) fix A assume "A \<in> sets generator" @@ -422,13 +422,20 @@ have "\<lparr>space = space generator, sets = sets (sigma generator), measure = measure I.P\<rparr> = I.P" (is "?P = _") by (auto intro!: measure_space.equality simp: finite_index_eq_finite_product[OF `finite I`]) - then show "measure_space ?P" by simp default + show "prob_space ?P" + proof + show "measure_space ?P" using `?P = I.P` by simp default + show "measure ?P (space ?P) = 1" + using I.measure_space_1 by simp + qed qed next let ?G = generator assume "\<not> finite I" + then have I_not_empty: "I \<noteq> {}" by auto + interpret G!: algebra generator by (rule algebra_generator) fact note \<mu>G_mono = - G.additive_increasing[OF positive_\<mu>G additive_\<mu>G, THEN increasingD] + G.additive_increasing[OF positive_\<mu>G[OF I_not_empty] additive_\<mu>G[OF I_not_empty], THEN increasingD] { fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> sets ?G" @@ -488,7 +495,9 @@ note this fold le_1 merge_in_G(3) } note fold = this - show ?thesis + have "\<exists>\<mu>. (\<forall>s\<in>sets ?G. \<mu> s = \<mu>G s) \<and> + measure_space \<lparr>space = space ?G, sets = sets (sigma ?G), measure = \<mu>\<rparr>" + (is "\<exists>\<mu>. _ \<and> measure_space (?ms \<mu>)") proof (rule G.caratheodory_empty_continuous[OF positive_\<mu>G additive_\<mu>G]) fix A assume "A \<in> sets ?G" with generatorE guess J X . note JX = this @@ -503,7 +512,7 @@ proof (rule ccontr) assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0") moreover have "0 \<le> ?a" - using A positive_\<mu>G by (auto intro!: INF_greatest simp: positive_def) + using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def) ultimately have "0 < ?a" by auto have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = measure (Pi\<^isub>M J M) X" @@ -659,7 +668,7 @@ moreover from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto then have "?M (J k) (A k) (w k) \<noteq> {}" - using positive_\<mu>G[unfolded positive_def] `0 < ?a` `?a \<le> 1` + using positive_\<mu>G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq) then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto @@ -713,28 +722,42 @@ qed ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0" using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp + qed fact+ + then guess \<mu> .. note \<mu> = this + show ?thesis + proof (intro exI[of _ \<mu>] conjI) + show "\<forall>S\<in>sets ?G. \<mu> S = \<mu>G S" using \<mu> by simp + show "prob_space (?ms \<mu>)" + proof + show "measure_space (?ms \<mu>)" using \<mu> by simp + obtain i where "i \<in> I" using I_not_empty by auto + interpret i: finite_product_sigma_finite M "{i}" by default auto + let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)" + have X: "?X \<in> sets (Pi\<^isub>M {i} M)" + by auto + with `i \<in> I` have "emb I {i} ?X \<in> sets generator" + by (intro generatorI') auto + with \<mu> have "\<mu> (emb I {i} ?X) = \<mu>G (emb I {i} ?X)" by auto + with \<mu>G_eq[OF _ _ _ X] `i \<in> I` + have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))" + by (simp add: i.measure_times) + also have "emb I {i} ?X = space (Pi\<^isub>P I M)" + using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def) + finally show "measure (?ms \<mu>) (space (?ms \<mu>)) = 1" + using M.measure_space_1 by (simp add: infprod_algebra_def) + qed qed qed lemma (in product_prob_space) infprod_spec: - shows "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> measure_space (Pi\<^isub>P I M)" -proof - - let ?P = "\<lambda>\<mu>. (\<forall>A\<in>sets generator. \<mu> A = \<mu>G A) \<and> - measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>" - have **: "measure infprod_algebra = (SOME \<mu>. ?P \<mu>)" - unfolding infprod_algebra_def by simp - have *: "Pi\<^isub>P I M = \<lparr>space = space generator, sets = sets (sigma generator), measure = measure (Pi\<^isub>P I M)\<rparr>" - unfolding infprod_algebra_def by auto - show ?thesis - apply (subst (2) *) - apply (unfold **) - apply (rule someI_ex[where P="?P"]) - apply (rule extend_\<mu>G) - done -qed + "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> prob_space (Pi\<^isub>P I M)" + (is "?Q infprod_algebra") + unfolding infprod_algebra_def + by (rule someI2_ex[OF extend_\<mu>G]) + (auto simp: sigma_def generator_def) -sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M" - using infprod_spec by auto +sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M" + using infprod_spec by simp lemma (in product_prob_space) measure_infprod_emb: assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" @@ -745,22 +768,6 @@ with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto qed -sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M" -proof - obtain i where "i \<in> I" using I_not_empty by auto - interpret i: finite_product_sigma_finite M "{i}" by default auto - let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)" - have "?X \<in> sets (Pi\<^isub>M {i} M)" - by auto - from measure_infprod_emb[OF _ _ _ this] `i \<in> I` - have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))" - by (simp add: i.measure_times) - also have "emb I {i} ?X = space (Pi\<^isub>P I M)" - using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def) - finally show "\<mu> (space (Pi\<^isub>P I M)) = 1" - using M.measure_space_1 by simp -qed - lemma (in product_prob_space) measurable_component: assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)" @@ -821,7 +828,8 @@ assume "J = {}" then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra" by (auto simp: infprod_algebra_def generator_def sigma_def emb_def) - then show ?thesis using `J = {}` prob_space by simp + then show ?thesis using `J = {}` P.prob_space + by simp next assume "J \<noteq> {}" interpret J: finite_product_prob_space M J by default fact+

--- a/src/HOL/Probability/Information.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Information.thy Wed Dec 07 15:10:29 2011 +0100 @@ -198,7 +198,7 @@ proof - interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default - have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by default + have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales note RN = RN_deriv[OF ms ac] from real_RN_deriv[OF fms ac] guess D . note D = this @@ -460,7 +460,7 @@ proof - interpret information_space M by default fact interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact - have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by default + have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis . qed @@ -558,7 +558,7 @@ have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A" proof (rule XY.KL_eq_0_imp) - show "prob_space ?J" by default + show "prob_space ?J" by unfold_locales show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)" using ac by (simp add: P_def) show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))" @@ -624,7 +624,7 @@ have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" using X Y by (auto intro!: distribution_prob_space random_variable_pairI) then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" - unfolding prob_space_def by simp + unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp qed auto qed @@ -654,7 +654,7 @@ note rv = assms[THEN finite_random_variableD] show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)" proof (rule XY.absolutely_continuousI) - show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default + show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0" then obtain a b where "x = (a, b)" and "distribution X {a} = 0 \<or> distribution Y {b} = 0" @@ -684,8 +684,8 @@ interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>" using assms by (auto intro!: joint_distribution_finite_prob_space) - have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default - have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default + have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales + have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales show ?sum unfolding Let_def mutual_information_def

--- a/src/HOL/Probability/Measure.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Measure.thy Wed Dec 07 15:10:29 2011 +0100 @@ -1175,13 +1175,21 @@ finally show ?thesis by simp qed -locale finite_measure = measure_space + +locale finite_measure = sigma_finite_measure + assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<infinity>" -sublocale finite_measure < sigma_finite_measure -proof - show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)" - using finite_measure_of_space by (auto intro!: exI[of _ "\<lambda>x. space M"]) +lemma finite_measureI[Pure.intro!]: + assumes "measure_space M" + assumes *: "measure M (space M) \<noteq> \<infinity>" + shows "finite_measure M" +proof - + interpret measure_space M by fact + show "finite_measure M" + proof + show "measure M (space M) \<noteq> \<infinity>" by fact + show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)" + using * by (auto intro!: exI[of _ "\<lambda>x. space M"]) + qed qed lemma (in finite_measure) finite_measure[simp, intro]: @@ -1222,22 +1230,19 @@ assumes "S \<in> sets M" shows "finite_measure (restricted_space S)" (is "finite_measure ?r") - unfolding finite_measure_def finite_measure_axioms_def -proof (intro conjI) +proof show "measure_space ?r" using restricted_measure_space[OF assms] . -next show "measure ?r (space ?r) \<noteq> \<infinity>" using finite_measure[OF `S \<in> sets M`] by auto qed lemma (in measure_space) restricted_to_finite_measure: assumes "S \<in> sets M" "\<mu> S \<noteq> \<infinity>" shows "finite_measure (restricted_space S)" -proof - - have "measure_space (restricted_space S)" +proof + show "measure_space (restricted_space S)" using `S \<in> sets M` by (rule restricted_measure_space) - then show ?thesis - unfolding finite_measure_def finite_measure_axioms_def - using assms by auto + show "measure (restricted_space S) (space (restricted_space S)) \<noteq> \<infinity>" + by simp fact qed lemma (in finite_measure) finite_measure_Diff: @@ -1357,66 +1362,43 @@ section "Finite spaces" -locale finite_measure_space = measure_space + finite_sigma_algebra + - assumes finite_single_measure[simp]: "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<infinity>" +locale finite_measure_space = finite_measure + finite_sigma_algebra + +lemma finite_measure_spaceI[Pure.intro!]: + assumes "finite (space M)" + assumes sets_Pow: "sets M = Pow (space M)" + and space: "measure M (space M) \<noteq> \<infinity>" + and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}" + and add: "\<And>A. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})" + shows "finite_measure_space M" +proof - + interpret finite_sigma_algebra M + proof + show "finite (space M)" by fact + qed (auto simp: sets_Pow) + interpret measure_space M + proof (rule finite_additivity_sufficient) + show "sigma_algebra M" by default + show "finite (space M)" by fact + show "positive M (measure M)" + by (auto simp: add positive_def intro!: setsum_nonneg pos) + show "additive M (measure M)" + using `finite (space M)` + by (auto simp add: additive_def add + intro!: setsum_Un_disjoint dest: finite_subset) + qed + interpret finite_measure M + proof + show "\<mu> (space M) \<noteq> \<infinity>" by fact + qed default + show "finite_measure_space M" + by default +qed lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)" using measure_setsum[of "space M" "\<lambda>i. {i}"] by (simp add: sets_eq_Pow disjoint_family_on_def finite_space) -lemma finite_measure_spaceI: - assumes "finite (space M)" "sets M = Pow(space M)" and space: "measure M (space M) \<noteq> \<infinity>" - and add: "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B" - and "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A" - shows "finite_measure_space M" - unfolding finite_measure_space_def finite_measure_space_axioms_def -proof (intro allI impI conjI) - show "measure_space M" - proof (rule finite_additivity_sufficient) - have *: "\<lparr>space = space M, sets = Pow (space M), \<dots> = algebra.more M\<rparr> = M" - unfolding assms(2)[symmetric] by (auto intro!: algebra.equality) - show "sigma_algebra M" - using sigma_algebra_Pow[of "space M" "algebra.more M"] - unfolding * . - show "finite (space M)" by fact - show "positive M (measure M)" unfolding positive_def using assms by auto - show "additive M (measure M)" unfolding additive_def using assms by simp - qed - then interpret measure_space M . - show "finite_sigma_algebra M" - proof - show "finite (space M)" by fact - show "sets M = Pow (space M)" using assms by auto - qed - { fix x assume *: "x \<in> space M" - with add[of "{x}" "space M - {x}"] space - show "\<mu> {x} \<noteq> \<infinity>" by (auto simp: insert_absorb[OF *] Diff_subset) } -qed - -sublocale finite_measure_space \<subseteq> finite_measure -proof - show "\<mu> (space M) \<noteq> \<infinity>" - unfolding sum_over_space[symmetric] setsum_Pinfty - using finite_space finite_single_measure by auto -qed - -lemma finite_measure_space_iff: - "finite_measure_space M \<longleftrightarrow> - finite (space M) \<and> sets M = Pow(space M) \<and> measure M (space M) \<noteq> \<infinity> \<and> - measure M {} = 0 \<and> (\<forall>A\<subseteq>space M. 0 \<le> measure M A) \<and> - (\<forall>A\<subseteq>space M. \<forall>B\<subseteq>space M. A \<inter> B = {} \<longrightarrow> measure M (A \<union> B) = measure M A + measure M B)" - (is "_ = ?rhs") -proof (intro iffI) - assume "finite_measure_space M" - then interpret finite_measure_space M . - show ?rhs - using finite_space sets_eq_Pow measure_additive empty_measure finite_measure - by auto -next - assume ?rhs then show "finite_measure_space M" - by (auto intro!: finite_measure_spaceI) -qed - lemma (in finite_measure_space) finite_measure_singleton: assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})" using A finite_subset[OF A finite_space]

--- a/src/HOL/Probability/Probability_Measure.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Wed Dec 07 15:10:29 2011 +0100 @@ -9,12 +9,20 @@ imports Lebesgue_Measure begin -locale prob_space = measure_space + +locale prob_space = finite_measure + assumes measure_space_1: "measure M (space M) = 1" -sublocale prob_space < finite_measure -proof - from measure_space_1 show "\<mu> (space M) \<noteq> \<infinity>" by simp +lemma prob_spaceI[Pure.intro!]: + assumes "measure_space M" + assumes *: "measure M (space M) = 1" + shows "prob_space M" +proof - + interpret finite_measure M + proof + show "measure_space M" by fact + show "measure M (space M) \<noteq> \<infinity>" using * by simp + qed + show "prob_space M" by default fact qed abbreviation (in prob_space) "events \<equiv> sets M" @@ -31,9 +39,10 @@ lemma (in prob_space) prob_space_cong: assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M" shows "prob_space N" -proof - - interpret N: measure_space N by (intro measure_space_cong assms) - show ?thesis by default (insert assms measure_space_1, simp) +proof + show "measure_space N" by (intro measure_space_cong assms) + show "measure N (space N) = 1" + using measure_space_1 assms by simp qed lemma (in prob_space) distribution_cong: @@ -201,18 +210,17 @@ assumes S: "sigma_algebra S" assumes T: "T \<in> measure_preserving M S" shows "prob_space S" -proof - +proof interpret S: measure_space S using S and T by (rule measure_space_vimage) - show ?thesis - proof - from T[THEN measure_preservingD2] - have "T -` space S \<inter> space M = space M" - by (auto simp: measurable_def) - with T[THEN measure_preservingD, of "space S", symmetric] - show "measure S (space S) = 1" - using measure_space_1 by simp - qed + show "measure_space S" .. + + from T[THEN measure_preservingD2] + have "T -` space S \<inter> space M = space M" + by (auto simp: measurable_def) + with T[THEN measure_preservingD, of "space S", symmetric] + show "measure S (space S) = 1" + using measure_space_1 by simp qed lemma prob_space_unique_Int_stable: @@ -539,12 +547,14 @@ joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}" unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>']) -locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2 - -sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 M2 by default +locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2 sublocale pair_prob_space \<subseteq> P: prob_space P -by default (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure) +proof + show "measure_space P" .. + show "measure P (space P) = 1" + by (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure) +qed lemma countably_additiveI[case_names countably]: assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow> @@ -557,20 +567,21 @@ shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := ereal \<circ> joint_distribution X Y\<rparr>)" using random_variable_pairI[OF assms] by (rule distribution_prob_space) +locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" + + fixes I :: "'i set" + assumes prob_space: "\<And>i. prob_space (M i)" -locale finite_product_prob_space = - fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" - and I :: "'i set" - assumes prob_space: "\<And>i. prob_space (M i)" and finite_index: "finite I" - -sublocale finite_product_prob_space \<subseteq> M: prob_space "M i" for i +sublocale product_prob_space \<subseteq> M: prob_space "M i" for i by (rule prob_space) -sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite M I - by default (rule finite_index) +locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i" - proof qed (simp add: measure_times M.measure_space_1 setprod_1) +proof + show "measure_space P" .. + show "measure P (space P) = 1" + by (simp add: measure_times M.measure_space_1 setprod_1) +qed lemma (in finite_product_prob_space) prob_times: assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)" @@ -667,7 +678,7 @@ interpret MX: finite_sigma_algebra MX using assms by simp interpret MY: finite_sigma_algebra MY using assms by simp interpret P: pair_finite_sigma_algebra MX MY by default - show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" by default + show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" .. have sa: "sigma_algebra M" by default show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)" unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def) @@ -754,25 +765,9 @@ using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"] using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp -locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2 - -sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default -sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2 by default -sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default +locale pair_finite_prob_space = pair_prob_space M1 M2 + pair_finite_space M1 M2 + M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2 -locale product_finite_prob_space = - fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" - and I :: "'i set" - assumes finite_space: "\<And>i. finite_prob_space (M i)" and finite_index: "finite I" - -sublocale product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space . -sublocale product_finite_prob_space \<subseteq> finite_product_sigma_finite M I by default (rule finite_index) -sublocale product_finite_prob_space \<subseteq> prob_space "Pi\<^isub>M I M" -proof - show "\<mu> (space P) = 1" - using measure_times[OF M.top] M.measure_space_1 - by (simp add: setprod_1 space_product_algebra) -qed +sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default lemma funset_eq_UN_fun_upd_I: assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A" @@ -815,7 +810,12 @@ using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto qed -lemma (in product_finite_prob_space) singleton_eq_product: +locale finite_product_finite_prob_space = finite_product_prob_space M I for M I + + assumes finite_space: "\<And>i. finite_prob_space (M i)" + +sublocale finite_product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space . + +lemma (in finite_product_finite_prob_space) singleton_eq_product: assumes x: "x \<in> space P" shows "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})" proof (safe intro!: ext[of _ x]) fix y i assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I" @@ -823,7 +823,7 @@ by (cases "i \<in> I") (auto simp: extensional_def) qed (insert x, auto) -sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M" +sublocale finite_product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M" proof show "finite (space P)" using finite_index M.finite_space by auto @@ -844,23 +844,18 @@ then show "X \<in> sets P" by simp qed with space_closed show [simp]: "sets P = Pow (space P)" .. - - { fix x assume "x \<in> space P" - from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto - then show "\<mu> {x} \<noteq> \<infinity>" - using measure_space_1 by auto } qed -lemma (in product_finite_prob_space) measure_finite_times: +lemma (in finite_product_finite_prob_space) measure_finite_times: "(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))" by (rule measure_times) simp -lemma (in product_finite_prob_space) measure_singleton_times: +lemma (in finite_product_finite_prob_space) measure_singleton_times: assumes x: "x \<in> space P" shows "\<mu> {x} = (\<Prod>i\<in>I. M.\<mu> i {x i})" unfolding singleton_eq_product[OF x] using x by (intro measure_finite_times) auto -lemma (in product_finite_prob_space) prob_finite_times: +lemma (in finite_product_finite_prob_space) prob_finite_times: assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)" shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))" proof - @@ -873,13 +868,13 @@ finally show ?thesis by simp qed -lemma (in product_finite_prob_space) prob_singleton_times: +lemma (in finite_product_finite_prob_space) prob_singleton_times: assumes x: "x \<in> space P" shows "prob {x} = (\<Prod>i\<in>I. M.prob i {x i})" unfolding singleton_eq_product[OF x] using x by (intro prob_finite_times) auto -lemma (in product_finite_prob_space) prob_finite_product: +lemma (in finite_product_finite_prob_space) prob_finite_product: "A \<subseteq> space P \<Longrightarrow> prob A = (\<Sum>x\<in>A. \<Prod>i\<in>I. M.prob i {x i})" by (auto simp add: finite_measure_singleton prob_singleton_times simp del: space_product_algebra @@ -1010,11 +1005,12 @@ assumes "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" and "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A" shows "prob_space N" -proof - +proof interpret N: measure_space N by (rule measure_space_subalgebra[OF assms]) - show ?thesis - proof qed (insert assms(4)[OF N.top], simp add: assms measure_space_1) + show "measure_space N" .. + show "measure N (space N) = 1" + using assms(4)[OF N.top] by (simp add: assms measure_space_1) qed lemma (in prob_space) prob_space_of_restricted_space: @@ -1028,44 +1024,76 @@ by (rule A.sigma_algebra_cong) auto show "prob_space ?P" proof + show "measure_space ?P" + proof + show "positive ?P (measure ?P)" + proof (simp add: positive_def, safe) + show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def) + fix B assume "B \<in> events" + with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M` + show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int) + qed + show "countably_additive ?P (measure ?P)" + proof (simp add: countably_additive_def, safe) + fix B and F :: "nat \<Rightarrow> 'a set" + assume F: "range F \<subseteq> op \<inter> A ` events" "disjoint_family F" + { fix i + from F have "F i \<in> op \<inter> A ` events" by auto + with `A \<in> events` have "F i \<in> events" by auto } + moreover then have "range F \<subseteq> events" by auto + moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" + by (simp add: mult_commute divide_ereal_def) + moreover have "0 \<le> inverse (\<mu> A)" + using real_measure[OF `A \<in> events`] by auto + ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A" + using measure_countably_additive[of F] F + by (auto simp: suminf_cmult_ereal) + qed + qed show "measure ?P (space ?P) = 1" using real_measure[OF `A \<in> events`] `\<mu> A \<noteq> 0` by auto - show "positive ?P (measure ?P)" - proof (simp add: positive_def, safe) - show "0 / \<mu> A = 0" using `\<mu> A \<noteq> 0` by (cases "\<mu> A") (auto simp: zero_ereal_def) - fix B assume "B \<in> events" - with real_measure[of "A \<inter> B"] real_measure[OF `A \<in> events`] `A \<in> sets M` - show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int) - qed - show "countably_additive ?P (measure ?P)" - proof (simp add: countably_additive_def, safe) - fix B and F :: "nat \<Rightarrow> 'a set" - assume F: "range F \<subseteq> op \<inter> A ` events" "disjoint_family F" - { fix i - from F have "F i \<in> op \<inter> A ` events" by auto - with `A \<in> events` have "F i \<in> events" by auto } - moreover then have "range F \<subseteq> events" by auto - moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S" - by (simp add: mult_commute divide_ereal_def) - moreover have "0 \<le> inverse (\<mu> A)" - using real_measure[OF `A \<in> events`] by auto - ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A" - using measure_countably_additive[of F] F - by (auto simp: suminf_cmult_ereal) - qed qed qed lemma finite_prob_spaceI: assumes "finite (space M)" "sets M = Pow(space M)" - and "measure M (space M) = 1" "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A" - and "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B" + and 1: "measure M (space M) = 1" and "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}" + and add: "\<And>A B. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})" shows "finite_prob_space M" - unfolding finite_prob_space_eq -proof - show "finite_measure_space M" using assms - by (auto intro!: finite_measure_spaceI) - show "measure M (space M) = 1" by fact +proof - + interpret finite_measure_space M + proof + show "measure M (space M) \<noteq> \<infinity>" using 1 by simp + qed fact+ + show ?thesis by default fact +qed + +lemma (in finite_prob_space) distribution_eq_setsum: + "distribution X A = (\<Sum>x\<in>A \<inter> X ` space M. distribution X {x})" +proof - + have *: "X -` A \<inter> space M = (\<Union>x\<in>A \<inter> X ` space M. X -` {x} \<inter> space M)" + by auto + then show "distribution X A = (\<Sum>x\<in>A \<inter> X ` space M. distribution X {x})" + using finite_space unfolding distribution_def * + by (intro finite_measure_finite_Union) + (auto simp: disjoint_family_on_def) +qed + +lemma (in finite_prob_space) distribution_eq_setsum_finite: + assumes "finite A" + shows "distribution X A = (\<Sum>x\<in>A. distribution X {x})" +proof - + note distribution_eq_setsum[of X A] + also have "(\<Sum>x\<in>A \<inter> X ` space M. distribution X {x}) = (\<Sum>x\<in>A. distribution X {x})" + proof (intro setsum_mono_zero_cong_left ballI) + fix i assume "i\<in>A - A \<inter> X ` space M" + then have "X -` {i} \<inter> space M = {}" by auto + then show "distribution X {i} = 0" + by (simp add: distribution_def) + next + show "finite A" by fact + qed simp_all + finally show ?thesis . qed lemma (in finite_prob_space) finite_measure_space: @@ -1075,11 +1103,9 @@ proof (rule finite_measure_spaceI, simp_all) show "finite (X ` space M)" using finite_space by simp next - fix A B :: "'x set" assume "A \<inter> B = {}" - then show "distribution X (A \<union> B) = distribution X A + distribution X B" - unfolding distribution_def - by (subst finite_measure_Union[symmetric]) - (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow) + fix A assume "A \<subseteq> X ` space M" + then show "distribution X A = (\<Sum>x\<in>A. distribution X {x})" + by (subst distribution_eq_setsum) (simp add: Int_absorb2) qed lemma (in finite_prob_space) finite_prob_space_of_images: @@ -1095,11 +1121,9 @@ show "finite (s1 \<times> s2)" using assms by auto next - fix A B :: "('x*'y) set" assume "A \<inter> B = {}" - then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B" - unfolding distribution_def - by (subst finite_measure_Union[symmetric]) - (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow) + fix A assume "A \<subseteq> (s1 \<times> s2)" + with assms show "joint_distribution X Y A = (\<Sum>x\<in>A. joint_distribution X Y {x})" + by (intro distribution_eq_setsum_finite) (auto dest: finite_subset) qed lemma (in finite_prob_space) finite_product_measure_space_of_images: @@ -1140,7 +1164,10 @@ by (simp add: pborel_def) interpretation pborel: prob_space pborel - by default (simp add: one_ereal_def pborel_def) +proof + show "measure pborel (space pborel) = 1" + by (simp add: one_ereal_def pborel_def) +qed default lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 ..< 1} then real (lborel.\<mu> A) else 0)" unfolding pborel.\<mu>'_def by (auto simp: pborel_def)

--- a/src/HOL/Probability/Radon_Nikodym.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 07 15:10:29 2011 +0100 @@ -427,35 +427,38 @@ have f_le_\<nu>: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. ?F A x \<partial>M) \<le> \<nu> A" using `f \<in> G` unfolding G_def by auto have fmM: "finite_measure ?M" - proof (default, simp_all add: countably_additive_def positive_def, safe del: notI) - fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" - have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)" - using `range A \<subseteq> sets M` `\<And>x. 0 \<le> f x` - by (intro positive_integral_suminf[symmetric]) auto - also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" - using `\<And>x. 0 \<le> f x` - by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF `disjoint_family A`]) - finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" . - moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)" - using M'.measure_countably_additive A by (simp add: comp_def) - moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN) - moreover { - have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)" - using A `f \<in> G` unfolding G_def by (auto simp: countable_UN) - also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp - finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp } - moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)" - using A by (intro f_le_\<nu>) auto - ultimately - show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)" - by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive) + proof + show "measure_space ?M" + proof (default, simp_all add: countably_additive_def positive_def, safe del: notI) + fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" + have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)" + using `range A \<subseteq> sets M` `\<And>x. 0 \<le> f x` + by (intro positive_integral_suminf[symmetric]) auto + also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" + using `\<And>x. 0 \<le> f x` + by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF `disjoint_family A`]) + finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" . + moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)" + using M'.measure_countably_additive A by (simp add: comp_def) + moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN) + moreover { + have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)" + using A `f \<in> G` unfolding G_def by (auto simp: countable_UN) + also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp + finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp } + moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)" + using A by (intro f_le_\<nu>) auto + ultimately + show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)" + by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive) + next + fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A - \<integral>\<^isup>+ x. ?F A x \<partial>M" + using f_le_\<nu>[OF A] `f \<in> G` M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff) + qed next - fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A - \<integral>\<^isup>+ x. ?F A x \<partial>M" - using f_le_\<nu>[OF A] `f \<in> G` M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff) - next - show "\<nu> (space M) - (\<integral>\<^isup>+ x. ?F (space M) x \<partial>M) \<noteq> \<infinity>" (is "?a - ?b \<noteq> _") + show "measure ?M (space ?M) \<noteq> \<infinity>" using positive_integral_positive[of "?F (space M)"] - by (cases rule: ereal2_cases[of ?a ?b]) auto + by (cases rule: ereal2_cases[of "\<nu> (space M)" "\<integral>\<^isup>+ x. ?F (space M) x \<partial>M"]) auto qed then interpret M: finite_measure ?M where "space ?M = space M" and "sets ?M = sets M" and "measure ?M = ?t" @@ -498,11 +501,14 @@ interpret b: sigma_algebra ?Mb by (intro sigma_algebra_cong) auto have Mb: "finite_measure ?Mb" proof - show "positive ?Mb (measure ?Mb)" - using `0 \<le> b` by (auto simp: positive_def) - show "countably_additive ?Mb (measure ?Mb)" - using `0 \<le> b` measure_countably_additive - by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq) + show "measure_space ?Mb" + proof + show "positive ?Mb (measure ?Mb)" + using `0 \<le> b` by (auto simp: positive_def) + show "countably_additive ?Mb (measure ?Mb)" + using `0 \<le> b` measure_countably_additive + by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq) + qed show "measure ?Mb (space ?Mb) \<noteq> \<infinity>" using b by auto qed @@ -772,7 +778,6 @@ (is "finite_measure ?R") by (rule restricted_finite_measure[OF Q_sets[of i]]) then interpret R: finite_measure ?R . have fmv: "finite_measure (restricted_space (Q i) \<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?Q") - unfolding finite_measure_def finite_measure_axioms_def proof show "measure_space ?Q" using v.restricted_measure_space Q_sets[of i] by auto @@ -849,8 +854,8 @@ let ?MT = "M\<lparr> measure := ?T \<rparr>" interpret T: finite_measure ?MT where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T" - unfolding finite_measure_def finite_measure_axioms_def using borel finite nn - by (auto intro!: measure_space_density cong: positive_integral_cong) + using borel finite nn + by (auto intro!: measure_space_density finite_measureI cong: positive_integral_cong) have "T.absolutely_continuous \<nu>" proof (unfold T.absolutely_continuous_def, safe) fix N assume "N \<in> sets M" "(\<integral>\<^isup>+x. h x * indicator N x \<partial>M) = 0" @@ -1000,7 +1005,7 @@ using h_borel h_nn by (rule measure_space_density) simp then interpret h: measure_space ?H . interpret h: finite_measure "M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M) \<rparr>" - by default (simp cong: positive_integral_cong add: fin) + by (intro H finite_measureI) (simp cong: positive_integral_cong add: fin) let ?fM = "M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)\<rparr>" interpret f: measure_space ?fM using f by (rule measure_space_density) simp

--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Dec 07 15:10:29 2011 +0100 @@ -22,11 +22,8 @@ by (simp_all add: M_def) sublocale finite_space \<subseteq> finite_measure_space M -proof (rule finite_measure_spaceI) - fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M" - then show "measure M (A \<union> B) = measure M A + measure M B" - by (simp add: M_def card_Un_disjoint finite_subset[OF _ finite] field_simps) -qed (auto simp: M_def divide_nonneg_nonneg) + by (rule finite_measure_spaceI) + (simp_all add: M_def real_of_nat_def) sublocale finite_space \<subseteq> information_space M 2 by default (simp_all add: M_def one_ereal_def)