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)
authorhoelzl
Fri Sep 30 11:35:39 2016 +0200 (2016-09-30)
changeset 639684359400adfe7
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)
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Complete_Measure.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Library/Extended_Real.thy
     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.74 +      using U(1) by (intro add_mono emeasure_subadditive_countably) auto
    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.5    using additiveD[OF emeasure_additive] ..
     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.10 +lemma INF_ereal_add_left:
    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.21 +lemma INF_ereal_add_right:
    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.24 +  using INF_ereal_add_left[OF assms] by (simp add: ac_simps)
    6.25 +
    6.26 +lemma INF_ereal_add_directed:
    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 +
    6.51  lemma INF_ereal_add:
    6.52    fixes f :: "nat \<Rightarrow> ereal"
    6.53    assumes "decseq f" "decseq g"