# HG changeset patch
# User hoelzl
# Date 1306425579 -7200
# Node ID 40adeda9a8d2c766f558ab8a2a53d43dfed4d9bc
# Parent  d8f3fc934ff678a9355354ba019ec5438342305b
introduce independence of two random variables

diff -r d8f3fc934ff6 -r 40adeda9a8d2 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu May 26 17:40:01 2011 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Thu May 26 17:59:39 2011 +0200
@@ -37,10 +37,13 @@
   "indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV"
 
 definition (in prob_space)
-  "indep_rv M' X I \<longleftrightarrow>
+  "indep_vars M' X I \<longleftrightarrow>
     (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and>
     indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I"
 
+definition (in prob_space)
+  "indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV"
+
 lemma (in prob_space) indep_sets_cong[cong]:
   "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J"
   by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+
@@ -694,13 +697,13 @@
   qed
 qed
 
-lemma (in prob_space) indep_rv_finite:
+lemma (in prob_space) indep_vars_finite:
   fixes I :: "'i set"
   assumes I: "I \<noteq> {}" "finite I"
     and rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (sigma (M' i)) (X i)"
     and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)"
     and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)"
-  shows "indep_rv (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
+  shows "indep_vars (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow>
     (\<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)))"
 proof -
   from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)"
@@ -761,28 +764,28 @@
       by simp
   qed
   then show ?thesis using `I \<noteq> {}`
-    by (simp add: rv indep_rv_def)
+    by (simp add: rv indep_vars_def)
 qed
 
-lemma (in prob_space) indep_rv_compose:
-  assumes "indep_rv M' X I"
+lemma (in prob_space) indep_vars_compose:
+  assumes "indep_vars M' X I"
   assumes rv:
     "\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)"
     "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)"
-  shows "indep_rv N (\<lambda>i. Y i \<circ> X i) I"
-  unfolding indep_rv_def
+  shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I"
+  unfolding indep_vars_def
 proof
-  from rv `indep_rv M' X I`
+  from rv `indep_vars M' X I`
   show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)"
-    by (auto intro!: measurable_comp simp: indep_rv_def)
+    by (auto intro!: measurable_comp simp: indep_vars_def)
 
   have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
-    using `indep_rv M' X I` by (simp add: indep_rv_def)
+    using `indep_vars M' X I` by (simp add: indep_vars_def)
   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"
   proof (rule indep_sets_mono_sets)
     fix i assume "i \<in> I"
-    with `indep_rv M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
-      unfolding indep_rv_def measurable_def by auto
+    with `indep_vars M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
+      unfolding indep_vars_def measurable_def by auto
     { fix A assume "A \<in> sets (N i)"
       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)"
         by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
@@ -793,13 +796,13 @@
   qed
 qed
 
-lemma (in prob_space) indep_rvD:
-  assumes X: "indep_rv M' X I"
+lemma (in prob_space) indep_varsD:
+  assumes X: "indep_vars M' X I"
   assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
   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))"
 proof (rule indep_setsD)
   show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
-    using X by (auto simp: indep_rv_def)
+    using X by (auto simp: indep_vars_def)
   show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto
   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)}"
     using I by (auto intro: sigma_sets.Basic)
@@ -808,7 +811,7 @@
 lemma (in prob_space) indep_distribution_eq_measure:
   assumes I: "I \<noteq> {}" "finite I"
   assumes rv: "\<And>i. random_variable (M' i) (X i)"
-  shows "indep_rv M' X I \<longleftrightarrow>
+  shows "indep_vars M' X I \<longleftrightarrow>
     (\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)).
       distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A =
       finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)) A)"
@@ -827,7 +830,7 @@
 
   show ?thesis
   proof (intro iffI ballI)
-    assume "indep_rv M' X I"
+    assume "indep_vars M' X I"
     fix A assume "A \<in> sets P.P"
     moreover
     have "D.prob A = P.prob A"
@@ -856,7 +859,7 @@
       with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i -` F i \<inter> space M)"
         using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def)
       also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` F i \<inter> space M))"
-        using `indep_rv M' X I` I F by (rule indep_rvD)
+        using `indep_vars M' X I` I F by (rule indep_varsD)
       also have "\<dots> = P.prob E"
         using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def)
       finally show "D.prob E = P.prob E" .
@@ -867,8 +870,8 @@
     assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A"
     have [simp]: "\<And>i. sigma (M' i) = M' i"
       using rv by (intro sigma_algebra.sigma_eq) simp
-    have "indep_rv (\<lambda>i. sigma (M' i)) X I"
-    proof (subst indep_rv_finite[OF I])
+    have "indep_vars (\<lambda>i. sigma (M' i)) X I"
+    proof (subst indep_vars_finite[OF I])
       fix i assume [simp]: "i \<in> I"
       show "random_variable (sigma (M' i)) (X i)"
         using rv[of i] by simp
@@ -890,9 +893,32 @@
         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))" .
       qed
     qed
-    then show "indep_rv M' X I"
+    then show "indep_vars M' X I"
       by simp
   qed
 qed
 
+lemma (in prob_space) indep_varD:
+  assumes indep: "indep_var Ma A Mb B"
+  assumes sets: "Xa \<in> sets Ma" "Xb \<in> sets Mb"
+  shows "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
+    prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
+proof -
+  have "prob ((\<lambda>x. (A x, B x)) -` (Xa \<times> Xb) \<inter> space M) =
+    prob (\<Inter>i\<in>UNIV. (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
+    by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool)
+  also have "\<dots> = (\<Prod>i\<in>UNIV. prob (bool_case A B i -` bool_case Xa Xb i \<inter> space M))"
+    using indep unfolding indep_var_def
+    by (rule indep_varsD) (auto split: bool.split intro: sets)
+  also have "\<dots> = prob (A -` Xa \<inter> space M) * prob (B -` Xb \<inter> space M)"
+    unfolding UNIV_bool by simp
+  finally show ?thesis .
+qed
+
+lemma (in prob_space) indep_var_distributionD:
+  assumes "indep_var Ma A Mb B"
+  assumes "Xa \<in> sets Ma" "Xb \<in> sets Mb"
+  shows "joint_distribution A B (Xa \<times> Xb) = distribution A Xa * distribution B Xb"
+  unfolding distribution_def using assms by (rule indep_varD)
+
 end