src/HOL/Analysis/Complete_Measure.thy

 (*  Title:      HOL/Analysis/Complete_Measure.thy
     Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
 *)
-
+section \<open>Complete Measures\<close>
 theory Complete_Measure
   imports Bochner_Integration
 begin
 
-locale complete_measure =
+locale%important complete_measure =
   fixes M :: "'a measure"
   assumes complete: "\<And>A B. B \<subseteq> A \<Longrightarrow> A \<in> null_sets M \<Longrightarrow> B \<in> sets M"
 
-definition
+definition%important
   "split_completion M A p = (if A \<in> sets M then p = (A, {}) else
    \<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and> fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets M)"
 
-definition
+definition%important
   "main_part M A = fst (Eps (split_completion M A))"
 
-definition
+definition%important
   "null_part M A = snd (Eps (split_completion M A))"
 
-definition completion :: "'a measure \<Rightarrow> 'a measure" where
+definition%important completion :: "'a measure \<Rightarrow> 'a measure" where
   "completion M = measure_of (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }
     (emeasure M \<circ> main_part M)"
 
 lemma completion_into_space:
   "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"

   then show "\<Union>(A ` UNIV) \<in> ?A"
     using null_sets_UN[of N']
     by (intro completionI[of _ "\<Union>(S ` UNIV)" "\<Union>(N ` UNIV)" "\<Union>(N' ` UNIV)"]) auto
 qed
 
-lemma sets_completion:
+lemma%important sets_completion:
   "sets (completion M) = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
-  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] by (simp add: completion_def)
+  using%unimportant sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] 
+  by (simp add: completion_def)
 
 lemma sets_completionE:
   assumes "A \<in> sets (completion M)"
   obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
   using assms unfolding sets_completion by auto

 
 lemma sets_completionI_sets[intro, simp]:
   "A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)"
   unfolding sets_completion by force
 
-lemma measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
-  by (auto simp: measurable_def)
+lemma%important measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
+  by%unimportant (auto simp: measurable_def)
 
 lemma null_sets_completion:
   assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)"
   using assms by (intro sets_completionI[of N "{}" N N']) auto
 
-lemma split_completion:
+lemma%important split_completion:
   assumes "A \<in> sets (completion M)"
   shows "split_completion M A (main_part M A, null_part M A)"
-proof cases
+proof%unimportant cases
   assume "A \<in> sets M" then show ?thesis
     by (simp add: split_completion_def[abs_def] main_part_def null_part_def)
 next
   assume nA: "A \<notin> sets M"
   show ?thesis

   also have "\<dots> = emeasure M (\<Union>i. main_part M (S i))"
     using null_set S by (intro emeasure_Un_null_set) auto
   finally show ?thesis .
 qed
 
-lemma emeasure_completion[simp]:
-  assumes S: "S \<in> sets (completion M)" shows "emeasure (completion M) S = emeasure M (main_part M S)"
-proof (subst emeasure_measure_of[OF completion_def completion_into_space])
+lemma%important emeasure_completion[simp]:
+  assumes S: "S \<in> sets (completion M)"
+  shows "emeasure (completion M) S = emeasure M (main_part M S)"
+proof%unimportant (subst emeasure_measure_of[OF completion_def completion_into_space])
   let ?\<mu> = "emeasure M \<circ> main_part M"
   show "S \<in> sets (completion M)" "?\<mu> S = emeasure M (main_part M S) " using S by simp_all
   show "positive (sets (completion M)) ?\<mu>"
     by (simp add: positive_def)
   show "countably_additive (sets (completion M)) ?\<mu>"

     show "AE x in M. f x = ?f' x"
       by (rule AE_I', rule sets) auto
   qed
 qed
 
-lemma completion_ex_borel_measurable:
+lemma%important completion_ex_borel_measurable:
   fixes g :: "'a \<Rightarrow> ennreal"
   assumes g: "g \<in> borel_measurable (completion M)"
   shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
-proof -
+proof%unimportant -
   from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
   from this(1)[THEN completion_ex_simple_function]
   have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" ..
   from this[THEN choice] obtain f' where
     sf: "\<And>i. simple_function M (f' i)" and

 lemma integral_completion:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
   by (rule integral_subalgebra[symmetric]) (auto intro: f)
 
-locale semifinite_measure =
+locale%important semifinite_measure =
   fixes M :: "'a measure"
   assumes semifinite:
     "\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A = \<infinity> \<Longrightarrow> \<exists>B\<in>sets M. B \<subseteq> A \<and> emeasure M B < \<infinity>"
 
-locale locally_determined_measure = semifinite_measure +
+locale%important locally_determined_measure = semifinite_measure +
   assumes locally_determined:
     "\<And>A. A \<subseteq> space M \<Longrightarrow> (\<And>B. B \<in> sets M \<Longrightarrow> emeasure M B < \<infinity> \<Longrightarrow> A \<inter> B \<in> sets M) \<Longrightarrow> A \<in> sets M"
 
-locale cld_measure = complete_measure M + locally_determined_measure M for M :: "'a measure"
-
-definition outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
+locale%important cld_measure =
+  complete_measure M + locally_determined_measure M for M :: "'a measure"
+
+definition%important outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
   where "outer_measure_of M A = (INF B \<in> {B\<in>sets M. A \<subseteq> B}. emeasure M B)"
 
 lemma outer_measure_of_eq[simp]: "A \<in> sets M \<Longrightarrow> outer_measure_of M A = emeasure M A"
   by (auto simp: outer_measure_of_def intro!: INF_eqI emeasure_mono)
 

     using F by (simp add: SUP_emeasure_incseq subset_eq)
   finally show "outer_measure_of M (\<Union>n. A n) \<le> (SUP n. outer_measure_of M (A n))"
     by (simp add: eq F)
 qed (auto intro: SUP_least outer_measure_of_mono)
 
-definition measurable_envelope :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+definition%important measurable_envelope :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   where "measurable_envelope M A E \<longleftrightarrow>
     (A \<subseteq> E \<and> E \<in> sets M \<and> (\<forall>F\<in>sets M. emeasure M (F \<inter> E) = outer_measure_of M (F \<inter> A)))"
 
 lemma measurable_envelopeD:
   assumes "measurable_envelope M A E"

     by (auto simp: measurable_envelope_def)
   with measurable_envelopeD[OF E] show "emeasure M E = outer_measure_of M A"
     by (auto simp: Int_absorb1)
 qed
 
-lemma measurable_envelope_eq2:
+lemma%important measurable_envelope_eq2:
   assumes "A \<subseteq> E" "E \<in> sets M" "emeasure M E < \<infinity>"
   shows "measurable_envelope M A E \<longleftrightarrow> (emeasure M E = outer_measure_of M A)"
 proof safe
   assume *: "emeasure M E = outer_measure_of M A"
   show "measurable_envelope M A E"