introduce independence of two random variables
authorhoelzl
Thu May 26 17:59:39 2011 +0200 (2011-05-26)
changeset 4298940adeda9a8d2
parent 42988 d8f3fc934ff6
child 42990 3706951a6421
introduce independence of two random variables
src/HOL/Probability/Independent_Family.thy
     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