# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1544617926 -3600
# Node ID b7b9cbe0bd432c6a41b1c3ee6afce00e5a533324
# Parent  9cf0b79dfb7f0d5fb4048d72188efca307d862d9
Tagged some of HOL-Analysis

diff -r 9cf0b79dfb7f -r b7b9cbe0bd43 src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Mon Dec 10 23:36:29 2018 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy	Wed Dec 12 13:32:06 2018 +0100
@@ -1,26 +1,26 @@
 (*  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)"
 
@@ -67,9 +67,10 @@
     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)"
@@ -85,17 +86,17 @@
   "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
@@ -180,9 +181,10 @@
   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>"
@@ -281,11 +283,11 @@
   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)" ..
@@ -440,18 +442,19 @@
   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"
+locale%important cld_measure =
+  complete_measure M + locally_determined_measure M for M :: "'a measure"
 
-definition outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
+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"
@@ -550,7 +553,7 @@
     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)))"
 
@@ -615,7 +618,7 @@
     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
diff -r 9cf0b79dfb7f -r b7b9cbe0bd43 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Dec 10 23:36:29 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Dec 12 13:32:06 2018 +0100
@@ -29,17 +29,22 @@
     using fin by (auto intro: Rats_no_bot_less simp: less_top)
 qed (auto intro: assms countable_rat)
 
-subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
+subsection \<open>Measures defined by monotonous functions\<close>
+
+text \<open>
+  Every right-continuous and nondecreasing function gives rise to a measure on the reals:
+\<close>
 
-definition interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where
-  "interval_measure F = extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a <.. b}) (\<lambda>(a, b). ennreal (F b - F a))"
+definition%important interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where
+  "interval_measure F =
+     extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a<..b}) (\<lambda>(a, b). ennreal (F b - F a))"
 
-lemma emeasure_interval_measure_Ioc:
+lemma%important emeasure_interval_measure_Ioc:
   assumes "a \<le> b"
   assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
   assumes right_cont_F : "\<And>a. continuous (at_right a) F"
-  shows "emeasure (interval_measure F) {a <.. b} = F b - F a"
-proof (rule extend_measure_caratheodory_pair[OF interval_measure_def \<open>a \<le> b\<close>])
+  shows "emeasure (interval_measure F) {a<..b} = F b - F a"
+proof%unimportant (rule extend_measure_caratheodory_pair[OF interval_measure_def \<open>a \<le> b\<close>])
   show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \<le> b}"
   proof (unfold_locales, safe)
     fix a b c d :: real assume *: "a \<le> b" "c \<le> d"
@@ -309,7 +314,8 @@
     emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)"
   using emeasure_interval_measure_Ioc[of a b F] by auto
 
-lemma sets_interval_measure [simp, measurable_cong]: "sets (interval_measure F) = sets borel"
+lemma%important sets_interval_measure [simp, measurable_cong]:
+    "sets (interval_measure F) = sets borel"
   apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
   apply (rule sigma_sets_eqI)
   apply auto
@@ -360,7 +366,7 @@
        (auto simp: continuous_on_ennreal continuous_on_diff cont_F continuous_on_const)
 qed (rule trivial_limit_at_left_real)
 
-lemma sigma_finite_interval_measure:
+lemma%important sigma_finite_interval_measure:
   assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
   assumes right_cont_F : "\<And>a. continuous (at_right a) F"
   shows "sigma_finite_measure (interval_measure F)"
@@ -371,13 +377,13 @@
 
 subsection \<open>Lebesgue-Borel measure\<close>
 
-definition lborel :: "('a :: euclidean_space) measure" where
+definition%important lborel :: "('a :: euclidean_space) measure" where
   "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
 
-abbreviation lebesgue :: "'a::euclidean_space measure"
+abbreviation%important lebesgue :: "'a::euclidean_space measure"
   where "lebesgue \<equiv> completion lborel"
 
-abbreviation lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure"
+abbreviation%important lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure"
   where "lebesgue_on \<Omega> \<equiv> restrict_space (completion lborel) \<Omega>"
 
 lemma
@@ -398,7 +404,8 @@
   shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
   by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
 
-text\<open>Measurability of continuous functions\<close>
+text%unimportant \<open>Measurability of continuous functions\<close>
+
 lemma continuous_imp_measurable_on_sets_lebesgue:
   assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue"
   shows "f \<in> borel_measurable (lebesgue_on S)"
@@ -448,10 +455,10 @@
 lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \<le> u then u - l else 0)"
   by simp
 
-lemma emeasure_lborel_cbox[simp]:
+lemma%important emeasure_lborel_cbox[simp]:
   assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
   shows "emeasure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
-proof -
+proof%unimportant -
   have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b) :: ennreal) = indicator (cbox l u)"
     by (auto simp: fun_eq_iff cbox_def split: split_indicator)
   then have "emeasure lborel (cbox l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
@@ -642,12 +649,12 @@
 
 subsection \<open>Affine transformation on the Lebesgue-Borel\<close>
 
-lemma lborel_eqI:
+lemma%important lborel_eqI:
   fixes M :: "'a::euclidean_space measure"
   assumes emeasure_eq: "\<And>l u. (\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b) \<Longrightarrow> emeasure M (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
   assumes sets_eq: "sets M = sets borel"
   shows "lborel = M"
-proof (rule measure_eqI_generator_eq)
+proof%unimportant (rule measure_eqI_generator_eq)
   let ?E = "range (\<lambda>(a, b). box a b::'a set)"
   show "Int_stable ?E"
     by (auto simp: Int_stable_def box_Int_box)
@@ -667,12 +674,12 @@
       done }
 qed
 
-lemma lborel_affine_euclidean:
+lemma%important lborel_affine_euclidean:
   fixes c :: "'a::euclidean_space \<Rightarrow> real" and t
   defines "T x \<equiv> t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j)"
   assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0"
   shows "lborel = density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D")
-proof (rule lborel_eqI)
+proof%unimportant (rule lborel_eqI)
   let ?B = "Basis :: 'a set"
   fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
   have [measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel"
@@ -724,10 +731,10 @@
     lborel_integrable_real_affine[of "\<lambda>x. f (t + c * x)" "1/c" "-t/c"]
   by (auto simp add: field_simps)
 
-lemma lborel_integral_real_affine:
+lemma%important lborel_integral_real_affine:
   fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" and c :: real
   assumes c: "c \<noteq> 0" shows "(\<integral>x. f x \<partial> lborel) = \<bar>c\<bar> *\<^sub>R (\<integral>x. f (t + c * x) \<partial>lborel)"
-proof cases
+proof%unimportant cases
   assume f[measurable]: "integrable lborel f" then show ?thesis
     using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t]
     by (subst lborel_real_affine[OF c, of t])
@@ -889,9 +896,9 @@
 
 interpretation lborel_pair: pair_sigma_finite lborel lborel ..
 
-lemma lborel_prod:
+lemma%important lborel_prod:
   "lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)"
-proof (rule lborel_eqI[symmetric], clarify)
+proof%unimportant (rule lborel_eqI[symmetric], clarify)
   fix la ua :: 'a and lb ub :: 'b
   assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)"
   have [simp]:
@@ -964,16 +971,16 @@
     by (auto simp: mult.commute)
 qed
 
-subsection\<open>Lebesgue measurable sets\<close>
+subsection \<open>Lebesgue measurable sets\<close>
 
-abbreviation lmeasurable :: "'a::euclidean_space set set"
+abbreviation%important lmeasurable :: "'a::euclidean_space set set"
 where
   "lmeasurable \<equiv> fmeasurable lebesgue"
 
 lemma not_measurable_UNIV [simp]: "UNIV \<notin> lmeasurable"
   by (simp add: fmeasurable_def)
 
-lemma lmeasurable_iff_integrable:
+lemma%important lmeasurable_iff_integrable:
   "S \<in> lmeasurable \<longleftrightarrow> integrable lebesgue (indicator S :: 'a::euclidean_space \<Rightarrow> real)"
   by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator)
 
@@ -1027,7 +1034,7 @@
   by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)
 
 
-subsection\<open>Translation preserves Lebesgue measure\<close>
+subsection%unimportant\<open>Translation preserves Lebesgue measure\<close>
 
 lemma sigma_sets_image:
   assumes S: "S \<in> sigma_sets \<Omega> M" and "M \<subseteq> Pow \<Omega>" "f ` \<Omega> = \<Omega>" "inj_on f \<Omega>"
@@ -1108,12 +1115,12 @@
 lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
   by (metis summable_suminf_not_top)
 
-proposition starlike_negligible_bounded_gmeasurable:
+proposition%important starlike_negligible_bounded_gmeasurable:
   fixes S :: "'a :: euclidean_space set"
   assumes S: "S \<in> sets lebesgue" and "bounded S"
       and eq1: "\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
     shows "S \<in> null_sets lebesgue"
-proof -
+proof%unimportant -
   obtain M where "0 < M" "S \<subseteq> ball 0 M"
     using \<open>bounded S\<close> by (auto dest: bounded_subset_ballD)
 
@@ -1232,10 +1239,10 @@
   qed
 qed
 
-lemma outer_regular_lborel:
+lemma%important outer_regular_lborel:
   assumes B: "B \<in> sets borel" and "0 < (e::real)"
   obtains U where "open U" "B \<subseteq> U" "emeasure lborel (U - B) < e"
-proof -
+proof%unimportant -
   obtain U where U: "open U" "B \<subseteq> U" and "emeasure lborel (U-B) \<le> e/2"
     using outer_regular_lborel_le [OF B, of "e/2"] \<open>e > 0\<close>
     by force