(* 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 [intro]:
assumes a: "range a \<subseteq> sets M"
shows "(\<Inter>i::nat. a i) \<in> sets M"
proof -
from a have "\<forall>i. a i \<in> sets M" by fast
hence "space M - (\<Union>i. space M - a i) \<in> sets M" by blast
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 (in sigma_algebra) gen_countable_UN:
fixes f :: "nat \<Rightarrow> 'c"
shows "I = range f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> (\<Union>x\<in>I. A x) \<in> sets M"
by auto
lemma (in sigma_algebra) gen_countable_INT:
fixes f :: "nat \<Rightarrow> 'c"
shows "I = range f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> (\<Inter>x\<in>I. A x) \<in> sets M"
by auto
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 (rule Union, simp add: binary_def COMBK_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)
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 (rule sigma_sets.Union, fast)
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