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