(* Title: HOL/Analysis/Sigma_Algebra.thy Author: Stefan Richter, Markus Wenzel, TU München Author: Johannes Hölzl, TU München Plus material from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
*)
chapter\<open>Measure and Integration Theory\<close>
theory Sigma_Algebra imports
Complex_Main "HOL-Library.Countable_Set" "HOL-Library.FuncSet" "HOL-Library.Indicator_Function" "HOL-Library.Extended_Nonnegative_Real" "HOL-Library.Disjoint_Sets" begin
section \<open>Sigma Algebra\<close>
text\<open>Sigma algebras are an elementary concept in measure theory. To measure --- that isto 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.\<close>
subsection \<open>Families of sets\<close>
locale\<^marker>\<open>tag important\<close> subset_class = fixes\<Omega> :: "'a set" and M :: "'a set set" assumes space_closed: "M \ Pow \"
lemma (in subset_class) sets_into_space: "x \ M \ x \ \" by (metis PowD contra_subsetD space_closed)
subsubsection \<open>Semiring of sets\<close>
locale\<^marker>\<open>tag important\<close> semiring_of_sets = subset_class + assumes empty_sets[iff]: "{} \ M" assumes Int[intro]: "\a b. a \ M \ b \ M \ a \ b \ M" assumes Diff_cover: "\a b. a \ M \ b \ M \ \C\M. finite C \ disjoint C \ a - b = \C"
lemma (in semiring_of_sets) finite_INT[intro]: assumes"finite I""I \ {}" "\i. i \ I \ A i \ M" shows"(\i\I. A i) \ M" using assms by (induct rule: finite_ne_induct) auto
lemma (in semiring_of_sets) Int_space_eq1 [simp]: "x \ M \ \ \ x = x" by (metis Int_absorb1 sets_into_space)
lemma (in semiring_of_sets) Int_space_eq2 [simp]: "x \ M \ x \ \ = x" by (metis Int_absorb2 sets_into_space)
lemma (in semiring_of_sets) sets_Collect_conj: assumes"{x\\. P x} \ M" "{x\\. Q x} \ M" shows"{x\\. Q x \ P x} \ M" proof - have"{x\\. Q x \ P x} = {x\\. Q x} \ {x\\. P x}" by auto with assms show ?thesis by auto qed
lemma (in semiring_of_sets) sets_Collect_finite_All': assumes"\i. i \ S \ {x\\. P i x} \ M" "finite S" "S \ {}" shows"{x\\. \i\S. P i x} \ M" proof - have"{x\\. \i\S. P i x} = (\i\S. {x\\. P i x})" using\<open>S \<noteq> {}\<close> by auto with assms show ?thesis by auto qed
subsubsection \<open>Ring of sets\<close>
locale\<^marker>\<open>tag important\<close> ring_of_sets = semiring_of_sets + assumes Un [intro]: "\a b. a \ M \ b \ M \ a \ b \ M"
lemma (in ring_of_sets) finite_Union [intro]: "finite X \ X \ M \ \X \ M" by (induct set: finite) (auto simp add: Un)
lemma (in ring_of_sets) finite_UN[intro]: assumes"finite I"and"\i. i \ I \ A i \ M" shows"(\i\I. A i) \ M" using assms by induct auto
lemma (in ring_of_sets) Diff [intro]: assumes"a \ M" "b \ M" shows "a - b \ M" using Diff_cover[OF assms] by auto
lemma ring_of_setsI: assumes space_closed: "M \ Pow \" assumes empty_sets[iff]: "{} \ M" assumes Un[intro]: "\a b. a \ M \ b \ M \ a \ b \ M" assumes Diff[intro]: "\a b. a \ M \ b \ M \ a - b \ M" shows"ring_of_sets \ M" proof fix a b assume ab: "a \ M" "b \ M" from ab show"\C\M. finite C \ disjoint C \ a - b = \C" by (intro exI[of _ "{a - b}"]) (auto simp: disjoint_def) have"a \ b = a - (a - b)" by auto alsohave"\ \ M" using ab by auto finallyshow"a \ b \ M" . qed fact+
lemma ring_of_sets_iff: "ring_of_sets \ M \ M \ Pow \ \ {} \ M \ (\a\M. \b\M. a \b \ M) \ (\a\M. \b\M. a - b \ M)" proof assume"ring_of_sets \ M" theninterpret ring_of_sets \<Omega> M . show"M \ Pow \ \ {} \ M \ (\a\M. \b\M. a \ b \ M) \ (\a\M. \b\M. a - b \ M)" using space_closed by auto qed (auto intro!: ring_of_setsI)
lemma (in ring_of_sets) insert_in_sets: assumes"{x} \ M" "A \ M" shows "insert x A \ M" proof - have"{x} \ A \ M" using assms by (rule Un) thus ?thesis by auto qed
lemma (in ring_of_sets) sets_Collect_disj: assumes"{x\\. P x} \ M" "{x\\. Q x} \ M" shows"{x\\. Q x \ P x} \ M" proof - have"{x\\. Q x \ P x} = {x\\. Q x} \ {x\\. P x}" by auto with assms show ?thesis by auto qed
lemma (in ring_of_sets) sets_Collect_finite_Ex: assumes"\i. i \ S \ {x\\. P i x} \ M" "finite S" shows"{x\\. \i\S. P i x} \ M" proof - have"{x\\. \i\S. P i x} = (\i\S. {x\\. P i x})" by auto with assms show ?thesis by auto qed
lemma (in algebra) compl_sets [intro]: "a \ M \ \ - a \ M" by auto
proposition algebra_iff_Un: "algebra \ M \
M \<subseteq> Pow \<Omega> \<and>
{} \<in> M \<and>
(\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
(\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un") proof assume"algebra \ M" theninterpret algebra \<Omega> M . show ?Un using sets_into_space by auto next assume ?Un thenhave"\ \ M" by auto interpret ring_of_sets \<Omega> M proof (rule ring_of_setsI) show\<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" using\<open>?Un\<close> by auto fix a b assume a: "a \ M" and b: "b \ M" thenshow"a \ b \ M" using \?Un\ by auto have"a - b = \ - ((\ - a) \ b)" using\<Omega> a b by auto thenshow"a - b \ M" using a b \<open>?Un\<close> by auto qed show"algebra \ M" proof qed fact qed
proposition algebra_iff_Int: "algebra \ M \
M \<subseteq> Pow \<Omega> & {} \<in> M &
(\<forall>a \<in> M. \<Omega> - a \<in> M) &
(\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int") proof assume"algebra \ M" theninterpret algebra \<Omega> M . show ?Int using sets_into_space by auto next assume ?Int show"algebra \ M" unfolding algebra_iff_Un proof (intro conjI ballI) show\<Omega>: "M \<subseteq> Pow \<Omega>" "{} \<in> M" using\<open>?Int\<close> by auto from\<open>?Int\<close> show "\<And>a. a \<in> M \<Longrightarrow> \<Omega> - a \<in> M" by auto fix a b assume M: "a \ M" "b \ M" hence"a \ b = \ - ((\ - a) \ (\ - b))" using\<Omega> by blast alsohave"... \ M" using M \<open>?Int\<close> by auto finallyshow"a \ b \ M" . qed qed
lemma (in algebra) sets_Collect_neg: assumes"{x\\. P x} \ M" shows"{x\\. \ P x} \ M" proof - have"{x\\. \ P x} = \ - {x\\. P x}" by auto with assms show ?thesis by auto qed
lemma (in algebra) sets_Collect_imp: "{x\\. P x} \ M \ {x\\. Q x} \ M \ {x\\. Q x \ P x} \ M" unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg)
lemma (in algebra) sets_Collect_const: "{x\\. P} \ M" by (cases P) auto
lemma algebra_single_set: "X \ S \ algebra S { {}, X, S - X, S }" by (auto simp: algebra_iff_Int)
abbreviation (in algebra) "restricted_space A \ ((\) A) ` M"
lemma (in algebra) restricted_algebra: assumes"A \ M" shows "algebra A (restricted_space A)" using assms by (auto simp: algebra_iff_Int)
subsubsection \<open>Sigma Algebras\<close>
locale\<^marker>\<open>tag important\<close> sigma_algebra = algebra + assumes countable_nat_UN [intro]: "\A. range A \ M \ (\i::nat. A i) \ M"
lemma (in algebra) is_sigma_algebra: assumes"finite M" shows"sigma_algebra \ M" proof fix A :: "nat \ 'a set" assume "range A \ M" thenhave"(\i. A i) = (\s\M \ range A. s)" by auto alsohave"(\s\M \ range A. s) \ M" using\<open>finite M\<close> by auto finallyshow"(\i. A i) \ M" . qed
lemma countable_UN_eq: fixes A :: "'i::countable \ 'a set" shows"(range A \ M \ (\i. A i) \ M) \
(range (A \<circ> from_nat) \<subseteq> M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> M)" proof - let ?A' = "A \ from_nat" have *: "(\i. ?A' i) = (\i. A i)" by (metis fun.set_map surj_from_nat) have"A ` range from_nat = range A" using surj_from_nat by simp thenhave **: "range ?A' = range A" by (metis image_comp) show ?thesis unfolding * ** .. qed
lemma (in sigma_algebra) countable_Union [intro]: assumes"countable X""X \ M" shows "\X \ M" proof cases assume"X \ {}" hence"\X = (\n. from_nat_into X n)" using assms by (auto cong del: SUP_cong) alsohave"\ \ M" using assms by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into subsetD) finallyshow ?thesis . qed simp
lemma (in sigma_algebra) countable_UN[intro]: fixes A :: "'i::countable \ 'a set" assumes"A`X \ M" shows"(\x\X. A x) \ M" proof - let ?A = "\i. if i \ X then A i else {}" from assms have"range ?A \ M" by auto with countable_nat_UN[of "?A \ from_nat"] countable_UN_eq[of ?A M] have"(\x. ?A x) \ M" by auto moreoverhave"(\x. ?A x) = (\x\X. A x)" by (auto split: if_split_asm) ultimatelyshow ?thesis by simp qed
lemma (in sigma_algebra) countable_UN': fixes A :: "'i \ 'a set" assumes X: "countable X" assumes A: "A`X \ M" shows"(\x\X. A x) \ M" using A X countable_Union countable_image by blast
lemma (in sigma_algebra) countable_UN'': "\ countable X; \x y. x \ X \ A x \ M \ \ (\x\X. A x) \ M" by blast
lemma (in sigma_algebra) countable_INT [intro]: fixes A :: "'i::countable \ 'a set" assumes A: "A`X \ M" "X \ {}" shows"(\i\X. A i) \ M" proof - from A have"\i\X. A i \ M" by fast hence"\ - (\i\X. \ - A i) \ M" by blast moreover have"(\i\X. A i) = \ - (\i\X. \ - A i)" using space_closed A by blast ultimatelyshow ?thesis by metis qed
lemma (in sigma_algebra) countable_INT': fixes A :: "'i \ 'a set" assumes X: "countable X""X \ {}" assumes A: "A`X \ M" shows"(\x\X. A x) \ M" proof - have"(\x\X. A x) = (\i\to_nat_on X ` X. A (from_nat_into X i))" using X by auto alsohave"\ \ M" using A X by (intro countable_INT) auto finallyshow ?thesis . qed
lemma (in sigma_algebra) countable_INT'': "UNIV \ M \ countable I \ (\i. i \ I \ F i \ M) \ (\i\I. F i) \ M" by (cases "I = {}") (auto intro: countable_INT')
lemma (in sigma_algebra) countable: assumes"\a. a \ A \ {a} \ M" "countable A" shows"A \ M" proof - have"(\a\A. {a}) \ M" using assms by (intro countable_UN') auto alsohave"(\a\A. {a}) = A" by auto finallyshow ?thesis by auto qed
lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)" by (auto simp: ring_of_sets_iff)
lemma algebra_Pow: "algebra sp (Pow sp)" by (auto simp: algebra_iff_Un)
lemma sigma_algebra_iff: "sigma_algebra \ M \ algebra \ M \ (\A. range A \ M \ (\i::nat. A i) \ M)" by (simp add: sigma_algebra_def sigma_algebra_axioms_def)
lemma (in sigma_algebra) sets_Collect_countable_All: assumes"\i. {x\\. P i x} \ M" shows"{x\\. \i::'i::countable. P i x} \ M" proof - have"{x\\. \i. P i x} = (\i. {x\\. P i x})" by auto with assms show ?thesis by auto qed
lemma (in sigma_algebra) sets_Collect_countable_Ex: assumes"\i. {x\\. P i x} \ M" shows"{x\\. \i::'i::countable. P i x} \ M" proof - have"{x\\. \i. P i x} = (\i. {x\\. P i x})" by auto with assms show ?thesis by auto qed
lemma (in sigma_algebra) sets_Collect_countable_Ex': assumes"\i. i \ I \ {x\\. P i x} \ M" assumes"countable I" shows"{x\\. \i\I. P i x} \ M" proof - have"{x\\. \i\I. P i x} = (\i\I. {x\\. P i x})" by auto with assms show ?thesis by (auto intro!: countable_UN') qed
lemma (in sigma_algebra) sets_Collect_countable_All': assumes"\i. i \ I \ {x\\. P i x} \ M" assumes"countable I" shows"{x\\. \i\I. P i x} \ M" proof - have"{x\\. \i\I. P i x} = (\i\I. {x\\. P i x}) \ \" by auto with assms show ?thesis by (cases "I = {}") (auto intro!: countable_INT') qed
lemma (in sigma_algebra) sets_Collect_countable_Ex1': assumes"\i. i \ I \ {x\\. P i x} \ M" assumes"countable I" shows"{x\\. \!i\I. P i x} \ M" proof - have"{x\\. \!i\I. P i x} = {x\\. \i\I. P i x \ (\j\I. P j x \ i = j)}" by auto with assms show ?thesis by (auto intro!: sets_Collect_countable_All' sets_Collect_countable_Ex' sets_Collect_conj sets_Collect_imp sets_Collect_const) qed
lemma (in sigma_algebra) sets_Collect_countable_Ball: assumes"\i. {x\\. P i x} \ M" shows"{x\\. \i::'i::countable\X. P i x} \ M" unfolding Ball_def by (intro sets_Collect assms)
lemma (in sigma_algebra) sets_Collect_countable_Bex: assumes"\i. {x\\. P i x} \ M" shows"{x\\. \i::'i::countable\X. P i x} \ M" unfolding Bex_def by (intro sets_Collect assms)
lemma sigma_algebra_single_set: assumes"X \ S" shows"sigma_algebra S { {}, X, S - X, S }" using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp
definition binary :: "'a \ 'a \ nat \ 'a" where"binary a b = (\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 \ b = (\i::nat. binary a b i)" by (simp add: range_binary_eq cong del: SUP_cong_simp)
lemma Int_range_binary: "a \ b = (\i::nat. binary a b i)" by (simp add: range_binary_eq cong del: INF_cong_simp)
lemma sigma_algebra_iff2: "sigma_algebra \ M \
M \<subseteq> Pow \<Omega> \<and> {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M) \<and> (\<forall>A. range A \<subseteq> M \<longrightarrow>(\<Union> i::nat. A i) \<in> M)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?V \<and> ?W") proof assume ?P theninterpret sigma_algebra \<Omega> M . from space_closed show"?R \ ?S \ ?V \ ?W" by auto next assume"?R \ ?S \ ?V \ ?W" thenhave ?R ?S ?V ?W by simp_all show ?P proof (rule sigma_algebra.intro) show"sigma_algebra_axioms M" using\<open>?W\<close> sigma_algebra_axioms_def by blast from\<open>?W\<close> have *: "range (binary a b) \<subseteq> M \<Longrightarrow> \<Union> (range (binary a b)) \<in> M" for a b by auto show"algebra \ M" unfolding algebra_iff_Un using\<open>?R\<close> \<open>?S\<close> \<open>?V\<close> * by (auto simp add: range_binary_eq) qed qed
text\<^marker>\<open>tag important\<close> \<open>Sigma algebras can naturally be created as the closure of any set of
M with regard to the properties just postulated.\<close>
inductive_set\<^marker>\<open>tag important\<close> sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" for sp :: "'a set"and A :: "'a set set" where
Basic[intro, simp]: "a \ A \ a \ sigma_sets sp A"
| Empty: "{} \ sigma_sets sp A"
| Compl: "a \ sigma_sets sp A \ sp - a \ sigma_sets sp A"
| Union: "(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A"
lemma (in sigma_algebra) sigma_sets_subset: assumes a: "a \ M" shows"sigma_sets \ a \ M" proof fix x assume"x \ sigma_sets \ a" thenshow"x \ M" by (induct rule: sigma_sets.induct, auto) (metis a subsetD) qed
lemma sigma_sets_into_sp: "A \ Pow sp \ x \ sigma_sets sp A \ x \ sp" by (erule sigma_sets.induct, auto)
lemma sigma_sets_least_sigma_algebra: assumes"A \ Pow S" shows"sigma_sets S A = \{B. A \ B \ sigma_algebra S B}" proof safe fix B X assume"A \ B" and sa: "sigma_algebra S B" and X: "X \ sigma_sets S A" from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF \<open>A \<subseteq> B\<close>] X show"X \ B" by auto next fix X assume"X \ \{B. A \ B \ sigma_algebra S B}" thenhave [intro!]: "\B. A \ B \ sigma_algebra S B \ X \ B" by simp have"A \ sigma_sets S A" using assms by auto moreoverhave"sigma_algebra S (sigma_sets S A)" using assms by (intro sigma_algebra_sigma_sets[of A]) auto ultimatelyshow"X \ sigma_sets S A" by auto qed
lemma binary_in_sigma_sets: "binary a b i \ sigma_sets sp A" if "a \ sigma_sets sp A" and "b \ sigma_sets sp A" using that by (simp add: binary_def)
lemma sigma_sets_Un: "a \ b \ sigma_sets sp A" if "a \ sigma_sets sp A" and "b \ sigma_sets sp A" using that by (simp add: Un_range_binary binary_in_sigma_sets Union)
lemma sigma_sets_Inter: assumes Asb: "A \ Pow sp" shows"(\i::nat. a i \ sigma_sets sp A) \ (\i. a i) \ sigma_sets sp A" proof - assume ai: "\i::nat. a i \ sigma_sets sp A" hence"\i::nat. sp-(a i) \ sigma_sets sp A" by (rule sigma_sets.Compl) hence"(\i. sp-(a i)) \ sigma_sets sp A" by (rule sigma_sets.Union) hence"sp-(\i. sp-(a i)) \ sigma_sets sp A" by (rule sigma_sets.Compl) alsohave"sp-(\i. sp-(a i)) = sp Int (\i. a i)" by auto alsohave"... = (\i. a i)" using ai by (blast dest: sigma_sets_into_sp [OF Asb]) finallyshow ?thesis . qed
lemma sigma_sets_INTER: assumes Asb: "A \ Pow sp" and ai: "\i::nat. i \ S \ a i \ sigma_sets sp A" and non: "S \ {}" shows"(\i\S. a i) \ sigma_sets sp A" proof - from ai have"\i. (if i\S then a i else sp) \ sigma_sets sp A" by (simp add: sigma_sets.intros(2-) sigma_sets_top) hence"(\i. (if i\S then a i else sp)) \ sigma_sets sp A" by (rule sigma_sets_Inter [OF Asb]) alsohave"(\i. (if i\S then a i else sp)) = (\i\S. a i)" by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ finallyshow ?thesis . qed
lemma sigma_sets_UNION: "countable B \ (\b. b \ B \ b \ sigma_sets X A) \ \ B \ sigma_sets X A" using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A] by (cases "B = {}") (simp_all add: sigma_sets.Empty cong del: SUP_cong)
lemma (in sigma_algebra) sigma_sets_eq: "sigma_sets \ M = M" using sigma_sets_subset by blast
lemma sigma_sets_eqI: assumes A: "\a. a \ A \ a \ sigma_sets M B" assumes B: "\b. b \ B \ b \ sigma_sets M A" shows"sigma_sets M A = sigma_sets M B" proof (intro set_eqI iffI) fix a assume"a \ sigma_sets M A" from this A show"a \ sigma_sets M B" by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic) next fix b assume"b \ sigma_sets M B" from this B show"b \ sigma_sets M A" by induct (auto intro!: sigma_sets.intros(2-) del: sigma_sets.Basic) qed
lemma sigma_sets_subseteq: assumes"A \ B" shows"sigma_sets X A \ sigma_sets X B" proof fix x assume"x \ sigma_sets X A" then show "x \ sigma_sets X B" by induct (insert \<open>A \<subseteq> B\<close>, auto intro: sigma_sets.intros(2-)) qed
lemma sigma_sets_mono: assumes"A \ sigma_sets X B" shows"sigma_sets X A \ sigma_sets X B" proof fix x assume"x \ sigma_sets X A" thenshow"x \ sigma_sets X B" by induct (insert \<open>A \<subseteq> sigma_sets X B\<close>, auto intro: sigma_sets.intros(2-)) qed
lemma sigma_sets_mono': assumes"A \ B" shows"sigma_sets X A \ sigma_sets X B" by (simp add: assms sigma_sets_subseteq)
lemma sigma_sets_superset_generator: "A \ sigma_sets X A" by auto
lemma (in sigma_algebra) restriction_in_sets: fixes A :: "nat \ 'a set" assumes"S \ M" and *: "range A \ (\A. S \ A) ` M" (is "_ \ ?r") shows"range A \ M" "(\i. A i) \ (\A. S \ A) ` M" proof -
{ fix i have"A i \ ?r" using * by auto hence"\B. A i = B \ S \ B \ M" by auto hence"A i \ S" "A i \ M" using \S \ M\ by auto } thus"range A \ M" "(\i. A i) \ (\A. S \ A) ` M" by (auto intro!: image_eqI[of _ _ "(\i. A i)"]) qed
lemma (in sigma_algebra) restricted_sigma_algebra: assumes"S \ M" shows"sigma_algebra S (restricted_space S)" unfolding sigma_algebra_def sigma_algebra_axioms_def using assms restricted_algebra restriction_in_sets(2) by presburger
lemma sigma_sets_Int: assumes"A \ sigma_sets sp st" "A \ sp" shows"(\) A ` sigma_sets sp st = sigma_sets A ((\) A ` st)" proof (intro equalityI subsetI) fix x assume"x \ (\) A ` sigma_sets sp st" thenobtain y where"y \ sigma_sets sp st" "x = y \ A" by auto thenhave"x \ sigma_sets (A \ sp) ((\) A ` st)" proof (induct arbitrary: x) case (Compl a) thenshow ?case by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps) next case (Union a) thenshow ?case by (auto intro!: sigma_sets.Union
simp add: UN_extend_simps simp del: UN_simps) qed (auto intro!: sigma_sets.intros(2-)) thenshow"x \ sigma_sets A ((\) A ` st)" using\<open>A \<subseteq> sp\<close> by (simp add: Int_absorb2) next fix x assume"x \ sigma_sets A ((\) A ` st)" thenshow"x \ (\) A ` sigma_sets sp st" proof induct case (Compl a) thenobtain x where"a = A \ x" "x \ sigma_sets sp st" by auto thenshow ?caseusing\<open>A \<subseteq> sp\<close> by (force simp add: image_iff intro!: bexI[of _ "sp - x"] sigma_sets.Compl) next case (Union a) thenhave"\i. \x. x \ sigma_sets sp st \ a i = A \ x" by (auto simp: image_iff Bex_def) thenobtain f where"\x. f x \ sigma_sets sp st \ a x = A \ f x" by metis thenshow ?case by (auto intro!: bexI[of _ "(\x. f x)"] sigma_sets.Union
simp add: image_iff) qed (auto intro!: sigma_sets.intros(2-)) qed
lemma sigma_sets_empty_eq: "sigma_sets A {} = {{}, A}" proof (intro set_eqI iffI) fix a assume"a \ sigma_sets A {}" then show "a \ {{}, A}" by induct blast+ qed (auto intro: sigma_sets.Empty sigma_sets_top)
lemma sigma_sets_single[simp]: "sigma_sets A {A} = {{}, A}" proof (intro set_eqI iffI) fix x assume"x \ sigma_sets A {A}" thenshow"x \ {{}, A}" by induct blast+ next fix x assume"x \ {{}, A}" thenshow"x \ sigma_sets A {A}" by (auto intro: sigma_sets.Empty sigma_sets_top) qed
lemma sigma_sets_sigma_sets_eq: "M \ Pow S \ sigma_sets S (sigma_sets S M) = sigma_sets S M" by (rule sigma_algebra.sigma_sets_eq[OF sigma_algebra_sigma_sets, of M S]) auto
lemma sigma_sets_singleton: assumes"X \ S" shows"sigma_sets S { X } = { {}, X, S - X, S }" proof - interpret sigma_algebra S "{ {}, X, S - X, S }" by (rule sigma_algebra_single_set) fact have"sigma_sets S { X } \ sigma_sets S { {}, X, S - X, S }" by (rule sigma_sets_subseteq) simp moreoverhave"\ = { {}, X, S - X, S }" using sigma_sets_eq by simp moreover
{ fix A assume"A \ { {}, X, S - X, S }" thenhave"A \ sigma_sets S { X }" by (auto intro: sigma_sets.intros(2-) sigma_sets_top) } ultimatelyhave"sigma_sets S { X } = sigma_sets S { {}, X, S - X, S }" by (intro antisym) auto with sigma_sets_eq show ?thesis by simp qed
lemma restricted_sigma: assumes S: "S \ sigma_sets \ M" and M: "M \ Pow \" shows"algebra.restricted_space (sigma_sets \ M) S = sigma_sets S (algebra.restricted_space M S)" by (meson M S sigma_sets_Int sigma_sets_into_sp)
lemma sigma_sets_vimage_commute: assumes X: "X \ \ \ \'" shows"{X -` A \ \ |A. A \ sigma_sets \' M'}
= sigma_sets \<Omega> {X -` A \<inter> \<Omega> |A. A \<in> M'}" (is "?L = ?R") proof show"?L \ ?R" proof clarify fix A assume"A \ sigma_sets \' M'" thenshow"X -` A \ \ \ ?R" proof induct case Empty thenshow ?case by (auto intro!: sigma_sets.Empty) next case (Compl B) have [simp]: "X -` (\' - B) \ \ = \ - (X -` B \ \)" by (auto simp add: funcset_mem [OF X]) with Compl show ?case by (auto intro!: sigma_sets.Compl) next case (Union F) thenshow ?case by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps
intro!: sigma_sets.Union) qed auto qed show"?R \ ?L" proof clarify fix A assume"A \ ?R" thenshow"\B. A = X -` B \ \ \ B \ sigma_sets \' M'" proof induct case (Basic B) thenshow ?caseby auto next case Empty thenshow ?case by (auto intro!: sigma_sets.Empty exI[of _ "{}"]) next case (Compl B) thenobtain A where A: "B = X -` A \ \" "A \ sigma_sets \' M'" by auto thenhave [simp]: "\ - B = X -` (\' - A) \ \" by (auto simp add: funcset_mem [OF X]) with A(2) show ?case by (auto intro: sigma_sets.Compl) next case (Union F) thenhave"\i. \B. F i = X -` B \ \ \ B \ sigma_sets \' M'" by auto thenobtain A where"\x. F x = X -` A x \ \ \ A x \ sigma_sets \' M'" by metis thenshow ?case by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union) qed qed qed
lemma (in ring_of_sets) UNION_in_sets: fixes A:: "nat \ 'a set" assumes A: "range A \ M" shows"(\i\{0.. M" proof (induct n) case 0 show ?caseby simp next case (Suc n) thus ?case using assms by blast qed
lemma (in ring_of_sets) range_disjointed_sets: assumes A: "range A \ M" shows"range (disjointed A) \ M" proof - have"A n - (\i\{0.. M" for n using UNION_in_sets by (metis A Diff UNIV_I image_subset_iff) thenshow ?thesis by (auto simp: disjointed_def) qed
lemma (in algebra) range_disjointed_sets': "range A \ M \ range (disjointed A) \ M" using range_disjointed_sets .
lemma sigma_algebra_disjoint_iff: "sigma_algebra \ M \ algebra \ M \
(\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)" proof (auto simp add: sigma_algebra_iff) fix A :: "nat \ 'a set" assume M: "algebra \ M" and A: "range A \ M" and UnA: "\A. range A \ M \ disjoint_family A \ (\i::nat. A i) \ M" hence"range (disjointed A) \ M \
disjoint_family (disjointed A) \<longrightarrow>
(\<Union>i. disjointed A i) \<in> M" by blast hence"(\i. disjointed A i) \ M" by (simp add: algebra.range_disjointed_sets'[of \] M A disjoint_family_disjointed) thus"(\i::nat. A i) \ M" by (simp add: UN_disjointed_eq) qed
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Ring generated by a semiring\<close>
definition (in semiring_of_sets) generated_ring :: "'a set set"where "generated_ring = { \C | C. C \ M \ finite C \ disjoint C }"
lemma (in semiring_of_sets) generated_ringE[elim?]: assumes"a \ generated_ring" obtains C where"finite C""disjoint C""C \ M" "a = \C" using assms unfolding generated_ring_def by auto
lemma (in semiring_of_sets) generated_ringI[intro?]: assumes"finite C""disjoint C""C \ M" "a = \C" shows"a \ generated_ring" using assms unfolding generated_ring_def by auto
lemma (in semiring_of_sets) generated_ringI_Basic: "A \ M \ A \ generated_ring" using generated_ring_def by auto
lemma (in semiring_of_sets) generated_ring_disjoint_Un[intro]: assumes a: "a \ generated_ring" and b: "b \ generated_ring" and"a \ b = {}" shows"a \ b \ generated_ring" proof - from a b obtain Ca Cb where"finite Ca""disjoint Ca""Ca \ M" "a = \ Ca" and"finite Cb""disjoint Cb""Cb \ M" "b = \ Cb" using generated_ringE by metis thenshow ?thesis by (metis (mono_tags) Union_Un_distrib \<open>a \<inter> b = {}\<close> disjoint_union finite_Un generated_ringI le_sup_iff) qed
lemma (in semiring_of_sets) generated_ring_empty: "{} \ generated_ring" by (auto simp: generated_ring_def disjoint_def)
lemma (in semiring_of_sets) generated_ring_disjoint_Union: assumes"finite A"shows"A \ generated_ring \ disjoint A \ \A \ generated_ring" using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)
lemma (in semiring_of_sets) generated_ring_disjoint_UNION: "finite I \ disjoint (A ` I) \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring" by (intro generated_ring_disjoint_Union) auto
lemma (in semiring_of_sets) generated_ring_Int: assumes a: "a \ generated_ring" and b: "b \ generated_ring" shows"a \ b \ generated_ring" proof - from a b obtain Ca Cb where Ca: "finite Ca""disjoint Ca""Ca \ M" "a = \ Ca" and Cb: "finite Cb""disjoint Cb""Cb \ M" "b = \ Cb" using generated_ringE by metis
define C where"C = (\(a,b). a \ b)` (Ca\Cb)" show ?thesis proof show"disjoint C" proof (simp add: disjoint_def C_def, intro ballI impI) fix a1 b1 a2 b2 assume sets: "a1 \ Ca" "b1 \ Cb" "a2 \ Ca" "b2 \ Cb" assume"a1 \ b1 \ a2 \ b2" thenhave"a1 \ a2 \ b1 \ b2" by auto with Ca Cb show"(a1 \ b1) \ (a2 \ b2) = {}" by (metis (no_types, opaque_lifting) boolean_algebra.conj_zero_left
disjoint_def inf.left_commute inf_assoc sets) qed qed (use Ca Cb in\<open>auto simp: C_def\<close>) qed
lemma (in semiring_of_sets) generated_ring_Inter: assumes"finite A""A \ {}" shows "A \ generated_ring \ \A \ generated_ring" using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)
lemma (in semiring_of_sets) generated_ring_INTER: "finite I \ I \ {} \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring" by (intro generated_ring_Inter) auto
lemma (in semiring_of_sets) generating_ring: "ring_of_sets \ generated_ring" proof (rule ring_of_setsI) let ?R = generated_ring show"?R \ Pow \" using sets_into_space by (auto simp: generated_ring_def generated_ring_empty) show"{} \ ?R" by (rule generated_ring_empty)
{ fix a b assume"a \ ?R" "b \ ?R" thenobtain Ca Cb where Ca: "finite Ca""disjoint Ca""Ca \ M" "a = \ Ca" and Cb: "finite Cb""disjoint Cb""Cb \ M" "b = \ Cb" using generated_ringE by metis show"a - b \ ?R" proof cases assume"Cb = {}"with Cb \<open>a \<in> ?R\<close> show ?thesis by simp next assume"Cb \ {}" with Ca Cb have"a - b = (\a'\Ca. \b'\Cb. a' - b')" by auto alsohave"\ \ ?R" proof (intro generated_ring_INTER generated_ring_disjoint_UNION) fix a b assume"a \ Ca" "b \ Cb" with Ca Cb Diff_cover[of a b] show"a - b \ ?R" by (auto simp add: generated_ring_def)
(metis DiffI Diff_eq_empty_iff empty_iff) next show"disjoint ((\a'. \b'\Cb. a' - b')`Ca)" using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>) next show"finite Ca""finite Cb""Cb \ {}" by fact+ qed finallyshow"a - b \ ?R" . qed
} note Diff = this
fix a b assume sets: "a \ ?R" "b \ ?R" have"a \ b = (a - b) \ (a \ b) \ (b - a)" by auto alsohave"\ \ ?R" by (intro sets generated_ring_disjoint_Un generated_ring_Int Diff) auto finallyshow"a \ b \ ?R" . qed
lemma (in semiring_of_sets) sigma_sets_generated_ring_eq: "sigma_sets \ generated_ring = sigma_sets \ M" proof interpret M: sigma_algebra \<Omega> "sigma_sets \<Omega> M" using space_closed by (rule sigma_algebra_sigma_sets) show"sigma_sets \ generated_ring \ sigma_sets \ M" by (blast intro!: sigma_sets_mono elim: generated_ringE) qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
definition binaryset :: "'a set \ 'a set \ nat \ 'a set" where"binaryset A B = (\x. {})(0 := A, Suc 0 := B)"
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" by (auto simp add: binaryset_def)
lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B" by (simp add: range_binaryset_eq cong del: SUP_cong_simp)
subsubsection \<open>Closed CDI\<close>
definition\<^marker>\<open>tag important\<close> closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where "closed_cdi \ M \
M \<subseteq> Pow \<Omega> &
(\<forall>s \<in> M. \<Omega> - s \<in> M) &
(\<forall>A. (range A \<subseteq> M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
(\<Union>i. A i) \<in> M) &
(\<forall>A. (range A \<subseteq> M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> M)"
inductive_set
smallest_ccdi_sets :: "'a set \ 'a set set \ 'a set set" for\<Omega> M where
Basic [intro]: "a \ M \ a \ smallest_ccdi_sets \ M"
| Compl [intro]: "a \ smallest_ccdi_sets \ M \ \ - a \ smallest_ccdi_sets \ M"
| Inc: "range A \ Pow(smallest_ccdi_sets \ M) \ A 0 = {} \ (\n. A n \ A (Suc n)) \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets \<Omega> M"
| Disj: "range A \ Pow(smallest_ccdi_sets \ M) \ disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets \<Omega> M"
lemma (in subset_class) smallest_closed_cdi1: "M \ smallest_ccdi_sets \ M" by auto
lemma (in subset_class) smallest_closed_cdi2: "closed_cdi \ (smallest_ccdi_sets \ M)" by (simp add: closed_cdi_def smallest_ccdi_sets smallest_ccdi_sets.intros)
lemma closed_cdi_subset: "closed_cdi \ M \ M \ Pow \" by (simp add: closed_cdi_def)
lemma closed_cdi_Compl: "closed_cdi \ M \ s \ M \ \ - s \ M" by (simp add: closed_cdi_def)
lemma closed_cdi_Inc: "closed_cdi \ M \ range A \ M \ A 0 = {} \ (!!n. A n \ A (Suc n)) \ (\i. A i) \M" by (simp add: closed_cdi_def)
lemma closed_cdi_Disj: "closed_cdi \ M \ range A \ M \ disjoint_family A \ (\i::nat. A i) \ M" by (simp add: closed_cdi_def)
lemma closed_cdi_Un: assumes cdi: "closed_cdi \ M" and empty: "{} \ M" and A: "A \ M" and B: "B \ M" and disj: "A \ B = {}" shows"A \ B \ M" proof - have ra: "range (binaryset A B) \ M" by (simp add: range_binaryset_eq empty A B) have di: "disjoint_family (binaryset A B)"using disj by (simp add: disjoint_family_on_def binaryset_def Int_commute) from closed_cdi_Disj [OF cdi ra di] show ?thesis by (simp add: UN_binaryset_eq) qed
lemma (in algebra) smallest_ccdi_sets_Un: assumes A: "A \ smallest_ccdi_sets \ M" and B: "B \ smallest_ccdi_sets \ M" and disj: "A \ B = {}" shows"A \ B \ smallest_ccdi_sets \ M" proof - have ra: "range (binaryset A B) \ Pow (smallest_ccdi_sets \ M)" by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic) have di: "disjoint_family (binaryset A B)"using disj by (simp add: disjoint_family_on_def binaryset_def Int_commute) from Disj [OF ra di] show ?thesis by (simp add: UN_binaryset_eq) qed
lemma (in algebra) smallest_ccdi_sets_Int1: assumes a: "a \ M" shows"b \ smallest_ccdi_sets \ M \ a \ b \ smallest_ccdi_sets \ M" proof (induct rule: smallest_ccdi_sets.induct) case (Basic x) thus ?case by (metis a Int smallest_ccdi_sets.Basic) next case (Compl x) have 0: "(\ - a) \ (a \ x) = {}" by blast have"a \ (\ - x) = \ - ((\ - a) \ (a \ x))" by blast alsohave"... \ smallest_ccdi_sets \ M" by (intro 0 smallest_ccdi_sets.intros smallest_ccdi_sets_Un Compl.hyps assms) finallyshow ?case . next case (Inc A) have"range (\i. a \ A i) \ Pow(smallest_ccdi_sets \ M)" using Inc by blast moreoverhave"(\i. a \ A i) 0 = {}" by (simp add: Inc) moreoverhave"!!n. (\i. a \ A i) n \ (\i. a \ A i) (Suc n)" using Inc by blast ultimatelyhave"(\i. (\i. a \ A i) i) \ smallest_ccdi_sets \ M" by (rule smallest_ccdi_sets.Inc) moreoverhave"(\i. (\i. a \ A i) i) = a \ (\i. A i)" by blast ultimatelyshow ?case by metis next case (Disj A) have"range (\i. a \ A i) \ Pow(smallest_ccdi_sets \ M)" using Disj by blast moreoverhave"disjoint_family (\i. a \ A i)" using Disj by (auto simp add: disjoint_family_on_def) ultimatelyhave"(\i. (\i. a \ A i) i) \ smallest_ccdi_sets \ M" by (rule smallest_ccdi_sets.Disj) moreoverhave"(\i. (\i. a \ A i) i) = a \ (\i. A i)" by blast ultimatelyshow ?case by metis qed
lemma (in algebra) smallest_ccdi_sets_Int: assumes b: "b \ smallest_ccdi_sets \ M" shows"a \ smallest_ccdi_sets \ M \ a \ b \ smallest_ccdi_sets \ M" proof (induct rule: smallest_ccdi_sets.induct) case (Basic x) thus ?case by (metis b smallest_ccdi_sets_Int1) next case (Compl x) have"(\ - x) \ b = \ - (x \ b \ (\ - b))" by blast alsohave"... \ smallest_ccdi_sets \ M" by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) finallyshow ?case . next case (Inc A) have"range (\i. A i \ b) \ Pow(smallest_ccdi_sets \ M)" using Inc by blast moreoverhave"(\i. A i \ b) 0 = {}" by (simp add: Inc) moreoverhave"!!n. (\i. A i \ b) n \ (\i. A i \ b) (Suc n)" using Inc by blast ultimatelyhave"(\i. (\i. A i \ b) i) \ smallest_ccdi_sets \ M" by (rule smallest_ccdi_sets.Inc) moreoverhave"(\i. (\i. A i \ b) i) = (\i. A i) \ b" by blast ultimatelyshow ?case by metis next case (Disj A) have"range (\i. A i \ b) \ Pow(smallest_ccdi_sets \ M)" using Disj by blast moreoverhave"disjoint_family (\i. A i \ b)" using Disj by (auto simp add: disjoint_family_on_def) ultimatelyhave"(\i. (\i. A i \ b) i) \ smallest_ccdi_sets \ M" by (rule smallest_ccdi_sets.Disj) moreoverhave"(\i. (\i. A i \ b) i) = (\i. A i) \ b" by blast ultimatelyshow ?case by metis qed
lemma (in algebra) sigma_property_disjoint_lemma: assumes sbC: "M \ C" and ccdi: "closed_cdi \ C" shows"sigma_sets \ M \ C" proof - have"smallest_ccdi_sets \ M \ {B . M \ B \ sigma_algebra \ B}" using smallest_ccdi_sets by (auto simp: sigma_algebra_disjoint_iff algebra_iff_Int
smallest_ccdi_sets_Int intro: smallest_ccdi_sets.Disj) hence"sigma_sets (\) (M) \ smallest_ccdi_sets \ M" by (simp add: sigma_algebra.sigma_sets_subset) alsohave"... \ C" proof fix x assume x: "x \ smallest_ccdi_sets \ M" thus"x \ C" proof (induct rule: smallest_ccdi_sets.induct) case (Basic x) thus ?case by (metis Basic subsetD sbC) next case (Compl x) thus ?case by (blast intro: closed_cdi_Compl [OF ccdi, simplified]) next case (Inc A) thus ?case by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) next case (Disj A) thus ?case by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) qed qed finallyshow ?thesis . qed
lemma (in algebra) sigma_property_disjoint: assumes sbC: "M \ C" and compl: "!!s. s \ C \ sigma_sets (\) (M) \ \ - s \ C" and inc: "!!A. range A \ C \ sigma_sets (\) (M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow> (\<Union>i. A i) \<in> C" and disj: "!!A. range A \ C \ sigma_sets (\) (M) \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C" shows"sigma_sets (\) (M) \ C" proof - have"sigma_sets (\) (M) \ C \ sigma_sets (\) (M)" proof (rule sigma_property_disjoint_lemma) show"M \ C \ sigma_sets (\) (M)" by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic) next show"closed_cdi \ (C \ sigma_sets (\) (M))" unfolding closed_cdi_def compl inc disj by (auto simp: image_subset_iff compl inc disj le_infI2 sigma_algebra.sigma_sets_subset sigma_algebra_Pow
space_closed intro: sigma_sets.intros) qed thus ?thesis by blast qed
subsubsection \<open>Dynkin systems\<close>
locale\<^marker>\<open>tag important\<close> Dynkin_system = subset_class + assumes space: "\ \ M" and compl[intro!]: "\A. A \ M \ \ - A \ M" and UN[intro!]: "\A. disjoint_family A \ range A \ M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
lemma (in Dynkin_system) empty[intro, simp]: "{} \ M" using space compl[of "\"] by simp
lemma (in Dynkin_system) diff: assumes sets: "D \ M" "E \ M" and "D \ E" shows"E - D \ M" proof - let ?f = "\x. if x = 0 then D else if x = Suc 0 then \ - E else {}" have"range ?f = {D, \ - E, {}}" by (auto simp: image_iff) moreoverhave"D \ (\ - E) = (\i. ?f i)" by (auto simp: image_iff split: if_split_asm) moreover have"disjoint_family ?f"unfolding disjoint_family_on_def using\<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto ultimatelyhave"\ - (D \ (\ - E)) \ M" using sets UN by auto fastforce alsohave"\ - (D \ (\ - E)) = E - D" using assms sets_into_space by auto finallyshow ?thesis . qed
lemma Dynkin_systemI: assumes"\ A. A \ M \ A \ \" "\ \ M" assumes"\ A. A \ M \ \ - A \ M" assumes"\ A. disjoint_family A \ range A \ M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M" shows"Dynkin_system \ M" using assms by (auto simp: Dynkin_system_def Dynkin_system_axioms_def subset_class_def)
lemma Dynkin_systemI': assumes"\ A. A \ M \ A \ \" assumes empty: "{} \ M" assumes Diff: "\ A. A \ M \ \ - A \ M" assumes"\A. disjoint_family A \ range A \ M \ (\i::nat. A i) \ M" shows"Dynkin_system \ M" using Diff[OF empty] assms by (simp add: Dynkin_systemI)
lemma Dynkin_system_trivial: shows"Dynkin_system A (Pow A)" by (rule Dynkin_systemI) auto
lemma sigma_algebra_imp_Dynkin_system: assumes"sigma_algebra \ M" shows "Dynkin_system \ M" proof - interpret sigma_algebra \<Omega> M by fact show ?thesis using sets_into_space by (fastforce intro!: Dynkin_systemI) qed
subsubsection "Intersection sets systems"
definition\<^marker>\<open>tag important\<close> Int_stable :: "'a set set \<Rightarrow> bool" where "Int_stable M \ (\ a \ M. \ b \ M. a \ b \ M)"
lemma (in algebra) Int_stable: "Int_stable M" unfolding Int_stable_def by auto
lemma Int_stableI_image: "(\i j. i \ I \ j \ I \ \k\I. A i \ A j = A k) \ Int_stable (A ` I)" by (auto simp: Int_stable_def image_def)
lemma Int_stableI: "(\a b. a \ A \ b \ A \ a \ b \ A) \ Int_stable A" unfolding Int_stable_def by auto
lemma Int_stableD: "Int_stable M \ a \ M \ b \ M \ a \ b \ M" unfolding Int_stable_def by auto
lemma (in Dynkin_system) sigma_algebra_eq_Int_stable: "sigma_algebra \ M \ Int_stable M" proof assume"sigma_algebra \ M" then show "Int_stable M" unfolding sigma_algebra_def using algebra.Int_stable by auto next assume"Int_stable M" show"sigma_algebra \ M" unfolding sigma_algebra_disjoint_iff algebra_iff_Un proof (intro conjI ballI allI impI) show"M \ Pow (\)" using sets_into_space by auto next fix A B assume"A \ M" "B \ M" thenhave"A \ B = \ - ((\ - A) \ (\ - B))" "\ - A \ M" "\ - B \ M" using sets_into_space by auto thenshow"A \ B \ M" using\<open>Int_stable M\<close> unfolding Int_stable_def by auto qed auto qed
subsubsection "Smallest Dynkin systems"
definition\<^marker>\<open>tag important\<close> Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where "Dynkin \ M = (\{D. Dynkin_system \ D \ M \ D})"
lemma Dynkin_system_Dynkin: assumes"M \ Pow (\)" shows"Dynkin_system \ (Dynkin \ M)" proof (rule Dynkin_systemI) fix A assume"A \ Dynkin \ M" moreover
{ fix D assume"A \ D" and d: "Dynkin_system \ D" thenhave"A \ \" by (auto simp: Dynkin_system_def subset_class_def) } moreoverhave"{D. Dynkin_system \ D \ M \ D} \ {}" using assms Dynkin_system_trivial by fastforce ultimatelyshow"A \ \" unfolding Dynkin_def using assms by auto next show"\ \ Dynkin \ M" unfolding Dynkin_def using Dynkin_system.space by fastforce next fix A assume"A \ Dynkin \ M" thenshow"\ - A \ Dynkin \ M" unfolding Dynkin_def using Dynkin_system.compl by force next fix A :: "nat \ 'a set" assume A: "disjoint_family A""range A \ Dynkin \ M" thenshow"(\i. A i) \ Dynkin \ M" unfolding Dynkin_def by (auto intro!: Dynkin_system.UN) qed
lemma Dynkin_Basic[intro]: "A \ M \ A \ Dynkin \ M" unfolding Dynkin_def by auto
lemma (in Dynkin_system) restricted_Dynkin_system: assumes"D \ M" shows"Dynkin_system \ {Q. Q \ \ \ Q \ D \ M}" proof (rule Dynkin_systemI, simp_all) have"\ \ D = D" using\<open>D \<in> M\<close> sets_into_space by auto thenshow"\ \ D \ M" using\<open>D \<in> M\<close> by auto next fix A assume"A \ \ \ A \ D \ M" moreoverhave"(\ - A) \ D = (\ - (A \ D)) - (\ - D)" by auto ultimatelyshow"(\ - A) \ D \ M" using\<open>D \<in> M\<close> by (auto intro: diff) next fix A :: "nat \ 'a set" assume"disjoint_family A""range A \ {Q. Q \ \ \ Q \ D \ M}" thenhave"\i. A i \ \" "disjoint_family (\i. A i \ D)" "range (\i. A i \ D) \ M" "(\x. A x) \ D = (\x. A x \ D)" by ((fastforce simp: disjoint_family_on_def)+) thenshow"(\x. A x) \ \ \ (\x. A x) \ D \ M" by (auto simp del: UN_simps) qed
lemma (in Dynkin_system) Dynkin_subset: assumes"N \ M" shows"Dynkin \ N \ M" proof - have"Dynkin_system \ M" .. thenhave"Dynkin_system \ M" using assms unfolding Dynkin_system_def Dynkin_system_axioms_def subset_class_def by simp with\<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: Dynkin_def) qed
lemma sigma_eq_Dynkin: assumes sets: "M \ Pow \" assumes"Int_stable M" shows"sigma_sets \ M = Dynkin \ M" proof - have"Dynkin \ M \ sigma_sets (\) (M)" using sigma_algebra_imp_Dynkin_system unfolding Dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto moreover interpret Dynkin_system \<Omega> "Dynkin \<Omega> M" using Dynkin_system_Dynkin[OF sets] . have"sigma_algebra \ (Dynkin \ M)" unfolding sigma_algebra_eq_Int_stable Int_stable_def proof (intro ballI) fix A B assume"A \ Dynkin \ M" "B \ Dynkin \ M" let ?D = "\E. {Q. Q \ \ \ Q \ E \ Dynkin \ M}" have"M \ ?D B" proof fix E assume"E \ M" thenhave"M \ ?D E" "E \ Dynkin \ M" using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def) thenhave"Dynkin \ M \ ?D E" using restricted_Dynkin_system \<open>E \<in> Dynkin \<Omega> M\<close> by (intro Dynkin_system.Dynkin_subset) simp_all thenhave"B \ ?D E" using\<open>B \<in> Dynkin \<Omega> M\<close> by auto thenhave"E \ B \ Dynkin \ M" by (subst Int_commute) simp thenshow"E \ ?D B" using sets \<open>E \<in> M\<close> by auto qed thenhave"Dynkin \ M \ ?D B" using restricted_Dynkin_system \<open>B \<in> Dynkin \<Omega> M\<close> by (intro Dynkin_system.Dynkin_subset) simp_all thenshow"A \ B \ Dynkin \ M" using\<open>A \<in> Dynkin \<Omega> M\<close> sets_into_space by auto qed from sigma_algebra.sigma_sets_subset[OF this, of "M"] have"sigma_sets (\) (M) \ Dynkin \ M" by auto ultimatelyhave"sigma_sets (\) (M) = Dynkin \ M" by auto thenshow ?thesis by (auto simp: Dynkin_def) qed
lemma (in Dynkin_system) Dynkin_idem: "Dynkin \ M = M" proof - have"Dynkin \ M = M" using Dynkin_subset by blast thenshow ?thesis by (auto simp: Dynkin_def) qed
lemma (in Dynkin_system) Dynkin_lemma: assumes"Int_stable E" and E: "E \ M" "M \ sigma_sets \ E" shows"sigma_sets \ E = M" proof - have"E \ Pow \" using E sets_into_space by force thenhave *: "sigma_sets \ E = Dynkin \ E" using\<open>Int_stable E\<close> by (rule sigma_eq_Dynkin) thenhave"Dynkin \ E = M" using assms Dynkin_subset[OF \<open>E \<subseteq> M\<close>] by simp with * show ?thesis using assms by (auto simp: Dynkin_def) qed
subsubsection \<open>Induction rule for intersection-stable generators\<close>
text\<^marker>\<open>tag important\<close> \<open>The reason to introduce Dynkin-systems is the following induction rules for \<open>\<sigma>\<close>-algebras
generated by a generator closed under intersection.\<close>
proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]: assumes"Int_stable G" and closed: "G \ Pow \" and A: "A \ sigma_sets \ G" assumes basic: "\A. A \ G \ P A" and empty: "P {}" and compl: "\A. A \ sigma_sets \ G \ P A \ P (\ - A)" and union: "\A. disjoint_family A \ range A \ sigma_sets \ G \ (\i. P (A i)) \ P (\i::nat. A i)" shows"P A" proof - let ?D = "{ A \ sigma_sets \ G. P A }" interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G" using closed by (rule sigma_algebra_sigma_sets) from compl[OF _ empty] closed have space: "P \" by simp interpret Dynkin_system \<Omega> ?D by standard (auto dest: sets_into_space intro!: space compl union) have"sigma_sets \ G = ?D" by (rule Dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>) with A show ?thesis by auto qed
subsection \<open>Measure type\<close>
definition\<^marker>\<open>tag important\<close> positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where "positive M \ \ \ {} = 0"
definition\<^marker>\<open>tag important\<close> countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where "countably_additive M f \
(\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
(\<Sum>i. f (A i)) = f (\<Union>i. A i))"
definition\<^marker>\<open>tag important\<close> measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where "measure_space \ A \ \
sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
typedef\<^marker>\<open>tag important\<close> 'a measure = "{(\::'a set, A, \). (\a\-A. \ a = 0) \ measure_space \ A \ }" proof have"sigma_algebra UNIV {{}, UNIV}" by (auto simp: sigma_algebra_iff2) thenshow"(UNIV, {{}, UNIV}, \A. 0) \ {(\, A, \). (\a\-A. \ a = 0) \ measure_space \ A \} " by (auto simp: measure_space_def positive_def countably_additive_def) qed
definition\<^marker>\<open>tag important\<close> space :: "'a measure \<Rightarrow> 'a set" where "space M = fst (Rep_measure M)"
definition\<^marker>\<open>tag important\<close> sets :: "'a measure \<Rightarrow> 'a set set" where "sets M = fst (snd (Rep_measure M))"
definition\<^marker>\<open>tag important\<close> emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where "emeasure M = snd (snd (Rep_measure M))"
definition\<^marker>\<open>tag important\<close> measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where "measure M A = enn2real (emeasure M A)"
declare [[coercion sets]]
declare [[coercion measure]]
declare [[coercion emeasure]]
lemma measure_space: "measure_space (space M) (sets M) (emeasure M)" by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
interpretation sets: sigma_algebra "space M""sets M"for M :: "'a measure" using measure_space[of M] by (auto simp: measure_space_def)
definition\<^marker>\<open>tag important\<close> measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where "measure_of \ A \ \
Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>}, \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
abbreviation"sigma \ A \ measure_of \ A (\x. 0)"
lemma measure_space_0: "A \ Pow \ \ measure_space \ (sigma_sets \ A) (\x. 0)" unfolding measure_space_def by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def)
lemma measure_space_closed: assumes"measure_space \ M \" shows"M \ Pow \" proof - interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def) show ?thesis by(rule space_closed) qed
lemma (in ring_of_sets) positive_cong_eq: "(\a. a \ M \ \' a = \ a) \ positive M \' = positive M \" by (auto simp add: positive_def)
lemma (in sigma_algebra) countably_additive_eq: "(\a. a \ M \ \' a = \ a) \ countably_additive M \' = countably_additive M \" unfolding countably_additive_def by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq)
lemma measure_space_eq: assumes closed: "A \ Pow \" and eq: "\a. a \ sigma_sets \ A \ \ a = \' a" shows"measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) \'" proof - interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" using closed by (rule sigma_algebra_sigma_sets) from positive_cong_eq[OF eq, of "\i. i"] countably_additive_eq[OF eq, of "\i. i"] show ?thesis by (auto simp: measure_space_def) qed
lemma measure_of_eq: assumes closed: "A \ Pow \" and eq: "(\a. a \ sigma_sets \ A \ \ a = \' a)" shows"measure_of \ A \ = measure_of \ A \'" proof - have"measure_space \ (sigma_sets \ A) \ = measure_space \ (sigma_sets \ A) \'" using assms by (rule measure_space_eq) with eq show ?thesis by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure]) qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
