--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,229 @@
+(* Title: Sigma_Algebra.thy
+ Author: Stefan Richter, Markus Wenzel, TU Muenchen
+ Plus material from the Hurd/Coble measure theory development,
+ translated by Lawrence Paulson.
+*)
+
+header {* Sigma Algebras *}
+
+theory Sigma_Algebra imports Complex_Main begin
+
+text {* Sigma algebras are an elementary concept in measure
+ theory. To measure --- that is to integrate --- functions, we first have
+ to measure sets. Unfortunately, when dealing with a large universe,
+ it is often not possible to consistently assign a measure to every
+ subset. Therefore it is necessary to define the set of measurable
+ subsets of the universe. A sigma algebra is such a set that has
+ three very natural and desirable properties. *}
+
+subsection {* Algebras *}
+
+record 'a algebra =
+ space :: "'a set"
+ sets :: "'a set set"
+
+locale algebra =
+ fixes M
+ assumes space_closed: "sets M \<subseteq> Pow (space M)"
+ and empty_sets [iff]: "{} \<in> sets M"
+ and compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
+ and Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
+
+lemma (in algebra) top [iff]: "space M \<in> sets M"
+ by (metis Diff_empty compl_sets empty_sets)
+
+lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
+ by (metis PowD contra_subsetD space_closed)
+
+lemma (in algebra) Int [intro]:
+ assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
+proof -
+ have "((space M - a) \<union> (space M - b)) \<in> sets M"
+ by (metis a b compl_sets Un)
+ moreover
+ have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))"
+ using space_closed a b
+ by blast
+ ultimately show ?thesis
+ by (metis compl_sets)
+qed
+
+lemma (in algebra) Diff [intro]:
+ assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
+proof -
+ have "(a \<inter> (space M - b)) \<in> sets M"
+ by (metis a b compl_sets Int)
+ moreover
+ have "a - b = (a \<inter> (space M - b))"
+ by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
+ ultimately show ?thesis
+ by metis
+qed
+
+lemma (in algebra) finite_union [intro]:
+ "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
+ by (induct set: finite) (auto simp add: Un)
+
+
+subsection {* Sigma Algebras *}
+
+locale sigma_algebra = algebra +
+ assumes countable_UN [intro]:
+ "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+
+lemma (in sigma_algebra) countable_INT:
+ assumes a: "range a \<subseteq> sets M"
+ shows "(\<Inter>i::nat. a i) \<in> sets M"
+proof -
+ have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
+ by (blast intro: countable_UN compl_sets a)
+ moreover
+ have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a
+ by blast
+ ultimately show ?thesis by metis
+qed
+
+
+lemma algebra_Pow:
+ "algebra (| space = sp, sets = Pow sp |)"
+ by (auto simp add: algebra_def)
+
+lemma sigma_algebra_Pow:
+ "sigma_algebra (| space = sp, sets = Pow sp |)"
+ by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow)
+
+subsection {* Binary Unions *}
+
+definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
+ where "binary a b = (\<lambda>\<^isup>x. b)(0 := a)"
+
+lemma range_binary_eq: "range(binary a b) = {a,b}"
+ by (auto simp add: binary_def)
+
+lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
+ by (simp add: UNION_eq_Union_image range_binary_eq)
+
+lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
+ by (simp add: INTER_eq_Inter_image range_binary_eq)
+
+lemma sigma_algebra_iff:
+ "sigma_algebra M \<longleftrightarrow>
+ algebra M & (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+ by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
+
+lemma sigma_algebra_iff2:
+ "sigma_algebra M \<longleftrightarrow>
+ sets M \<subseteq> Pow (space M) &
+ {} \<in> sets M & (\<forall>s \<in> sets M. space M - s \<in> sets M) &
+ (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+ by (force simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
+ algebra_def Un_range_binary)
+
+
+subsection {* Initial Sigma Algebra *}
+
+text {*Sigma algebras can naturally be created as the closure of any set of
+ sets with regard to the properties just postulated. *}
+
+inductive_set
+ sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+ for sp :: "'a set" and A :: "'a set set"
+ where
+ Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
+ | Empty: "{} \<in> sigma_sets sp A"
+ | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
+ | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
+
+
+definition
+ sigma where
+ "sigma sp A = (| space = sp, sets = sigma_sets sp A |)"
+
+
+lemma space_sigma [simp]: "space (sigma X B) = X"
+ by (simp add: sigma_def)
+
+lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
+ by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
+
+lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
+ by (erule sigma_sets.induct, auto)
+
+lemma sigma_sets_Un:
+ "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
+apply (simp add: Un_range_binary range_binary_eq)
+apply (metis Union COMBK_def binary_def fun_upd_apply)
+done
+
+lemma sigma_sets_Inter:
+ assumes Asb: "A \<subseteq> Pow sp"
+ shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
+proof -
+ assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
+ hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A"
+ by (rule sigma_sets.Compl)
+ hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
+ by (rule sigma_sets.Union)
+ hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A"
+ by (rule sigma_sets.Compl)
+ also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)"
+ by auto
+ also have "... = (\<Inter>i. a i)" using ai
+ by (blast dest: sigma_sets_into_sp [OF Asb])
+ finally show ?thesis .
+qed
+
+lemma sigma_sets_INTER:
+ assumes Asb: "A \<subseteq> Pow sp"
+ and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
+ shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
+proof -
+ from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
+ by (simp add: sigma_sets.intros sigma_sets_top)
+ hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
+ by (rule sigma_sets_Inter [OF Asb])
+ also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
+ by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
+ finally show ?thesis .
+qed
+
+lemma (in sigma_algebra) sigma_sets_subset:
+ assumes a: "a \<subseteq> sets M"
+ shows "sigma_sets (space M) a \<subseteq> sets M"
+proof
+ fix x
+ assume "x \<in> sigma_sets (space M) a"
+ from this show "x \<in> sets M"
+ by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
+qed
+
+lemma (in sigma_algebra) sigma_sets_eq:
+ "sigma_sets (space M) (sets M) = sets M"
+proof
+ show "sets M \<subseteq> sigma_sets (space M) (sets M)"
+ by (metis Set.subsetI sigma_sets.Basic space_closed)
+ next
+ show "sigma_sets (space M) (sets M) \<subseteq> sets M"
+ by (metis sigma_sets_subset subset_refl)
+qed
+
+lemma sigma_algebra_sigma_sets:
+ "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
+ apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
+ algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un)
+ apply (blast dest: sigma_sets_into_sp)
+ apply (blast intro: sigma_sets.intros)
+ done
+
+lemma sigma_algebra_sigma:
+ "a \<subseteq> Pow X \<Longrightarrow> sigma_algebra (sigma X a)"
+ apply (rule sigma_algebra_sigma_sets)
+ apply (auto simp add: sigma_def)
+ done
+
+lemma (in sigma_algebra) sigma_subset:
+ "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)"
+ by (simp add: sigma_def sigma_sets_subset)
+
+end
+