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)