author hoelzl Thu May 26 17:59:39 2011 +0200 (2011-05-26) changeset 42989 40adeda9a8d2 parent 42988 d8f3fc934ff6 child 42990 3706951a6421
introduce independence of two random variables
```     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
```