src/HOL/Analysis/Lebesgue_Measure.thy

 
   show "?LT`Rats \<subseteq> ?E" "(\<Union>i\<in>Rats. ?LT i) = UNIV" "\<And>a. a \<in> ?LT`Rats \<Longrightarrow> emeasure M a \<noteq> \<infinity>"
     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>
-
-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))"
-
-lemma emeasure_interval_measure_Ioc:
+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%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%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"
     then show "\<exists>C\<subseteq>{{a<..b} |a b. a \<le> b}. finite C \<and> disjoint C \<and> {a<..b} - {c<..d} = \<Union>C"
     proof cases

 lemma emeasure_interval_measure_Ioc_eq:
   "(\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow>
     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
   apply (case_tac "a \<le> ba")
   apply (auto intro: sigma_sets.Empty)

   show "((\<lambda>a. ennreal (F b - F a)) \<longlongrightarrow> F b - F a) (at_left a)"
     by (rule continuous_on_tendsto_compose[where g="\<lambda>x. x" and s=UNIV])
        (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)"
   apply unfold_locales
   apply (intro exI[of _ "(\<lambda>(a, b). {a <.. b}) ` (\<rat> \<times> \<rat>)"])
   apply (auto intro!: Rats_no_top_le Rats_no_bot_less countable_rat simp: emeasure_interval_measure_Ioc_eq[OF assms])
   done
 
 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
   shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
     and space_lborel[simp]: "space lborel = space borel"

 lemma measurable_lebesgue_cong:
   assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   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)"
 proof -
   have "sets (restrict_space borel S) \<subseteq> sets (lebesgue_on S)"

 qed
 
 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)"
     by simp
   also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"

   using mem_closed_if_AE_lebesgue_open[OF open_UNIV] by simp
 
 
 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)
 
   show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E"

       apply (subst box_eq_empty(1)[THEN iffD2])
       apply (auto intro: less_imp_le simp: not_le)
       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"
     by (simp add: T_def[abs_def])
   have eq: "T -` box l u = box

   using
     lborel_integrable_real_affine[of f c t]
     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])
        (simp add: integral_density integral_distr)
 next

 interpretation lborel: sigma_finite_measure lborel
   by (rule sigma_finite_lborel)
 
 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]:
     "\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b"
     "\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b"

   qed simp
   then show ?thesis
     by (auto simp: mult.commute)
 qed
 
-subsection\<open>Lebesgue measurable sets\<close>
-
-abbreviation lmeasurable :: "'a::euclidean_space set set"
+subsection \<open>Lebesgue measurable sets\<close>
+
+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)
 
 lemma lmeasurable_cbox [iff]: "cbox a b \<in> lmeasurable"
   and lmeasurable_box [iff]: "box a b \<in> lmeasurable"

 lemma bounded_set_imp_lmeasurable:
   assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
   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>"
     and M: "\<And>y. y \<in> M \<Longrightarrow> f ` y \<in> M"
   shows "(f ` S) \<in> sigma_sets \<Omega> M"

 subsection \<open>A nice lemma for negligibility proofs\<close>
 
 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)
 
   let ?f = "\<lambda>n. root DIM('a) (Suc n)"
 

     finally show "emeasure lborel ((\<Union>n. U n) - B) \<le> ennreal e"
       by simp
   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
   moreover have "ennreal (e/2) < ennreal e"
     using \<open>e > 0\<close> by (simp add: ennreal_lessI)