# HG changeset patch # User hoelzl # Date 1323267029 -3600 # Node ID c36637603821a010650e35cba4e569c4abcf06ae # Parent 714100f5fda4949be68dcd0411771977cfae4bcc 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 diff -r 714100f5fda4 -r c36637603821 src/HOL/Probability/Binary_Product_Measure.thy --- 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 \ pair_sigma_algebra M1 M2 - by default - lemma (in pair_sigma_finite) measure_cut_measurable_fst: assumes "Q \ sets P" shows "(\x. measure M2 (Pair x -` Q)) \ borel_measurable M1" (is "?s Q \ _") proof - @@ -919,10 +916,7 @@ show "a \ A" and "b \ 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 \ 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 = \ space = space M1 \ space M2, sets = Pow (space M1 \ space M2), \ = algebra.more P \" @@ -933,20 +927,16 @@ qed sublocale pair_finite_sigma_algebra \ 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 \ pair_finite_sigma_algebra - by default - -sublocale pair_finite_space \ 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 \ space M1" "b \ space M2" @@ -964,6 +954,10 @@ using pair_measure_Pair assms by (cases x) auto sublocale pair_finite_space \ finite_measure_space P - by default (auto simp: space_pair_measure) +proof unfold_locales + show "measure P (space P) \ \" + by (subst (2) finite_pair_sigma_algebra) + (simp add: pair_measure_times) +qed end \ No newline at end of file diff -r 714100f5fda4 -r c36637603821 src/HOL/Probability/Finite_Product_Measure.thy --- 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 \ ('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 = \ space = (\\<^isub>E i \ I. space (M i)), @@ -508,22 +508,15 @@ finally show "(\x. \i\I. X i x) -` E \ space M \ sets M" . qed -locale product_sigma_finite = - fixes M :: "'i \ ('a,'b) measure_space_scheme" +locale product_sigma_finite = product_sigma_algebra M + for M :: "'i \ ('a,'b) measure_space_scheme" + assumes sigma_finite_measures: "\i. sigma_finite_measure (M i)" -locale finite_product_sigma_finite = product_sigma_finite M - for M :: "'i \ ('a,'b) measure_space_scheme" + - fixes I :: "'i set" assumes finite_index'[intro]: "finite I" - sublocale product_sigma_finite \ M: sigma_finite_measure "M i" for i by (rule sigma_finite_measures) -sublocale product_sigma_finite \ product_sigma_algebra - by default - -sublocale finite_product_sigma_finite \ 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 \ ('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 \ sets G" diff -r 714100f5fda4 -r c36637603821 src/HOL/Probability/Independent_Family.thy --- 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 \ 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) diff -r 714100f5fda4 -r c36637603821 src/HOL/Probability/Infinite_Product_Measure.thy --- 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 \ ('a,'b) measure_space_scheme" and I :: "'i set" - assumes prob_spaces: "\i. prob_space (M i)" - and I_not_empty: "I \ {}" - -locale finite_product_prob_space = product_prob_space M I - for M :: "'i \ ('a,'b) measure_space_scheme" and I :: "'i set" + - assumes finite_index'[intro]: "finite I" - -sublocale product_prob_space \ M: prob_space "M i" for i - by (rule prob_spaces) - -sublocale product_prob_space \ product_sigma_finite - by default - -sublocale finite_product_prob_space \ finite_product_sigma_finite - by default (fact finite_index') - -sublocale finite_product_prob_space \ 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 \ {}" "J \ K" "finite K" shows "(\f. restrict f J) \ measure_preserving (\\<^isub>M i\K. M i) (\\<^isub>M i\J. M i)" (is "?R \ _") 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 \ {}" "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 \ 'a) measure_space" where "infprod_algebra = sigma generator \ measure := (SOME \. (\s\sets generator. \ s = \G s) \ - measure_space \space = space generator, sets = sets (sigma generator), measure = \\)\" + prob_space \space = space generator, sets = sets (sigma generator), measure = \\)\" 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 \ G!: algebra generator +lemma (in product_prob_space) algebra_generator: + assumes "I \ {}" shows "algebra generator" proof let ?G = generator show "sets ?G \ Pow (space ?G)" by (auto simp: generator_def emb_def) - from I_not_empty - obtain i where "i \ I" by auto + from `I \ {}` obtain i where "i \ I" by auto then show "{} \ sets ?G" by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\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_\G: "positive generator \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 "\G {} = 0" by simp -next - fix A assume "A \ 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 \ \G A" by simp +lemma (in product_prob_space) positive_\G: + assumes "I \ {}" + shows "positive generator \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 "\G {} = 0" by simp + next + fix A assume "A \ 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 \ \G A" by simp + qed qed -lemma (in product_prob_space) additive_\G: "additive generator \G" -proof (intro additive_def[THEN iffD2] ballI impI) - fix A assume "A \ sets generator" with generatorE guess J X . note J = this - fix B assume "B \ sets generator" with generatorE guess K Y . note K = this - assume "A \ B = {}" - have JK: "J \ K \ {}" "J \ K \ I" "finite (J \ K)" - using J K by auto - interpret JK: finite_product_sigma_finite M "J \ K" by default fact - have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}" - apply (rule emb_injective[of "J \ K" I]) - apply (insert `A \ B = {}` JK J K) - apply (simp_all add: JK.Int emb_simps) - done - have AB: "A = emb I (J \ K) (emb (J \ K) J X)" "B = emb I (J \ K) (emb (J \ K) K Y)" - using J K by simp_all - then have "\G (A \ B) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))" - by (simp add: emb_simps) - also have "\ = measure (Pi\<^isub>M (J \ K) M) (emb (J \ K) J X \ emb (J \ K) K Y)" - using JK J(1, 4) K(1, 4) by (simp add: \G_eq JK.Un) - also have "\ = \G A + \G B" - using J K JK_disj by (simp add: JK.measure_additive[symmetric]) - finally show "\G (A \ B) = \G A + \G B" . +lemma (in product_prob_space) additive_\G: + assumes "I \ {}" + shows "additive generator \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 \ sets generator" with generatorE guess J X . note J = this + fix B assume "B \ sets generator" with generatorE guess K Y . note K = this + assume "A \ B = {}" + have JK: "J \ K \ {}" "J \ K \ I" "finite (J \ K)" + using J K by auto + interpret JK: finite_product_sigma_finite M "J \ K" by default fact + have JK_disj: "emb (J \ K) J X \ emb (J \ K) K Y = {}" + apply (rule emb_injective[of "J \ K" I]) + apply (insert `A \ B = {}` JK J K) + apply (simp_all add: JK.Int emb_simps) + done + have AB: "A = emb I (J \ K) (emb (J \ K) J X)" "B = emb I (J \ K) (emb (J \ K) K Y)" + using J K by simp_all + then have "\G (A \ B) = \G (emb I (J \ K) (emb (J \ K) J X \ emb (J \ K) K Y))" + by (simp add: emb_simps) + also have "\ = measure (Pi\<^isub>M (J \ K) M) (emb (J \ K) J X \ emb (J \ K) K Y)" + using JK J(1, 4) K(1, 4) by (simp add: \G_eq JK.Un) + also have "\ = \G A + \G B" + using J K JK_disj by (simp add: JK.measure_additive[symmetric]) + finally show "\G (A \ B) = \G A + \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 \ sets (sigma generator)" then show "A \ sets I.P" unfolding sets_sigma @@ -396,19 +383,32 @@ with `finite I` have "emb I J X \ sets I.P" by auto with `emb I J X = A` show "A \ sets I.P" by simp qed auto } - { fix A assume "A \ sets I.P" - moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto - ultimately show "A \ 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 \ sets I.P" + show "A \ sets (sigma generator)" + proof cases + assume "I = {}" + with I.P_empty[OF this] A + have "A = space generator \ 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 \ {}" + note A this + moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto + ultimately show "A \ 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_\G: "\\. (\s\sets generator. \ s = \G s) \ - measure_space \space = space generator, sets = sets (sigma generator), measure = \\" + prob_space \space = space generator, sets = sets (sigma generator), measure = \\" 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 \ sets generator" @@ -422,13 +422,20 @@ have "\space = space generator, sets = sets (sigma generator), measure = measure I.P\ = 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 "\ finite I" + then have I_not_empty: "I \ {}" by auto + interpret G!: algebra generator by (rule algebra_generator) fact note \G_mono = - G.additive_increasing[OF positive_\G additive_\G, THEN increasingD] + G.additive_increasing[OF positive_\G[OF I_not_empty] additive_\G[OF I_not_empty], THEN increasingD] { fix Z J assume J: "J \ {}" "finite J" "J \ I" and Z: "Z \ sets ?G" @@ -488,7 +495,9 @@ note this fold le_1 merge_in_G(3) } note fold = this - show ?thesis + have "\\. (\s\sets ?G. \ s = \G s) \ + measure_space \space = space ?G, sets = sets (sigma ?G), measure = \\" + (is "\\. _ \ measure_space (?ms \)") proof (rule G.caratheodory_empty_continuous[OF positive_\G additive_\G]) fix A assume "A \ sets ?G" with generatorE guess J X . note JX = this @@ -503,7 +512,7 @@ proof (rule ccontr) assume "(INF i. \G (A i)) \ 0" (is "?a \ 0") moreover have "0 \ ?a" - using A positive_\G by (auto intro!: INF_greatest simp: positive_def) + using A positive_\G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def) ultimately have "0 < ?a" by auto have "\n. \J X. J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^isub>M J M) \ A n = emb I J X \ \G (A n) = measure (Pi\<^isub>M J M) X" @@ -659,7 +668,7 @@ moreover from w have "?a / 2 ^ (k + 1) \ ?q k k (w k)" by auto then have "?M (J k) (A k) (w k) \ {}" - using positive_\G[unfolded positive_def] `0 < ?a` `?a \ 1` + using positive_\G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \ 1` by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq) then obtain x where "x \ ?M (J k) (A k) (w k)" by auto then have "merge (J k) (w k) (I - J k) x \ A k" by auto @@ -713,28 +722,42 @@ qed ultimately show "(\i. \G (A i)) ----> 0" using LIMSEQ_ereal_INFI[of "\i. \G (A i)"] by simp + qed fact+ + then guess \ .. note \ = this + show ?thesis + proof (intro exI[of _ \] conjI) + show "\S\sets ?G. \ S = \G S" using \ by simp + show "prob_space (?ms \)" + proof + show "measure_space (?ms \)" using \ by simp + obtain i where "i \ I" using I_not_empty by auto + interpret i: finite_product_sigma_finite M "{i}" by default auto + let ?X = "\\<^isub>E i\{i}. space (M i)" + have X: "?X \ sets (Pi\<^isub>M {i} M)" + by auto + with `i \ I` have "emb I {i} ?X \ sets generator" + by (intro generatorI') auto + with \ have "\ (emb I {i} ?X) = \G (emb I {i} ?X)" by auto + with \G_eq[OF _ _ _ X] `i \ I` + have "\ (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 \ I` by (auto simp: emb_def infprod_algebra_def generator_def) + finally show "measure (?ms \) (space (?ms \)) = 1" + using M.measure_space_1 by (simp add: infprod_algebra_def) + qed qed qed lemma (in product_prob_space) infprod_spec: - shows "(\s\sets generator. measure (Pi\<^isub>P I M) s = \G s) \ measure_space (Pi\<^isub>P I M)" -proof - - let ?P = "\\. (\A\sets generator. \ A = \G A) \ - measure_space \space = space generator, sets = sets (sigma generator), measure = \\" - have **: "measure infprod_algebra = (SOME \. ?P \)" - unfolding infprod_algebra_def by simp - have *: "Pi\<^isub>P I M = \space = space generator, sets = sets (sigma generator), measure = measure (Pi\<^isub>P I M)\" - unfolding infprod_algebra_def by auto - show ?thesis - apply (subst (2) *) - apply (unfold **) - apply (rule someI_ex[where P="?P"]) - apply (rule extend_\G) - done -qed + "(\s\sets generator. measure (Pi\<^isub>P I M) s = \G s) \ prob_space (Pi\<^isub>P I M)" + (is "?Q infprod_algebra") + unfolding infprod_algebra_def + by (rule someI2_ex[OF extend_\G]) + (auto simp: sigma_def generator_def) -sublocale product_prob_space \ P: measure_space "Pi\<^isub>P I M" - using infprod_spec by auto +sublocale product_prob_space \ P: prob_space "Pi\<^isub>P I M" + using infprod_spec by simp lemma (in product_prob_space) measure_infprod_emb: assumes "J \ {}" "finite J" "J \ I" "X \ sets (Pi\<^isub>M J M)" @@ -745,22 +768,6 @@ with \G_eq[OF assms] infprod_spec show ?thesis by auto qed -sublocale product_prob_space \ P: prob_space "Pi\<^isub>P I M" -proof - obtain i where "i \ I" using I_not_empty by auto - interpret i: finite_product_sigma_finite M "{i}" by default auto - let ?X = "\\<^isub>E i\{i}. space (M i)" - have "?X \ sets (Pi\<^isub>M {i} M)" - by auto - from measure_infprod_emb[OF _ _ _ this] `i \ I` - have "\ (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 \ I` by (auto simp: emb_def infprod_algebra_def generator_def) - finally show "\ (space (Pi\<^isub>P I M)) = 1" - using M.measure_space_1 by simp -qed - lemma (in product_prob_space) measurable_component: assumes "i \ I" shows "(\x. x i) \ 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 \ {}" interpret J: finite_product_prob_space M J by default fact+ diff -r 714100f5fda4 -r c36637603821 src/HOL/Probability/Information.thy --- 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 \: prob_space "M\measure := \\" by fact have ms: "measure_space (M\measure := \\)" by default - have fms: "finite_measure (M\measure := \\)" by default + have fms: "finite_measure (M\measure := \\)" 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\measure := \\" by fact - have ps: "prob_space (M\measure := \\)" by default + have ps: "prob_space (M\measure := \\)" by unfold_locales from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis . qed @@ -558,7 +558,7 @@ have eq: "\A\sets XY.P. (ereal \ joint_distribution X Y) A = XY.\ 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\joint_distribution X Y)" using ac by (simp add: P_def) show "integrable ?J (entropy_density b XY.P (ereal\joint_distribution X Y))" @@ -624,7 +624,7 @@ have "prob_space (P.P\ measure := ereal\joint_distribution X Y\)" using X Y by (auto intro!: distribution_prob_space random_variable_pairI) then show "measure_space (P.P\ measure := ereal\joint_distribution X Y\)" - 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\joint_distribution X Y)" proof (rule XY.absolutely_continuousI) - show "finite_measure_space (XY.P\ measure := ereal\joint_distribution X Y\)" by default + show "finite_measure_space (XY.P\ measure := ereal\joint_distribution X Y\)" by unfold_locales fix x assume "x \ space XY.P" and "XY.\ {x} = 0" then obtain a b where "x = (a, b)" and "distribution X {a} = 0 \ distribution Y {b} = 0" @@ -684,8 +684,8 @@ interpret P: finite_prob_space "XY.P\measure := ereal\joint_distribution X Y\" using assms by (auto intro!: joint_distribution_finite_prob_space) - have P_ms: "finite_measure_space (XY.P\measure := ereal\joint_distribution X Y\)" by default - have P_ps: "finite_prob_space (XY.P\measure := ereal\joint_distribution X Y\)" by default + have P_ms: "finite_measure_space (XY.P\measure := ereal\joint_distribution X Y\)" by unfold_locales + have P_ps: "finite_prob_space (XY.P\measure := ereal\joint_distribution X Y\)" by unfold_locales show ?sum unfolding Let_def mutual_information_def diff -r 714100f5fda4 -r c36637603821 src/HOL/Probability/Measure.thy --- 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: "\ (space M) \ \" -sublocale finite_measure < sigma_finite_measure -proof - show "\A. range A \ sets M \ (\i. A i) = space M \ (\i. \ (A i) \ \)" - using finite_measure_of_space by (auto intro!: exI[of _ "\