src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy

 
 theory Nonnegative_Lebesgue_Integration
   imports Measure_Space Borel_Space
 begin
 
-subsection%unimportant \<open>Approximating functions\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Approximating functions\<close>
 
 lemma AE_upper_bound_inf_ennreal:
   fixes F G::"'a \<Rightarrow> ennreal"
   assumes "\<And>e. (e::real) > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e"
   shows "AE x in M. F x \<le> G x"

 they are just functions with a finite range and are measurable when singleton
 sets are measurable.
 
 \<close>
 
-definition%important "simple_function M g \<longleftrightarrow>
+definition\<^marker>\<open>tag important\<close> "simple_function M g \<longleftrightarrow>
     finite (g ` space M) \<and>
     (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"
 
 lemma simple_functionD:
   assumes "simple_function M g"

 lemma simple_function_real_of_nat[intro, simp]:
   fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
   shows "simple_function M (\<lambda>x. real (f x))"
   by (rule simple_function_compose1[OF sf])
 
-lemma%important borel_measurable_implies_simple_function_sequence:
+lemma\<^marker>\<open>tag important\<close> borel_measurable_implies_simple_function_sequence:
   fixes u :: "'a \<Rightarrow> ennreal"
   assumes u[measurable]: "u \<in> borel_measurable M"
   shows "\<exists>f. incseq f \<and> (\<forall>i. (\<forall>x. f i x < top) \<and> simple_function M (f i)) \<and> u = (SUP i. f i)"
-proof%unimportant -
+proof -
   define f where [abs_def]:
     "f i x = real_of_int (floor (enn2real (min i (u x)) * 2^i)) / 2^i" for i x
 
   have [simp]: "0 \<le> f i x" for i x
     by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg enn2real_nonneg)

   obtains f where
     "\<And>i. simple_function M (f i)" "incseq f" "\<And>i x. f i x < top" "\<And>x. (SUP i. f i x) = u x"
   using borel_measurable_implies_simple_function_sequence [OF u]
   by (metis SUP_apply)
 
-lemma%important simple_function_induct
+lemma\<^marker>\<open>tag important\<close> simple_function_induct
     [consumes 1, case_names cong set mult add, induct set: simple_function]:
   fixes u :: "'a \<Rightarrow> ennreal"
   assumes u: "simple_function M u"
   assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
   assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
   assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)"
   assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
   shows "P u"
-proof%unimportant (rule cong)
+proof (rule cong)
   from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x"
   proof eventually_elim
     fix x assume x: "x \<in> space M"
     from simple_function_indicator_representation[OF u x]
     show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" ..

         by (auto intro!: add mult set simple_functionD u simple_function_sum disj)
     qed
   qed fact
 qed
 
-lemma%important borel_measurable_induct
+lemma\<^marker>\<open>tag important\<close> borel_measurable_induct
     [consumes 1, case_names cong set mult add seq, induct set: borel_measurable]:
   fixes u :: "'a \<Rightarrow> ennreal"
   assumes u: "u \<in> borel_measurable M"
   assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
   assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
   assumes mult': "\<And>u c. c < top \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
   assumes add: "\<And>u v. u \<in> borel_measurable M\<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> v x < top) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
   assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. x \<in> space M \<Longrightarrow> U i x < top) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> u = (SUP i. U i) \<Longrightarrow> P (SUP i. U i)"
   shows "P u"
-  using%unimportant u
-proof%unimportant (induct rule: borel_measurable_implies_simple_function_sequence')
+  using u
+proof (induct rule: borel_measurable_implies_simple_function_sequence')
   fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and sup: "\<And>x. (SUP i. U i x) = u x"
   have u_eq: "u = (SUP i. U i)"
     using u by (auto simp add: image_comp sup)
 
   have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top"

   finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
 qed
 
 subsection "Simple integral"
 
-definition%important simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>S") where
+definition\<^marker>\<open>tag important\<close> simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>S") where
   "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
 
 syntax
   "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110)
 

   then show ?thesis by simp
 qed
 
 subsection \<open>Integral on nonnegative functions\<close>
 
-definition%important nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where
+definition\<^marker>\<open>tag important\<close> nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where
   "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
 
 syntax
   "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
 

 qed
 
 lemma nn_integral_bot[simp]: "nn_integral bot f = 0"
   by (simp add: nn_integral_empty)
 
-subsubsection%unimportant \<open>Distributions\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Distributions\<close>
 
 lemma nn_integral_distr:
   assumes T: "T \<in> measurable M M'" and f: "f \<in> borel_measurable (distr M M' T)"
   shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
   using f

     by (subst nn_integral_cong[OF eq])
        (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
 qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
                    nn_integral_monotone_convergence_SUP le_fun_def incseq_def image_comp)
 
-subsubsection%unimportant \<open>Counting space\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Counting space\<close>
 
 lemma simple_function_count_space[simp]:
   "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"
   unfolding simple_function_def by simp
 

   finally show ?thesis .
 qed
 
 subsubsection \<open>Measure spaces with an associated density\<close>
 
-definition%important density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
+definition\<^marker>\<open>tag important\<close> density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
   "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)"
 
 lemma
   shows sets_density[simp, measurable_cong]: "sets (density M f) = sets M"
     and space_density[simp]: "space (density M f) = space M"

     using ae2
     unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f]
     by (intro exI[of _ "N \<union> {x\<in>space M. f x = 0}"] conjI *) (auto elim: eventually_elim2)
 qed
 
-lemma%important nn_integral_density:
+lemma\<^marker>\<open>tag important\<close> nn_integral_density:
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
-using%unimportant g proof%unimportant induct
+using g proof induct
   case (cong u v)
   then show ?case
     apply (subst nn_integral_cong[OF cong(3)])
     apply (simp_all cong: nn_integral_cong)
     done

   apply (intro nn_integral_cong, simp split: split_indicator)
   done
 
 subsubsection \<open>Point measure\<close>
 
-definition%important point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
+definition\<^marker>\<open>tag important\<close> point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
   "point_measure A f = density (count_space A) f"
 
 lemma
   shows space_point_measure: "space (point_measure A f) = A"
     and sets_point_measure: "sets (point_measure A f) = Pow A"

   "finite A \<Longrightarrow> integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
   by (subst nn_integral_point_measure) (auto intro!: sum.mono_neutral_left simp: less_le)
 
 subsubsection \<open>Uniform measure\<close>
 
-definition%important "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)"
+definition\<^marker>\<open>tag important\<close> "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)"
 
 lemma
   shows sets_uniform_measure[simp, measurable_cong]: "sets (uniform_measure M A) = sets M"
     and space_uniform_measure[simp]: "space (uniform_measure M A) = space M"
   by (auto simp: uniform_measure_def)

     by (cases "emeasure M A") (auto split: split_indicator simp: ennreal_zero_less_divide)
   ultimately show ?thesis
     unfolding uniform_measure_def by (simp add: AE_density)
 qed
 
-subsubsection%unimportant \<open>Null measure\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Null measure\<close>
 
 lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)"
   by (intro measure_eqI) (simp_all add: emeasure_density)
 
 lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0"

     by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure)
 qed simp
 
 subsubsection \<open>Uniform count measure\<close>
 
-definition%important "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
+definition\<^marker>\<open>tag important\<close> "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
 
 lemma
   shows space_uniform_count_measure: "space (uniform_count_measure A) = A"
     and sets_uniform_count_measure: "sets (uniform_count_measure A) = Pow A"
     unfolding uniform_count_measure_def by (auto simp: space_point_measure sets_point_measure)

 lemma sets_uniform_count_measure_eq_UNIV [simp]:
   "sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True"
   "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True"
 by(simp_all add: sets_uniform_count_measure)
 
-subsubsection%unimportant \<open>Scaled measure\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Scaled measure\<close>
 
 lemma nn_integral_scale_measure:
   assumes f: "f \<in> borel_measurable M"
   shows "nn_integral (scale_measure r M) f = r * nn_integral M f"
   using f