# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1563460815 -3600
# Node ID 2b0dca68c3ee27464d3a5bccaa179da89d0bf90a
# Parent  8a7053892d8e5ed3eef59e7ebab0800c5bfed856
More analysis / measure theory material

diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Change_Of_Vars.thy
--- 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"
diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- 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)
diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- 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)"
diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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)
diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Lebesgue_Measure.thy
--- 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
diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Analysis/Measure_Space.thy
--- 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"
diff -r 8a7053892d8e -r 2b0dca68c3ee src/HOL/Library/Extended_Nonnegative_Real.thy
--- 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>