--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu May 26 14:12:06 2011 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu May 26 17:40:01 2011 +0200
@@ -325,6 +325,10 @@
"\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
by (auto simp: sets_product_algebra)
+lemma Int_stable_product_algebra_generator:
+ "(\<And>i. i \<in> I \<Longrightarrow> Int_stable (M i)) \<Longrightarrow> Int_stable (product_algebra_generator I M)"
+ by (auto simp add: product_algebra_generator_def Int_stable_def PiE_Int Pi_iff)
+
section "Generating set generates also product algebra"
lemma sigma_product_algebra_sigma_eq:
@@ -478,6 +482,32 @@
using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
qed (insert `i \<in> I`, auto)
+lemma (in sigma_algebra) measurable_restrict:
+ assumes I: "finite I"
+ assumes "\<And>i. i \<in> I \<Longrightarrow> sets (N i) \<subseteq> Pow (space (N i))"
+ assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (N i)"
+ shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"
+ unfolding product_algebra_def
+proof (simp, rule measurable_sigma)
+ show "sets (product_algebra_generator I N) \<subseteq> Pow (space (product_algebra_generator I N))"
+ by (rule product_algebra_generator_sets_into_space) fact
+ show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> space M \<rightarrow> space (product_algebra_generator I N)"
+ using X by (auto simp: measurable_def)
+ fix E assume "E \<in> sets (product_algebra_generator I N)"
+ then obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (N i)"
+ by (auto simp: product_algebra_generator_def)
+ then have "(\<lambda>x. \<lambda>i\<in>I. X i x) -` E \<inter> space M = (\<Inter>i\<in>I. X i -` F i \<inter> space M) \<inter> space M"
+ by (auto simp: Pi_iff)
+ also have "\<dots> \<in> sets M"
+ proof cases
+ assume "I = {}" then show ?thesis by simp
+ next
+ assume "I \<noteq> {}" with X F I show ?thesis
+ by (intro finite_INT measurable_sets Int) auto
+ qed
+ 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"
assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
@@ -719,9 +749,8 @@
using A unfolding product_algebra_def by auto
next
show "Int_stable IJ.G"
- by (simp add: PiE_Int Int_stable_def product_algebra_def
- product_algebra_generator_def)
- auto
+ by (rule Int_stable_product_algebra_generator)
+ (auto simp: Int_stable_def)
show "range ?F \<subseteq> sets IJ.G" using F
by (simp add: image_subset_iff product_algebra_def
product_algebra_generator_def)
--- a/src/HOL/Probability/Independent_Family.thy Thu May 26 14:12:06 2011 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Thu May 26 17:40:01 2011 +0200
@@ -120,19 +120,6 @@
and indep_setD_ev2: "B \<subseteq> events"
using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
-lemma dynkin_systemI':
- assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
- assumes empty: "{} \<in> sets M"
- assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
- assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
- \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
- shows "dynkin_system M"
-proof -
- from Diff[OF empty] have "space M \<in> sets M" by auto
- from 1 this Diff 2 show ?thesis
- by (intro dynkin_systemI) auto
-qed
-
lemma (in prob_space) indep_sets_dynkin:
assumes indep: "indep_sets F I"
shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I"
@@ -714,7 +701,7 @@
and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)"
and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)"
shows "indep_rv (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
- (\<forall>A\<in>(\<Pi> i\<in>I. sets (M' i)). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. distribution (X j) (A j)))"
+ (\<forall>A\<in>(\<Pi> i\<in>I. sets (M' i)). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M)))"
proof -
from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)"
unfolding measurable_def by simp
@@ -774,7 +761,138 @@
by simp
qed
then show ?thesis using `I \<noteq> {}`
- by (simp add: rv distribution_def indep_rv_def)
+ by (simp add: rv indep_rv_def)
+qed
+
+lemma (in prob_space) indep_rv_compose:
+ assumes "indep_rv M' X I"
+ assumes rv:
+ "\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)"
+ "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)"
+ shows "indep_rv N (\<lambda>i. Y i \<circ> X i) I"
+ unfolding indep_rv_def
+proof
+ from rv `indep_rv M' X I`
+ show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)"
+ by (auto intro!: measurable_comp simp: indep_rv_def)
+
+ have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
+ using `indep_rv M' X I` by (simp add: indep_rv_def)
+ then show "indep_sets (\<lambda>i. sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)}) I"
+ proof (rule indep_sets_mono_sets)
+ fix i assume "i \<in> I"
+ with `indep_rv M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
+ unfolding indep_rv_def measurable_def by auto
+ { fix A assume "A \<in> sets (N i)"
+ then have "\<exists>B. (Y i \<circ> X i) -` A \<inter> space M = X i -` B \<inter> space M \<and> B \<in> sets (M' i)"
+ by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
+ (auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
+ then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
+ sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+ by (intro sigma_sets_subseteq) (auto simp: vimage_compose)
+ qed
+qed
+
+lemma (in prob_space) indep_rvD:
+ assumes X: "indep_rv M' X I"
+ assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
+ shows "prob (\<Inter>i\<in>I. X i -` A i \<inter> space M) = (\<Prod>i\<in>I. prob (X i -` A i \<inter> space M))"
+proof (rule indep_setsD)
+ show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
+ using X by (auto simp: indep_rv_def)
+ show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto
+ show "\<forall>i\<in>I. X i -` A i \<inter> space M \<in> sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+ using I by (auto intro: sigma_sets.Basic)
+qed
+
+lemma (in prob_space) indep_distribution_eq_measure:
+ assumes I: "I \<noteq> {}" "finite I"
+ assumes rv: "\<And>i. random_variable (M' i) (X i)"
+ shows "indep_rv M' X I \<longleftrightarrow>
+ (\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)).
+ distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A =
+ finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)) A)"
+ (is "_ \<longleftrightarrow> (\<forall>X\<in>_. distribution ?D X = finite_measure.\<mu>' (Pi\<^isub>M I ?M) X)")
+proof -
+ interpret M': prob_space "?M i" for i
+ using rv by (rule distribution_prob_space)
+ interpret P: finite_product_prob_space ?M I
+ proof qed fact
+
+ let ?D' = "(Pi\<^isub>M I ?M) \<lparr> measure := extreal \<circ> distribution ?D \<rparr>"
+ have "random_variable P.P ?D"
+ using `finite I` rv by (intro random_variable_restrict) auto
+ then interpret D: prob_space ?D'
+ by (rule distribution_prob_space)
+
+ show ?thesis
+ proof (intro iffI ballI)
+ assume "indep_rv M' X I"
+ fix A assume "A \<in> sets P.P"
+ 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 "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"
+ using M'.top by (simp add: product_algebra_generator_def)
+ show "space ?D' = space P.G" "sets ?D' = sets (sigma P.G)"
+ by (simp_all add: product_algebra_def product_algebra_generator_def sets_sigma)
+ show "space P.P = space P.G" "sets P.P = sets (sigma P.G)"
+ by (simp_all add: product_algebra_def)
+ show "A \<in> sets (sigma P.G)"
+ using `A \<in> sets P.P` by (simp add: product_algebra_def)
+
+ fix E assume E: "E \<in> sets P.G"
+ then have "E \<in> sets P.P"
+ by (simp add: sets_sigma sigma_sets.Basic product_algebra_def)
+ then have "D.prob E = distribution ?D E"
+ unfolding D.\<mu>'_def by simp
+ also
+ from E obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M' i)"
+ by (auto simp: product_algebra_generator_def)
+ with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i -` F i \<inter> space M)"
+ using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
+ also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` F i \<inter> space M))"
+ using `indep_rv M' X I` I F by (rule indep_rvD)
+ also have "\<dots> = P.prob E"
+ using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def)
+ finally show "D.prob E = P.prob E" .
+ qed
+ ultimately show "distribution ?D A = P.prob A"
+ by (simp add: D.\<mu>'_def)
+ next
+ assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A"
+ have [simp]: "\<And>i. sigma (M' i) = M' i"
+ using rv by (intro sigma_algebra.sigma_eq) simp
+ have "indep_rv (\<lambda>i. sigma (M' i)) X I"
+ proof (subst indep_rv_finite[OF I])
+ fix i assume [simp]: "i \<in> I"
+ show "random_variable (sigma (M' i)) (X i)"
+ using rv[of i] by simp
+ show "Int_stable (M' i)" "space (M' i) \<in> sets (M' i)"
+ using M'.Int[of _ i] M'.top by (auto simp: Int_stable_def)
+ next
+ show "\<forall>A\<in>\<Pi> i\<in>I. sets (M' i). prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M))"
+ proof
+ fix A assume A: "A \<in> (\<Pi> i\<in>I. sets (M' i))"
+ then have A_in_P: "(Pi\<^isub>E I A) \<in> sets P.P"
+ by (auto intro!: product_algebraI)
+ have "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = distribution ?D (Pi\<^isub>E I A)"
+ using `I \<noteq> {}`by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
+ also have "\<dots> = P.prob (Pi\<^isub>E I A)" using A_in_P eq by simp
+ also have "\<dots> = (\<Prod>i\<in>I. M'.prob i (A i))"
+ using A by (intro P.prob_times) auto
+ also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` A i \<inter> space M))"
+ using A by (auto intro!: setprod_cong simp: M'.\<mu>'_def Pi_iff distribution_def)
+ finally show "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M))" .
+ qed
+ qed
+ then show "indep_rv M' X I"
+ by simp
+ qed
qed
end
--- a/src/HOL/Probability/Probability_Measure.thy Thu May 26 14:12:06 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Thu May 26 17:40:01 2011 +0200
@@ -188,6 +188,37 @@
qed
qed
+lemma prob_space_unique_Int_stable:
+ fixes E :: "('a, 'b) algebra_scheme" and A :: "nat \<Rightarrow> 'a set"
+ assumes E: "Int_stable E" "space E \<in> sets E"
+ and M: "prob_space M" "space M = space E" "sets M = sets (sigma E)"
+ and N: "prob_space N" "space N = space E" "sets N = sets (sigma E)"
+ and eq: "\<And>X. X \<in> sets E \<Longrightarrow> finite_measure.\<mu>' M X = finite_measure.\<mu>' N X"
+ assumes "X \<in> sets (sigma E)"
+ shows "finite_measure.\<mu>' M X = finite_measure.\<mu>' N X"
+proof -
+ interpret M!: prob_space M by fact
+ interpret N!: prob_space N by fact
+ have "measure M X = measure N X"
+ proof (rule measure_unique_Int_stable[OF `Int_stable E`])
+ show "range (\<lambda>i. space M) \<subseteq> sets E" "incseq (\<lambda>i. space M)" "(\<Union>i. space M) = space E"
+ using E M N by auto
+ show "\<And>i. M.\<mu> (space M) \<noteq> \<infinity>"
+ using M.measure_space_1 by simp
+ show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure_space.measure = M.\<mu>\<rparr>"
+ using E M N by (auto intro!: M.measure_space_cong)
+ show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure_space.measure = N.\<mu>\<rparr>"
+ using E M N by (auto intro!: N.measure_space_cong)
+ { fix X assume "X \<in> sets E"
+ then have "X \<in> sets (sigma E)"
+ by (auto simp: sets_sigma sigma_sets.Basic)
+ with eq[OF `X \<in> sets E`] M N show "M.\<mu> X = N.\<mu> X"
+ by (simp add: M.finite_measure_eq N.finite_measure_eq) }
+ qed fact
+ with `X \<in> sets (sigma E)` M N show ?thesis
+ by (simp add: M.finite_measure_eq N.finite_measure_eq)
+qed
+
lemma (in prob_space) distribution_prob_space:
assumes X: "random_variable S X"
shows "prob_space (S\<lparr>measure := extreal \<circ> distribution X\<rparr>)" (is "prob_space ?S")
@@ -359,6 +390,50 @@
shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := extreal \<circ> joint_distribution X Y\<rparr>)"
using random_variable_pairI[OF assms] by (rule distribution_prob_space)
+
+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
+ by (rule prob_space)
+
+sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite M I
+ by default (rule finite_index)
+
+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)
+
+lemma (in finite_product_prob_space) prob_times:
+ assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
+ shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
+proof -
+ have "extreal (\<mu>' (\<Pi>\<^isub>E i\<in>I. X i)) = \<mu> (\<Pi>\<^isub>E i\<in>I. X i)"
+ using X by (intro finite_measure_eq[symmetric] in_P) auto
+ also have "\<dots> = (\<Prod>i\<in>I. M.\<mu> i (X i))"
+ using measure_times X by simp
+ also have "\<dots> = extreal (\<Prod>i\<in>I. M.\<mu>' i (X i))"
+ using X by (simp add: M.finite_measure_eq setprod_extreal)
+ finally show ?thesis by simp
+qed
+
+lemma (in prob_space) random_variable_restrict:
+ assumes I: "finite I"
+ assumes X: "\<And>i. i \<in> I \<Longrightarrow> random_variable (N i) (X i)"
+ shows "random_variable (Pi\<^isub>M I N) (\<lambda>x. \<lambda>i\<in>I. X i x)"
+proof
+ { fix i assume "i \<in> I"
+ with X interpret N: sigma_algebra "N i" by simp
+ have "sets (N i) \<subseteq> Pow (space (N i))" by (rule N.space_closed) }
+ note N_closed = this
+ then show "sigma_algebra (Pi\<^isub>M I N)"
+ by (simp add: product_algebra_def)
+ (intro sigma_algebra_sigma product_algebra_generator_sets_into_space)
+ show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable M (Pi\<^isub>M I N)"
+ using X by (intro measurable_restrict[OF I N_closed]) auto
+qed
+
section "Probability spaces on finite sets"
locale finite_prob_space = prob_space + finite_measure_space
--- a/src/HOL/Probability/Sigma_Algebra.thy Thu May 26 14:12:06 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu May 26 17:40:01 2011 +0200
@@ -1406,6 +1406,19 @@
shows "dynkin_system M"
using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
+lemma dynkin_systemI':
+ assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
+ assumes empty: "{} \<in> sets M"
+ assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
+ assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
+ \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+ shows "dynkin_system M"
+proof -
+ from Diff[OF empty] have "space M \<in> sets M" by auto
+ from 1 this Diff 2 show ?thesis
+ by (intro dynkin_systemI) auto
+qed
+
lemma dynkin_system_trivial:
shows "dynkin_system \<lparr> space = A, sets = Pow A \<rparr>"
by (rule dynkin_systemI) auto