# HG changeset patch
# User hoelzl
# Date 1306411926 -7200
# Node ID 73e2d802ea417f6b74786e6dfbd8f9d6a0cbc2a5
# Parent  11fd8c04ea2436d64dd599559fb45b3ce7b31b23
add lemma indep_rv_finite

diff -r 11fd8c04ea24 -r 73e2d802ea41 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:12:03 2011 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Thu May 26 14:12:06 2011 +0200
@@ -41,7 +41,7 @@
     (\<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"
 
-lemma (in prob_space) indep_sets_cong:
+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+
 
@@ -194,7 +194,7 @@
         qed }
       note indep_sets_insert = this
       have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>"
-      proof (rule dynkin_systemI', simp_all, safe)
+      proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe)
         show "indep_sets (G(j := {{}})) K"
           by (rule indep_sets_insert) auto
       next
@@ -266,7 +266,7 @@
       qed (insert sets_into_space, auto)
       then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq>
         sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>"
-      proof (rule dynkin_system.dynkin_subset, simp_all, safe)
+      proof (rule dynkin_system.dynkin_subset, simp_all cong del: indep_sets_cong, safe)
         fix X assume "X \<in> G j"
         then show "X \<in> events" using G `j \<in> K` by auto
         from `indep_sets G K`
@@ -322,6 +322,17 @@
   shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
   using indep_sets_sigma[OF assms] by (simp add: sets_sigma)
 
+lemma (in prob_space) indep_sets_sigma_sets_iff:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>"
+  shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I \<longleftrightarrow> indep_sets F I"
+proof
+  assume "indep_sets F I" then show "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
+    by (rule indep_sets_sigma_sets) fact
+next
+  assume "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" then show "indep_sets F I"
+    by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic)
+qed
+
 lemma (in prob_space) indep_sets2_eq:
   "indep_set 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)"
   unfolding indep_set_def
@@ -666,4 +677,104 @@
   qed
 qed
 
+lemma (in prob_space) indep_sets_finite:
+  assumes I: "I \<noteq> {}" "finite I"
+    and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events" "\<And>i. i \<in> I \<Longrightarrow> space M \<in> F i"
+  shows "indep_sets F I \<longleftrightarrow> (\<forall>A\<in>Pi I F. prob (\<Inter>j\<in>I. A j) = (\<Prod>j\<in>I. prob (A j)))"
+proof
+  assume *: "indep_sets F I"
+  from I show "\<forall>A\<in>Pi I F. prob (\<Inter>j\<in>I. A j) = (\<Prod>j\<in>I. prob (A j))"
+    by (intro indep_setsD[OF *] ballI) auto
+next
+  assume indep: "\<forall>A\<in>Pi I F. prob (\<Inter>j\<in>I. A j) = (\<Prod>j\<in>I. prob (A j))"
+  show "indep_sets F I"
+  proof (rule indep_setsI[OF F(1)])
+    fix A J assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
+    assume A: "\<forall>j\<in>J. A j \<in> F j"
+    let "?A j" = "if j \<in> J then A j else space M"
+    have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
+      using subset_trans[OF F(1) space_closed] J A
+      by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
+    also
+    from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
+      by (auto split: split_if_asm)
+    with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))"
+      by auto
+    also have "\<dots> = (\<Prod>j\<in>J. prob (A j))"
+      unfolding if_distrib setprod.If_cases[OF `finite I`]
+      using prob_space `J \<subseteq> I` by (simp add: Int_absorb1 setprod_1)
+    finally show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" ..
+  qed
+qed
+
+lemma (in prob_space) indep_rv_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>
+    (\<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. distribution (X j) (A j)))"
+proof -
+  from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)"
+    unfolding measurable_def by simp
+
+  { fix i assume "i\<in>I"
+    have "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (sigma (M' i))}
+      = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+      unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`]
+      by (subst sigma_sets_sigma_sets_eq) auto }
+  note this[simp]
+
+  { fix i assume "i\<in>I"
+    have "Int_stable \<lparr>space = space M, sets = {X i -` A \<inter> space M |A. A \<in> sets (M' i)}\<rparr>"
+    proof (rule Int_stableI)
+      fix a assume "a \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+      then obtain A where "a = X i -` A \<inter> space M" "A \<in> sets (M' i)" by auto
+      moreover
+      fix b assume "b \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+      then obtain B where "b = X i -` B \<inter> space M" "B \<in> sets (M' i)" by auto
+      moreover
+      have "(X i -` A \<inter> space M) \<inter> (X i -` B \<inter> space M) = X i -` (A \<inter> B) \<inter> space M" by auto
+      moreover note Int_stable[OF `i \<in> I`]
+      ultimately
+      show "a \<inter> b \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+        by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD)
+    qed }
+  note indep_sets_sigma_sets_iff[OF this, simp]
+ 
+  { fix i assume "i \<in> I"
+    { fix A assume "A \<in> sets (M' i)"
+      then have "A \<in> sets (sigma (M' i))" by (auto simp: sets_sigma intro: sigma_sets.Basic)
+      moreover
+      from rv[OF `i\<in>I`] have "X i \<in> measurable M (sigma (M' i))" by auto
+      ultimately
+      have "X i -` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) }
+    with X[OF `i\<in>I`] space[OF `i\<in>I`]
+    have "{X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events"
+      "space M \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+      by (auto intro!: exI[of _ "space (M' i)"]) }
+  note indep_sets_finite[OF I this, simp]
+  
+  have "(\<forall>A\<in>\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}. prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))) =
+    (\<forall>A\<in>\<Pi> i\<in>I. sets (M' i). prob ((\<Inter>j\<in>I. X j -` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x -` A x \<inter> space M)))"
+    (is "?L = ?R")
+  proof safe
+    fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. sets (M' i))"
+    from `?L`[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A `I \<noteq> {}`
+    show "prob ((\<Inter>j\<in>I. X j -` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x -` A x \<inter> space M))"
+      by (auto simp add: Pi_iff)
+  next
+    fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> sets (M' i)})"
+    from A have "\<forall>i\<in>I. \<exists>B. A i = X i -` B \<inter> space M \<and> B \<in> sets (M' i)" by auto
+    from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M"
+      "B \<in> (\<Pi> i\<in>I. sets (M' i))" by auto
+    from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}`
+    show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))"
+      by simp
+  qed
+  then show ?thesis using `I \<noteq> {}`
+    by (simp add: rv distribution_def indep_rv_def)
+qed
+
 end
diff -r 11fd8c04ea24 -r 73e2d802ea41 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:03 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu May 26 14:12:06 2011 +0200
@@ -555,6 +555,16 @@
 lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
   unfolding sigma_def sigma_sets_eq by simp
 
+lemma sigma_sigma_eq:
+  assumes "sets M \<subseteq> Pow (space M)"
+  shows "sigma (sigma M) = sigma M"
+  using sigma_algebra.sigma_eq[OF sigma_algebra_sigma, OF assms] .
+
+lemma sigma_sets_sigma_sets_eq:
+  "M \<subseteq> Pow S \<Longrightarrow> sigma_sets S (sigma_sets S M) = sigma_sets S M"
+  using sigma_sigma_eq[of "\<lparr> space = S, sets = M \<rparr>"]
+  by (simp add: sigma_def)
+
 lemma sigma_sets_singleton:
   assumes "X \<subseteq> S"
   shows "sigma_sets S { X } = { {}, X, S - X, S }"
@@ -587,6 +597,61 @@
     by (simp add: sigma_def)
 qed
 
+lemma sigma_sets_vimage_commute:
+  assumes X: "X \<in> space M \<rightarrow> space M'"
+  shows "{X -` A \<inter> space M |A. A \<in> sets (sigma M')}
+       = sigma_sets (space M) {X -` A \<inter> space M |A. A \<in> sets M'}" (is "?L = ?R")
+proof
+  show "?L \<subseteq> ?R"
+  proof clarify
+    fix A assume "A \<in> sets (sigma M')"
+    then have "A \<in> sigma_sets (space M') (sets M')" by (simp add: sets_sigma)
+    then show "X -` A \<inter> space M \<in> ?R"
+    proof induct
+      case (Basic B) then show ?case
+        by (auto intro!: sigma_sets.Basic)
+    next
+      case Empty then show ?case
+        by (auto intro!: sigma_sets.Empty)
+    next
+      case (Compl B)
+      have [simp]: "X -` (space M' - B) \<inter> space M = space M - (X -` B \<inter> space M)"
+        by (auto simp add: funcset_mem [OF X])
+      with Compl show ?case
+        by (auto intro!: sigma_sets.Compl)
+    next
+      case (Union F)
+      then show ?case
+        by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps
+                 intro!: sigma_sets.Union)
+    qed
+  qed
+  show "?R \<subseteq> ?L"
+  proof clarify
+    fix A assume "A \<in> ?R"
+    then show "\<exists>B. A = X -` B \<inter> space M \<and> B \<in> sets (sigma M')"
+    proof induct
+      case (Basic B) then show ?case by auto
+    next
+      case Empty then show ?case
+        by (auto simp: sets_sigma intro!: sigma_sets.Empty exI[of _ "{}"])
+    next
+      case (Compl B)
+      then obtain A where A: "B = X -` A \<inter> space M" "A \<in> sets (sigma M')" by auto
+      then have [simp]: "space M - B = X -` (space M' - A) \<inter> space M"
+        by (auto simp add: funcset_mem [OF X])
+      with A(2) show ?case
+        by (auto simp: sets_sigma intro: sigma_sets.Compl)
+    next
+      case (Union F)
+      then have "\<forall>i. \<exists>B. F i = X -` B \<inter> space M \<and> B \<in> sets (sigma M')" by auto
+      from choice[OF this] guess A .. note A = this
+      with A show ?case
+        by (auto simp: sets_sigma vimage_UN[symmetric] intro: sigma_sets.Union)
+    qed
+  qed
+qed
+
 section {* Measurable functions *}
 
 definition