--- 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
--- 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