# HG changeset patch
# User hoelzl
# Date 1475228139 -7200
# Node ID 4359400adfe7afd29f771ec0bcb2bba795c257f0
# Parent  2aa42596edc3b3756d7f4fa922c55c2ae30a5aab
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)

diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Fri Sep 30 11:35:39 2016 +0200
@@ -1,6 +1,5 @@
 theory Analysis
 imports
-  Regularity
   Lebesgue_Integral_Substitution
   Embed_Measure
   Complete_Measure
diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 30 11:35:39 2016 +0200
@@ -199,6 +199,9 @@
   qed
 qed
 
+lemma measure_completion[simp]: "S \<in> sets M \<Longrightarrow> measure (completion M) S = measure M S"
+  unfolding measure_def by auto
+
 lemma emeasure_completion_UN:
   "range S \<subseteq> sets (completion M) \<Longrightarrow>
     emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 30 11:35:39 2016 +0200
@@ -962,7 +962,7 @@
 lemma
   assumes \<D>: "\<D> division_of S"
   shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
-    and content_divsion: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
+    and content_division: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
 proof -
   { fix d1 d2 assume *: "d1 \<in> \<D>" "d2 \<in> \<D>" "d1 \<noteq> d2"
     then obtain a b c d where "d1 = cbox a b" "d2 = cbox c d"
@@ -1133,6 +1133,368 @@
                   not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
             intro: eq_refl antisym less_imp_le)
 
+subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
+
+lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
+  by (auto simp: measure_def null_sets_def)
+
+text\<open>The bound will be eliminated by a sort of onion argument\<close>
+lemma locally_Lipschitz_negl_bounded:
+  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+  assumes MleN: "DIM('M) \<le> DIM('N)" "0 < B" "bounded S" "negligible S"
+      and lips: "\<And>x. x \<in> S
+                      \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and>
+                              (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
+  shows "negligible (f ` S)"
+  unfolding negligible_iff_null_sets
+proof (clarsimp simp: completion.null_sets_outer)
+  fix e::real
+  assume "0 < e"
+  have "S \<in> lmeasurable"
+    using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets fmeasurableI_null_sets)
+  have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)"
+    using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
+  obtain T
+    where "open T" "S \<subseteq> T" "T \<in> lmeasurable"
+      and "measure lebesgue T \<le> measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+    by (rule lmeasurable_outer_open [OF \<open>S \<in> lmeasurable\<close> e22])
+  then have T: "measure lebesgue T \<le> e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+    using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets measure_eq_0_null_sets)
+  have "\<exists>r. 0 < r \<and> r \<le> 1/2 \<and>
+            (x \<in> S \<longrightarrow> (\<forall>y. norm(y - x) < r
+                       \<longrightarrow> y \<in> T \<and> (y \<in> S \<longrightarrow> norm(f y - f x) \<le> B * norm(y - x))))"
+        for x
+  proof (cases "x \<in> S")
+    case True
+    obtain U where "open U" "x \<in> U" and U: "\<And>y. y \<in> S \<inter> U \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
+      using lips [OF \<open>x \<in> S\<close>] by auto
+    have "x \<in> T \<inter> U"
+      using \<open>S \<subseteq> T\<close> \<open>x \<in> U\<close> \<open>x \<in> S\<close> by auto
+    then obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T \<inter> U"
+      by (metis \<open>open T\<close> \<open>open U\<close> openE open_Int)
+    then show ?thesis
+      apply (rule_tac x="min (1/2) \<epsilon>" in exI)
+      apply (simp del: divide_const_simps)
+      apply (intro allI impI conjI)
+       apply (metis dist_commute dist_norm mem_ball subsetCE)
+      by (metis Int_iff subsetCE U dist_norm mem_ball norm_minus_commute)
+  next
+    case False
+    then show ?thesis
+      by (rule_tac x="1/4" in exI) auto
+  qed
+  then obtain R where R12: "\<And>x. 0 < R x \<and> R x \<le> 1/2"
+                and RT: "\<And>x y. \<lbrakk>x \<in> S; norm(y - x) < R x\<rbrakk> \<Longrightarrow> y \<in> T"
+                and RB: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; norm(y - x) < R x\<rbrakk> \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
+    by metis+
+  then have gaugeR: "gauge (\<lambda>x. ball x (R x))"
+    by (simp add: gauge_def)
+  obtain c where c: "S \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)" "box (-c *\<^sub>R One:: 'M) (c *\<^sub>R One) \<noteq> {}"
+  proof -
+    obtain B where B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
+      using \<open>bounded S\<close> bounded_iff by blast
+    show ?thesis
+      apply (rule_tac c = "abs B + 1" in that)
+      using norm_bound_Basis_le Basis_le_norm
+       apply (fastforce simp: box_eq_empty mem_box dest!: B intro: order_trans)+
+      done
+  qed
+  obtain \<D> where "countable \<D>"
+     and Dsub: "\<Union>\<D> \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)"
+     and cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+     and pw:   "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
+     and Ksub: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> (\<lambda>x. ball x (R x)) x"
+     and exN:  "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (2*c) / 2^n"
+     and "S \<subseteq> \<Union>\<D>"
+    using covering_lemma [OF c gaugeR]  by force
+  have "\<exists>u v z. K = cbox u v \<and> box u v \<noteq> {} \<and> z \<in> S \<and> z \<in> cbox u v \<and>
+                cbox u v \<subseteq> ball z (R z)" if "K \<in> \<D>" for K
+  proof -
+    obtain u v where "K = cbox u v"
+      using \<open>K \<in> \<D>\<close> cbox by blast
+    with that show ?thesis
+      apply (rule_tac x=u in exI)
+      apply (rule_tac x=v in exI)
+      apply (metis Int_iff interior_cbox cbox Ksub)
+      done
+  qed
+  then obtain uf vf zf
+    where uvz: "\<And>K. K \<in> \<D> \<Longrightarrow>
+                K = cbox (uf K) (vf K) \<and> box (uf K) (vf K) \<noteq> {} \<and> zf K \<in> S \<and>
+                zf K \<in> cbox (uf K) (vf K) \<and> cbox (uf K) (vf K) \<subseteq> ball (zf K) (R (zf K))"
+    by metis
+  define prj1 where "prj1 \<equiv> \<lambda>x::'M. x \<bullet> (SOME i. i \<in> Basis)"
+  define fbx where "fbx \<equiv> \<lambda>D. cbox (f(zf D) - (B * DIM('M) * (prj1(vf D - uf D))) *\<^sub>R One::'N)
+                                    (f(zf D) + (B * DIM('M) * prj1(vf D - uf D)) *\<^sub>R One)"
+  have vu_pos: "0 < prj1 (vf X - uf X)" if "X \<in> \<D>" for X
+    using uvz [OF that] by (simp add: prj1_def box_ne_empty SOME_Basis inner_diff_left)
+  have prj1_idem: "prj1 (vf X - uf X) = (vf X - uf X) \<bullet> i" if  "X \<in> \<D>" "i \<in> Basis" for X i
+  proof -
+    have "cbox (uf X) (vf X) \<in> \<D>"
+      using uvz \<open>X \<in> \<D>\<close> by auto
+    with exN obtain n where "\<And>i. i \<in> Basis \<Longrightarrow> vf X \<bullet> i - uf X \<bullet> i = (2*c) / 2^n"
+      by blast
+    then show ?thesis
+      by (simp add: \<open>i \<in> Basis\<close> SOME_Basis inner_diff prj1_def)
+  qed
+  have countbl: "countable (fbx ` \<D>)"
+    using \<open>countable \<D>\<close> by blast
+  have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e / 2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
+  proof -
+    have BM_ge0: "0 \<le> B * (DIM('M) * prj1 (vf X - uf X))" if "X \<in> \<D>'" for X
+      using \<open>0 < B\<close> \<open>\<D>' \<subseteq> \<D>\<close> that vu_pos by fastforce
+    have "{} \<notin> \<D>'"
+      using cbox \<open>\<D>' \<subseteq> \<D>\<close> interior_empty by blast
+    have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> setsum (measure lebesgue o fbx) \<D>'"
+      by (rule setsum_image_le [OF \<open>finite \<D>'\<close>]) (force simp: fbx_def)
+    also have "\<dots> \<le> (\<Sum>X\<in>\<D>'. (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X)"
+    proof (rule setsum_mono)
+      fix X assume "X \<in> \<D>'"
+      then have "X \<in> \<D>" using \<open>\<D>' \<subseteq> \<D>\<close> by blast
+      then have ufvf: "cbox (uf X) (vf X) = X"
+        using uvz by blast
+      have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
+        by (rule setprod_constant [symmetric])
+      also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
+        using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: setprod.cong)
+      finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
+      have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
+        using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
+      moreover have "cbox (uf X) (vf X) \<subseteq> ball (zf X) (1/2)"
+        by (meson R12 order_trans subset_ball uvz [OF \<open>X \<in> \<D>\<close>])
+      ultimately have "uf X \<in> ball (zf X) (1/2)"  "vf X \<in> ball (zf X) (1/2)"
+        by auto
+      then have "dist (vf X) (uf X) \<le> 1"
+        unfolding mem_ball
+        by (metis dist_commute dist_triangle_half_l dual_order.order_iff_strict)
+      then have 1: "prj1 (vf X - uf X) \<le> 1"
+        unfolding prj1_def dist_norm using Basis_le_norm SOME_Basis order_trans by fastforce
+      have 0: "0 \<le> prj1 (vf X - uf X)"
+        using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
+      have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
+        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> setprod_constant)
+        apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
+        using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
+        apply (fastforce simp add: box_ne_empty power_decreasing)
+        done
+      also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
+        by (subst (3) ufvf[symmetric]) simp
+      finally show "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
+    qed
+    also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \<D>'"
+      by (simp add: setsum_distrib_left)
+    also have "\<dots> \<le> e / 2"
+    proof -
+      have div: "\<D>' division_of \<Union>\<D>'"
+        apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
+        using cbox that apply blast
+        using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
+        done
+      have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
+      proof (rule measure_mono_fmeasurable [OF _ _ \<open>T : lmeasurable\<close>])
+        show "(\<Union>\<D>') \<in> sets lebesgue"
+          using div lmeasurable_division by auto
+        have "\<Union>\<D>' \<subseteq> \<Union>\<D>"
+          using \<open>\<D>' \<subseteq> \<D>\<close> by blast
+        also have "... \<subseteq> T"
+        proof (clarify)
+          fix x D
+          assume "x \<in> D" "D \<in> \<D>"
+          show "x \<in> T"
+            using Ksub [OF \<open>D \<in> \<D>\<close>]
+            by (metis \<open>x \<in> D\<close> Int_iff dist_norm mem_ball norm_minus_commute subsetD RT)
+        qed
+        finally show "\<Union>\<D>' \<subseteq> T" .
+      qed
+      have "setsum (measure lebesgue) \<D>' = setsum content \<D>'"
+        using  \<open>\<D>' \<subseteq> \<D>\<close> cbox by (force intro: setsum.cong)
+      then have "(2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \<D>' =
+                 (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\<Union>\<D>')"
+        using content_division [OF div] by auto
+      also have "\<dots> \<le> (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
+        apply (rule mult_left_mono [OF le_meaT])
+        using \<open>0 < B\<close>
+        apply (simp add: algebra_simps)
+        done
+      also have "\<dots> \<le> e / 2"
+        using T \<open>0 < B\<close> by (simp add: field_simps)
+      finally show ?thesis .
+    qed
+    finally show ?thesis .
+  qed
+  then have e2: "setsum (measure lebesgue) \<G> \<le> e / 2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
+    by (metis finite_subset_image that)
+  show "\<exists>W\<in>lmeasurable. f ` S \<subseteq> W \<and> measure lebesgue W < e"
+  proof (intro bexI conjI)
+    have "\<exists>X\<in>\<D>. f y \<in> fbx X" if "y \<in> S" for y
+    proof -
+      obtain X where "y \<in> X" "X \<in> \<D>"
+        using \<open>S \<subseteq> \<Union>\<D>\<close> \<open>y \<in> S\<close> by auto
+      then have y: "y \<in> ball(zf X) (R(zf X))"
+        using uvz by fastforce
+      have conj_le_eq: "z - b \<le> y \<and> y \<le> z + b \<longleftrightarrow> abs(y - z) \<le> b" for z y b::real
+        by auto
+      have yin: "y \<in> cbox (uf X) (vf X)" and zin: "(zf X) \<in> cbox (uf X) (vf X)"
+        using uvz \<open>X \<in> \<D>\<close> \<open>y \<in> X\<close> by auto
+      have "norm (y - zf X) \<le> (\<Sum>i\<in>Basis. \<bar>(y - zf X) \<bullet> i\<bar>)"
+        by (rule norm_le_l1)
+      also have "\<dots> \<le> real DIM('M) * prj1 (vf X - uf X)"
+      proof (rule setsum_bounded_above)
+        fix j::'M assume j: "j \<in> Basis"
+        show "\<bar>(y - zf X) \<bullet> j\<bar> \<le> prj1 (vf X - uf X)"
+          using yin zin j
+          by (fastforce simp add: mem_box prj1_idem [OF \<open>X \<in> \<D>\<close> j] inner_diff_left)
+      qed
+      finally have nole: "norm (y - zf X) \<le> DIM('M) * prj1 (vf X - uf X)"
+        by simp
+      have fle: "\<bar>f y \<bullet> i - f(zf X) \<bullet> i\<bar> \<le> B * DIM('M) * prj1 (vf X - uf X)" if "i \<in> Basis" for i
+      proof -
+        have "\<bar>f y \<bullet> i - f (zf X) \<bullet> i\<bar> = \<bar>(f y - f (zf X)) \<bullet> i\<bar>"
+          by (simp add: algebra_simps)
+        also have "\<dots> \<le> norm (f y - f (zf X))"
+          by (simp add: Basis_le_norm that)
+        also have "\<dots> \<le> B * norm(y - zf X)"
+          by (metis uvz RB \<open>X \<in> \<D>\<close> dist_commute dist_norm mem_ball \<open>y \<in> S\<close> y)
+        also have "\<dots> \<le> B * real DIM('M) * prj1 (vf X - uf X)"
+          using \<open>0 < B\<close> by (simp add: nole)
+        finally show ?thesis .
+      qed
+      show ?thesis
+        by (rule_tac x=X in bexI)
+           (auto simp: fbx_def prj1_idem mem_box conj_le_eq inner_add inner_diff fle \<open>X \<in> \<D>\<close>)
+    qed
+    then show "f ` S \<subseteq> (\<Union>D\<in>\<D>. fbx D)" by auto
+  next
+    have 1: "\<And>D. D \<in> \<D> \<Longrightarrow> fbx D \<in> lmeasurable"
+      by (auto simp: fbx_def)
+    have 2: "I' \<subseteq> \<D> \<Longrightarrow> finite I' \<Longrightarrow> measure lebesgue (\<Union>D\<in>I'. fbx D) \<le> e/2" for I'
+      by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def)
+    have 3: "0 \<le> e/2"
+      using \<open>0<e\<close> by auto
+    show "(\<Union>D\<in>\<D>. fbx D) \<in> lmeasurable"
+      by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
+    have "measure lebesgue (\<Union>D\<in>\<D>. fbx D) \<le> e/2"
+      by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
+    then show "measure lebesgue (\<Union>D\<in>\<D>. fbx D) < e"
+      using \<open>0 < e\<close> by linarith
+  qed
+qed
+
+proposition negligible_locally_Lipschitz_image:
+  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+  assumes MleN: "DIM('M) \<le> DIM('N)" "negligible S"
+      and lips: "\<And>x. x \<in> S
+                      \<Longrightarrow> \<exists>T B. open T \<and> x \<in> T \<and>
+                              (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
+    shows "negligible (f ` S)"
+proof -
+  let ?S = "\<lambda>n. ({x \<in> S. norm x \<le> n \<and>
+                          (\<exists>T. open T \<and> x \<in> T \<and>
+                               (\<forall>y\<in>S \<inter> T. norm (f y - f x) \<le> (real n + 1) * norm (y - x)))})"
+  have negfn: "f ` ?S n \<in> null_sets lebesgue" for n::nat
+    unfolding negligible_iff_null_sets[symmetric]
+    apply (rule_tac B = "real n + 1" in locally_Lipschitz_negl_bounded)
+    by (auto simp: MleN bounded_iff intro: negligible_subset [OF \<open>negligible S\<close>])
+  have "S = (\<Union>n. ?S n)"
+  proof (intro set_eqI iffI)
+    fix x assume "x \<in> S"
+    with lips obtain T B where T: "open T" "x \<in> T"
+                           and B: "\<And>y. y \<in> S \<inter> T \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
+      by metis+
+    have no: "norm (f y - f x) \<le> (nat \<lceil>max B (norm x)\<rceil> + 1) * norm (y - x)" if "y \<in> S \<inter> T" for y
+    proof -
+      have "B * norm(y - x) \<le> (nat \<lceil>max B (norm x)\<rceil> + 1) * norm (y - x)"
+        by (meson max.cobounded1 mult_right_mono nat_ceiling_le_eq nat_le_iff_add norm_ge_zero order_trans)
+      then show ?thesis
+        using B order_trans that by blast
+    qed
+    have "x \<in> ?S (nat (ceiling (max B (norm x))))"
+      apply (simp add: \<open>x \<in> S \<close>, rule)
+      using real_nat_ceiling_ge max.bounded_iff apply blast
+      using T no
+      apply (force simp: algebra_simps)
+      done
+    then show "x \<in> (\<Union>n. ?S n)" by force
+  qed auto
+  then show ?thesis
+    by (rule ssubst) (auto simp: image_Union negligible_iff_null_sets intro: negfn)
+qed
+
+corollary negligible_differentiable_image_negligible:
+  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+  assumes MleN: "DIM('M) \<le> DIM('N)" "negligible S"
+      and diff_f: "f differentiable_on S"
+    shows "negligible (f ` S)"
+proof -
+  have "\<exists>T B. open T \<and> x \<in> T \<and> (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
+        if "x \<in> S" for x
+  proof -
+    obtain f' where "linear f'"
+      and f': "\<And>e. e>0 \<Longrightarrow>
+                  \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
+                              norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
+      using diff_f \<open>x \<in> S\<close>
+      by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
+    obtain B where "B > 0" and B: "\<forall>x. norm (f' x) \<le> B * norm x"
+      using linear_bounded_pos \<open>linear f'\<close> by blast
+    obtain d where "d>0"
+              and d: "\<And>y. \<lbrakk>y \<in> S; norm (y - x) < d\<rbrakk> \<Longrightarrow>
+                          norm (f y - f x - f' (y - x)) \<le> norm (y - x)"
+      using f' [of 1] by (force simp:)
+    have *: "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
+              if "y \<in> S" "norm (y - x) < d" for y
+    proof -
+      have "norm (f y - f x) -B *  norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
+        by (simp add: B)
+      also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
+        by (rule norm_triangle_ineq2)
+      also have "... \<le> norm (y - x)"
+        by (rule d [OF that])
+      finally show ?thesis
+        by (simp add: algebra_simps)
+    qed
+    show ?thesis
+      apply (rule_tac x="ball x d" in exI)
+      apply (rule_tac x="B+1" in exI)
+      using \<open>d>0\<close>
+      apply (auto simp: dist_norm norm_minus_commute intro!: *)
+      done
+  qed
+  with negligible_locally_Lipschitz_image assms show ?thesis by metis
+qed
+
+corollary negligible_differentiable_image_lowdim:
+  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+  assumes MlessN: "DIM('M) < DIM('N)" and diff_f: "f differentiable_on S"
+    shows "negligible (f ` S)"
+proof -
+  have "x \<le> DIM('M) \<Longrightarrow> x \<le> DIM('N)" for x
+    using MlessN by linarith
+  obtain lift :: "'M * real \<Rightarrow> 'N" and drop :: "'N \<Rightarrow> 'M * real" and j :: 'N
+    where "linear lift" "linear drop" and dropl [simp]: "\<And>z. drop (lift z) = z"
+      and "j \<in> Basis" and j: "\<And>x. lift(x,0) \<bullet> j = 0"
+    using lowerdim_embeddings [OF MlessN] by metis
+  have "negligible {x. x\<bullet>j = 0}"
+    by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
+  then have neg0S: "negligible ((\<lambda>x. lift (x, 0)) ` S)"
+    apply (rule negligible_subset)
+    by (simp add: image_subsetI j)
+  have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
+    using diff_f
+    apply (clarsimp simp add: differentiable_on_def)
+    apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
+             linear_imp_differentiable [OF fst_linear])
+    apply (force simp: image_comp o_def)
+    done
+  have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
+    by (simp add: o_def)
+  then show ?thesis
+    apply (rule ssubst)
+    apply (subst image_comp [symmetric])
+    apply (metis negligible_differentiable_image_negligible order_refl diff_f' neg0S)
+    done
+qed
+
 lemma set_integral_norm_bound:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Sep 30 11:35:39 2016 +0200
@@ -8,7 +8,7 @@
 section \<open>Lebesgue measure\<close>
 
 theory Lebesgue_Measure
-  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests
+  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity
 begin
 
 subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
@@ -986,4 +986,92 @@
   "compact S \<Longrightarrow> (\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1) \<Longrightarrow> S \<in> null_sets lebesgue"
   using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed)
 
+lemma outer_regular_lborel:
+  assumes B: "B \<in> fmeasurable lborel" "0 < (e::real)"
+  shows "\<exists>U. open U \<and> B \<subseteq> U \<and> emeasure lborel U \<le> emeasure lborel B + e"
+proof -
+  let ?\<mu> = "emeasure lborel"
+  let ?B = "\<lambda>n::nat. ball 0 n :: 'a set"
+  have B[measurable]: "B \<in> sets borel"
+    using B by auto
+  let ?e = "\<lambda>n. e*((1/2)^Suc n)"
+  have "\<forall>n. \<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n"
+  proof
+    fix n :: nat
+    let ?A = "density lborel (indicator (?B n))"
+    have emeasure_A: "X \<in> sets borel \<Longrightarrow> emeasure ?A X = ?\<mu> (?B n \<inter> X)" for X
+      by (auto simp add: emeasure_density borel_measurable_indicator indicator_inter_arith[symmetric])
+
+    have finite_A: "emeasure ?A (space ?A) \<noteq> \<infinity>"
+      using emeasure_bounded_finite[of "?B n"] by (auto simp add: emeasure_A)
+    interpret A: finite_measure ?A
+      by rule fact
+    have "emeasure ?A B + ?e n > (INF U:{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
+      using \<open>0<e\<close> by (auto simp: outer_regular[OF _ finite_A B, symmetric])
+    then obtain U where U: "B \<subseteq> U" "open U" "?\<mu> (?B n \<inter> B) + ?e n > ?\<mu> (?B n \<inter> U)"
+      unfolding INF_less_iff by (auto simp: emeasure_A)
+    moreover
+    { have "?\<mu> ((?B n \<inter> U) - B) = ?\<mu> ((?B n \<inter> U) - (?B n \<inter> B))"
+        using U by (intro arg_cong[where f="?\<mu>"]) auto
+      also have "\<dots> = ?\<mu> (?B n \<inter> U) - ?\<mu> (?B n \<inter> B)"
+        using U A.emeasure_finite[of B]
+        by (intro emeasure_Diff) (auto simp del: A.emeasure_finite simp: emeasure_A)
+      also have "\<dots> < ?e n"
+        using U(1,2,3) A.emeasure_finite[of B]
+        by (subst minus_less_iff_ennreal)
+          (auto simp del: A.emeasure_finite simp: emeasure_A less_top ac_simps intro!: emeasure_mono)
+      finally have "?\<mu> ((?B n \<inter> U) - B) < ?e n" . }
+    ultimately show "\<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n"
+      by (intro exI[of _ "?B n \<inter> U"]) auto
+  qed
+  then obtain U
+    where U: "\<And>n. open (U n)" "\<And>n. ?B n \<inter> B \<subseteq> U n" "\<And>n. ?\<mu> (U n - B) < ?e n"
+    by metis
+  then show ?thesis
+  proof (intro exI conjI)
+    { fix x assume "x \<in> B"
+      moreover
+      have "\<exists>n. norm x < real n"
+        by (simp add: reals_Archimedean2)
+      then guess n ..
+      ultimately have "x \<in> (\<Union>n. U n)"
+        using U(2)[of n] by auto }
+    note * = this
+    then show "open (\<Union>n. U n)" "B \<subseteq> (\<Union>n. U n)"
+      using U(1,2) by auto
+    have "?\<mu> (\<Union>n. U n) = ?\<mu> (B \<union> (\<Union>n. U n - B))"
+      using * U(2) by (intro arg_cong[where ?f="?\<mu>"]) auto
+    also have "\<dots> = ?\<mu> B + ?\<mu> (\<Union>n. U n - B)"
+      using U(1) by (intro plus_emeasure[symmetric]) auto
+    also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ?\<mu> (U n - B))"
+      using U(1) by (intro add_mono emeasure_subadditive_countably) auto
+    also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ennreal (?e n))"
+      using U(3) by (intro add_mono suminf_le) (auto intro: less_imp_le)
+    also have "(\<Sum>n. ennreal (?e n)) = ennreal (e * 1)"
+      using \<open>0<e\<close> by (intro suminf_ennreal_eq sums_mult power_half_series) auto
+    finally show "emeasure lborel (\<Union>n. U n) \<le> emeasure lborel B + ennreal e"
+      by simp
+  qed
+qed
+
+lemma lmeasurable_outer_open:
+  assumes S: "S \<in> lmeasurable" and "0 < e"
+  obtains T where "open T" "S \<subseteq> T" "T \<in> lmeasurable" "measure lebesgue T \<le> measure lebesgue S + e"
+proof -
+  obtain S' where S': "S \<subseteq> S'" "S' \<in> sets borel" "emeasure lborel S' = emeasure lebesgue S"
+    using completion_upper[of S lborel] S by auto
+  then have f_S': "S' \<in> fmeasurable lborel"
+    using S by (auto simp: fmeasurable_def)
+  from outer_regular_lborel[OF this \<open>0<e\<close>] guess U .. note U = this
+  show thesis
+  proof (rule that)
+    show "open U" "S \<subseteq> U" "U \<in> lmeasurable"
+      using f_S' U S' by (auto simp: fmeasurable_def less_top[symmetric] top_unique)
+    then have "U \<in> fmeasurable lborel"
+      by (auto simp: fmeasurable_def)
+    with S U \<open>0<e\<close> show "measure lebesgue U \<le> measure lebesgue S + e"
+      unfolding S'(3) by (simp add: emeasure_eq_measure2 ennreal_plus[symmetric] del: ennreal_plus)
+  qed
+qed
+
 end
diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Sep 30 11:35:39 2016 +0200
@@ -472,6 +472,10 @@
   "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
   using additiveD[OF emeasure_additive] ..
 
+lemma emeasure_Union:
+  "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
+  using plus_emeasure[of A M "B - A"] by auto
+
 lemma setsum_emeasure:
   "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
     (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
@@ -1749,6 +1753,42 @@
   "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> sets M) \<Longrightarrow> measure M (\<Union>F) \<le> (\<Sum>S\<in>F. measure M S)"
   using measure_UNION_le[of F "\<lambda>x. x" M] by simp
 
+lemma
+  assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> fmeasurable M"
+    and bound: "\<And>I'. I' \<subseteq> I \<Longrightarrow> finite I' \<Longrightarrow> measure M (\<Union>i\<in>I'. A i) \<le> B" and "0 \<le> B"
+  shows fmeasurable_UN_bound: "(\<Union>i\<in>I. A i) \<in> fmeasurable M" (is ?fm)
+    and measure_UN_bound: "measure M (\<Union>i\<in>I. A i) \<le> B" (is ?m)
+proof -
+  have "?fm \<and> ?m"
+  proof cases
+    assume "I = {}" with \<open>0 \<le> B\<close> show ?thesis by simp
+  next
+    assume "I \<noteq> {}"
+    have "(\<Union>i\<in>I. A i) = (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))"
+      by (subst range_from_nat_into[symmetric, OF \<open>I \<noteq> {}\<close> \<open>countable I\<close>]) auto
+    then have "emeasure M (\<Union>i\<in>I. A i) = emeasure M (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))" by simp
+    also have "\<dots> = (SUP i. emeasure M (\<Union>n\<le>i. A (from_nat_into I n)))"
+      using I \<open>I \<noteq> {}\<close>[THEN from_nat_into] by (intro SUP_emeasure_incseq[symmetric]) (fastforce simp: incseq_Suc_iff)+
+    also have "\<dots> \<le> B"
+    proof (intro SUP_least)
+      fix i :: nat
+      have "emeasure M (\<Union>n\<le>i. A (from_nat_into I n)) = measure M (\<Union>n\<le>i. A (from_nat_into I n))"
+        using I \<open>I \<noteq> {}\<close>[THEN from_nat_into] by (intro emeasure_eq_measure2 fmeasurable.finite_UN) auto
+      also have "\<dots> = measure M (\<Union>n\<in>from_nat_into I ` {..i}. A n)"
+        by simp
+      also have "\<dots> \<le> B"
+        by (intro ennreal_leI bound) (auto intro:  from_nat_into[OF \<open>I \<noteq> {}\<close>])
+      finally show "emeasure M (\<Union>n\<le>i. A (from_nat_into I n)) \<le> ennreal B" .
+    qed
+    finally have *: "emeasure M (\<Union>i\<in>I. A i) \<le> B" .
+    then have ?fm
+      using I \<open>countable I\<close> by (intro fmeasurableI conjI) (auto simp: less_top[symmetric] top_unique)
+    with * \<open>0\<le>B\<close> show ?thesis
+      by (simp add: emeasure_eq_measure2)
+  qed
+  then show ?fm ?m by auto
+qed
+
 subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
 
 locale finite_measure = sigma_finite_measure M for M +
diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 30 11:35:39 2016 +0200
@@ -2106,6 +2106,50 @@
   apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
   done
 
+lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
+  unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less)
+
+lemma INF_ereal_add_left:
+  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
+  shows "(INF i:I. f i + c :: ereal) = (INF i:I. f i) + c"
+proof -
+  have "(INF i:I. f i) \<noteq> -\<infinity>"
+    unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
+  then show ?thesis
+    by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
+       (auto simp: mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at)
+qed
+
+lemma INF_ereal_add_right:
+  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
+  shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)"
+  using INF_ereal_add_left[OF assms] by (simp add: ac_simps)
+
+lemma INF_ereal_add_directed:
+  fixes f g :: "'a \<Rightarrow> ereal"
+  assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
+  assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<ge> f k + g k"
+  shows "(INF i:I. f i + g i) = (INF i:I. f i) + (INF i:I. g i)"
+proof cases
+  assume "I = {}" then show ?thesis
+    by (simp add: top_ereal_def)
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof (rule antisym)
+    show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)"
+      by (rule INF_greatest; intro ereal_add_mono INF_lower)
+  next
+    have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))"
+      using directed by (intro INF_greatest) (blast intro: INF_lower2)
+    also have "\<dots> = (INF i:I. f i + (INF i:I. g i))"
+      using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
+    also have "\<dots> = (INF i:I. f i) + (INF i:I. g i)"
+      using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
+    finally show "(INF i:I. f i + g i) \<le> (INF i:I. f i) + (INF i:I. g i)" .
+  qed
+qed
+
 lemma INF_ereal_add:
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "decseq f" "decseq g"