--- a/src/HOL/Analysis/Sigma_Algebra.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Apr 06 17:34:50 2018 +0200
@@ -5,7 +5,7 @@
translated by Lawrence Paulson.
*)
-section \<open>Describing measurable sets\<close>
+section \<open>Sigma Algebra\<close>
theory Sigma_Algebra
imports
@@ -27,7 +27,7 @@
subsection \<open>Families of sets\<close>
-locale subset_class =
+locale%important subset_class =
fixes \<Omega> :: "'a set" and M :: "'a set set"
assumes space_closed: "M \<subseteq> Pow \<Omega>"
@@ -36,7 +36,7 @@
subsubsection \<open>Semiring of sets\<close>
-locale semiring_of_sets = subset_class +
+locale%important semiring_of_sets = subset_class +
assumes empty_sets[iff]: "{} \<in> M"
assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
assumes Diff_cover:
@@ -71,7 +71,9 @@
with assms show ?thesis by auto
qed
-locale ring_of_sets = semiring_of_sets +
+subsubsection \<open>Ring of sets\<close>
+
+locale%important ring_of_sets = semiring_of_sets +
assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
lemma (in ring_of_sets) finite_Union [intro]:
@@ -135,20 +137,22 @@
with assms show ?thesis by auto
qed
-locale algebra = ring_of_sets +
+subsubsection \<open>Algebra of sets\<close>
+
+locale%important algebra = ring_of_sets +
assumes top [iff]: "\<Omega> \<in> M"
lemma (in algebra) compl_sets [intro]:
"a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
by auto
-lemma algebra_iff_Un:
+lemma%important algebra_iff_Un:
"algebra \<Omega> M \<longleftrightarrow>
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
+proof%unimportant
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Un using sets_into_space by auto
@@ -169,12 +173,12 @@
show "algebra \<Omega> M" proof qed fact
qed
-lemma algebra_iff_Int:
+lemma%important algebra_iff_Int:
"algebra \<Omega> M \<longleftrightarrow>
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
+proof%unimportant
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Int using sets_into_space by auto
@@ -214,7 +218,7 @@
"X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
by (auto simp: algebra_iff_Int)
-subsubsection \<open>Restricted algebras\<close>
+subsubsection%unimportant \<open>Restricted algebras\<close>
abbreviation (in algebra)
"restricted_space A \<equiv> ((\<inter>) A) ` M"
@@ -225,7 +229,7 @@
subsubsection \<open>Sigma Algebras\<close>
-locale sigma_algebra = algebra +
+locale%important sigma_algebra = algebra +
assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
lemma (in algebra) is_sigma_algebra:
@@ -423,7 +427,7 @@
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
-subsubsection \<open>Binary Unions\<close>
+subsubsection%unimportant \<open>Binary Unions\<close>
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
where "binary a b = (\<lambda>x. b)(0 := a)"
@@ -447,10 +451,10 @@
subsubsection \<open>Initial Sigma Algebra\<close>
-text \<open>Sigma algebras can naturally be created as the closure of any set of
+text%important \<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 sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+inductive_set%important 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 \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
@@ -796,7 +800,7 @@
thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
qed
-subsubsection \<open>Ring generated by a semiring\<close>
+subsubsection%unimportant \<open>Ring generated by a semiring\<close>
definition (in semiring_of_sets)
"generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
@@ -927,7 +931,7 @@
by (blast intro!: sigma_sets_mono elim: generated_ringE)
qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
-subsubsection \<open>A Two-Element Series\<close>
+subsubsection%unimportant \<open>A Two-Element Series\<close>
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
@@ -943,7 +947,7 @@
subsubsection \<open>Closed CDI\<close>
-definition closed_cdi where
+definition%important closed_cdi where
"closed_cdi \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> &
(\<forall>s \<in> M. \<Omega> - s \<in> M) &
@@ -1177,7 +1181,7 @@
subsubsection \<open>Dynkin systems\<close>
-locale dynkin_system = subset_class +
+locale%important dynkin_system = subset_class +
assumes space: "\<Omega> \<in> M"
and compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
@@ -1239,7 +1243,7 @@
subsubsection "Intersection sets systems"
-definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
+definition%important "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
lemma (in algebra) Int_stable: "Int_stable M"
unfolding Int_stable_def by auto
@@ -1279,7 +1283,7 @@
subsubsection "Smallest Dynkin systems"
-definition dynkin where
+definition%important dynkin where
"dynkin \<Omega> M = (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
lemma dynkin_system_dynkin:
@@ -1426,10 +1430,10 @@
subsubsection \<open>Induction rule for intersection-stable generators\<close>
-text \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
+text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
generated by a generator closed under intersection.\<close>
-lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
assumes "Int_stable G"
and closed: "G \<subseteq> Pow \<Omega>"
and A: "A \<in> sigma_sets \<Omega> G"
@@ -1438,7 +1442,7 @@
and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
shows "P A"
-proof -
+proof%unimportant -
let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
using closed by (rule sigma_algebra_sigma_sets)
@@ -1452,34 +1456,34 @@
subsection \<open>Measure type\<close>
-definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
-definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"countably_additive M f \<longleftrightarrow> (\<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 measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
-typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
-proof
+typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+proof%unimportant
have "sigma_algebra UNIV {{}, UNIV}"
by (auto simp: sigma_algebra_iff2)
then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
by (auto simp: measure_space_def positive_def countably_additive_def)
qed
-definition space :: "'a measure \<Rightarrow> 'a set" where
+definition%important space :: "'a measure \<Rightarrow> 'a set" where
"space M = fst (Rep_measure M)"
-definition sets :: "'a measure \<Rightarrow> 'a set set" where
+definition%important sets :: "'a measure \<Rightarrow> 'a set set" where
"sets M = fst (snd (Rep_measure M))"
-definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
+definition%important emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
"emeasure M = snd (snd (Rep_measure M))"
-definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
+definition%important measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
"measure M A = enn2real (emeasure M A)"
declare [[coercion sets]]
@@ -1494,7 +1498,7 @@
interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
using measure_space[of M] by (auto simp: measure_space_def)
-definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
+definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
"measure_of \<Omega> A \<mu> = 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)"
@@ -1629,12 +1633,12 @@
subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
-lemma emeasure_measure_of:
+lemma%important emeasure_measure_of:
assumes M: "M = measure_of \<Omega> A \<mu>"
assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
assumes X: "X \<in> sets M"
shows "emeasure M X = \<mu> X"
-proof -
+proof%unimportant -
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
@@ -1711,7 +1715,7 @@
subsubsection \<open>Measurable functions\<close>
-definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
+definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
"measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
lemma measurableI:
@@ -1873,7 +1877,7 @@
subsubsection \<open>Counting space\<close>
-definition count_space :: "'a set \<Rightarrow> 'a measure" where
+definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
"count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
lemma
@@ -1949,7 +1953,7 @@
"space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
by (auto simp add: measurable_def Pi_iff)
-subsubsection \<open>Extend measure\<close>
+subsubsection%unimportant \<open>Extend measure\<close>
definition "extend_measure \<Omega> I G \<mu> =
(if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
@@ -2011,7 +2015,7 @@
subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
-definition
+definition%important
"vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"