1.1 --- a/src/HOL/Probability/Independent_Family.thy Thu May 26 14:12:06 2011 +0200
1.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu May 26 17:40:01 2011 +0200
1.3 @@ -120,19 +120,6 @@
1.4 and indep_setD_ev2: "B \<subseteq> events"
1.5 using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
1.6
1.7 -lemma dynkin_systemI':
1.8 - assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
1.9 - assumes empty: "{} \<in> sets M"
1.10 - assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
1.11 - assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
1.12 - \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1.13 - shows "dynkin_system M"
1.14 -proof -
1.15 - from Diff[OF empty] have "space M \<in> sets M" by auto
1.16 - from 1 this Diff 2 show ?thesis
1.17 - by (intro dynkin_systemI) auto
1.18 -qed
1.19 -
1.20 lemma (in prob_space) indep_sets_dynkin:
1.21 assumes indep: "indep_sets F I"
1.22 shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I"
1.23 @@ -714,7 +701,7 @@
1.24 and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)"
1.25 and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)"
1.26 shows "indep_rv (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
1.27 - (\<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)))"
1.28 + (\<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)))"
1.29 proof -
1.30 from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)"
1.31 unfolding measurable_def by simp
1.32 @@ -774,7 +761,138 @@
1.33 by simp
1.34 qed
1.35 then show ?thesis using `I \<noteq> {}`
1.36 - by (simp add: rv distribution_def indep_rv_def)
1.37 + by (simp add: rv indep_rv_def)
1.38 +qed
1.39 +
1.40 +lemma (in prob_space) indep_rv_compose:
1.41 + assumes "indep_rv M' X I"
1.42 + assumes rv:
1.43 + "\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)"
1.44 + "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)"
1.45 + shows "indep_rv N (\<lambda>i. Y i \<circ> X i) I"
1.46 + unfolding indep_rv_def
1.47 +proof
1.48 + from rv `indep_rv M' X I`
1.49 + show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)"
1.50 + by (auto intro!: measurable_comp simp: indep_rv_def)
1.51 +
1.52 + have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
1.53 + using `indep_rv M' X I` by (simp add: indep_rv_def)
1.54 + 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"
1.55 + proof (rule indep_sets_mono_sets)
1.56 + fix i assume "i \<in> I"
1.57 + with `indep_rv M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
1.58 + unfolding indep_rv_def measurable_def by auto
1.59 + { fix A assume "A \<in> sets (N i)"
1.60 + 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)"
1.61 + by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
1.62 + (auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
1.63 + then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
1.64 + sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
1.65 + by (intro sigma_sets_subseteq) (auto simp: vimage_compose)
1.66 + qed
1.67 +qed
1.68 +
1.69 +lemma (in prob_space) indep_rvD:
1.70 + assumes X: "indep_rv M' X I"
1.71 + assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
1.72 + 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))"
1.73 +proof (rule indep_setsD)
1.74 + show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
1.75 + using X by (auto simp: indep_rv_def)
1.76 + show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto
1.77 + 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)}"
1.78 + using I by (auto intro: sigma_sets.Basic)
1.79 +qed
1.80 +
1.81 +lemma (in prob_space) indep_distribution_eq_measure:
1.82 + assumes I: "I \<noteq> {}" "finite I"
1.83 + assumes rv: "\<And>i. random_variable (M' i) (X i)"
1.84 + shows "indep_rv M' X I \<longleftrightarrow>
1.85 + (\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)).
1.86 + distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A =
1.87 + finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)) A)"
1.88 + (is "_ \<longleftrightarrow> (\<forall>X\<in>_. distribution ?D X = finite_measure.\<mu>' (Pi\<^isub>M I ?M) X)")
1.89 +proof -
1.90 + interpret M': prob_space "?M i" for i
1.91 + using rv by (rule distribution_prob_space)
1.92 + interpret P: finite_product_prob_space ?M I
1.93 + proof qed fact
1.94 +
1.95 + let ?D' = "(Pi\<^isub>M I ?M) \<lparr> measure := extreal \<circ> distribution ?D \<rparr>"
1.96 + have "random_variable P.P ?D"
1.97 + using `finite I` rv by (intro random_variable_restrict) auto
1.98 + then interpret D: prob_space ?D'
1.99 + by (rule distribution_prob_space)
1.100 +
1.101 + show ?thesis
1.102 + proof (intro iffI ballI)
1.103 + assume "indep_rv M' X I"
1.104 + fix A assume "A \<in> sets P.P"
1.105 + moreover
1.106 + have "D.prob A = P.prob A"
1.107 + proof (rule prob_space_unique_Int_stable)
1.108 + show "prob_space ?D'" by default
1.109 + show "prob_space (Pi\<^isub>M I ?M)" by default
1.110 + show "Int_stable P.G" using M'.Int
1.111 + by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def)
1.112 + show "space P.G \<in> sets P.G"
1.113 + using M'.top by (simp add: product_algebra_generator_def)
1.114 + show "space ?D' = space P.G" "sets ?D' = sets (sigma P.G)"
1.115 + by (simp_all add: product_algebra_def product_algebra_generator_def sets_sigma)
1.116 + show "space P.P = space P.G" "sets P.P = sets (sigma P.G)"
1.117 + by (simp_all add: product_algebra_def)
1.118 + show "A \<in> sets (sigma P.G)"
1.119 + using `A \<in> sets P.P` by (simp add: product_algebra_def)
1.120 +
1.121 + fix E assume E: "E \<in> sets P.G"
1.122 + then have "E \<in> sets P.P"
1.123 + by (simp add: sets_sigma sigma_sets.Basic product_algebra_def)
1.124 + then have "D.prob E = distribution ?D E"
1.125 + unfolding D.\<mu>'_def by simp
1.126 + also
1.127 + 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)"
1.128 + by (auto simp: product_algebra_generator_def)
1.129 + with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i -` F i \<inter> space M)"
1.130 + using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
1.131 + also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` F i \<inter> space M))"
1.132 + using `indep_rv M' X I` I F by (rule indep_rvD)
1.133 + also have "\<dots> = P.prob E"
1.134 + using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def)
1.135 + finally show "D.prob E = P.prob E" .
1.136 + qed
1.137 + ultimately show "distribution ?D A = P.prob A"
1.138 + by (simp add: D.\<mu>'_def)
1.139 + next
1.140 + assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A"
1.141 + have [simp]: "\<And>i. sigma (M' i) = M' i"
1.142 + using rv by (intro sigma_algebra.sigma_eq) simp
1.143 + have "indep_rv (\<lambda>i. sigma (M' i)) X I"
1.144 + proof (subst indep_rv_finite[OF I])
1.145 + fix i assume [simp]: "i \<in> I"
1.146 + show "random_variable (sigma (M' i)) (X i)"
1.147 + using rv[of i] by simp
1.148 + show "Int_stable (M' i)" "space (M' i) \<in> sets (M' i)"
1.149 + using M'.Int[of _ i] M'.top by (auto simp: Int_stable_def)
1.150 + next
1.151 + 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))"
1.152 + proof
1.153 + fix A assume A: "A \<in> (\<Pi> i\<in>I. sets (M' i))"
1.154 + then have A_in_P: "(Pi\<^isub>E I A) \<in> sets P.P"
1.155 + by (auto intro!: product_algebraI)
1.156 + have "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = distribution ?D (Pi\<^isub>E I A)"
1.157 + using `I \<noteq> {}`by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
1.158 + also have "\<dots> = P.prob (Pi\<^isub>E I A)" using A_in_P eq by simp
1.159 + also have "\<dots> = (\<Prod>i\<in>I. M'.prob i (A i))"
1.160 + using A by (intro P.prob_times) auto
1.161 + also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` A i \<inter> space M))"
1.162 + using A by (auto intro!: setprod_cong simp: M'.\<mu>'_def Pi_iff distribution_def)
1.163 + 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))" .
1.164 + qed
1.165 + qed
1.166 + then show "indep_rv M' X I"
1.167 + by simp
1.168 + qed
1.169 qed
1.170
1.171 end