Vitali covering theorem
authorpaulson <lp15@cam.ac.uk>
Tue Apr 17 12:09:23 2018 +0100 (16 months ago)
changeset 679966a9d1b31a7c5
parent 67991 53ab458395a8
child 67997 ae76012879c6
Vitali covering theorem
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Vitali_Covering_Theorem.thy
     1.1 --- a/src/HOL/Analysis/Analysis.thy	Tue Apr 17 10:22:42 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Analysis.thy	Tue Apr 17 12:09:23 2018 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    FPS_Convergence
     1.5    Generalised_Binomial_Theorem
     1.6    Gamma_Function
     1.7 -  Ball_Volume
     1.8 +  Vitali_Covering_Theorem
     1.9    Lipschitz
    1.10  begin
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Tue Apr 17 12:09:23 2018 +0100
     2.3 @@ -0,0 +1,652 @@
     2.4 +theory Vitali_Covering_Theorem
     2.5 +  imports Ball_Volume "HOL-Library.Permutations"
     2.6 +
     2.7 +begin
     2.8 +
     2.9 +lemma stretch_Galois:
    2.10 +  fixes x :: "real^'n"
    2.11 +  shows "(\<And>k. m k \<noteq> 0) \<Longrightarrow> ((y = (\<chi> k. m k * x$k)) \<longleftrightarrow> (\<chi> k. y$k / m k) = x)"
    2.12 +  by auto
    2.13 +
    2.14 +lemma lambda_swap_Galois:
    2.15 +   "(x = (\<chi> i. y $ Fun.swap m n id i) \<longleftrightarrow> (\<chi> i. x $ Fun.swap m n id i) = y)"
    2.16 +  by (auto; simp add: pointfree_idE vec_eq_iff)
    2.17 +
    2.18 +lemma lambda_add_Galois:
    2.19 +  fixes x :: "real^'n"
    2.20 +  shows "m \<noteq> n \<Longrightarrow> (x = (\<chi> i. if i = m then y$m + y$n else y$i) \<longleftrightarrow> (\<chi> i. if i = m then x$m - x$n else x$i) = y)"
    2.21 +  by (safe; simp add: vec_eq_iff)
    2.22 +
    2.23 +
    2.24 +lemma Vitali_covering_lemma_cballs_balls:
    2.25 +  fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
    2.26 +  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
    2.27 +  obtains C where "countable C" "C \<subseteq> K"
    2.28 +     "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
    2.29 +     "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and>
    2.30 +                        \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
    2.31 +                        cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
    2.32 +proof (cases "K = {}")
    2.33 +  case True
    2.34 +  with that show ?thesis
    2.35 +    by auto
    2.36 +next
    2.37 +  case False
    2.38 +  then have "B > 0"
    2.39 +    using assms less_le_trans by auto
    2.40 +  have rgt0[simp]: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i"
    2.41 +    using assms by auto
    2.42 +  let ?djnt = "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j)))"
    2.43 +  have "\<exists>C. \<forall>n. (C n \<subseteq> K \<and>
    2.44 +             (\<forall>i \<in> C n. B/2 ^ n \<le> r i) \<and> ?djnt (C n) \<and>
    2.45 +             (\<forall>i \<in> K. B/2 ^ n < r i
    2.46 +                 \<longrightarrow> (\<exists>j. j \<in> C n \<and>
    2.47 +                         \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
    2.48 +                         cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)))) \<and> (C n \<subseteq> C(Suc n))"
    2.49 +  proof (rule dependent_nat_choice, safe)
    2.50 +    fix C n
    2.51 +    define D where "D \<equiv> {i \<in> K. B/2 ^ Suc n < r i \<and> (\<forall>j\<in>C. disjnt (cball(a i)(r i)) (cball (a j) (r j)))}"
    2.52 +    let ?cover_ar = "\<lambda>i j. \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
    2.53 +                             cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
    2.54 +    assume "C \<subseteq> K"
    2.55 +      and Ble: "\<forall>i\<in>C. B/2 ^ n \<le> r i"
    2.56 +      and djntC: "?djnt C"
    2.57 +      and cov_n: "\<forall>i\<in>K. B/2 ^ n < r i \<longrightarrow> (\<exists>j. j \<in> C \<and> ?cover_ar i j)"
    2.58 +    have *: "\<forall>C\<in>chains {C. C \<subseteq> D \<and> ?djnt C}. \<Union>C \<in> {C. C \<subseteq> D \<and> ?djnt C}"
    2.59 +    proof (clarsimp simp: chains_def)
    2.60 +      fix C
    2.61 +      assume C: "C \<subseteq> {C. C \<subseteq> D \<and> ?djnt C}" and "chain\<^sub>\<subseteq> C"
    2.62 +      show "\<Union>C \<subseteq> D \<and> ?djnt (\<Union>C)"
    2.63 +        unfolding pairwise_def
    2.64 +      proof (intro ballI conjI impI)
    2.65 +        show "\<Union>C \<subseteq> D"
    2.66 +          using C by blast
    2.67 +      next
    2.68 +        fix x y
    2.69 +        assume "x \<in> \<Union>C" and "y \<in> \<Union>C" and "x \<noteq> y"
    2.70 +        then obtain X Y where XY: "x \<in> X" "X \<in> C" "y \<in> Y" "Y \<in> C"
    2.71 +          by blast
    2.72 +        then consider "X \<subseteq> Y" | "Y \<subseteq> X"
    2.73 +          by (meson \<open>chain\<^sub>\<subseteq> C\<close> chain_subset_def)
    2.74 +        then show "disjnt (cball (a x) (r x)) (cball (a y) (r y))"
    2.75 +        proof cases
    2.76 +          case 1
    2.77 +          with C XY \<open>x \<noteq> y\<close> show ?thesis
    2.78 +            unfolding pairwise_def by blast
    2.79 +        next
    2.80 +          case 2
    2.81 +          with C XY \<open>x \<noteq> y\<close> show ?thesis
    2.82 +            unfolding pairwise_def by blast
    2.83 +        qed
    2.84 +      qed
    2.85 +    qed
    2.86 +    obtain E where "E \<subseteq> D" and djntE: "?djnt E" and maximalE: "\<And>X. \<lbrakk>X \<subseteq> D; ?djnt X; E \<subseteq> X\<rbrakk> \<Longrightarrow> X = E"
    2.87 +      using Zorn_Lemma [OF *] by safe blast
    2.88 +    show "\<exists>L. (L \<subseteq> K \<and>
    2.89 +               (\<forall>i\<in>L. B/2 ^ Suc n \<le> r i) \<and> ?djnt L \<and>
    2.90 +               (\<forall>i\<in>K. B/2 ^ Suc n < r i \<longrightarrow> (\<exists>j. j \<in> L \<and> ?cover_ar i j))) \<and> C \<subseteq> L"
    2.91 +    proof (intro exI conjI ballI)
    2.92 +      show "C \<union> E \<subseteq> K"
    2.93 +        using D_def \<open>C \<subseteq> K\<close> \<open>E \<subseteq> D\<close> by blast
    2.94 +      show "B/2 ^ Suc n \<le> r i" if i: "i \<in> C \<union> E" for i
    2.95 +        using i
    2.96 +      proof
    2.97 +        assume "i \<in> C"
    2.98 +        have "B/2 ^ Suc n \<le> B/2 ^ n"
    2.99 +          using \<open>B > 0\<close> by (simp add: divide_simps)
   2.100 +        also have "\<dots> \<le> r i"
   2.101 +          using Ble \<open>i \<in> C\<close> by blast
   2.102 +        finally show ?thesis .
   2.103 +      qed (use D_def \<open>E \<subseteq> D\<close> in auto)
   2.104 +      show "?djnt (C \<union> E)"
   2.105 +        using D_def \<open>C \<subseteq> K\<close> \<open>E \<subseteq> D\<close> djntC djntE
   2.106 +        unfolding pairwise_def disjnt_def by blast
   2.107 +    next
   2.108 +      fix i
   2.109 +      assume "i \<in> K"
   2.110 +      show "B/2 ^ Suc n < r i \<longrightarrow> (\<exists>j. j \<in> C \<union> E \<and> ?cover_ar i j)"
   2.111 +      proof (cases "r i \<le> B/2^n")
   2.112 +        case False
   2.113 +        then show ?thesis
   2.114 +          using cov_n \<open>i \<in> K\<close> by auto
   2.115 +      next
   2.116 +        case True
   2.117 +        have "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.118 +          if less: "B/2 ^ Suc n < r i" and j: "j \<in> C \<union> E"
   2.119 +            and nondis: "\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j))" for j
   2.120 +        proof -
   2.121 +          obtain x where x: "dist (a i) x \<le> r i" "dist (a j) x \<le> r j"
   2.122 +            using nondis by (force simp: disjnt_def)
   2.123 +          have "dist (a i) (a j) \<le> dist (a i) x + dist x (a j)"
   2.124 +            by (simp add: dist_triangle)
   2.125 +          also have "\<dots> \<le> r i + r j"
   2.126 +            by (metis add_mono_thms_linordered_semiring(1) dist_commute x)
   2.127 +          finally have aij: "dist (a i) (a j) + r i < 5 * r j" if "r i < 2 * r j"
   2.128 +            using that by auto
   2.129 +          show ?thesis
   2.130 +            using j
   2.131 +          proof
   2.132 +            assume "j \<in> C"
   2.133 +            have "B/2^n < 2 * r j"
   2.134 +              using Ble True \<open>j \<in> C\<close> less by auto
   2.135 +            with aij True show "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.136 +              by (simp add: cball_subset_ball_iff)
   2.137 +          next
   2.138 +            assume "j \<in> E"
   2.139 +            then have "B/2 ^ n < 2 * r j"
   2.140 +              using D_def \<open>E \<subseteq> D\<close> by auto
   2.141 +            with True have "r i < 2 * r j"
   2.142 +              by auto
   2.143 +            with aij show "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.144 +              by (simp add: cball_subset_ball_iff)
   2.145 +          qed
   2.146 +        qed
   2.147 +      moreover have "\<exists>j. j \<in> C \<union> E \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j))"
   2.148 +        if "B/2 ^ Suc n < r i"
   2.149 +      proof (rule classical)
   2.150 +        assume NON: "\<not> ?thesis"
   2.151 +        show ?thesis
   2.152 +        proof (cases "i \<in> D")
   2.153 +          case True
   2.154 +          have "insert i E = E"
   2.155 +          proof (rule maximalE)
   2.156 +            show "insert i E \<subseteq> D"
   2.157 +              by (simp add: True \<open>E \<subseteq> D\<close>)
   2.158 +            show "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) (insert i E)"
   2.159 +              using False NON by (auto simp: pairwise_insert djntE disjnt_sym)
   2.160 +          qed auto
   2.161 +          then show ?thesis
   2.162 +            using \<open>i \<in> K\<close> assms by fastforce
   2.163 +        next
   2.164 +          case False
   2.165 +          with that show ?thesis
   2.166 +            by (auto simp: D_def disjnt_def \<open>i \<in> K\<close>)
   2.167 +        qed
   2.168 +      qed
   2.169 +      ultimately
   2.170 +      show "B/2 ^ Suc n < r i \<longrightarrow>
   2.171 +            (\<exists>j. j \<in> C \<union> E \<and>
   2.172 +                 \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
   2.173 +                 cball (a i) (r i) \<subseteq> ball (a j) (5 * r j))"
   2.174 +        by blast
   2.175 +      qed
   2.176 +    qed auto
   2.177 +  qed (use assms in force)
   2.178 +  then obtain F where FK: "\<And>n. F n \<subseteq> K"
   2.179 +               and Fle: "\<And>n i. i \<in> F n \<Longrightarrow> B/2 ^ n \<le> r i"
   2.180 +               and Fdjnt:  "\<And>n. ?djnt (F n)"
   2.181 +               and FF:  "\<And>n i. \<lbrakk>i \<in> K; B/2 ^ n < r i\<rbrakk>
   2.182 +                        \<Longrightarrow> \<exists>j. j \<in> F n \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
   2.183 +                                cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.184 +               and inc:  "\<And>n. F n \<subseteq> F(Suc n)"
   2.185 +    by (force simp: all_conj_distrib)
   2.186 +  show thesis
   2.187 +  proof
   2.188 +    have *: "countable I"
   2.189 +      if "I \<subseteq> K" and pw: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) I" for I
   2.190 +    proof -
   2.191 +      show ?thesis
   2.192 +      proof (rule countable_image_inj_on [of "\<lambda>i. cball(a i)(r i)"])
   2.193 +        show "countable ((\<lambda>i. cball (a i) (r i)) ` I)"
   2.194 +        proof (rule countable_disjoint_nonempty_interior_subsets)
   2.195 +          show "disjoint ((\<lambda>i. cball (a i) (r i)) ` I)"
   2.196 +            by (auto simp: dest: pairwiseD [OF pw] intro: pairwise_imageI)
   2.197 +          show "\<And>S. \<lbrakk>S \<in> (\<lambda>i. cball (a i) (r i)) ` I; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
   2.198 +            using \<open>I \<subseteq> K\<close>
   2.199 +            by (auto simp: not_less [symmetric])
   2.200 +        qed
   2.201 +      next
   2.202 +        have "\<And>x y. \<lbrakk>x \<in> I; y \<in> I; a x = a y; r x = r y\<rbrakk> \<Longrightarrow> x = y"
   2.203 +          using pw \<open>I \<subseteq> K\<close> assms
   2.204 +          apply (clarsimp simp: pairwise_def disjnt_def)
   2.205 +          by (metis assms centre_in_cball subsetD empty_iff inf.idem less_eq_real_def)
   2.206 +        then show "inj_on (\<lambda>i. cball (a i) (r i)) I"
   2.207 +          using \<open>I \<subseteq> K\<close> by (fastforce simp: inj_on_def cball_eq_cball_iff dest: assms)
   2.208 +      qed
   2.209 +    qed
   2.210 +    show "(Union(range F)) \<subseteq> K"
   2.211 +      using FK by blast
   2.212 +    moreover show "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) (Union(range F))"
   2.213 +    proof (rule pairwise_chain_Union)
   2.214 +      show "chain\<^sub>\<subseteq> (range F)"
   2.215 +        unfolding chain_subset_def by clarify (meson inc lift_Suc_mono_le linear subsetCE)
   2.216 +    qed (use Fdjnt in blast)
   2.217 +    ultimately show "countable (Union(range F))"
   2.218 +      by (blast intro: *)
   2.219 +  next
   2.220 +    fix i assume "i \<in> K"
   2.221 +    then obtain n where "(1/2) ^ n < r i / B"
   2.222 +      using  \<open>B > 0\<close> assms real_arch_pow_inv by fastforce
   2.223 +    then have B2: "B/2 ^ n < r i"
   2.224 +      using \<open>B > 0\<close> by (simp add: divide_simps)
   2.225 +    have "0 < r i" "r i \<le> B"
   2.226 +      by (auto simp: \<open>i \<in> K\<close> assms)
   2.227 +    show "\<exists>j. j \<in> (Union(range F)) \<and>
   2.228 +          \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
   2.229 +          cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.230 +      using FF [OF \<open>i \<in> K\<close> B2] by auto
   2.231 +  qed
   2.232 +qed
   2.233 +
   2.234 +subsection\<open>Vitali covering theorem\<close>
   2.235 +
   2.236 +lemma Vitali_covering_lemma_cballs:
   2.237 +  fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
   2.238 +  assumes S: "S \<subseteq> (\<Union>i\<in>K. cball (a i) (r i))"
   2.239 +      and r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
   2.240 +  obtains C where "countable C" "C \<subseteq> K"
   2.241 +     "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
   2.242 +     "S \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
   2.243 +proof -
   2.244 +  obtain C where C: "countable C" "C \<subseteq> K"
   2.245 +                    "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
   2.246 +           and cov: "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
   2.247 +                        cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.248 +    by (rule Vitali_covering_lemma_cballs_balls [OF r, where a=a]) (blast intro: that)+
   2.249 +  show ?thesis
   2.250 +  proof
   2.251 +    have "(\<Union>i\<in>K. cball (a i) (r i)) \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
   2.252 +      using cov subset_iff by fastforce
   2.253 +    with S show "S \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
   2.254 +      by blast
   2.255 +  qed (use C in auto)
   2.256 +qed
   2.257 +
   2.258 +lemma Vitali_covering_lemma_balls:
   2.259 +  fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
   2.260 +  assumes S: "S \<subseteq> (\<Union>i\<in>K. ball (a i) (r i))"
   2.261 +      and r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
   2.262 +  obtains C where "countable C" "C \<subseteq> K"
   2.263 +     "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
   2.264 +     "S \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
   2.265 +proof -
   2.266 +  obtain C where C: "countable C" "C \<subseteq> K"
   2.267 +           and pw:  "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
   2.268 +           and cov: "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
   2.269 +                        cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.270 +    by (rule Vitali_covering_lemma_cballs_balls [OF r, where a=a]) (blast intro: that)+
   2.271 +  show ?thesis
   2.272 +  proof
   2.273 +    have "(\<Union>i\<in>K. ball (a i) (r i)) \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
   2.274 +      using cov subset_iff
   2.275 +      by clarsimp (meson less_imp_le mem_ball mem_cball subset_eq)
   2.276 +    with S show "S \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
   2.277 +      by blast
   2.278 +    show "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
   2.279 +      using pw
   2.280 +      by (clarsimp simp: pairwise_def) (meson ball_subset_cball disjnt_subset1 disjnt_subset2)
   2.281 +  qed (use C in auto)
   2.282 +qed
   2.283 +
   2.284 +
   2.285 +proposition Vitali_covering_theorem_cballs:
   2.286 +  fixes a :: "'a \<Rightarrow> 'n::euclidean_space"
   2.287 +  assumes r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i"
   2.288 +      and S: "\<And>x d. \<lbrakk>x \<in> S; 0 < d\<rbrakk>
   2.289 +                     \<Longrightarrow> \<exists>i. i \<in> K \<and> x \<in> cball (a i) (r i) \<and> r i < d"
   2.290 +  obtains C where "countable C" "C \<subseteq> K"
   2.291 +     "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
   2.292 +     "negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
   2.293 +proof -
   2.294 +  let ?\<mu> = "measure lebesgue"
   2.295 +  have *: "\<exists>C. countable C \<and> C \<subseteq> K \<and>
   2.296 +            pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C \<and>
   2.297 +            negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
   2.298 +    if r01: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> 1"
   2.299 +       and Sd: "\<And>x d. \<lbrakk>x \<in> S; 0 < d\<rbrakk> \<Longrightarrow> \<exists>i. i \<in> K \<and> x \<in> cball (a i) (r i) \<and> r i < d"
   2.300 +     for K r and a :: "'a \<Rightarrow> 'n"
   2.301 +  proof -
   2.302 +    obtain C where C: "countable C" "C \<subseteq> K"
   2.303 +      and pwC: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
   2.304 +      and cov: "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
   2.305 +                        cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.306 +      by (rule Vitali_covering_lemma_cballs_balls [of K r 1 a]) (auto simp: r01)
   2.307 +    have ar_injective: "\<And>x y. \<lbrakk>x \<in> C; y \<in> C; a x = a y; r x = r y\<rbrakk> \<Longrightarrow> x = y"
   2.308 +      using \<open>C \<subseteq> K\<close> pwC cov
   2.309 +      by (force simp: pairwise_def disjnt_def)
   2.310 +    show ?thesis
   2.311 +    proof (intro exI conjI)
   2.312 +      show "negligible (S - (\<Union>i\<in>C. cball (a i) (r i)))"
   2.313 +      proof (clarsimp simp: negligible_on_intervals [of "S-T" for T])
   2.314 +        fix l u
   2.315 +        show "negligible ((S - (\<Union>i\<in>C. cball (a i) (r i))) \<inter> cbox l u)"
   2.316 +          unfolding negligible_outer_le
   2.317 +        proof (intro allI impI)
   2.318 +          fix e::real
   2.319 +          assume "e > 0"
   2.320 +          define D where "D \<equiv> {i \<in> C. \<not> disjnt (ball(a i) (5 * r i)) (cbox l u)}"
   2.321 +          then have "D \<subseteq> C"
   2.322 +            by auto
   2.323 +          have "countable D"
   2.324 +            unfolding D_def using \<open>countable C\<close> by simp
   2.325 +          have UD: "(\<Union>i\<in>D. cball (a i) (r i)) \<in> lmeasurable"
   2.326 +          proof (rule fmeasurableI2)
   2.327 +            show "cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One) \<in> lmeasurable"
   2.328 +              by blast
   2.329 +            have "y \<in> cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One)"
   2.330 +              if "i \<in> C" and x: "x \<in> cbox l u" and ai: "dist (a i) y \<le> r i" "dist (a i) x < 5 * r i"
   2.331 +              for i x y
   2.332 +            proof -
   2.333 +              have d6: "dist y x < 6 * r i"
   2.334 +                using dist_triangle3 [of y x "a i"] that by linarith
   2.335 +              show ?thesis
   2.336 +              proof (clarsimp simp: mem_box algebra_simps)
   2.337 +                fix j::'n
   2.338 +                assume j: "j \<in> Basis"
   2.339 +                then have xyj: "\<bar>x \<bullet> j - y \<bullet> j\<bar> \<le> dist y x"
   2.340 +                  by (metis Basis_le_norm dist_commute dist_norm inner_diff_left)
   2.341 +                have "l \<bullet> j \<le> x \<bullet> j"
   2.342 +                  using \<open>j \<in> Basis\<close> mem_box \<open>x \<in> cbox l u\<close> by blast
   2.343 +                also have "\<dots> \<le> y \<bullet> j + 6 * r i"
   2.344 +                  using d6 xyj by (auto simp: algebra_simps)
   2.345 +                also have "\<dots> \<le> y \<bullet> j + 6"
   2.346 +                  using r01 [of i] \<open>C \<subseteq> K\<close> \<open>i \<in> C\<close> by auto
   2.347 +                finally have l: "l \<bullet> j \<le> y \<bullet> j + 6" .
   2.348 +                have "y \<bullet> j \<le> x \<bullet> j + 6 * r i"
   2.349 +                  using d6 xyj by (auto simp: algebra_simps)
   2.350 +                also have "\<dots> \<le> u \<bullet> j + 6 * r i"
   2.351 +                  using j  x by (auto simp: mem_box)
   2.352 +                also have "\<dots> \<le> u \<bullet> j + 6"
   2.353 +                  using r01 [of i] \<open>C \<subseteq> K\<close> \<open>i \<in> C\<close> by auto
   2.354 +                finally have u: "y \<bullet> j \<le> u \<bullet> j + 6" .
   2.355 +                show "l \<bullet> j \<le> y \<bullet> j + 6 \<and> y \<bullet> j \<le> u \<bullet> j + 6"
   2.356 +                  using l u by blast
   2.357 +              qed
   2.358 +            qed
   2.359 +            then show "(\<Union>i\<in>D. cball (a i) (r i)) \<subseteq> cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One)"
   2.360 +              by (force simp: D_def disjnt_def)
   2.361 +            show "(\<Union>i\<in>D. cball (a i) (r i)) \<in> sets lebesgue"
   2.362 +              using \<open>countable D\<close> by auto
   2.363 +          qed
   2.364 +          obtain D1 where "D1 \<subseteq> D" "finite D1"
   2.365 +            and measD1: "?\<mu> (\<Union>i\<in>D. cball (a i) (r i)) - e / 5 ^ DIM('n) < ?\<mu> (\<Union>i\<in>D1. cball (a i) (r i))"
   2.366 +          proof (rule measure_countable_Union_approachable [where e = "e / 5 ^ (DIM('n))"])
   2.367 +            show "countable ((\<lambda>i. cball (a i) (r i)) ` D)"
   2.368 +              using \<open>countable D\<close> by auto
   2.369 +            show "\<And>d. d \<in> (\<lambda>i. cball (a i) (r i)) ` D \<Longrightarrow> d \<in> lmeasurable"
   2.370 +              by auto
   2.371 +            show "\<And>D'. \<lbrakk>D' \<subseteq> (\<lambda>i. cball (a i) (r i)) ` D; finite D'\<rbrakk> \<Longrightarrow> ?\<mu> (\<Union>D') \<le> ?\<mu> (\<Union>i\<in>D. cball (a i) (r i))"
   2.372 +              by (fastforce simp add: intro!: measure_mono_fmeasurable UD)
   2.373 +          qed (use \<open>e > 0\<close> in \<open>auto dest: finite_subset_image\<close>)
   2.374 +          show "\<exists>T. (S - (\<Union>i\<in>C. cball (a i) (r i))) \<inter>
   2.375 +                    cbox l u \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
   2.376 +          proof (intro exI conjI)
   2.377 +            show "(S - (\<Union>i\<in>C. cball (a i) (r i))) \<inter> cbox l u \<subseteq> (\<Union>i\<in>D - D1. ball (a i) (5 * r i))"
   2.378 +            proof clarify
   2.379 +              fix x
   2.380 +              assume x: "x \<in> cbox l u" "x \<in> S" "x \<notin> (\<Union>i\<in>C. cball (a i) (r i))"
   2.381 +              have "closed (\<Union>i\<in>D1. cball (a i) (r i))"
   2.382 +                using \<open>finite D1\<close> by blast
   2.383 +              moreover have "x \<notin> (\<Union>j\<in>D1. cball (a j) (r j))"
   2.384 +                using x \<open>D1 \<subseteq> D\<close> unfolding D_def by blast
   2.385 +              ultimately obtain q where "q > 0" and q: "ball x q \<subseteq> - (\<Union>i\<in>D1. cball (a i) (r i))"
   2.386 +                by (metis (no_types, lifting) ComplI open_contains_ball closed_def)
   2.387 +              obtain i where "i \<in> K" and xi: "x \<in> cball (a i) (r i)" and ri: "r i < q/2"
   2.388 +                using Sd [OF \<open>x \<in> S\<close>] \<open>q > 0\<close> half_gt_zero by blast
   2.389 +              then obtain j where "j \<in> C"
   2.390 +                             and nondisj: "\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j))"
   2.391 +                             and sub5j:  "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
   2.392 +                using cov [OF \<open>i \<in> K\<close>] by metis
   2.393 +              show "x \<in> (\<Union>i\<in>D - D1. ball (a i) (5 * r i))"
   2.394 +              proof
   2.395 +                show "j \<in> D - D1"
   2.396 +                proof
   2.397 +                  show "j \<in> D"
   2.398 +                    using \<open>j \<in> C\<close> sub5j \<open>x \<in> cbox l u\<close> xi by (auto simp: D_def disjnt_def)
   2.399 +                  obtain y where yi: "dist (a i) y \<le> r i" and yj: "dist (a j) y \<le> r j"
   2.400 +                    using disjnt_def nondisj by fastforce
   2.401 +                  have "dist x y \<le> r i + r i"
   2.402 +                    by (metis add_mono dist_commute dist_triangle_le mem_cball xi yi)
   2.403 +                  also have "\<dots> < q"
   2.404 +                    using ri by linarith
   2.405 +                  finally have "y \<in> ball x q"
   2.406 +                    by simp
   2.407 +                  with yj q show "j \<notin> D1"
   2.408 +                    by (auto simp: disjoint_UN_iff)
   2.409 +                qed
   2.410 +                show "x \<in> ball (a j) (5 * r j)"
   2.411 +                  using xi sub5j by blast
   2.412 +              qed
   2.413 +            qed
   2.414 +            have 3: "?\<mu> (\<Union>i\<in>D2. ball (a i) (5 * r i)) \<le> e"
   2.415 +              if D2: "D2 \<subseteq> D - D1" and "finite D2" for D2
   2.416 +            proof -
   2.417 +              have rgt0: "0 < r i" if "i \<in> D2" for i
   2.418 +                using \<open>C \<subseteq> K\<close> D_def \<open>i \<in> D2\<close> D2 r01
   2.419 +                by (simp add: subset_iff)
   2.420 +              then have inj: "inj_on (\<lambda>i. ball (a i) (5 * r i)) D2"
   2.421 +                using \<open>C \<subseteq> K\<close> D2 by (fastforce simp: inj_on_def D_def ball_eq_ball_iff intro: ar_injective)
   2.422 +              have "?\<mu> (\<Union>i\<in>D2. ball (a i) (5 * r i)) \<le> sum (?\<mu>) ((\<lambda>i. ball (a i) (5 * r i)) ` D2)"
   2.423 +                using that by (force intro: measure_Union_le)
   2.424 +              also have "\<dots>  = (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (5 * r i)))"
   2.425 +                by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
   2.426 +              also have "\<dots> = (\<Sum>i\<in>D2. 5 ^ DIM('n) * ?\<mu> (ball (a i) (r i)))"
   2.427 +              proof (rule sum.cong [OF refl])
   2.428 +                fix i
   2.429 +                assume "i \<in> D2"
   2.430 +                show "?\<mu> (ball (a i) (5 * r i)) = 5 ^ DIM('n) * ?\<mu> (ball (a i) (r i))"
   2.431 +                  using rgt0 [OF \<open>i \<in> D2\<close>] by (simp add: content_ball)
   2.432 +              qed
   2.433 +              also have "\<dots> = (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) * 5 ^ DIM('n)"
   2.434 +                by (simp add: sum_distrib_left mult.commute)
   2.435 +              finally have "?\<mu> (\<Union>i\<in>D2. ball (a i) (5 * r i)) \<le> (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) * 5 ^ DIM('n)" .
   2.436 +              moreover have "(\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) \<le> e / 5 ^ DIM('n)"
   2.437 +              proof -
   2.438 +                have D12_dis: "((\<Union>x\<in>D1. cball (a x) (r x)) \<inter> (\<Union>x\<in>D2. cball (a x) (r x))) \<le> {}"
   2.439 +                proof clarify
   2.440 +                  fix w d1 d2
   2.441 +                  assume "d1 \<in> D1" "w d1 d2 \<in> cball (a d1) (r d1)" "d2 \<in> D2" "w d1 d2 \<in> cball (a d2) (r d2)"
   2.442 +                  then show "w d1 d2 \<in> {}"
   2.443 +                    by (metis DiffE disjnt_iff subsetCE D2 \<open>D1 \<subseteq> D\<close> \<open>D \<subseteq> C\<close> pairwiseD [OF pwC, of d1 d2])
   2.444 +                qed
   2.445 +                have inj: "inj_on (\<lambda>i. cball (a i) (r i)) D2"
   2.446 +                  using rgt0 D2 \<open>D \<subseteq> C\<close> by (force simp: inj_on_def cball_eq_cball_iff intro!: ar_injective)
   2.447 +                have ds: "disjoint ((\<lambda>i. cball (a i) (r i)) ` D2)"
   2.448 +                  using D2 \<open>D \<subseteq> C\<close> by (auto intro: pairwiseI pairwiseD [OF pwC])
   2.449 +                have "(\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) = (\<Sum>i\<in>D2. ?\<mu> (cball (a i) (r i)))"
   2.450 +                  using rgt0 by (simp add: content_ball content_cball less_eq_real_def)
   2.451 +                also have "\<dots> = sum ?\<mu> ((\<lambda>i. cball (a i) (r i)) ` D2)"
   2.452 +                  by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
   2.453 +                also have "\<dots> = ?\<mu> (\<Union>i\<in>D2. cball (a i) (r i))"
   2.454 +                  by (auto intro: measure_Union' [symmetric] ds simp add: \<open>finite D2\<close>)
   2.455 +                finally have "?\<mu> (\<Union>i\<in>D1. cball (a i) (r i)) + (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) =
   2.456 +                              ?\<mu> (\<Union>i\<in>D1. cball (a i) (r i)) + ?\<mu> (\<Union>i\<in>D2. cball (a i) (r i))"
   2.457 +                  by simp
   2.458 +                also have "\<dots> = ?\<mu> (\<Union>i \<in> D1 \<union> D2. cball (a i) (r i))"
   2.459 +                  using D12_dis by (simp add: measure_Un3 \<open>finite D1\<close> \<open>finite D2\<close> fmeasurable.finite_UN)
   2.460 +                also have "\<dots> \<le> ?\<mu> (\<Union>i\<in>D. cball (a i) (r i))"
   2.461 +                  using D2 \<open>D1 \<subseteq> D\<close> by (fastforce intro!: measure_mono_fmeasurable [OF _ _ UD] \<open>finite D1\<close> \<open>finite D2\<close>)
   2.462 +                finally have "?\<mu> (\<Union>i\<in>D1. cball (a i) (r i)) + (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) \<le> ?\<mu> (\<Union>i\<in>D. cball (a i) (r i))" .
   2.463 +                with measD1 show ?thesis
   2.464 +                  by simp
   2.465 +              qed
   2.466 +                ultimately show ?thesis
   2.467 +                  by (simp add: divide_simps)
   2.468 +            qed
   2.469 +            have co: "countable (D - D1)"
   2.470 +              by (simp add: \<open>countable D\<close>)
   2.471 +            show "(\<Union>i\<in>D - D1. ball (a i) (5 * r i)) \<in> lmeasurable"
   2.472 +              using \<open>e > 0\<close> by (auto simp: fmeasurable_UN_bound [OF co _ 3])
   2.473 +            show "?\<mu> (\<Union>i\<in>D - D1. ball (a i) (5 * r i)) \<le> e"
   2.474 +              using \<open>e > 0\<close> by (auto simp: measure_UN_bound [OF co _ 3])
   2.475 +          qed
   2.476 +        qed
   2.477 +      qed
   2.478 +    qed (use C pwC in auto)
   2.479 +  qed
   2.480 +  define K' where "K' \<equiv> {i \<in> K. r i \<le> 1}"
   2.481 +  have 1: "\<And>i. i \<in> K' \<Longrightarrow> 0 < r i \<and> r i \<le> 1"
   2.482 +    using K'_def r by auto
   2.483 +  have 2: "\<exists>i. i \<in> K' \<and> x \<in> cball (a i) (r i) \<and> r i < d"
   2.484 +    if "x \<in> S \<and> 0 < d" for x d
   2.485 +    using that by (auto simp: K'_def dest!: S [where d = "min d 1"])
   2.486 +  have "K' \<subseteq> K"
   2.487 +    using K'_def by auto
   2.488 +  then show thesis
   2.489 +    using * [OF 1 2] that by fastforce
   2.490 +qed
   2.491 +
   2.492 +
   2.493 +proposition Vitali_covering_theorem_balls:
   2.494 +  fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
   2.495 +  assumes S: "\<And>x d. \<lbrakk>x \<in> S; 0 < d\<rbrakk> \<Longrightarrow> \<exists>i. i \<in> K \<and> x \<in> ball (a i) (r i) \<and> r i < d"
   2.496 +  obtains C where "countable C" "C \<subseteq> K"
   2.497 +     "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
   2.498 +     "negligible(S - (\<Union>i \<in> C. ball (a i) (r i)))"
   2.499 +proof -
   2.500 +  have 1: "\<exists>i. i \<in> {i \<in> K. 0 < r i} \<and> x \<in> cball (a i) (r i) \<and> r i < d"
   2.501 +         if xd: "x \<in> S" "d > 0" for x d
   2.502 +    by (metis (mono_tags, lifting) assms ball_eq_empty less_eq_real_def mem_Collect_eq mem_ball mem_cball not_le xd(1) xd(2))
   2.503 +  obtain C where C: "countable C" "C \<subseteq> K"
   2.504 +             and pw: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
   2.505 +             and neg: "negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
   2.506 +    by (rule Vitali_covering_theorem_cballs [of "{i \<in> K. 0 < r i}" r S a, OF _ 1]) auto
   2.507 +  show thesis
   2.508 +  proof
   2.509 +    show "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
   2.510 +      apply (rule pairwise_mono [OF pw])
   2.511 +      apply (auto simp: disjnt_def)
   2.512 +      by (meson disjoint_iff_not_equal less_imp_le mem_cball)
   2.513 +    have "negligible (\<Union>i\<in>C. sphere (a i) (r i))"
   2.514 +      by (auto intro: negligible_sphere \<open>countable C\<close>)
   2.515 +    then have "negligible (S - (\<Union>i \<in> C. cball(a i)(r i)) \<union> (\<Union>i \<in> C. sphere (a i) (r i)))"
   2.516 +      by (rule negligible_Un [OF neg])
   2.517 +    then show "negligible (S - (\<Union>i\<in>C. ball (a i) (r i)))"
   2.518 +      by (rule negligible_subset) force
   2.519 +  qed (use C in auto)
   2.520 +qed
   2.521 +
   2.522 +
   2.523 +lemma negligible_eq_zero_density_alt:
   2.524 +     "negligible S \<longleftrightarrow>
   2.525 +      (\<forall>x \<in> S. \<forall>e > 0.
   2.526 +        \<exists>d U. 0 < d \<and> d \<le> e \<and> S \<inter> ball x d \<subseteq> U \<and>
   2.527 +              U \<in> lmeasurable \<and> measure lebesgue U < e * measure lebesgue (ball x d))"
   2.528 +     (is "_ = (\<forall>x \<in> S. \<forall>e > 0. ?Q x e)")
   2.529 +proof (intro iffI ballI allI impI)
   2.530 +  fix x and e :: real
   2.531 +  assume "negligible S" and "x \<in> S" and "e > 0"
   2.532 +  then
   2.533 +  show "\<exists>d U. 0 < d \<and> d \<le> e \<and> S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and>
   2.534 +              measure lebesgue U < e * measure lebesgue (ball x d)"
   2.535 +    apply (rule_tac x=e in exI)
   2.536 +    apply (rule_tac x="S \<inter> ball x e" in exI)
   2.537 +    apply (auto simp: negligible_imp_measurable negligible_Int negligible_imp_measure0 zero_less_measure_iff)
   2.538 +    done
   2.539 +next
   2.540 +  assume R [rule_format]: "\<forall>x \<in> S. \<forall>e > 0. ?Q x e"
   2.541 +  let ?\<mu> = "measure lebesgue"
   2.542 +  have "\<exists>U. openin (subtopology euclidean S) U \<and> z \<in> U \<and> negligible U"
   2.543 +    if "z \<in> S" for z
   2.544 +  proof (intro exI conjI)
   2.545 +    show "openin (subtopology euclidean S) (S \<inter> ball z 1)"
   2.546 +      by (simp add: openin_open_Int)
   2.547 +    show "z \<in> S \<inter> ball z 1"
   2.548 +      using \<open>z \<in> S\<close> by auto
   2.549 +    show "negligible (S \<inter> ball z 1)"
   2.550 +    proof (clarsimp simp: negligible_outer_le)
   2.551 +      fix e :: "real"
   2.552 +      assume "e > 0"
   2.553 +      let ?K = "{(x,d). x \<in> S \<and> 0 < d \<and> ball x d \<subseteq> ball z 1 \<and>
   2.554 +                     (\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and>
   2.555 +                         ?\<mu> U < e / ?\<mu> (ball z 1) * ?\<mu> (ball x d))}"
   2.556 +      obtain C where "countable C" and Csub: "C \<subseteq> ?K"
   2.557 +        and pwC: "pairwise (\<lambda>i j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C"
   2.558 +        and negC: "negligible((S \<inter> ball z 1) - (\<Union>i \<in> C. ball (fst i) (snd i)))"
   2.559 +      proof (rule Vitali_covering_theorem_balls [of "S \<inter> ball z 1" ?K fst snd])
   2.560 +        fix x and d :: "real"
   2.561 +        assume x: "x \<in> S \<inter> ball z 1" and "d > 0"
   2.562 +        obtain k where "k > 0" and k: "ball x k \<subseteq> ball z 1"
   2.563 +          by (meson Int_iff open_ball openE x)
   2.564 +        let ?\<epsilon> = "min (e / ?\<mu> (ball z 1) / 2) (min (d / 2) k)"
   2.565 +        obtain r U where r: "r > 0" "r \<le> ?\<epsilon>" and U: "S \<inter> ball x r \<subseteq> U" "U \<in> lmeasurable"
   2.566 +          and mU: "?\<mu> U < ?\<epsilon> * ?\<mu> (ball x r)"
   2.567 +          using R [of x ?\<epsilon>] \<open>d > 0\<close> \<open>e > 0\<close> \<open>k > 0\<close> x by auto
   2.568 +        show "\<exists>i. i \<in> ?K \<and> x \<in> ball (fst i) (snd i) \<and> snd i < d"
   2.569 +        proof (rule exI [of _ "(x,r)"], simp, intro conjI exI)
   2.570 +          have "ball x r \<subseteq> ball x k"
   2.571 +            using r by (simp add: ball_subset_ball_iff)
   2.572 +          also have "\<dots> \<subseteq> ball z 1"
   2.573 +            using ball_subset_ball_iff k by auto
   2.574 +          finally show "ball x r \<subseteq> ball z 1" .
   2.575 +          have "?\<epsilon> * ?\<mu> (ball x r) \<le> e * content (ball x r) / content (ball z 1)"
   2.576 +            using r \<open>e > 0\<close> by (simp add: ord_class.min_def divide_simps)
   2.577 +          with mU show "?\<mu> U < e * content (ball x r) / content (ball z 1)"
   2.578 +            by auto
   2.579 +        qed (use r U x in auto)
   2.580 +      qed
   2.581 +      have "\<exists>U. case p of (x,d) \<Rightarrow> S \<inter> ball x d \<subseteq> U \<and>
   2.582 +                        U \<in> lmeasurable \<and> ?\<mu> U < e / ?\<mu> (ball z 1) * ?\<mu> (ball x d)"
   2.583 +        if "p \<in> C" for p
   2.584 +        using that Csub by auto
   2.585 +      then obtain U where U:
   2.586 +                "\<And>p. p \<in> C \<Longrightarrow>
   2.587 +                       case p of (x,d) \<Rightarrow> S \<inter> ball x d \<subseteq> U p \<and>
   2.588 +                        U p \<in> lmeasurable \<and> ?\<mu> (U p) < e / ?\<mu> (ball z 1) * ?\<mu> (ball x d)"
   2.589 +        by (rule that [OF someI_ex])
   2.590 +      let ?T = "((S \<inter> ball z 1) - (\<Union>(x,d)\<in>C. ball x d)) \<union> \<Union>(U ` C)"
   2.591 +      show "\<exists>T. S \<inter> ball z 1 \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
   2.592 +      proof (intro exI conjI)
   2.593 +        show "S \<inter> ball z 1 \<subseteq> ?T"
   2.594 +          using U by fastforce
   2.595 +        { have Um: "U i \<in> lmeasurable" if "i \<in> C" for i
   2.596 +            using that U by blast
   2.597 +          have lee: "?\<mu> (\<Union>i\<in>I. U i) \<le> e" if "I \<subseteq> C" "finite I" for I
   2.598 +          proof -
   2.599 +            have "?\<mu> (\<Union>(x,d)\<in>I. ball x d) \<le> ?\<mu> (ball z 1)"
   2.600 +              apply (rule measure_mono_fmeasurable)
   2.601 +              using \<open>I \<subseteq> C\<close> \<open>finite I\<close> Csub by (force simp: prod.case_eq_if sets.finite_UN)+
   2.602 +            then have le1: "(?\<mu> (\<Union>(x,d)\<in>I. ball x d) / ?\<mu> (ball z 1)) \<le> 1"
   2.603 +              by simp
   2.604 +            have "?\<mu> (\<Union>i\<in>I. U i) \<le> (\<Sum>i\<in>I. ?\<mu> (U i))"
   2.605 +              using that U by (blast intro: measure_UNION_le)
   2.606 +            also have "\<dots> \<le> (\<Sum>(x,r)\<in>I. e / ?\<mu> (ball z 1) * ?\<mu> (ball x r))"
   2.607 +              by (rule sum_mono) (use \<open>I \<subseteq> C\<close> U in force)
   2.608 +            also have "\<dots> = (e / ?\<mu> (ball z 1)) * (\<Sum>(x,r)\<in>I. ?\<mu> (ball x r))"
   2.609 +              by (simp add: case_prod_app prod.case_distrib sum_distrib_left)
   2.610 +            also have "\<dots> = e * (?\<mu> (\<Union>(x,r)\<in>I. ball x r) / ?\<mu> (ball z 1))"
   2.611 +              apply (subst measure_UNION')
   2.612 +              using that pwC by (auto simp: case_prod_unfold elim: pairwise_mono)
   2.613 +            also have "\<dots> \<le> e"
   2.614 +              by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \<open>e > 0\<close> le1)
   2.615 +            finally show ?thesis .
   2.616 +          qed
   2.617 +          have "UNION C U \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
   2.618 +            using \<open>e > 0\<close> Um lee
   2.619 +            by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>])
   2.620 +        }
   2.621 +        moreover have "?\<mu> ?T = ?\<mu> (UNION C U)"
   2.622 +        proof (rule measure_negligible_symdiff [OF \<open>UNION C U \<in> lmeasurable\<close>])
   2.623 +          show "negligible((UNION C U - ?T) \<union> (?T - UNION C U))"
   2.624 +            by (force intro!: negligible_subset [OF negC])
   2.625 +        qed
   2.626 +        ultimately show "?T \<in> lmeasurable"  "?\<mu> ?T \<le> e"
   2.627 +          by (simp_all add: fmeasurable.Un negC negligible_imp_measurable split_def)
   2.628 +      qed
   2.629 +    qed
   2.630 +  qed
   2.631 +  with locally_negligible_alt show "negligible S"
   2.632 +    by metis
   2.633 +qed
   2.634 +
   2.635 +
   2.636 +proposition negligible_eq_zero_density:
   2.637 +   "negligible S \<longleftrightarrow>
   2.638 +    (\<forall>x\<in>S. \<forall>r>0. \<forall>e>0. \<exists>d. 0 < d \<and> d \<le> r \<and>
   2.639 +                   (\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and> measure lebesgue U < e * measure lebesgue (ball x d)))"
   2.640 +proof -
   2.641 +  let ?Q = "\<lambda>x d e. \<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and> measure lebesgue U < e * content (ball x d)"
   2.642 +  have "(\<forall>e>0. \<exists>d>0. d \<le> e \<and> ?Q x d e) = (\<forall>r>0. \<forall>e>0. \<exists>d>0. d \<le> r \<and> ?Q x d e)"
   2.643 +    if "x \<in> S" for x
   2.644 +  proof (intro iffI allI impI)
   2.645 +    fix r :: "real" and e :: "real"
   2.646 +    assume L [rule_format]: "\<forall>e>0. \<exists>d>0. d \<le> e \<and> ?Q x d e" and "r > 0" "e > 0"
   2.647 +    show "\<exists>d>0. d \<le> r \<and> ?Q x d e"
   2.648 +      using L [of "min r e"] apply (rule ex_forward)
   2.649 +      using \<open>r > 0\<close> \<open>e > 0\<close>  by (auto intro: less_le_trans elim!: ex_forward)
   2.650 +  qed auto
   2.651 +  then show ?thesis
   2.652 +    by (force simp: negligible_eq_zero_density_alt)
   2.653 +qed
   2.654 +
   2.655 +end