author hoelzl Fri Sep 30 11:35:39 2016 +0200 (2016-09-30) changeset 63968 4359400adfe7 parent 63967 2aa42596edc3 child 63969 f4b4fba60b1d
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)
```     1.1 --- a/src/HOL/Analysis/Analysis.thy	Fri Sep 30 14:05:51 2016 +0100
1.2 +++ b/src/HOL/Analysis/Analysis.thy	Fri Sep 30 11:35:39 2016 +0200
1.3 @@ -1,6 +1,5 @@
1.4  theory Analysis
1.5  imports
1.6 -  Regularity
1.7    Lebesgue_Integral_Substitution
1.8    Embed_Measure
1.9    Complete_Measure
```
```     2.1 --- a/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 30 14:05:51 2016 +0100
2.2 +++ b/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 30 11:35:39 2016 +0200
2.3 @@ -199,6 +199,9 @@
2.4    qed
2.5  qed
2.6
2.7 +lemma measure_completion[simp]: "S \<in> sets M \<Longrightarrow> measure (completion M) S = measure M S"
2.8 +  unfolding measure_def by auto
2.9 +
2.10  lemma emeasure_completion_UN:
2.11    "range S \<subseteq> sets (completion M) \<Longrightarrow>
2.12      emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
```
```     3.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 30 14:05:51 2016 +0100
3.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 30 11:35:39 2016 +0200
3.3 @@ -962,7 +962,7 @@
3.4  lemma
3.5    assumes \<D>: "\<D> division_of S"
3.6    shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
3.7 -    and content_divsion: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
3.8 +    and content_division: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
3.9  proof -
3.10    { fix d1 d2 assume *: "d1 \<in> \<D>" "d2 \<in> \<D>" "d1 \<noteq> d2"
3.11      then obtain a b c d where "d1 = cbox a b" "d2 = cbox c d"
3.12 @@ -1133,6 +1133,368 @@
3.13                    not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
3.14              intro: eq_refl antisym less_imp_le)
3.15
3.16 +subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
3.17 +
3.18 +lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
3.19 +  by (auto simp: measure_def null_sets_def)
3.20 +
3.21 +text\<open>The bound will be eliminated by a sort of onion argument\<close>
3.22 +lemma locally_Lipschitz_negl_bounded:
3.23 +  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
3.24 +  assumes MleN: "DIM('M) \<le> DIM('N)" "0 < B" "bounded S" "negligible S"
3.25 +      and lips: "\<And>x. x \<in> S
3.26 +                      \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and>
3.27 +                              (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
3.28 +  shows "negligible (f ` S)"
3.29 +  unfolding negligible_iff_null_sets
3.30 +proof (clarsimp simp: completion.null_sets_outer)
3.31 +  fix e::real
3.32 +  assume "0 < e"
3.33 +  have "S \<in> lmeasurable"
3.34 +    using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets fmeasurableI_null_sets)
3.35 +  have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)"
3.36 +    using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
3.37 +  obtain T
3.38 +    where "open T" "S \<subseteq> T" "T \<in> lmeasurable"
3.39 +      and "measure lebesgue T \<le> measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
3.40 +    by (rule lmeasurable_outer_open [OF \<open>S \<in> lmeasurable\<close> e22])
3.41 +  then have T: "measure lebesgue T \<le> e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
3.42 +    using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets measure_eq_0_null_sets)
3.43 +  have "\<exists>r. 0 < r \<and> r \<le> 1/2 \<and>
3.44 +            (x \<in> S \<longrightarrow> (\<forall>y. norm(y - x) < r
3.45 +                       \<longrightarrow> y \<in> T \<and> (y \<in> S \<longrightarrow> norm(f y - f x) \<le> B * norm(y - x))))"
3.46 +        for x
3.47 +  proof (cases "x \<in> S")
3.48 +    case True
3.49 +    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)"
3.50 +      using lips [OF \<open>x \<in> S\<close>] by auto
3.51 +    have "x \<in> T \<inter> U"
3.52 +      using \<open>S \<subseteq> T\<close> \<open>x \<in> U\<close> \<open>x \<in> S\<close> by auto
3.53 +    then obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T \<inter> U"
3.54 +      by (metis \<open>open T\<close> \<open>open U\<close> openE open_Int)
3.55 +    then show ?thesis
3.56 +      apply (rule_tac x="min (1/2) \<epsilon>" in exI)
3.57 +      apply (simp del: divide_const_simps)
3.58 +      apply (intro allI impI conjI)
3.59 +       apply (metis dist_commute dist_norm mem_ball subsetCE)
3.60 +      by (metis Int_iff subsetCE U dist_norm mem_ball norm_minus_commute)
3.61 +  next
3.62 +    case False
3.63 +    then show ?thesis
3.64 +      by (rule_tac x="1/4" in exI) auto
3.65 +  qed
3.66 +  then obtain R where R12: "\<And>x. 0 < R x \<and> R x \<le> 1/2"
3.67 +                and RT: "\<And>x y. \<lbrakk>x \<in> S; norm(y - x) < R x\<rbrakk> \<Longrightarrow> y \<in> T"
3.68 +                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)"
3.69 +    by metis+
3.70 +  then have gaugeR: "gauge (\<lambda>x. ball x (R x))"
3.71 +    by (simp add: gauge_def)
3.72 +  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> {}"
3.73 +  proof -
3.74 +    obtain B where B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
3.75 +      using \<open>bounded S\<close> bounded_iff by blast
3.76 +    show ?thesis
3.77 +      apply (rule_tac c = "abs B + 1" in that)
3.78 +      using norm_bound_Basis_le Basis_le_norm
3.79 +       apply (fastforce simp: box_eq_empty mem_box dest!: B intro: order_trans)+
3.80 +      done
3.81 +  qed
3.82 +  obtain \<D> where "countable \<D>"
3.83 +     and Dsub: "\<Union>\<D> \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)"
3.84 +     and cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
3.85 +     and pw:   "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
3.86 +     and Ksub: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> (\<lambda>x. ball x (R x)) x"
3.87 +     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"
3.88 +     and "S \<subseteq> \<Union>\<D>"
3.89 +    using covering_lemma [OF c gaugeR]  by force
3.90 +  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>
3.91 +                cbox u v \<subseteq> ball z (R z)" if "K \<in> \<D>" for K
3.92 +  proof -
3.93 +    obtain u v where "K = cbox u v"
3.94 +      using \<open>K \<in> \<D>\<close> cbox by blast
3.95 +    with that show ?thesis
3.96 +      apply (rule_tac x=u in exI)
3.97 +      apply (rule_tac x=v in exI)
3.98 +      apply (metis Int_iff interior_cbox cbox Ksub)
3.99 +      done
3.100 +  qed
3.101 +  then obtain uf vf zf
3.102 +    where uvz: "\<And>K. K \<in> \<D> \<Longrightarrow>
3.103 +                K = cbox (uf K) (vf K) \<and> box (uf K) (vf K) \<noteq> {} \<and> zf K \<in> S \<and>
3.104 +                zf K \<in> cbox (uf K) (vf K) \<and> cbox (uf K) (vf K) \<subseteq> ball (zf K) (R (zf K))"
3.105 +    by metis
3.106 +  define prj1 where "prj1 \<equiv> \<lambda>x::'M. x \<bullet> (SOME i. i \<in> Basis)"
3.107 +  define fbx where "fbx \<equiv> \<lambda>D. cbox (f(zf D) - (B * DIM('M) * (prj1(vf D - uf D))) *\<^sub>R One::'N)
3.108 +                                    (f(zf D) + (B * DIM('M) * prj1(vf D - uf D)) *\<^sub>R One)"
3.109 +  have vu_pos: "0 < prj1 (vf X - uf X)" if "X \<in> \<D>" for X
3.110 +    using uvz [OF that] by (simp add: prj1_def box_ne_empty SOME_Basis inner_diff_left)
3.111 +  have prj1_idem: "prj1 (vf X - uf X) = (vf X - uf X) \<bullet> i" if  "X \<in> \<D>" "i \<in> Basis" for X i
3.112 +  proof -
3.113 +    have "cbox (uf X) (vf X) \<in> \<D>"
3.114 +      using uvz \<open>X \<in> \<D>\<close> by auto
3.115 +    with exN obtain n where "\<And>i. i \<in> Basis \<Longrightarrow> vf X \<bullet> i - uf X \<bullet> i = (2*c) / 2^n"
3.116 +      by blast
3.117 +    then show ?thesis
3.118 +      by (simp add: \<open>i \<in> Basis\<close> SOME_Basis inner_diff prj1_def)
3.119 +  qed
3.120 +  have countbl: "countable (fbx ` \<D>)"
3.121 +    using \<open>countable \<D>\<close> by blast
3.122 +  have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e / 2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
3.123 +  proof -
3.124 +    have BM_ge0: "0 \<le> B * (DIM('M) * prj1 (vf X - uf X))" if "X \<in> \<D>'" for X
3.125 +      using \<open>0 < B\<close> \<open>\<D>' \<subseteq> \<D>\<close> that vu_pos by fastforce
3.126 +    have "{} \<notin> \<D>'"
3.127 +      using cbox \<open>\<D>' \<subseteq> \<D>\<close> interior_empty by blast
3.128 +    have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> setsum (measure lebesgue o fbx) \<D>'"
3.129 +      by (rule setsum_image_le [OF \<open>finite \<D>'\<close>]) (force simp: fbx_def)
3.130 +    also have "\<dots> \<le> (\<Sum>X\<in>\<D>'. (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X)"
3.131 +    proof (rule setsum_mono)
3.132 +      fix X assume "X \<in> \<D>'"
3.133 +      then have "X \<in> \<D>" using \<open>\<D>' \<subseteq> \<D>\<close> by blast
3.134 +      then have ufvf: "cbox (uf X) (vf X) = X"
3.135 +        using uvz by blast
3.136 +      have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
3.137 +        by (rule setprod_constant [symmetric])
3.138 +      also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
3.139 +        using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: setprod.cong)
3.140 +      finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
3.141 +      have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
3.142 +        using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
3.143 +      moreover have "cbox (uf X) (vf X) \<subseteq> ball (zf X) (1/2)"
3.144 +        by (meson R12 order_trans subset_ball uvz [OF \<open>X \<in> \<D>\<close>])
3.145 +      ultimately have "uf X \<in> ball (zf X) (1/2)"  "vf X \<in> ball (zf X) (1/2)"
3.146 +        by auto
3.147 +      then have "dist (vf X) (uf X) \<le> 1"
3.148 +        unfolding mem_ball
3.149 +        by (metis dist_commute dist_triangle_half_l dual_order.order_iff_strict)
3.150 +      then have 1: "prj1 (vf X - uf X) \<le> 1"
3.151 +        unfolding prj1_def dist_norm using Basis_le_norm SOME_Basis order_trans by fastforce
3.152 +      have 0: "0 \<le> prj1 (vf X - uf X)"
3.153 +        using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
3.154 +      have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
3.155 +        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> setprod_constant)
3.156 +        apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
3.157 +        using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
3.158 +        apply (fastforce simp add: box_ne_empty power_decreasing)
3.159 +        done
3.160 +      also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
3.161 +        by (subst (3) ufvf[symmetric]) simp
3.162 +      finally show "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
3.163 +    qed
3.164 +    also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \<D>'"
3.165 +      by (simp add: setsum_distrib_left)
3.166 +    also have "\<dots> \<le> e / 2"
3.167 +    proof -
3.168 +      have div: "\<D>' division_of \<Union>\<D>'"
3.169 +        apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
3.170 +        using cbox that apply blast
3.171 +        using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
3.172 +        done
3.173 +      have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
3.174 +      proof (rule measure_mono_fmeasurable [OF _ _ \<open>T : lmeasurable\<close>])
3.175 +        show "(\<Union>\<D>') \<in> sets lebesgue"
3.176 +          using div lmeasurable_division by auto
3.177 +        have "\<Union>\<D>' \<subseteq> \<Union>\<D>"
3.178 +          using \<open>\<D>' \<subseteq> \<D>\<close> by blast
3.179 +        also have "... \<subseteq> T"
3.180 +        proof (clarify)
3.181 +          fix x D
3.182 +          assume "x \<in> D" "D \<in> \<D>"
3.183 +          show "x \<in> T"
3.184 +            using Ksub [OF \<open>D \<in> \<D>\<close>]
3.185 +            by (metis \<open>x \<in> D\<close> Int_iff dist_norm mem_ball norm_minus_commute subsetD RT)
3.186 +        qed
3.187 +        finally show "\<Union>\<D>' \<subseteq> T" .
3.188 +      qed
3.189 +      have "setsum (measure lebesgue) \<D>' = setsum content \<D>'"
3.190 +        using  \<open>\<D>' \<subseteq> \<D>\<close> cbox by (force intro: setsum.cong)
3.191 +      then have "(2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \<D>' =
3.192 +                 (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\<Union>\<D>')"
3.193 +        using content_division [OF div] by auto
3.194 +      also have "\<dots> \<le> (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
3.195 +        apply (rule mult_left_mono [OF le_meaT])
3.196 +        using \<open>0 < B\<close>
3.197 +        apply (simp add: algebra_simps)
3.198 +        done
3.199 +      also have "\<dots> \<le> e / 2"
3.200 +        using T \<open>0 < B\<close> by (simp add: field_simps)
3.201 +      finally show ?thesis .
3.202 +    qed
3.203 +    finally show ?thesis .
3.204 +  qed
3.205 +  then have e2: "setsum (measure lebesgue) \<G> \<le> e / 2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
3.206 +    by (metis finite_subset_image that)
3.207 +  show "\<exists>W\<in>lmeasurable. f ` S \<subseteq> W \<and> measure lebesgue W < e"
3.208 +  proof (intro bexI conjI)
3.209 +    have "\<exists>X\<in>\<D>. f y \<in> fbx X" if "y \<in> S" for y
3.210 +    proof -
3.211 +      obtain X where "y \<in> X" "X \<in> \<D>"
3.212 +        using \<open>S \<subseteq> \<Union>\<D>\<close> \<open>y \<in> S\<close> by auto
3.213 +      then have y: "y \<in> ball(zf X) (R(zf X))"
3.214 +        using uvz by fastforce
3.215 +      have conj_le_eq: "z - b \<le> y \<and> y \<le> z + b \<longleftrightarrow> abs(y - z) \<le> b" for z y b::real
3.216 +        by auto
3.217 +      have yin: "y \<in> cbox (uf X) (vf X)" and zin: "(zf X) \<in> cbox (uf X) (vf X)"
3.218 +        using uvz \<open>X \<in> \<D>\<close> \<open>y \<in> X\<close> by auto
3.219 +      have "norm (y - zf X) \<le> (\<Sum>i\<in>Basis. \<bar>(y - zf X) \<bullet> i\<bar>)"
3.220 +        by (rule norm_le_l1)
3.221 +      also have "\<dots> \<le> real DIM('M) * prj1 (vf X - uf X)"
3.222 +      proof (rule setsum_bounded_above)
3.223 +        fix j::'M assume j: "j \<in> Basis"
3.224 +        show "\<bar>(y - zf X) \<bullet> j\<bar> \<le> prj1 (vf X - uf X)"
3.225 +          using yin zin j
3.226 +          by (fastforce simp add: mem_box prj1_idem [OF \<open>X \<in> \<D>\<close> j] inner_diff_left)
3.227 +      qed
3.228 +      finally have nole: "norm (y - zf X) \<le> DIM('M) * prj1 (vf X - uf X)"
3.229 +        by simp
3.230 +      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
3.231 +      proof -
3.232 +        have "\<bar>f y \<bullet> i - f (zf X) \<bullet> i\<bar> = \<bar>(f y - f (zf X)) \<bullet> i\<bar>"
3.233 +          by (simp add: algebra_simps)
3.234 +        also have "\<dots> \<le> norm (f y - f (zf X))"
3.235 +          by (simp add: Basis_le_norm that)
3.236 +        also have "\<dots> \<le> B * norm(y - zf X)"
3.237 +          by (metis uvz RB \<open>X \<in> \<D>\<close> dist_commute dist_norm mem_ball \<open>y \<in> S\<close> y)
3.238 +        also have "\<dots> \<le> B * real DIM('M) * prj1 (vf X - uf X)"
3.239 +          using \<open>0 < B\<close> by (simp add: nole)
3.240 +        finally show ?thesis .
3.241 +      qed
3.242 +      show ?thesis
3.243 +        by (rule_tac x=X in bexI)
3.244 +           (auto simp: fbx_def prj1_idem mem_box conj_le_eq inner_add inner_diff fle \<open>X \<in> \<D>\<close>)
3.245 +    qed
3.246 +    then show "f ` S \<subseteq> (\<Union>D\<in>\<D>. fbx D)" by auto
3.247 +  next
3.248 +    have 1: "\<And>D. D \<in> \<D> \<Longrightarrow> fbx D \<in> lmeasurable"
3.249 +      by (auto simp: fbx_def)
3.250 +    have 2: "I' \<subseteq> \<D> \<Longrightarrow> finite I' \<Longrightarrow> measure lebesgue (\<Union>D\<in>I'. fbx D) \<le> e/2" for I'
3.251 +      by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def)
3.252 +    have 3: "0 \<le> e/2"
3.253 +      using \<open>0<e\<close> by auto
3.254 +    show "(\<Union>D\<in>\<D>. fbx D) \<in> lmeasurable"
3.255 +      by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
3.256 +    have "measure lebesgue (\<Union>D\<in>\<D>. fbx D) \<le> e/2"
3.257 +      by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
3.258 +    then show "measure lebesgue (\<Union>D\<in>\<D>. fbx D) < e"
3.259 +      using \<open>0 < e\<close> by linarith
3.260 +  qed
3.261 +qed
3.262 +
3.263 +proposition negligible_locally_Lipschitz_image:
3.264 +  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
3.265 +  assumes MleN: "DIM('M) \<le> DIM('N)" "negligible S"
3.266 +      and lips: "\<And>x. x \<in> S
3.267 +                      \<Longrightarrow> \<exists>T B. open T \<and> x \<in> T \<and>
3.268 +                              (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
3.269 +    shows "negligible (f ` S)"
3.270 +proof -
3.271 +  let ?S = "\<lambda>n. ({x \<in> S. norm x \<le> n \<and>
3.272 +                          (\<exists>T. open T \<and> x \<in> T \<and>
3.273 +                               (\<forall>y\<in>S \<inter> T. norm (f y - f x) \<le> (real n + 1) * norm (y - x)))})"
3.274 +  have negfn: "f ` ?S n \<in> null_sets lebesgue" for n::nat
3.275 +    unfolding negligible_iff_null_sets[symmetric]
3.276 +    apply (rule_tac B = "real n + 1" in locally_Lipschitz_negl_bounded)
3.277 +    by (auto simp: MleN bounded_iff intro: negligible_subset [OF \<open>negligible S\<close>])
3.278 +  have "S = (\<Union>n. ?S n)"
3.279 +  proof (intro set_eqI iffI)
3.280 +    fix x assume "x \<in> S"
3.281 +    with lips obtain T B where T: "open T" "x \<in> T"
3.282 +                           and B: "\<And>y. y \<in> S \<inter> T \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
3.283 +      by metis+
3.284 +    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
3.285 +    proof -
3.286 +      have "B * norm(y - x) \<le> (nat \<lceil>max B (norm x)\<rceil> + 1) * norm (y - x)"
3.287 +        by (meson max.cobounded1 mult_right_mono nat_ceiling_le_eq nat_le_iff_add norm_ge_zero order_trans)
3.288 +      then show ?thesis
3.289 +        using B order_trans that by blast
3.290 +    qed
3.291 +    have "x \<in> ?S (nat (ceiling (max B (norm x))))"
3.292 +      apply (simp add: \<open>x \<in> S \<close>, rule)
3.293 +      using real_nat_ceiling_ge max.bounded_iff apply blast
3.294 +      using T no
3.295 +      apply (force simp: algebra_simps)
3.296 +      done
3.297 +    then show "x \<in> (\<Union>n. ?S n)" by force
3.298 +  qed auto
3.299 +  then show ?thesis
3.300 +    by (rule ssubst) (auto simp: image_Union negligible_iff_null_sets intro: negfn)
3.301 +qed
3.302 +
3.303 +corollary negligible_differentiable_image_negligible:
3.304 +  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
3.305 +  assumes MleN: "DIM('M) \<le> DIM('N)" "negligible S"
3.306 +      and diff_f: "f differentiable_on S"
3.307 +    shows "negligible (f ` S)"
3.308 +proof -
3.309 +  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))"
3.310 +        if "x \<in> S" for x
3.311 +  proof -
3.312 +    obtain f' where "linear f'"
3.313 +      and f': "\<And>e. e>0 \<Longrightarrow>
3.314 +                  \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
3.315 +                              norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
3.316 +      using diff_f \<open>x \<in> S\<close>
3.317 +      by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
3.318 +    obtain B where "B > 0" and B: "\<forall>x. norm (f' x) \<le> B * norm x"
3.319 +      using linear_bounded_pos \<open>linear f'\<close> by blast
3.320 +    obtain d where "d>0"
3.321 +              and d: "\<And>y. \<lbrakk>y \<in> S; norm (y - x) < d\<rbrakk> \<Longrightarrow>
3.322 +                          norm (f y - f x - f' (y - x)) \<le> norm (y - x)"
3.323 +      using f' [of 1] by (force simp:)
3.324 +    have *: "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
3.325 +              if "y \<in> S" "norm (y - x) < d" for y
3.326 +    proof -
3.327 +      have "norm (f y - f x) -B *  norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
3.328 +        by (simp add: B)
3.329 +      also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
3.330 +        by (rule norm_triangle_ineq2)
3.331 +      also have "... \<le> norm (y - x)"
3.332 +        by (rule d [OF that])
3.333 +      finally show ?thesis
3.334 +        by (simp add: algebra_simps)
3.335 +    qed
3.336 +    show ?thesis
3.337 +      apply (rule_tac x="ball x d" in exI)
3.338 +      apply (rule_tac x="B+1" in exI)
3.339 +      using \<open>d>0\<close>
3.340 +      apply (auto simp: dist_norm norm_minus_commute intro!: *)
3.341 +      done
3.342 +  qed
3.343 +  with negligible_locally_Lipschitz_image assms show ?thesis by metis
3.344 +qed
3.345 +
3.346 +corollary negligible_differentiable_image_lowdim:
3.347 +  fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
3.348 +  assumes MlessN: "DIM('M) < DIM('N)" and diff_f: "f differentiable_on S"
3.349 +    shows "negligible (f ` S)"
3.350 +proof -
3.351 +  have "x \<le> DIM('M) \<Longrightarrow> x \<le> DIM('N)" for x
3.352 +    using MlessN by linarith
3.353 +  obtain lift :: "'M * real \<Rightarrow> 'N" and drop :: "'N \<Rightarrow> 'M * real" and j :: 'N
3.354 +    where "linear lift" "linear drop" and dropl [simp]: "\<And>z. drop (lift z) = z"
3.355 +      and "j \<in> Basis" and j: "\<And>x. lift(x,0) \<bullet> j = 0"
3.356 +    using lowerdim_embeddings [OF MlessN] by metis
3.357 +  have "negligible {x. x\<bullet>j = 0}"
3.358 +    by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
3.359 +  then have neg0S: "negligible ((\<lambda>x. lift (x, 0)) ` S)"
3.360 +    apply (rule negligible_subset)
3.361 +    by (simp add: image_subsetI j)
3.362 +  have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
3.363 +    using diff_f
3.364 +    apply (clarsimp simp add: differentiable_on_def)
3.365 +    apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
3.366 +             linear_imp_differentiable [OF fst_linear])
3.367 +    apply (force simp: image_comp o_def)
3.368 +    done
3.369 +  have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
3.370 +    by (simp add: o_def)
3.371 +  then show ?thesis
3.372 +    apply (rule ssubst)
3.373 +    apply (subst image_comp [symmetric])
3.374 +    apply (metis negligible_differentiable_image_negligible order_refl diff_f' neg0S)
3.375 +    done
3.376 +qed
3.377 +
3.378  lemma set_integral_norm_bound:
3.379    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
3.380    shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
```
```     4.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Sep 30 14:05:51 2016 +0100
4.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Sep 30 11:35:39 2016 +0200
4.3 @@ -8,7 +8,7 @@
4.4  section \<open>Lebesgue measure\<close>
4.5
4.6  theory Lebesgue_Measure
4.7 -  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests
4.8 +  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity
4.9  begin
4.10
4.11  subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
4.12 @@ -986,4 +986,92 @@
4.13    "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"
4.14    using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed)
4.15
4.16 +lemma outer_regular_lborel:
4.17 +  assumes B: "B \<in> fmeasurable lborel" "0 < (e::real)"
4.18 +  shows "\<exists>U. open U \<and> B \<subseteq> U \<and> emeasure lborel U \<le> emeasure lborel B + e"
4.19 +proof -
4.20 +  let ?\<mu> = "emeasure lborel"
4.21 +  let ?B = "\<lambda>n::nat. ball 0 n :: 'a set"
4.22 +  have B[measurable]: "B \<in> sets borel"
4.23 +    using B by auto
4.24 +  let ?e = "\<lambda>n. e*((1/2)^Suc n)"
4.25 +  have "\<forall>n. \<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n"
4.26 +  proof
4.27 +    fix n :: nat
4.28 +    let ?A = "density lborel (indicator (?B n))"
4.29 +    have emeasure_A: "X \<in> sets borel \<Longrightarrow> emeasure ?A X = ?\<mu> (?B n \<inter> X)" for X
4.30 +      by (auto simp add: emeasure_density borel_measurable_indicator indicator_inter_arith[symmetric])
4.31 +
4.32 +    have finite_A: "emeasure ?A (space ?A) \<noteq> \<infinity>"
4.33 +      using emeasure_bounded_finite[of "?B n"] by (auto simp add: emeasure_A)
4.34 +    interpret A: finite_measure ?A
4.35 +      by rule fact
4.36 +    have "emeasure ?A B + ?e n > (INF U:{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
4.37 +      using \<open>0<e\<close> by (auto simp: outer_regular[OF _ finite_A B, symmetric])
4.38 +    then obtain U where U: "B \<subseteq> U" "open U" "?\<mu> (?B n \<inter> B) + ?e n > ?\<mu> (?B n \<inter> U)"
4.39 +      unfolding INF_less_iff by (auto simp: emeasure_A)
4.40 +    moreover
4.41 +    { have "?\<mu> ((?B n \<inter> U) - B) = ?\<mu> ((?B n \<inter> U) - (?B n \<inter> B))"
4.42 +        using U by (intro arg_cong[where f="?\<mu>"]) auto
4.43 +      also have "\<dots> = ?\<mu> (?B n \<inter> U) - ?\<mu> (?B n \<inter> B)"
4.44 +        using U A.emeasure_finite[of B]
4.45 +        by (intro emeasure_Diff) (auto simp del: A.emeasure_finite simp: emeasure_A)
4.46 +      also have "\<dots> < ?e n"
4.47 +        using U(1,2,3) A.emeasure_finite[of B]
4.48 +        by (subst minus_less_iff_ennreal)
4.49 +          (auto simp del: A.emeasure_finite simp: emeasure_A less_top ac_simps intro!: emeasure_mono)
4.50 +      finally have "?\<mu> ((?B n \<inter> U) - B) < ?e n" . }
4.51 +    ultimately show "\<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n"
4.52 +      by (intro exI[of _ "?B n \<inter> U"]) auto
4.53 +  qed
4.54 +  then obtain U
4.55 +    where U: "\<And>n. open (U n)" "\<And>n. ?B n \<inter> B \<subseteq> U n" "\<And>n. ?\<mu> (U n - B) < ?e n"
4.56 +    by metis
4.57 +  then show ?thesis
4.58 +  proof (intro exI conjI)
4.59 +    { fix x assume "x \<in> B"
4.60 +      moreover
4.61 +      have "\<exists>n. norm x < real n"
4.62 +        by (simp add: reals_Archimedean2)
4.63 +      then guess n ..
4.64 +      ultimately have "x \<in> (\<Union>n. U n)"
4.65 +        using U(2)[of n] by auto }
4.66 +    note * = this
4.67 +    then show "open (\<Union>n. U n)" "B \<subseteq> (\<Union>n. U n)"
4.68 +      using U(1,2) by auto
4.69 +    have "?\<mu> (\<Union>n. U n) = ?\<mu> (B \<union> (\<Union>n. U n - B))"
4.70 +      using * U(2) by (intro arg_cong[where ?f="?\<mu>"]) auto
4.71 +    also have "\<dots> = ?\<mu> B + ?\<mu> (\<Union>n. U n - B)"
4.72 +      using U(1) by (intro plus_emeasure[symmetric]) auto
4.73 +    also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ?\<mu> (U n - B))"
4.75 +    also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ennreal (?e n))"
4.76 +      using U(3) by (intro add_mono suminf_le) (auto intro: less_imp_le)
4.77 +    also have "(\<Sum>n. ennreal (?e n)) = ennreal (e * 1)"
4.78 +      using \<open>0<e\<close> by (intro suminf_ennreal_eq sums_mult power_half_series) auto
4.79 +    finally show "emeasure lborel (\<Union>n. U n) \<le> emeasure lborel B + ennreal e"
4.80 +      by simp
4.81 +  qed
4.82 +qed
4.83 +
4.84 +lemma lmeasurable_outer_open:
4.85 +  assumes S: "S \<in> lmeasurable" and "0 < e"
4.86 +  obtains T where "open T" "S \<subseteq> T" "T \<in> lmeasurable" "measure lebesgue T \<le> measure lebesgue S + e"
4.87 +proof -
4.88 +  obtain S' where S': "S \<subseteq> S'" "S' \<in> sets borel" "emeasure lborel S' = emeasure lebesgue S"
4.89 +    using completion_upper[of S lborel] S by auto
4.90 +  then have f_S': "S' \<in> fmeasurable lborel"
4.91 +    using S by (auto simp: fmeasurable_def)
4.92 +  from outer_regular_lborel[OF this \<open>0<e\<close>] guess U .. note U = this
4.93 +  show thesis
4.94 +  proof (rule that)
4.95 +    show "open U" "S \<subseteq> U" "U \<in> lmeasurable"
4.96 +      using f_S' U S' by (auto simp: fmeasurable_def less_top[symmetric] top_unique)
4.97 +    then have "U \<in> fmeasurable lborel"
4.98 +      by (auto simp: fmeasurable_def)
4.99 +    with S U \<open>0<e\<close> show "measure lebesgue U \<le> measure lebesgue S + e"
4.100 +      unfolding S'(3) by (simp add: emeasure_eq_measure2 ennreal_plus[symmetric] del: ennreal_plus)
4.101 +  qed
4.102 +qed
4.103 +
4.104  end
```
```     5.1 --- a/src/HOL/Analysis/Measure_Space.thy	Fri Sep 30 14:05:51 2016 +0100
5.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Sep 30 11:35:39 2016 +0200
5.3 @@ -472,6 +472,10 @@
5.4    "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)"
5.6
5.7 +lemma emeasure_Union:
5.8 +  "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
5.9 +  using plus_emeasure[of A M "B - A"] by auto
5.10 +
5.11  lemma setsum_emeasure:
5.12    "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
5.13      (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
5.14 @@ -1749,6 +1753,42 @@
5.15    "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)"
5.16    using measure_UNION_le[of F "\<lambda>x. x" M] by simp
5.17
5.18 +lemma
5.19 +  assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> fmeasurable M"
5.20 +    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"
5.21 +  shows fmeasurable_UN_bound: "(\<Union>i\<in>I. A i) \<in> fmeasurable M" (is ?fm)
5.22 +    and measure_UN_bound: "measure M (\<Union>i\<in>I. A i) \<le> B" (is ?m)
5.23 +proof -
5.24 +  have "?fm \<and> ?m"
5.25 +  proof cases
5.26 +    assume "I = {}" with \<open>0 \<le> B\<close> show ?thesis by simp
5.27 +  next
5.28 +    assume "I \<noteq> {}"
5.29 +    have "(\<Union>i\<in>I. A i) = (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))"
5.30 +      by (subst range_from_nat_into[symmetric, OF \<open>I \<noteq> {}\<close> \<open>countable I\<close>]) auto
5.31 +    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
5.32 +    also have "\<dots> = (SUP i. emeasure M (\<Union>n\<le>i. A (from_nat_into I n)))"
5.33 +      using I \<open>I \<noteq> {}\<close>[THEN from_nat_into] by (intro SUP_emeasure_incseq[symmetric]) (fastforce simp: incseq_Suc_iff)+
5.34 +    also have "\<dots> \<le> B"
5.35 +    proof (intro SUP_least)
5.36 +      fix i :: nat
5.37 +      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))"
5.38 +        using I \<open>I \<noteq> {}\<close>[THEN from_nat_into] by (intro emeasure_eq_measure2 fmeasurable.finite_UN) auto
5.39 +      also have "\<dots> = measure M (\<Union>n\<in>from_nat_into I ` {..i}. A n)"
5.40 +        by simp
5.41 +      also have "\<dots> \<le> B"
5.42 +        by (intro ennreal_leI bound) (auto intro:  from_nat_into[OF \<open>I \<noteq> {}\<close>])
5.43 +      finally show "emeasure M (\<Union>n\<le>i. A (from_nat_into I n)) \<le> ennreal B" .
5.44 +    qed
5.45 +    finally have *: "emeasure M (\<Union>i\<in>I. A i) \<le> B" .
5.46 +    then have ?fm
5.47 +      using I \<open>countable I\<close> by (intro fmeasurableI conjI) (auto simp: less_top[symmetric] top_unique)
5.48 +    with * \<open>0\<le>B\<close> show ?thesis
5.49 +      by (simp add: emeasure_eq_measure2)
5.50 +  qed
5.51 +  then show ?fm ?m by auto
5.52 +qed
5.53 +
5.54  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
5.55
5.56  locale finite_measure = sigma_finite_measure M for M +
```
```     6.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Sep 30 14:05:51 2016 +0100
6.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 30 11:35:39 2016 +0200
6.3 @@ -2106,6 +2106,50 @@
6.4    apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
6.5    done
6.6
6.7 +lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
6.8 +  unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less)
6.9 +
6.11 +  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
6.12 +  shows "(INF i:I. f i + c :: ereal) = (INF i:I. f i) + c"
6.13 +proof -
6.14 +  have "(INF i:I. f i) \<noteq> -\<infinity>"
6.15 +    unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
6.16 +  then show ?thesis
6.17 +    by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
6.18 +       (auto simp: mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at)
6.19 +qed
6.20 +
6.22 +  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
6.23 +  shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)"
6.25 +
6.27 +  fixes f g :: "'a \<Rightarrow> ereal"
6.28 +  assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
6.29 +  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"
6.30 +  shows "(INF i:I. f i + g i) = (INF i:I. f i) + (INF i:I. g i)"
6.31 +proof cases
6.32 +  assume "I = {}" then show ?thesis
6.33 +    by (simp add: top_ereal_def)
6.34 +next
6.35 +  assume "I \<noteq> {}"
6.36 +  show ?thesis
6.37 +  proof (rule antisym)
6.38 +    show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)"
6.39 +      by (rule INF_greatest; intro ereal_add_mono INF_lower)
6.40 +  next
6.41 +    have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))"
6.42 +      using directed by (intro INF_greatest) (blast intro: INF_lower2)
6.43 +    also have "\<dots> = (INF i:I. f i + (INF i:I. g i))"
6.44 +      using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
6.45 +    also have "\<dots> = (INF i:I. f i) + (INF i:I. g i)"
6.46 +      using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
6.47 +    finally show "(INF i:I. f i + g i) \<le> (INF i:I. f i) + (INF i:I. g i)" .
6.48 +  qed
6.49 +qed
6.50 +