Introduced sigma algebra generated by function preimages.
--- 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
--- 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 "