--- a/src/HOL/Analysis/Sigma_Algebra.thy Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Apr 12 22:09:25 2019 +0200
@@ -30,7 +30,7 @@
subsection \<open>Families of sets\<close>
-locale%important subset_class =
+locale\<^marker>\<open>tag important\<close> subset_class =
fixes \<Omega> :: "'a set" and M :: "'a set set"
assumes space_closed: "M \<subseteq> Pow \<Omega>"
@@ -39,7 +39,7 @@
subsubsection \<open>Semiring of sets\<close>
-locale%important semiring_of_sets = subset_class +
+locale\<^marker>\<open>tag important\<close> 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:
@@ -76,7 +76,7 @@
subsubsection \<open>Ring of sets\<close>
-locale%important ring_of_sets = semiring_of_sets +
+locale\<^marker>\<open>tag important\<close> 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]:
@@ -142,7 +142,7 @@
subsubsection \<open>Algebra of sets\<close>
-locale%important algebra = ring_of_sets +
+locale\<^marker>\<open>tag important\<close> algebra = ring_of_sets +
assumes top [iff]: "\<Omega> \<in> M"
lemma (in algebra) compl_sets [intro]:
@@ -221,7 +221,7 @@
"X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
by (auto simp: algebra_iff_Int)
-subsubsection%unimportant \<open>Restricted algebras\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Restricted algebras\<close>
abbreviation (in algebra)
"restricted_space A \<equiv> ((\<inter>) A) ` M"
@@ -232,7 +232,7 @@
subsubsection \<open>Sigma Algebras\<close>
-locale%important sigma_algebra = algebra +
+locale\<^marker>\<open>tag important\<close> 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:
@@ -431,7 +431,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%unimportant \<open>Binary Unions\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Binary Unions\<close>
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
where "binary a b = (\<lambda>x. b)(0 := a)"
@@ -473,10 +473,10 @@
subsubsection \<open>Initial Sigma Algebra\<close>
-text%important \<open>Sigma algebras can naturally be created as the closure of any set of
+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%important sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+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 \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
@@ -819,7 +819,7 @@
thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
qed
-subsubsection%unimportant \<open>Ring generated by a semiring\<close>
+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 = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
@@ -950,7 +950,7 @@
by (blast intro!: sigma_sets_mono elim: generated_ringE)
qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
-subsubsection%unimportant \<open>A Two-Element Series\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<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)"
@@ -966,7 +966,7 @@
subsubsection \<open>Closed CDI\<close>
-definition%important closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
"closed_cdi \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> &
(\<forall>s \<in> M. \<Omega> - s \<in> M) &
@@ -1200,7 +1200,7 @@
subsubsection \<open>Dynkin systems\<close>
-locale%important Dynkin_system = subset_class +
+locale\<^marker>\<open>tag important\<close> 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
@@ -1262,7 +1262,7 @@
subsubsection "Intersection sets systems"
-definition%important Int_stable :: "'a set set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> Int_stable :: "'a set set \<Rightarrow> bool" where
"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"
@@ -1303,7 +1303,7 @@
subsubsection "Smallest Dynkin systems"
-definition%important Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
+definition\<^marker>\<open>tag important\<close> Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
"Dynkin \<Omega> M = (\<Inter>{D. Dynkin_system \<Omega> D \<and> M \<subseteq> D})"
lemma Dynkin_system_Dynkin:
@@ -1450,7 +1450,7 @@
subsubsection \<open>Induction rule for intersection-stable generators\<close>
-text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for \<open>\<sigma>\<close>-algebras
+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]:
@@ -1476,37 +1476,37 @@
subsection \<open>Measure type\<close>
-definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
-definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> 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%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> 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%important 'a measure =
+typedef\<^marker>\<open>tag important\<close> 'a measure =
"{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
-proof%unimportant
+proof
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%important space :: "'a measure \<Rightarrow> 'a set" where
+definition\<^marker>\<open>tag important\<close> space :: "'a measure \<Rightarrow> 'a set" where
"space M = fst (Rep_measure M)"
-definition%important sets :: "'a measure \<Rightarrow> 'a set set" where
+definition\<^marker>\<open>tag important\<close> sets :: "'a measure \<Rightarrow> 'a set set" where
"sets M = fst (snd (Rep_measure M))"
-definition%important emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
+definition\<^marker>\<open>tag important\<close> emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
"emeasure M = snd (snd (Rep_measure M))"
-definition%important measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
+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]]
@@ -1521,7 +1521,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%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
+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 \<Omega> A \<mu> =
Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
@@ -1740,7 +1740,7 @@
subsubsection \<open>Measurable functions\<close>
-definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set"
+definition\<^marker>\<open>tag important\<close> 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}"
@@ -1903,7 +1903,7 @@
subsubsection \<open>Counting space\<close>
-definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
+definition\<^marker>\<open>tag important\<close> 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
@@ -1979,7 +1979,7 @@
"space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
by (auto simp add: measurable_def Pi_iff)
-subsubsection%unimportant \<open>Extend measure\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Extend measure\<close>
definition extend_measure :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('b \<Rightarrow> 'a set) \<Rightarrow> ('b \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
where
@@ -2043,7 +2043,7 @@
subsection \<open>The smallest \<open>\<sigma>\<close>-algebra regarding a function\<close>
-definition%important vimage_algebra :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure \<Rightarrow> 'a measure" where
+definition\<^marker>\<open>tag important\<close> vimage_algebra :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure \<Rightarrow> 'a measure" where
"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"