src/HOL/Analysis/Sigma_Algebra.thy

     Author:     Johannes Hölzl, TU München
     Plus material from the Hurd/Coble measure theory development,
     translated by Lawrence Paulson.
 *)
 
-section \<open>Describing measurable sets\<close>
+section \<open>Sigma Algebra\<close>
 
 theory Sigma_Algebra
 imports
   Complex_Main
   "HOL-Library.Countable_Set"

   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 subset_class =
+locale%important subset_class =
   fixes \<Omega> :: "'a set" and M :: "'a set set"
   assumes space_closed: "M \<subseteq> Pow \<Omega>"
 
 lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>"
   by (metis PowD contra_subsetD space_closed)
 
 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:
     "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> \<exists>C\<subseteq>M. finite C \<and> disjoint C \<and> a - b = \<Union>C"
 

   have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
     using \<open>S \<noteq> {}\<close> by auto
   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]:
   "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> \<Union>X \<in> M"
   by (induct set: finite) (auto simp add: Un)

   have "{x\<in>\<Omega>. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>\<Omega>. P i x})"
     by auto
   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
 next
   assume ?Un

       using a b  \<open>?Un\<close> by auto
   qed
   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
 next
   assume ?Int

 
 lemma algebra_single_set:
   "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"
 
 lemma (in algebra) restricted_algebra:
   assumes "A \<in> M" shows "algebra A (restricted_space A)"
   using assms by (auto simp: algebra_iff_Int)
 
 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:
   assumes "finite M"
   shows "sigma_algebra \<Omega> M"

 lemma sigma_algebra_single_set:
   assumes "X \<subseteq> 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
 
-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)"
 
 lemma range_binary_eq: "range(binary a b) = {a,b}"

   by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
          algebra_iff_Un Un_range_binary)
 
 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"
   | Empty: "{} \<in> sigma_sets sp A"
   | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"

   hence "(\<Union>i. disjointed A i) \<in> M"
     by (simp add: algebra.range_disjointed_sets'[of \<Omega>] M A disjoint_family_disjointed)
   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 }"
 
 lemma (in semiring_of_sets) generated_ringE[elim?]:

     using space_closed by (rule sigma_algebra_sigma_sets)
   show "sigma_sets \<Omega> generated_ring \<subseteq> sigma_sets \<Omega> M"
     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)"
 
 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"

 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
   by (simp add: range_binaryset_eq cong del: strong_SUP_cong)
 
 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) &
    (\<forall>A. (range A \<subseteq> M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
         (\<Union>i. A i) \<in> M) &

     by blast
 qed
 
 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
                            \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
 

   show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
 qed
 
 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
 
 lemma Int_stableI_image:

   qed auto
 qed
 
 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:
   assumes "M \<subseteq> Pow (\<Omega>)"
   shows "dynkin_system \<Omega> (dynkin \<Omega> M)"

     using assms by (auto simp: dynkin_def)
 qed
 
 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"
   assumes basic: "\<And>A. A \<in> G \<Longrightarrow> P A"
     and empty: "P {}"
     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)
   from compl[OF _ empty] closed have space: "P \<Omega>" by simp
   interpret dynkin_system \<Omega> ?D

   with A show ?thesis by auto
 qed
 
 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]]
 
 declare [[coercion measure]]

   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 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)"
 
 abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)"
 

   by (metis Pow_empty Sup_bot_conv(1) cSup_singleton empty_iff
             sets.sigma_sets_eq sets.space_closed sigma_sets_top subset_singletonD)
 
 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)
   thus ?thesis using X ms
     by(simp add: M emeasure_measure_of_conv sets_measure_of_conv)

   shows "sigma \<Omega> M = sigma \<Omega> N"
   by (rule measure_eqI) (simp_all add: emeasure_sigma)
 
 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:
   "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow> (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
     f \<in> measurable M N"

     measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
   using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
 
 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
   shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
     and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"

 
 lemma measurable_empty_iff:
   "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)
       then measure_of \<Omega> (G`I) (SOME \<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>')
       else measure_of \<Omega> (G`I) (\<lambda>_. 0))"

   using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) \<open>I i j\<close>
   by (auto simp: subset_eq)
 
 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"
   unfolding vimage_algebra_def by (rule space_measure_of) auto