--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Jul 18 15:40:15 2019 +0100
@@ -421,64 +421,6 @@
by (simp add: measure_linear_image \<open>linear f\<close> S f)
qed
-subsection\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
-
-text\<open>A Lebesgue set is almost an \<open>F_sigma\<close> or \<open>G_delta\<close>.\<close>
-lemma lebesgue_set_almost_fsigma:
- assumes "S \<in> sets lebesgue"
- obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T"
-proof -
- { fix n::nat
- obtain T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "emeasure lebesgue (S - T) < ennreal (1 / Suc n)"
- using sets_lebesgue_inner_closed [OF assms]
- by (metis of_nat_0_less_iff zero_less_Suc zero_less_divide_1_iff)
- then have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n"
- by (metis emeasure_eq_measure2 ennreal_leI not_le)
- }
- then obtain F where F: "\<And>n::nat. closed (F n) \<and> F n \<subseteq> S \<and> S - F n \<in> lmeasurable \<and> measure lebesgue (S - F n) < 1 / Suc n"
- by metis
- let ?C = "\<Union>(F ` UNIV)"
- show thesis
- proof
- show "fsigma ?C"
- using F by (simp add: fsigma.intros)
- show "negligible (S - ?C)"
- proof (clarsimp simp add: negligible_outer_le)
- fix e :: "real"
- assume "0 < e"
- then obtain n where n: "1 / Suc n < e"
- using nat_approx_posE by metis
- show "\<exists>T. S - (\<Union>x. F x) \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T \<le> e"
- proof (intro exI conjI)
- show "measure lebesgue (S - F n) \<le> e"
- by (meson F n less_trans not_le order.asym)
- qed (use F in auto)
- qed
- show "?C \<union> (S - ?C) = S"
- using F by blast
- show "disjnt ?C (S - ?C)"
- by (auto simp: disjnt_def)
- qed
-qed
-
-lemma lebesgue_set_almost_gdelta:
- assumes "S \<in> sets lebesgue"
- obtains C T where "gdelta C" "negligible T" "S \<union> T = C" "disjnt S T"
-proof -
- have "-S \<in> sets lebesgue"
- using assms Compl_in_sets_lebesgue by blast
- then obtain C T where C: "fsigma C" "negligible T" "C \<union> T = -S" "disjnt C T"
- using lebesgue_set_almost_fsigma by metis
- show thesis
- proof
- show "gdelta (-C)"
- by (simp add: \<open>fsigma C\<close> fsigma_imp_gdelta)
- show "S \<union> T = -C" "disjnt S T"
- using C by (auto simp: disjnt_def)
- qed (use C in auto)
-qed
-
-
proposition measure_semicontinuous_with_hausdist_explicit:
assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0"
obtains d where "d > 0"
@@ -3459,11 +3401,13 @@
integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f(g x)) = b
\<longleftrightarrow> f absolutely_integrable_on (g ` S) \<and> integral (g ` S) f = b"
proof -
- obtain C N where "fsigma C" "negligible N" and CNS: "C \<union> N = S" and "disjnt C N"
+ obtain C N where "fsigma C" and N: "N \<in> null_sets lebesgue" and CNS: "C \<union> N = S" and "disjnt C N"
using lebesgue_set_almost_fsigma [OF S] .
then obtain F :: "nat \<Rightarrow> (real^'m::_) set"
where F: "range F \<subseteq> Collect compact" and Ceq: "C = Union(range F)"
using fsigma_Union_compact by metis
+ have "negligible N"
+ using N by (simp add: negligible_iff_null_sets)
let ?D = "\<lambda>x. \<bar>det (matrix (g' x))\<bar> *\<^sub>R f (g x)"
have "?D absolutely_integrable_on C \<and> integral C ?D = b
\<longleftrightarrow> f absolutely_integrable_on (g ` C) \<and> integral (g ` C) f = b"
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Jul 18 15:40:15 2019 +0100
@@ -641,11 +641,8 @@
qed
lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)"
- apply (simp add: bounded_iff)
- apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)")
- apply metis
- apply arith
- done
+ unfolding bounded_iff
+ by (meson less_imp_le not_le order_trans zero_less_one)
lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
apply (simp add: bounded_pos)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jul 18 15:40:15 2019 +0100
@@ -957,6 +957,11 @@
using absolutely_integrable_on_def set_integrable_def by blast
qed
+lemma absolutely_integrable_imp_integrable:
+ assumes "f absolutely_integrable_on S" "S \<in> sets lebesgue"
+ shows "integrable (lebesgue_on S) f"
+ by (meson assms integrable_restrict_space set_integrable_def sets.Int sets.top)
+
lemma absolutely_integrable_on_null [intro]:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "content (cbox a b) = 0 \<Longrightarrow> f absolutely_integrable_on (cbox a b)"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jul 18 15:40:15 2019 +0100
@@ -119,6 +119,11 @@
"content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
by (simp add: content_Pair)
+lemma content_cbox_plus:
+ fixes x :: "'a::euclidean_space"
+ shows "content(cbox x (x + h *\<^sub>R One)) = (if h \<ge> 0 then h ^ DIM('a) else 0)"
+ by (simp add: algebra_simps content_cbox_if box_eq_empty)
+
lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
using emeasure_mono[of s "cbox a b" lborel]
by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Jul 18 15:40:15 2019 +0100
@@ -386,6 +386,16 @@
abbreviation\<^marker>\<open>tag important\<close> lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure"
where "lebesgue_on \<Omega> \<equiv> restrict_space (completion lborel) \<Omega>"
+lemma lebesgue_on_mono:
+ assumes major: "AE x in lebesgue_on S. P x" and minor: "\<And>x.\<lbrakk>P x; x \<in> S\<rbrakk> \<Longrightarrow> Q x"
+ shows "AE x in lebesgue_on S. Q x"
+proof -
+ have "AE a in lebesgue_on S. P a \<longrightarrow> Q a"
+ using minor space_restrict_space by fastforce
+ then show ?thesis
+ using major by auto
+qed
+
lemma
shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
and space_lborel[simp]: "space lborel = space borel"
@@ -425,6 +435,12 @@
space_restrict_space)
qed
+lemma id_borel_measurable_lebesgue [iff]: "id \<in> borel_measurable lebesgue"
+ by (simp add: measurable_completion)
+
+lemma id_borel_measurable_lebesgue_on [iff]: "id \<in> borel_measurable (lebesgue_on S)"
+ by (simp add: measurable_completion measurable_restrict_space1)
+
context
begin
@@ -617,6 +633,21 @@
lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel"
by (intro countable_imp_null_set_lborel countable_finite)
+lemma insert_null_sets_iff [simp]: "insert a N \<in> null_sets lebesgue \<longleftrightarrow> N \<in> null_sets lebesgue"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (meson completion.complete2 subset_insertI)
+next
+ assume ?rhs then show ?lhs
+ by (simp add: null_sets.insert_in_sets null_setsI)
+qed
+
+lemma insert_null_sets_lebesgue_on_iff [simp]:
+ assumes "a \<in> S" "S \<in> sets lebesgue"
+ shows "insert a N \<in> null_sets (lebesgue_on S) \<longleftrightarrow> N \<in> null_sets (lebesgue_on S)"
+ by (simp add: assms null_sets_restrict_space)
+
lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)"
proof
assume asm: "lborel = count_space A"
@@ -1418,4 +1449,58 @@
lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
using fsigma_imp_gdelta gdelta_imp_fsigma by force
+lemma lebesgue_set_almost_fsigma:
+ assumes "S \<in> sets lebesgue"
+ obtains C T where "fsigma C" "T \<in> null_sets lebesgue" "C \<union> T = S" "disjnt C T"
+proof -
+ { fix n::nat
+ obtain T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "emeasure lebesgue (S - T) < ennreal (1 / Suc n)"
+ using sets_lebesgue_inner_closed [OF assms]
+ by (metis of_nat_0_less_iff zero_less_Suc zero_less_divide_1_iff)
+ then have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n"
+ by (metis emeasure_eq_measure2 ennreal_leI not_le)
+ }
+ then obtain F where F: "\<And>n::nat. closed (F n) \<and> F n \<subseteq> S \<and> S - F n \<in> lmeasurable \<and> measure lebesgue (S - F n) < 1 / Suc n"
+ by metis
+ let ?C = "\<Union>(F ` UNIV)"
+ show thesis
+ proof
+ show "fsigma ?C"
+ using F by (simp add: fsigma.intros)
+ show "(S - ?C) \<in> null_sets lebesgue"
+ proof (clarsimp simp add: completion.null_sets_outer_le)
+ fix e :: "real"
+ assume "0 < e"
+ then obtain n where n: "1 / Suc n < e"
+ using nat_approx_posE by metis
+ show "\<exists>T \<in> lmeasurable. S - (\<Union>x. F x) \<subseteq> T \<and> measure lebesgue T \<le> e"
+ proof (intro bexI conjI)
+ show "measure lebesgue (S - F n) \<le> e"
+ by (meson F n less_trans not_le order.asym)
+ qed (use F in auto)
+ qed
+ show "?C \<union> (S - ?C) = S"
+ using F by blast
+ show "disjnt ?C (S - ?C)"
+ by (auto simp: disjnt_def)
+ qed
+qed
+
+lemma lebesgue_set_almost_gdelta:
+ assumes "S \<in> sets lebesgue"
+ obtains C T where "gdelta C" "T \<in> null_sets lebesgue" "S \<union> T = C" "disjnt S T"
+proof -
+ have "-S \<in> sets lebesgue"
+ using assms Compl_in_sets_lebesgue by blast
+ then obtain C T where C: "fsigma C" "T \<in> null_sets lebesgue" "C \<union> T = -S" "disjnt C T"
+ using lebesgue_set_almost_fsigma by metis
+ show thesis
+ proof
+ show "gdelta (-C)"
+ by (simp add: \<open>fsigma C\<close> fsigma_imp_gdelta)
+ show "S \<union> T = -C" "disjnt S T"
+ using C by (auto simp: disjnt_def)
+ qed (use C in auto)
+qed
+
end
--- a/src/HOL/Analysis/Measure_Space.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Jul 18 15:40:15 2019 +0100
@@ -1112,7 +1112,7 @@
lemma AE_impI:
"(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x"
- by (cases P) auto
+ by fastforce
lemma AE_measure:
assumes AE: "AE x in M. P x" and sets: "{x\<in>space M. P x} \<in> sets M" (is "?P \<in> sets M")
@@ -1562,6 +1562,9 @@
by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top
del: real_of_ereal_enn2ereal)
+lemma enn2real_sum:"(\<And>i. i \<in> I \<Longrightarrow> f i < top) \<Longrightarrow> enn2real (sum f I) = sum (enn2real \<circ> f) I"
+ by (induction I rule: infinite_finite_induct) (auto simp: enn2real_plus)
+
lemma measure_eq_AE:
assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
assumes A: "A \<in> sets M" and B: "B \<in> sets M"
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 18 14:08:44 2019 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jul 18 15:40:15 2019 +0100
@@ -1110,7 +1110,7 @@
lemma enn2real_positive_iff: "0 < enn2real x \<longleftrightarrow> (0 < x \<and> x < top)"
by (cases x rule: ennreal_cases) auto
-lemma enn2real_eq_1_iff[simp]: "enn2real x = 1 \<longleftrightarrow> x = 1"
+lemma enn2real_eq_posreal_iff[simp]: "c > 0 \<Longrightarrow> enn2real x = c \<longleftrightarrow> x = c"
by (cases x) auto
subsection \<open>Coercion from \<^typ>\<open>enat\<close> to \<^typ>\<open>ennreal\<close>\<close>