1.1 --- a/src/HOL/Probability/Independent_Family.thy Thu May 26 17:40:01 2011 +0200
1.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu May 26 17:59:39 2011 +0200
1.3 @@ -37,10 +37,13 @@
1.4 "indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
1.5
1.6 definition (in prob_space)
1.7 - "indep_rv M' X I \<longleftrightarrow>
1.8 + "indep_vars M' X I \<longleftrightarrow>
1.9 (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
1.10 indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
1.11
1.12 +definition (in prob_space)
1.13 + "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
1.14 +
1.15 lemma (in prob_space) indep_sets_cong[cong]:
1.16 "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
1.17 by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+
1.18 @@ -694,13 +697,13 @@
1.19 qed
1.20 qed
1.21
1.22 -lemma (in prob_space) indep_rv_finite:
1.23 +lemma (in prob_space) indep_vars_finite:
1.24 fixes I :: "'i set"
1.25 assumes I: "I \<noteq> {}" "finite I"
1.26 and rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (sigma (M' i)) (X i)"
1.27 and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)"
1.28 and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)"
1.29 - shows "indep_rv (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
1.30 + shows "indep_vars (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
1.31 (\<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.32 proof -
1.33 from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)"
1.34 @@ -761,28 +764,28 @@
1.35 by simp
1.36 qed
1.37 then show ?thesis using `I \<noteq> {}`
1.38 - by (simp add: rv indep_rv_def)
1.39 + by (simp add: rv indep_vars_def)
1.40 qed
1.41
1.42 -lemma (in prob_space) indep_rv_compose:
1.43 - assumes "indep_rv M' X I"
1.44 +lemma (in prob_space) indep_vars_compose:
1.45 + assumes "indep_vars M' X I"
1.46 assumes rv:
1.47 "\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)"
1.48 "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)"
1.49 - shows "indep_rv N (\<lambda>i. Y i \<circ> X i) I"
1.50 - unfolding indep_rv_def
1.51 + shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I"
1.52 + unfolding indep_vars_def
1.53 proof
1.54 - from rv `indep_rv M' X I`
1.55 + from rv `indep_vars M' X I`
1.56 show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)"
1.57 - by (auto intro!: measurable_comp simp: indep_rv_def)
1.58 + by (auto intro!: measurable_comp simp: indep_vars_def)
1.59
1.60 have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
1.61 - using `indep_rv M' X I` by (simp add: indep_rv_def)
1.62 + using `indep_vars M' X I` by (simp add: indep_vars_def)
1.63 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.64 proof (rule indep_sets_mono_sets)
1.65 fix i assume "i \<in> I"
1.66 - with `indep_rv M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
1.67 - unfolding indep_rv_def measurable_def by auto
1.68 + with `indep_vars M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
1.69 + unfolding indep_vars_def measurable_def by auto
1.70 { fix A assume "A \<in> sets (N i)"
1.71 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.72 by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
1.73 @@ -793,13 +796,13 @@
1.74 qed
1.75 qed
1.76
1.77 -lemma (in prob_space) indep_rvD:
1.78 - assumes X: "indep_rv M' X I"
1.79 +lemma (in prob_space) indep_varsD:
1.80 + assumes X: "indep_vars M' X I"
1.81 assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
1.82 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.83 proof (rule indep_setsD)
1.84 show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
1.85 - using X by (auto simp: indep_rv_def)
1.86 + using X by (auto simp: indep_vars_def)
1.87 show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto
1.88 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.89 using I by (auto intro: sigma_sets.Basic)
1.90 @@ -808,7 +811,7 @@
1.91 lemma (in prob_space) indep_distribution_eq_measure:
1.92 assumes I: "I \<noteq> {}" "finite I"
1.93 assumes rv: "\<And>i. random_variable (M' i) (X i)"
1.94 - shows "indep_rv M' X I \<longleftrightarrow>
1.95 + shows "indep_vars M' X I \<longleftrightarrow>
1.96 (\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)).
1.97 distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A =
1.98 finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)) A)"
1.99 @@ -827,7 +830,7 @@
1.100
1.101 show ?thesis
1.102 proof (intro iffI ballI)
1.103 - assume "indep_rv M' X I"
1.104 + assume "indep_vars M' X I"
1.105 fix A assume "A \<in> sets P.P"
1.106 moreover
1.107 have "D.prob A = P.prob A"
1.108 @@ -856,7 +859,7 @@
1.109 with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i -` F i \<inter> space M)"
1.110 using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
1.111 also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` F i \<inter> space M))"
1.112 - using `indep_rv M' X I` I F by (rule indep_rvD)
1.113 + using `indep_vars M' X I` I F by (rule indep_varsD)
1.114 also have "\<dots> = P.prob E"
1.115 using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def)
1.116 finally show "D.prob E = P.prob E" .
1.117 @@ -867,8 +870,8 @@
1.118 assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A"
1.119 have [simp]: "\<And>i. sigma (M' i) = M' i"
1.120 using rv by (intro sigma_algebra.sigma_eq) simp
1.121 - have "indep_rv (\<lambda>i. sigma (M' i)) X I"
1.122 - proof (subst indep_rv_finite[OF I])
1.123 + have "indep_vars (\<lambda>i. sigma (M' i)) X I"
1.124 + proof (subst indep_vars_finite[OF I])
1.125 fix i assume [simp]: "i \<in> I"
1.126 show "random_variable (sigma (M' i)) (X i)"
1.127 using rv[of i] by simp
1.128 @@ -890,9 +893,32 @@
1.129 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.130 qed
1.131 qed
1.132 - then show "indep_rv M' X I"
1.133 + then show "indep_vars M' X I"
1.134 by simp
1.135 qed
1.136 qed
1.137
1.138 +lemma (in prob_space) indep_varD:
1.139 + assumes indep: "indep_var Ma A Mb B"
1.140 + assumes sets: "Xa \<in> sets Ma" "Xb \<in> sets Mb"
1.141 + shows "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
1.142 + prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
1.143 +proof -
1.144 + have "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
1.145 + prob (\<Inter>i\<in>UNIV. (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
1.146 + by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)
1.147 + also have "\<dots> = (\<Prod>i\<in>UNIV. prob (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
1.148 + using indep unfolding indep_var_def
1.149 + by (rule indep_varsD) (auto split: bool.split intro: sets)
1.150 + also have "\<dots> = prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
1.151 + unfolding UNIV_bool by simp
1.152 + finally show ?thesis .
1.153 +qed
1.154 +
1.155 +lemma (in prob_space) indep_var_distributionD:
1.156 + assumes "indep_var Ma A Mb B"
1.157 + assumes "Xa \<in> sets Ma" "Xb \<in> sets Mb"
1.158 + shows "joint_distribution A B (Xa \<times> Xb) = distribution A Xa * distribution B Xb"
1.159 + unfolding distribution_def using assms by (rule indep_varD)
1.160 +
1.161 end