# HG changeset patch
# User hoelzl
# Date 1282914307 -7200
# Node ID a2d38b8b693e8b194bccbf2156a8bb93bcaf6f06
# Parent  df379a447753929edc688b279015e6e104dfc0c5
Introduced sigma algebra generated by function preimages.

diff -r df379a447753 -r a2d38b8b693e src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 14:06:12 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 15:05:07 2010 +0200
@@ -562,4 +562,5 @@
     unfolding conditional_expectation_def by (rule someI2_ex) blast
 qed
 
+
 end
diff -r df379a447753 -r a2d38b8b693e src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Aug 27 14:06:12 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Aug 27 15:05:07 2010 +0200
@@ -626,6 +626,51 @@
   thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
 qed
 
+subsection {* Sigma algebra generated by function preimages *}
+
+definition (in sigma_algebra)
+  "vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f -` A \<inter> S) ` sets M \<rparr>"
+
+lemma (in sigma_algebra) in_vimage_algebra[simp]:
+  "A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
+  by (simp add: vimage_algebra_def image_iff)
+
+lemma (in sigma_algebra) space_vimage_algebra[simp]:
+  "space (vimage_algebra S f) = S"
+  by (simp add: vimage_algebra_def)
+
+lemma (in sigma_algebra) sigma_algebra_vimage:
+  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
+  shows "sigma_algebra (vimage_algebra S f)"
+proof
+  fix A assume "A \<in> sets (vimage_algebra S f)"
+  then guess B unfolding in_vimage_algebra ..
+  then show "space (vimage_algebra S f) - A \<in> sets (vimage_algebra S f)"
+    using sets_into_space assms
+    by (auto intro!: bexI[of _ "space M - B"])
+next
+  fix A assume "A \<in> sets (vimage_algebra S f)"
+  then guess A' unfolding in_vimage_algebra .. note A' = this
+  fix B assume "B \<in> sets (vimage_algebra S f)"
+  then guess B' unfolding in_vimage_algebra .. note B' = this
+  then show "A \<union> B \<in> sets (vimage_algebra S f)"
+    using sets_into_space assms A' B'
+    by (auto intro!: bexI[of _ "A' \<union> B'"])
+next
+  fix A::"nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets (vimage_algebra S f)"
+  then have "\<forall>i. \<exists>B. A i = f -` B \<inter> S \<and> B \<in> sets M"
+    by (simp add: subset_eq) blast
+  from this[THEN choice] obtain B
+    where B: "\<And>i. A i = f -` B i \<inter> S" "range B \<subseteq> sets M" by auto
+  show "(\<Union>i. A i) \<in> sets (vimage_algebra S f)"
+    using B by (auto intro!: bexI[of _ "\<Union>i. B i"])
+qed auto
+
+lemma (in sigma_algebra) measurable_vimage_algebra:
+  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
+  shows "f \<in> measurable (vimage_algebra S f) M"
+    unfolding measurable_def using assms by force
+
 subsection {* A Two-Element Series *}
 
 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "