src/HOL/Probability/Independent_Family.thy
 changeset 42861 16375b493b64 child 42981 fe7f5a26e4c6
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue May 17 11:47:36 2011 +0200
1.3 @@ -0,0 +1,312 @@
1.4 +(*  Title:      HOL/Probability/Independent_Family.thy
1.5 +    Author:     Johannes Hölzl, TU München
1.6 +*)
1.7 +
1.8 +header {* Independent families of events, event sets, and random variables *}
1.9 +
1.10 +theory Independent_Family
1.11 +  imports Probability_Measure
1.12 +begin
1.13 +
1.14 +definition (in prob_space)
1.15 +  "indep_events A I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
1.16 +
1.17 +definition (in prob_space)
1.18 +  "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow>
1.19 +    (\<forall>A\<in>(\<Pi> j\<in>J. F j). prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"
1.20 +
1.21 +definition (in prob_space)
1.22 +  "indep_sets2 A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
1.23 +
1.24 +definition (in prob_space)
1.25 +  "indep_rv M' X I \<longleftrightarrow>
1.26 +    (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
1.27 +    indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
1.28 +
1.29 +lemma (in prob_space) indep_sets_finite_index_sets:
1.30 +  "indep_sets F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J)"
1.31 +proof (intro iffI allI impI)
1.32 +  assume *: "\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J"
1.33 +  show "indep_sets F I" unfolding indep_sets_def
1.34 +  proof (intro conjI ballI allI impI)
1.35 +    fix i assume "i \<in> I"
1.36 +    with *[THEN spec, of "{i}"] show "F i \<subseteq> events"
1.37 +      by (auto simp: indep_sets_def)
1.38 +  qed (insert *, auto simp: indep_sets_def)
1.39 +qed (auto simp: indep_sets_def)
1.40 +
1.41 +lemma (in prob_space) indep_sets_mono_index:
1.42 +  "J \<subseteq> I \<Longrightarrow> indep_sets F I \<Longrightarrow> indep_sets F J"
1.43 +  unfolding indep_sets_def by auto
1.44 +
1.45 +lemma (in prob_space) indep_sets_mono_sets:
1.46 +  assumes indep: "indep_sets F I"
1.47 +  assumes mono: "\<And>i. i\<in>I \<Longrightarrow> G i \<subseteq> F i"
1.48 +  shows "indep_sets G I"
1.49 +proof -
1.50 +  have "(\<forall>i\<in>I. F i \<subseteq> events) \<Longrightarrow> (\<forall>i\<in>I. G i \<subseteq> events)"
1.51 +    using mono by auto
1.52 +  moreover have "\<And>A J. J \<subseteq> I \<Longrightarrow> A \<in> (\<Pi> j\<in>J. G j) \<Longrightarrow> A \<in> (\<Pi> j\<in>J. F j)"
1.53 +    using mono by (auto simp: Pi_iff)
1.54 +  ultimately show ?thesis
1.55 +    using indep by (auto simp: indep_sets_def)
1.56 +qed
1.57 +
1.58 +lemma (in prob_space) indep_setsI:
1.59 +  assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events"
1.60 +    and "\<And>A J. J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<forall>j\<in>J. A j \<in> F j) \<Longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
1.61 +  shows "indep_sets F I"
1.62 +  using assms unfolding indep_sets_def by (auto simp: Pi_iff)
1.63 +
1.64 +lemma (in prob_space) indep_setsD:
1.65 +  assumes "indep_sets F I" and "J \<subseteq> I" "J \<noteq> {}" "finite J" "\<forall>j\<in>J. A j \<in> F j"
1.66 +  shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
1.67 +  using assms unfolding indep_sets_def by auto
1.68 +
1.69 +lemma dynkin_systemI':
1.70 +  assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
1.71 +  assumes empty: "{} \<in> sets M"
1.72 +  assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M"
1.73 +  assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M
1.74 +          \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
1.75 +  shows "dynkin_system M"
1.76 +proof -
1.77 +  from Diff[OF empty] have "space M \<in> sets M" by auto
1.78 +  from 1 this Diff 2 show ?thesis
1.79 +    by (intro dynkin_systemI) auto
1.80 +qed
1.81 +
1.82 +lemma (in prob_space) indep_sets_dynkin:
1.83 +  assumes indep: "indep_sets F I"
1.84 +  shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I"
1.85 +    (is "indep_sets ?F I")
1.86 +proof (subst indep_sets_finite_index_sets, intro allI impI ballI)
1.87 +  fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}"
1.88 +  with indep have "indep_sets F J"
1.89 +    by (subst (asm) indep_sets_finite_index_sets) auto
1.90 +  { fix J K assume "indep_sets F K"
1.91 +    let "?G S i" = "if i \<in> S then ?F i else F i"
1.92 +    assume "finite J" "J \<subseteq> K"
1.93 +    then have "indep_sets (?G J) K"
1.94 +    proof induct
1.95 +      case (insert j J)
1.96 +      moreover def G \<equiv> "?G J"
1.97 +      ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K"
1.98 +        by (auto simp: indep_sets_def)
1.99 +      let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }"
1.100 +      { fix X assume X: "X \<in> events"
1.101 +        assume indep: "\<And>J A. J \<noteq> {} \<Longrightarrow> J \<subseteq> K \<Longrightarrow> finite J \<Longrightarrow> j \<notin> J \<Longrightarrow> (\<forall>i\<in>J. A i \<in> G i)
1.102 +          \<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>J. prob (A i))"
1.103 +        have "indep_sets (G(j := {X})) K"
1.104 +        proof (rule indep_setsI)
1.105 +          fix i assume "i \<in> K" then show "(G(j:={X})) i \<subseteq> events"
1.106 +            using G X by auto
1.107 +        next
1.108 +          fix A J assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "\<forall>i\<in>J. A i \<in> (G(j := {X})) i"
1.109 +          show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
1.110 +          proof cases
1.111 +            assume "j \<in> J"
1.112 +            with J have "A j = X" by auto
1.113 +            show ?thesis
1.114 +            proof cases
1.115 +              assume "J = {j}" then show ?thesis by simp
1.116 +            next
1.117 +              assume "J \<noteq> {j}"
1.118 +              have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)"
1.119 +                using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.120 +              also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))"
1.121 +              proof (rule indep)
1.122 +                show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}"
1.123 +                  using J `J \<noteq> {j}` `j \<in> J` by auto
1.124 +                show "\<forall>i\<in>J - {j}. A i \<in> G i"
1.125 +                  using J by auto
1.126 +              qed
1.127 +              also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))"
1.128 +                using `A j = X` by simp
1.129 +              also have "\<dots> = (\<Prod>i\<in>J. prob (A i))"
1.130 +                unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob  (A i)"]
1.131 +                using `j \<in> J` by (simp add: insert_absorb)
1.132 +              finally show ?thesis .
1.133 +            qed
1.134 +          next
1.135 +            assume "j \<notin> J"
1.136 +            with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
1.137 +            with J show ?thesis
1.138 +              by (intro indep_setsD[OF G(1)]) auto
1.139 +          qed
1.140 +        qed }
1.141 +      note indep_sets_insert = this
1.142 +      have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>"
1.143 +      proof (rule dynkin_systemI', simp_all, safe)
1.144 +        show "indep_sets (G(j := {{}})) K"
1.145 +          by (rule indep_sets_insert) auto
1.146 +      next
1.147 +        fix X assume X: "X \<in> events" and G': "indep_sets (G(j := {X})) K"
1.148 +        show "indep_sets (G(j := {space M - X})) K"
1.149 +        proof (rule indep_sets_insert)
1.150 +          fix J A assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "j \<notin> J" and A: "\<forall>i\<in>J. A i \<in> G i"
1.151 +          then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
1.152 +            using G by auto
1.153 +          have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
1.154 +              prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
1.155 +            using A_sets sets_into_space X `J \<noteq> {}`
1.156 +            by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.157 +          also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
1.158 +            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
1.159 +            by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
1.160 +          finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
1.161 +              prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
1.162 +          moreover {
1.163 +            have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
1.164 +              using J A `finite J` by (intro indep_setsD[OF G(1)]) auto
1.165 +            then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))"
1.166 +              using prob_space by simp }
1.167 +          moreover {
1.168 +            have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))"
1.169 +              using J A `j \<in> K` by (intro indep_setsD[OF G']) auto
1.170 +            then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))"
1.171 +              using `finite J` `j \<notin> J` by (auto intro!: setprod_cong) }
1.172 +          ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = (prob (space M) - prob X) * (\<Prod>i\<in>J. prob (A i))"
1.173 +            by (simp add: field_simps)
1.174 +          also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))"
1.175 +            using X A by (simp add: finite_measure_compl)
1.176 +          finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" .
1.177 +        qed (insert X, auto)
1.178 +      next
1.179 +        fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F" and "range F \<subseteq> ?D"
1.180 +        then have F: "\<And>i. F i \<in> events" "\<And>i. indep_sets (G(j:={F i})) K" by auto
1.181 +        show "indep_sets (G(j := {\<Union>k. F k})) K"
1.182 +        proof (rule indep_sets_insert)
1.183 +          fix J A assume J: "j \<notin> J" "J \<noteq> {}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> G i"
1.184 +          then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
1.185 +            using G by auto
1.186 +          have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
1.187 +            using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.188 +          moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
1.189 +          proof (rule finite_measure_UNION)
1.190 +            show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
1.191 +              using disj by (rule disjoint_family_on_bisimulation) auto
1.192 +            show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
1.193 +              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
1.194 +          qed
1.195 +          moreover { fix k
1.196 +            from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
1.197 +              by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm)
1.198 +            also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
1.199 +              using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto
1.200 +            finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
1.201 +          ultimately have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)))"
1.202 +            by simp
1.203 +          moreover
1.204 +          have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i\<in>J. A i))"
1.205 +            using disj F(1) by (intro finite_measure_UNION sums_mult2) auto
1.206 +          then have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * (\<Prod>i\<in>J. prob (A i)))"
1.207 +            using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto
1.208 +          ultimately
1.209 +          show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
1.210 +            by (auto dest!: sums_unique)
1.211 +        qed (insert F, auto)
1.212 +      qed (insert sets_into_space, auto)
1.213 +      then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq>
1.214 +        sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>"
1.215 +      proof (rule dynkin_system.dynkin_subset, simp_all, safe)
1.216 +        fix X assume "X \<in> G j"
1.217 +        then show "X \<in> events" using G `j \<in> K` by auto
1.218 +        from `indep_sets G K`
1.219 +        show "indep_sets (G(j := {X})) K"
1.220 +          by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto)
1.221 +      qed
1.222 +      have "indep_sets (G(j:=?D)) K"
1.223 +      proof (rule indep_setsI)
1.224 +        fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events"
1.225 +          using G(2) by auto
1.226 +      next
1.227 +        fix A J assume J: "J\<noteq>{}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> (G(j := ?D)) i"
1.228 +        show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
1.229 +        proof cases
1.230 +          assume "j \<in> J"
1.231 +          with A have indep: "indep_sets (G(j := {A j})) K" by auto
1.232 +          from J A show ?thesis
1.233 +            by (intro indep_setsD[OF indep]) auto
1.234 +        next
1.235 +          assume "j \<notin> J"
1.236 +          with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
1.237 +          with J show ?thesis
1.238 +            by (intro indep_setsD[OF G(1)]) auto
1.239 +        qed
1.240 +      qed
1.241 +      then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K"
1.242 +        by (rule indep_sets_mono_sets) (insert mono, auto)
1.243 +      then show ?case
1.244 +        by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def)
1.245 +    qed (insert `indep_sets F K`, simp) }
1.246 +  from this[OF `indep_sets F J` `finite J` subset_refl]
1.247 +  show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J"
1.248 +    by (rule indep_sets_mono_sets) auto
1.249 +qed
1.250 +
1.251 +lemma (in prob_space) indep_sets_sigma:
1.252 +  assumes indep: "indep_sets F I"
1.253 +  assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
1.254 +  shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I"
1.255 +proof -
1.256 +  from indep_sets_dynkin[OF indep]
1.257 +  show ?thesis
1.258 +  proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
1.259 +    fix i assume "i \<in> I"
1.260 +    with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
1.261 +    with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
1.262 +  qed
1.263 +qed
1.264 +
1.265 +lemma (in prob_space) indep_sets_sigma_sets:
1.266 +  assumes "indep_sets F I"
1.267 +  assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
1.268 +  shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
1.269 +  using indep_sets_sigma[OF assms] by (simp add: sets_sigma)
1.270 +
1.271 +lemma (in prob_space) indep_sets2_eq:
1.272 +  "indep_sets2 A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
1.273 +  unfolding indep_sets2_def
1.274 +proof (intro iffI ballI conjI)
1.275 +  assume indep: "indep_sets (bool_case A B) UNIV"
1.276 +  { fix a b assume "a \<in> A" "b \<in> B"
1.277 +    with indep_setsD[OF indep, of UNIV "bool_case a b"]
1.278 +    show "prob (a \<inter> b) = prob a * prob b"
1.279 +      unfolding UNIV_bool by (simp add: ac_simps) }
1.280 +  from indep show "A \<subseteq> events" "B \<subseteq> events"
1.281 +    unfolding indep_sets_def UNIV_bool by auto
1.282 +next
1.283 +  assume *: "A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)"
1.284 +  show "indep_sets (bool_case A B) UNIV"
1.285 +  proof (rule indep_setsI)
1.286 +    fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events"
1.287 +      using * by (auto split: bool.split)
1.288 +  next
1.289 +    fix J X assume "J \<noteq> {}" "J \<subseteq> UNIV" and X: "\<forall>j\<in>J. X j \<in> (case j of True \<Rightarrow> A | False \<Rightarrow> B)"
1.290 +    then have "J = {True} \<or> J = {False} \<or> J = {True,False}"
1.291 +      by (auto simp: UNIV_bool)
1.292 +    then show "prob (\<Inter>j\<in>J. X j) = (\<Prod>j\<in>J. prob (X j))"
1.293 +      using X * by auto
1.294 +  qed
1.295 +qed
1.296 +
1.297 +lemma (in prob_space) indep_sets2_sigma_sets:
1.298 +  assumes "indep_sets2 A B"
1.299 +  assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>"
1.300 +  assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>"
1.301 +  shows "indep_sets2 (sigma_sets (space M) A) (sigma_sets (space M) B)"
1.302 +proof -
1.303 +  have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
1.304 +  proof (rule indep_sets_sigma_sets)
1.305 +    show "indep_sets (bool_case A B) UNIV"
1.306 +      by (rule `indep_sets2 A B`[unfolded indep_sets2_def])
1.307 +    fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A | False \<Rightarrow> B\<rparr>"
1.308 +      using A B by (cases i) auto
1.309 +  qed
1.310 +  then show ?thesis
1.311 +    unfolding indep_sets2_def
1.312 +    by (rule indep_sets_mono_sets) (auto split: bool.split)
1.313 +qed
1.314 +
1.315 +end
```