src/HOL/Analysis/Vitali_Covering_Theorem.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:      HOL/Analysis/Vitali_Covering_Theorem.thy
```
```     2     Authors:    LC Paulson, based on material from HOL Light
```
```     3 *)
```
```     4
```
```     5 section  \<open>Vitali Covering Theorem and an Application to Negligibility\<close>
```
```     6
```
```     7 theory Vitali_Covering_Theorem
```
```     8   imports Ball_Volume "HOL-Library.Permutations"
```
```     9
```
```    10 begin
```
```    11
```
```    12 lemma stretch_Galois:
```
```    13   fixes x :: "real^'n"
```
```    14   shows "(\<And>k. m k \<noteq> 0) \<Longrightarrow> ((y = (\<chi> k. m k * x\$k)) \<longleftrightarrow> (\<chi> k. y\$k / m k) = x)"
```
```    15   by auto
```
```    16
```
```    17 lemma lambda_swap_Galois:
```
```    18    "(x = (\<chi> i. y \$ Fun.swap m n id i) \<longleftrightarrow> (\<chi> i. x \$ Fun.swap m n id i) = y)"
```
```    19   by (auto; simp add: pointfree_idE vec_eq_iff)
```
```    20
```
```    21 lemma lambda_add_Galois:
```
```    22   fixes x :: "real^'n"
```
```    23   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)"
```
```    24   by (safe; simp add: vec_eq_iff)
```
```    25
```
```    26
```
```    27 lemma Vitali_covering_lemma_cballs_balls:
```
```    28   fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
```
```    29   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
```
```    30   obtains C where "countable C" "C \<subseteq> K"
```
```    31      "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```    32      "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and>
```
```    33                         \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
```
```    34                         cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```    35 proof (cases "K = {}")
```
```    36   case True
```
```    37   with that show ?thesis
```
```    38     by auto
```
```    39 next
```
```    40   case False
```
```    41   then have "B > 0"
```
```    42     using assms less_le_trans by auto
```
```    43   have rgt0[simp]: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i"
```
```    44     using assms by auto
```
```    45   let ?djnt = "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j)))"
```
```    46   have "\<exists>C. \<forall>n. (C n \<subseteq> K \<and>
```
```    47              (\<forall>i \<in> C n. B/2 ^ n \<le> r i) \<and> ?djnt (C n) \<and>
```
```    48              (\<forall>i \<in> K. B/2 ^ n < r i
```
```    49                  \<longrightarrow> (\<exists>j. j \<in> C n \<and>
```
```    50                          \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
```
```    51                          cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)))) \<and> (C n \<subseteq> C(Suc n))"
```
```    52   proof (rule dependent_nat_choice, safe)
```
```    53     fix C n
```
```    54     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)))}"
```
```    55     let ?cover_ar = "\<lambda>i j. \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
```
```    56                              cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```    57     assume "C \<subseteq> K"
```
```    58       and Ble: "\<forall>i\<in>C. B/2 ^ n \<le> r i"
```
```    59       and djntC: "?djnt C"
```
```    60       and cov_n: "\<forall>i\<in>K. B/2 ^ n < r i \<longrightarrow> (\<exists>j. j \<in> C \<and> ?cover_ar i j)"
```
```    61     have *: "\<forall>C\<in>chains {C. C \<subseteq> D \<and> ?djnt C}. \<Union>C \<in> {C. C \<subseteq> D \<and> ?djnt C}"
```
```    62     proof (clarsimp simp: chains_def)
```
```    63       fix C
```
```    64       assume C: "C \<subseteq> {C. C \<subseteq> D \<and> ?djnt C}" and "chain\<^sub>\<subseteq> C"
```
```    65       show "\<Union>C \<subseteq> D \<and> ?djnt (\<Union>C)"
```
```    66         unfolding pairwise_def
```
```    67       proof (intro ballI conjI impI)
```
```    68         show "\<Union>C \<subseteq> D"
```
```    69           using C by blast
```
```    70       next
```
```    71         fix x y
```
```    72         assume "x \<in> \<Union>C" and "y \<in> \<Union>C" and "x \<noteq> y"
```
```    73         then obtain X Y where XY: "x \<in> X" "X \<in> C" "y \<in> Y" "Y \<in> C"
```
```    74           by blast
```
```    75         then consider "X \<subseteq> Y" | "Y \<subseteq> X"
```
```    76           by (meson \<open>chain\<^sub>\<subseteq> C\<close> chain_subset_def)
```
```    77         then show "disjnt (cball (a x) (r x)) (cball (a y) (r y))"
```
```    78         proof cases
```
```    79           case 1
```
```    80           with C XY \<open>x \<noteq> y\<close> show ?thesis
```
```    81             unfolding pairwise_def by blast
```
```    82         next
```
```    83           case 2
```
```    84           with C XY \<open>x \<noteq> y\<close> show ?thesis
```
```    85             unfolding pairwise_def by blast
```
```    86         qed
```
```    87       qed
```
```    88     qed
```
```    89     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"
```
```    90       using Zorn_Lemma [OF *] by safe blast
```
```    91     show "\<exists>L. (L \<subseteq> K \<and>
```
```    92                (\<forall>i\<in>L. B/2 ^ Suc n \<le> r i) \<and> ?djnt L \<and>
```
```    93                (\<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"
```
```    94     proof (intro exI conjI ballI)
```
```    95       show "C \<union> E \<subseteq> K"
```
```    96         using D_def \<open>C \<subseteq> K\<close> \<open>E \<subseteq> D\<close> by blast
```
```    97       show "B/2 ^ Suc n \<le> r i" if i: "i \<in> C \<union> E" for i
```
```    98         using i
```
```    99       proof
```
```   100         assume "i \<in> C"
```
```   101         have "B/2 ^ Suc n \<le> B/2 ^ n"
```
```   102           using \<open>B > 0\<close> by (simp add: divide_simps)
```
```   103         also have "\<dots> \<le> r i"
```
```   104           using Ble \<open>i \<in> C\<close> by blast
```
```   105         finally show ?thesis .
```
```   106       qed (use D_def \<open>E \<subseteq> D\<close> in auto)
```
```   107       show "?djnt (C \<union> E)"
```
```   108         using D_def \<open>C \<subseteq> K\<close> \<open>E \<subseteq> D\<close> djntC djntE
```
```   109         unfolding pairwise_def disjnt_def by blast
```
```   110     next
```
```   111       fix i
```
```   112       assume "i \<in> K"
```
```   113       show "B/2 ^ Suc n < r i \<longrightarrow> (\<exists>j. j \<in> C \<union> E \<and> ?cover_ar i j)"
```
```   114       proof (cases "r i \<le> B/2^n")
```
```   115         case False
```
```   116         then show ?thesis
```
```   117           using cov_n \<open>i \<in> K\<close> by auto
```
```   118       next
```
```   119         case True
```
```   120         have "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   121           if less: "B/2 ^ Suc n < r i" and j: "j \<in> C \<union> E"
```
```   122             and nondis: "\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j))" for j
```
```   123         proof -
```
```   124           obtain x where x: "dist (a i) x \<le> r i" "dist (a j) x \<le> r j"
```
```   125             using nondis by (force simp: disjnt_def)
```
```   126           have "dist (a i) (a j) \<le> dist (a i) x + dist x (a j)"
```
```   127             by (simp add: dist_triangle)
```
```   128           also have "\<dots> \<le> r i + r j"
```
```   129             by (metis add_mono_thms_linordered_semiring(1) dist_commute x)
```
```   130           finally have aij: "dist (a i) (a j) + r i < 5 * r j" if "r i < 2 * r j"
```
```   131             using that by auto
```
```   132           show ?thesis
```
```   133             using j
```
```   134           proof
```
```   135             assume "j \<in> C"
```
```   136             have "B/2^n < 2 * r j"
```
```   137               using Ble True \<open>j \<in> C\<close> less by auto
```
```   138             with aij True show "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   139               by (simp add: cball_subset_ball_iff)
```
```   140           next
```
```   141             assume "j \<in> E"
```
```   142             then have "B/2 ^ n < 2 * r j"
```
```   143               using D_def \<open>E \<subseteq> D\<close> by auto
```
```   144             with True have "r i < 2 * r j"
```
```   145               by auto
```
```   146             with aij show "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   147               by (simp add: cball_subset_ball_iff)
```
```   148           qed
```
```   149         qed
```
```   150       moreover have "\<exists>j. j \<in> C \<union> E \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j))"
```
```   151         if "B/2 ^ Suc n < r i"
```
```   152       proof (rule classical)
```
```   153         assume NON: "\<not> ?thesis"
```
```   154         show ?thesis
```
```   155         proof (cases "i \<in> D")
```
```   156           case True
```
```   157           have "insert i E = E"
```
```   158           proof (rule maximalE)
```
```   159             show "insert i E \<subseteq> D"
```
```   160               by (simp add: True \<open>E \<subseteq> D\<close>)
```
```   161             show "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) (insert i E)"
```
```   162               using False NON by (auto simp: pairwise_insert djntE disjnt_sym)
```
```   163           qed auto
```
```   164           then show ?thesis
```
```   165             using \<open>i \<in> K\<close> assms by fastforce
```
```   166         next
```
```   167           case False
```
```   168           with that show ?thesis
```
```   169             by (auto simp: D_def disjnt_def \<open>i \<in> K\<close>)
```
```   170         qed
```
```   171       qed
```
```   172       ultimately
```
```   173       show "B/2 ^ Suc n < r i \<longrightarrow>
```
```   174             (\<exists>j. j \<in> C \<union> E \<and>
```
```   175                  \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
```
```   176                  cball (a i) (r i) \<subseteq> ball (a j) (5 * r j))"
```
```   177         by blast
```
```   178       qed
```
```   179     qed auto
```
```   180   qed (use assms in force)
```
```   181   then obtain F where FK: "\<And>n. F n \<subseteq> K"
```
```   182                and Fle: "\<And>n i. i \<in> F n \<Longrightarrow> B/2 ^ n \<le> r i"
```
```   183                and Fdjnt:  "\<And>n. ?djnt (F n)"
```
```   184                and FF:  "\<And>n i. \<lbrakk>i \<in> K; B/2 ^ n < r i\<rbrakk>
```
```   185                         \<Longrightarrow> \<exists>j. j \<in> F n \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
```
```   186                                 cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   187                and inc:  "\<And>n. F n \<subseteq> F(Suc n)"
```
```   188     by (force simp: all_conj_distrib)
```
```   189   show thesis
```
```   190   proof
```
```   191     have *: "countable I"
```
```   192       if "I \<subseteq> K" and pw: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) I" for I
```
```   193     proof -
```
```   194       show ?thesis
```
```   195       proof (rule countable_image_inj_on [of "\<lambda>i. cball(a i)(r i)"])
```
```   196         show "countable ((\<lambda>i. cball (a i) (r i)) ` I)"
```
```   197         proof (rule countable_disjoint_nonempty_interior_subsets)
```
```   198           show "disjoint ((\<lambda>i. cball (a i) (r i)) ` I)"
```
```   199             by (auto simp: dest: pairwiseD [OF pw] intro: pairwise_imageI)
```
```   200           show "\<And>S. \<lbrakk>S \<in> (\<lambda>i. cball (a i) (r i)) ` I; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
```
```   201             using \<open>I \<subseteq> K\<close>
```
```   202             by (auto simp: not_less [symmetric])
```
```   203         qed
```
```   204       next
```
```   205         have "\<And>x y. \<lbrakk>x \<in> I; y \<in> I; a x = a y; r x = r y\<rbrakk> \<Longrightarrow> x = y"
```
```   206           using pw \<open>I \<subseteq> K\<close> assms
```
```   207           apply (clarsimp simp: pairwise_def disjnt_def)
```
```   208           by (metis assms centre_in_cball subsetD empty_iff inf.idem less_eq_real_def)
```
```   209         then show "inj_on (\<lambda>i. cball (a i) (r i)) I"
```
```   210           using \<open>I \<subseteq> K\<close> by (fastforce simp: inj_on_def cball_eq_cball_iff dest: assms)
```
```   211       qed
```
```   212     qed
```
```   213     show "(Union(range F)) \<subseteq> K"
```
```   214       using FK by blast
```
```   215     moreover show "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) (Union(range F))"
```
```   216     proof (rule pairwise_chain_Union)
```
```   217       show "chain\<^sub>\<subseteq> (range F)"
```
```   218         unfolding chain_subset_def by clarify (meson inc lift_Suc_mono_le linear subsetCE)
```
```   219     qed (use Fdjnt in blast)
```
```   220     ultimately show "countable (Union(range F))"
```
```   221       by (blast intro: *)
```
```   222   next
```
```   223     fix i assume "i \<in> K"
```
```   224     then obtain n where "(1/2) ^ n < r i / B"
```
```   225       using  \<open>B > 0\<close> assms real_arch_pow_inv by fastforce
```
```   226     then have B2: "B/2 ^ n < r i"
```
```   227       using \<open>B > 0\<close> by (simp add: divide_simps)
```
```   228     have "0 < r i" "r i \<le> B"
```
```   229       by (auto simp: \<open>i \<in> K\<close> assms)
```
```   230     show "\<exists>j. j \<in> (Union(range F)) \<and>
```
```   231           \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
```
```   232           cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   233       using FF [OF \<open>i \<in> K\<close> B2] by auto
```
```   234   qed
```
```   235 qed
```
```   236
```
```   237 subsection\<open>Vitali covering theorem\<close>
```
```   238
```
```   239 lemma Vitali_covering_lemma_cballs:
```
```   240   fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
```
```   241   assumes S: "S \<subseteq> (\<Union>i\<in>K. cball (a i) (r i))"
```
```   242       and r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
```
```   243   obtains C where "countable C" "C \<subseteq> K"
```
```   244      "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```   245      "S \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
```
```   246 proof -
```
```   247   obtain C where C: "countable C" "C \<subseteq> K"
```
```   248                     "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```   249            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>
```
```   250                         cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   251     by (rule Vitali_covering_lemma_cballs_balls [OF r, where a=a]) (blast intro: that)+
```
```   252   show ?thesis
```
```   253   proof
```
```   254     have "(\<Union>i\<in>K. cball (a i) (r i)) \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
```
```   255       using cov subset_iff by fastforce
```
```   256     with S show "S \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
```
```   257       by blast
```
```   258   qed (use C in auto)
```
```   259 qed
```
```   260
```
```   261 lemma Vitali_covering_lemma_balls:
```
```   262   fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
```
```   263   assumes S: "S \<subseteq> (\<Union>i\<in>K. ball (a i) (r i))"
```
```   264       and r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
```
```   265   obtains C where "countable C" "C \<subseteq> K"
```
```   266      "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
```
```   267      "S \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
```
```   268 proof -
```
```   269   obtain C where C: "countable C" "C \<subseteq> K"
```
```   270            and pw:  "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```   271            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>
```
```   272                         cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   273     by (rule Vitali_covering_lemma_cballs_balls [OF r, where a=a]) (blast intro: that)+
```
```   274   show ?thesis
```
```   275   proof
```
```   276     have "(\<Union>i\<in>K. ball (a i) (r i)) \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
```
```   277       using cov subset_iff
```
```   278       by clarsimp (meson less_imp_le mem_ball mem_cball subset_eq)
```
```   279     with S show "S \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
```
```   280       by blast
```
```   281     show "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
```
```   282       using pw
```
```   283       by (clarsimp simp: pairwise_def) (meson ball_subset_cball disjnt_subset1 disjnt_subset2)
```
```   284   qed (use C in auto)
```
```   285 qed
```
```   286
```
```   287
```
```   288 theorem Vitali_covering_theorem_cballs:
```
```   289   fixes a :: "'a \<Rightarrow> 'n::euclidean_space"
```
```   290   assumes r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i"
```
```   291       and S: "\<And>x d. \<lbrakk>x \<in> S; 0 < d\<rbrakk>
```
```   292                      \<Longrightarrow> \<exists>i. i \<in> K \<and> x \<in> cball (a i) (r i) \<and> r i < d"
```
```   293   obtains C where "countable C" "C \<subseteq> K"
```
```   294      "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```   295      "negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
```
```   296 proof -
```
```   297   let ?\<mu> = "measure lebesgue"
```
```   298   have *: "\<exists>C. countable C \<and> C \<subseteq> K \<and>
```
```   299             pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C \<and>
```
```   300             negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
```
```   301     if r01: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> 1"
```
```   302        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"
```
```   303      for K r and a :: "'a \<Rightarrow> 'n"
```
```   304   proof -
```
```   305     obtain C where C: "countable C" "C \<subseteq> K"
```
```   306       and pwC: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```   307       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>
```
```   308                         cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   309       by (rule Vitali_covering_lemma_cballs_balls [of K r 1 a]) (auto simp: r01)
```
```   310     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"
```
```   311       using \<open>C \<subseteq> K\<close> pwC cov
```
```   312       by (force simp: pairwise_def disjnt_def)
```
```   313     show ?thesis
```
```   314     proof (intro exI conjI)
```
```   315       show "negligible (S - (\<Union>i\<in>C. cball (a i) (r i)))"
```
```   316       proof (clarsimp simp: negligible_on_intervals [of "S-T" for T])
```
```   317         fix l u
```
```   318         show "negligible ((S - (\<Union>i\<in>C. cball (a i) (r i))) \<inter> cbox l u)"
```
```   319           unfolding negligible_outer_le
```
```   320         proof (intro allI impI)
```
```   321           fix e::real
```
```   322           assume "e > 0"
```
```   323           define D where "D \<equiv> {i \<in> C. \<not> disjnt (ball(a i) (5 * r i)) (cbox l u)}"
```
```   324           then have "D \<subseteq> C"
```
```   325             by auto
```
```   326           have "countable D"
```
```   327             unfolding D_def using \<open>countable C\<close> by simp
```
```   328           have UD: "(\<Union>i\<in>D. cball (a i) (r i)) \<in> lmeasurable"
```
```   329           proof (rule fmeasurableI2)
```
```   330             show "cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One) \<in> lmeasurable"
```
```   331               by blast
```
```   332             have "y \<in> cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One)"
```
```   333               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"
```
```   334               for i x y
```
```   335             proof -
```
```   336               have d6: "dist y x < 6 * r i"
```
```   337                 using dist_triangle3 [of y x "a i"] that by linarith
```
```   338               show ?thesis
```
```   339               proof (clarsimp simp: mem_box algebra_simps)
```
```   340                 fix j::'n
```
```   341                 assume j: "j \<in> Basis"
```
```   342                 then have xyj: "\<bar>x \<bullet> j - y \<bullet> j\<bar> \<le> dist y x"
```
```   343                   by (metis Basis_le_norm dist_commute dist_norm inner_diff_left)
```
```   344                 have "l \<bullet> j \<le> x \<bullet> j"
```
```   345                   using \<open>j \<in> Basis\<close> mem_box \<open>x \<in> cbox l u\<close> by blast
```
```   346                 also have "\<dots> \<le> y \<bullet> j + 6 * r i"
```
```   347                   using d6 xyj by (auto simp: algebra_simps)
```
```   348                 also have "\<dots> \<le> y \<bullet> j + 6"
```
```   349                   using r01 [of i] \<open>C \<subseteq> K\<close> \<open>i \<in> C\<close> by auto
```
```   350                 finally have l: "l \<bullet> j \<le> y \<bullet> j + 6" .
```
```   351                 have "y \<bullet> j \<le> x \<bullet> j + 6 * r i"
```
```   352                   using d6 xyj by (auto simp: algebra_simps)
```
```   353                 also have "\<dots> \<le> u \<bullet> j + 6 * r i"
```
```   354                   using j  x by (auto simp: mem_box)
```
```   355                 also have "\<dots> \<le> u \<bullet> j + 6"
```
```   356                   using r01 [of i] \<open>C \<subseteq> K\<close> \<open>i \<in> C\<close> by auto
```
```   357                 finally have u: "y \<bullet> j \<le> u \<bullet> j + 6" .
```
```   358                 show "l \<bullet> j \<le> y \<bullet> j + 6 \<and> y \<bullet> j \<le> u \<bullet> j + 6"
```
```   359                   using l u by blast
```
```   360               qed
```
```   361             qed
```
```   362             then show "(\<Union>i\<in>D. cball (a i) (r i)) \<subseteq> cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One)"
```
```   363               by (force simp: D_def disjnt_def)
```
```   364             show "(\<Union>i\<in>D. cball (a i) (r i)) \<in> sets lebesgue"
```
```   365               using \<open>countable D\<close> by auto
```
```   366           qed
```
```   367           obtain D1 where "D1 \<subseteq> D" "finite D1"
```
```   368             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))"
```
```   369           proof (rule measure_countable_Union_approachable [where e = "e / 5 ^ (DIM('n))"])
```
```   370             show "countable ((\<lambda>i. cball (a i) (r i)) ` D)"
```
```   371               using \<open>countable D\<close> by auto
```
```   372             show "\<And>d. d \<in> (\<lambda>i. cball (a i) (r i)) ` D \<Longrightarrow> d \<in> lmeasurable"
```
```   373               by auto
```
```   374             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))"
```
```   375               by (fastforce simp add: intro!: measure_mono_fmeasurable UD)
```
```   376           qed (use \<open>e > 0\<close> in \<open>auto dest: finite_subset_image\<close>)
```
```   377           show "\<exists>T. (S - (\<Union>i\<in>C. cball (a i) (r i))) \<inter>
```
```   378                     cbox l u \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
```
```   379           proof (intro exI conjI)
```
```   380             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))"
```
```   381             proof clarify
```
```   382               fix x
```
```   383               assume x: "x \<in> cbox l u" "x \<in> S" "x \<notin> (\<Union>i\<in>C. cball (a i) (r i))"
```
```   384               have "closed (\<Union>i\<in>D1. cball (a i) (r i))"
```
```   385                 using \<open>finite D1\<close> by blast
```
```   386               moreover have "x \<notin> (\<Union>j\<in>D1. cball (a j) (r j))"
```
```   387                 using x \<open>D1 \<subseteq> D\<close> unfolding D_def by blast
```
```   388               ultimately obtain q where "q > 0" and q: "ball x q \<subseteq> - (\<Union>i\<in>D1. cball (a i) (r i))"
```
```   389                 by (metis (no_types, lifting) ComplI open_contains_ball closed_def)
```
```   390               obtain i where "i \<in> K" and xi: "x \<in> cball (a i) (r i)" and ri: "r i < q/2"
```
```   391                 using Sd [OF \<open>x \<in> S\<close>] \<open>q > 0\<close> half_gt_zero by blast
```
```   392               then obtain j where "j \<in> C"
```
```   393                              and nondisj: "\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j))"
```
```   394                              and sub5j:  "cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
```
```   395                 using cov [OF \<open>i \<in> K\<close>] by metis
```
```   396               show "x \<in> (\<Union>i\<in>D - D1. ball (a i) (5 * r i))"
```
```   397               proof
```
```   398                 show "j \<in> D - D1"
```
```   399                 proof
```
```   400                   show "j \<in> D"
```
```   401                     using \<open>j \<in> C\<close> sub5j \<open>x \<in> cbox l u\<close> xi by (auto simp: D_def disjnt_def)
```
```   402                   obtain y where yi: "dist (a i) y \<le> r i" and yj: "dist (a j) y \<le> r j"
```
```   403                     using disjnt_def nondisj by fastforce
```
```   404                   have "dist x y \<le> r i + r i"
```
```   405                     by (metis add_mono dist_commute dist_triangle_le mem_cball xi yi)
```
```   406                   also have "\<dots> < q"
```
```   407                     using ri by linarith
```
```   408                   finally have "y \<in> ball x q"
```
```   409                     by simp
```
```   410                   with yj q show "j \<notin> D1"
```
```   411                     by (auto simp: disjoint_UN_iff)
```
```   412                 qed
```
```   413                 show "x \<in> ball (a j) (5 * r j)"
```
```   414                   using xi sub5j by blast
```
```   415               qed
```
```   416             qed
```
```   417             have 3: "?\<mu> (\<Union>i\<in>D2. ball (a i) (5 * r i)) \<le> e"
```
```   418               if D2: "D2 \<subseteq> D - D1" and "finite D2" for D2
```
```   419             proof -
```
```   420               have rgt0: "0 < r i" if "i \<in> D2" for i
```
```   421                 using \<open>C \<subseteq> K\<close> D_def \<open>i \<in> D2\<close> D2 r01
```
```   422                 by (simp add: subset_iff)
```
```   423               then have inj: "inj_on (\<lambda>i. ball (a i) (5 * r i)) D2"
```
```   424                 using \<open>C \<subseteq> K\<close> D2 by (fastforce simp: inj_on_def D_def ball_eq_ball_iff intro: ar_injective)
```
```   425               have "?\<mu> (\<Union>i\<in>D2. ball (a i) (5 * r i)) \<le> sum (?\<mu>) ((\<lambda>i. ball (a i) (5 * r i)) ` D2)"
```
```   426                 using that by (force intro: measure_Union_le)
```
```   427               also have "\<dots>  = (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (5 * r i)))"
```
```   428                 by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
```
```   429               also have "\<dots> = (\<Sum>i\<in>D2. 5 ^ DIM('n) * ?\<mu> (ball (a i) (r i)))"
```
```   430               proof (rule sum.cong [OF refl])
```
```   431                 fix i
```
```   432                 assume "i \<in> D2"
```
```   433                 show "?\<mu> (ball (a i) (5 * r i)) = 5 ^ DIM('n) * ?\<mu> (ball (a i) (r i))"
```
```   434                   using rgt0 [OF \<open>i \<in> D2\<close>] by (simp add: content_ball)
```
```   435               qed
```
```   436               also have "\<dots> = (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) * 5 ^ DIM('n)"
```
```   437                 by (simp add: sum_distrib_left mult.commute)
```
```   438               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)" .
```
```   439               moreover have "(\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) \<le> e / 5 ^ DIM('n)"
```
```   440               proof -
```
```   441                 have D12_dis: "((\<Union>x\<in>D1. cball (a x) (r x)) \<inter> (\<Union>x\<in>D2. cball (a x) (r x))) \<le> {}"
```
```   442                 proof clarify
```
```   443                   fix w d1 d2
```
```   444                   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)"
```
```   445                   then show "w d1 d2 \<in> {}"
```
```   446                     by (metis DiffE disjnt_iff subsetCE D2 \<open>D1 \<subseteq> D\<close> \<open>D \<subseteq> C\<close> pairwiseD [OF pwC, of d1 d2])
```
```   447                 qed
```
```   448                 have inj: "inj_on (\<lambda>i. cball (a i) (r i)) D2"
```
```   449                   using rgt0 D2 \<open>D \<subseteq> C\<close> by (force simp: inj_on_def cball_eq_cball_iff intro!: ar_injective)
```
```   450                 have ds: "disjoint ((\<lambda>i. cball (a i) (r i)) ` D2)"
```
```   451                   using D2 \<open>D \<subseteq> C\<close> by (auto intro: pairwiseI pairwiseD [OF pwC])
```
```   452                 have "(\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) = (\<Sum>i\<in>D2. ?\<mu> (cball (a i) (r i)))"
```
```   453                   using rgt0 by (simp add: content_ball content_cball less_eq_real_def)
```
```   454                 also have "\<dots> = sum ?\<mu> ((\<lambda>i. cball (a i) (r i)) ` D2)"
```
```   455                   by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
```
```   456                 also have "\<dots> = ?\<mu> (\<Union>i\<in>D2. cball (a i) (r i))"
```
```   457                   by (auto intro: measure_Union' [symmetric] ds simp add: \<open>finite D2\<close>)
```
```   458                 finally have "?\<mu> (\<Union>i\<in>D1. cball (a i) (r i)) + (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) =
```
```   459                               ?\<mu> (\<Union>i\<in>D1. cball (a i) (r i)) + ?\<mu> (\<Union>i\<in>D2. cball (a i) (r i))"
```
```   460                   by simp
```
```   461                 also have "\<dots> = ?\<mu> (\<Union>i \<in> D1 \<union> D2. cball (a i) (r i))"
```
```   462                   using D12_dis by (simp add: measure_Un3 \<open>finite D1\<close> \<open>finite D2\<close> fmeasurable.finite_UN)
```
```   463                 also have "\<dots> \<le> ?\<mu> (\<Union>i\<in>D. cball (a i) (r i))"
```
```   464                   using D2 \<open>D1 \<subseteq> D\<close> by (fastforce intro!: measure_mono_fmeasurable [OF _ _ UD] \<open>finite D1\<close> \<open>finite D2\<close>)
```
```   465                 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))" .
```
```   466                 with measD1 show ?thesis
```
```   467                   by simp
```
```   468               qed
```
```   469                 ultimately show ?thesis
```
```   470                   by (simp add: divide_simps)
```
```   471             qed
```
```   472             have co: "countable (D - D1)"
```
```   473               by (simp add: \<open>countable D\<close>)
```
```   474             show "(\<Union>i\<in>D - D1. ball (a i) (5 * r i)) \<in> lmeasurable"
```
```   475               using \<open>e > 0\<close> by (auto simp: fmeasurable_UN_bound [OF co _ 3])
```
```   476             show "?\<mu> (\<Union>i\<in>D - D1. ball (a i) (5 * r i)) \<le> e"
```
```   477               using \<open>e > 0\<close> by (auto simp: measure_UN_bound [OF co _ 3])
```
```   478           qed
```
```   479         qed
```
```   480       qed
```
```   481     qed (use C pwC in auto)
```
```   482   qed
```
```   483   define K' where "K' \<equiv> {i \<in> K. r i \<le> 1}"
```
```   484   have 1: "\<And>i. i \<in> K' \<Longrightarrow> 0 < r i \<and> r i \<le> 1"
```
```   485     using K'_def r by auto
```
```   486   have 2: "\<exists>i. i \<in> K' \<and> x \<in> cball (a i) (r i) \<and> r i < d"
```
```   487     if "x \<in> S \<and> 0 < d" for x d
```
```   488     using that by (auto simp: K'_def dest!: S [where d = "min d 1"])
```
```   489   have "K' \<subseteq> K"
```
```   490     using K'_def by auto
```
```   491   then show thesis
```
```   492     using * [OF 1 2] that by fastforce
```
```   493 qed
```
```   494
```
```   495
```
```   496 theorem Vitali_covering_theorem_balls:
```
```   497   fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
```
```   498   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"
```
```   499   obtains C where "countable C" "C \<subseteq> K"
```
```   500      "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
```
```   501      "negligible(S - (\<Union>i \<in> C. ball (a i) (r i)))"
```
```   502 proof -
```
```   503   have 1: "\<exists>i. i \<in> {i \<in> K. 0 < r i} \<and> x \<in> cball (a i) (r i) \<and> r i < d"
```
```   504          if xd: "x \<in> S" "d > 0" for x d
```
```   505     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))
```
```   506   obtain C where C: "countable C" "C \<subseteq> K"
```
```   507              and pw: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
```
```   508              and neg: "negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
```
```   509     by (rule Vitali_covering_theorem_cballs [of "{i \<in> K. 0 < r i}" r S a, OF _ 1]) auto
```
```   510   show thesis
```
```   511   proof
```
```   512     show "pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
```
```   513       apply (rule pairwise_mono [OF pw])
```
```   514       apply (auto simp: disjnt_def)
```
```   515       by (meson disjoint_iff_not_equal less_imp_le mem_cball)
```
```   516     have "negligible (\<Union>i\<in>C. sphere (a i) (r i))"
```
```   517       by (auto intro: negligible_sphere \<open>countable C\<close>)
```
```   518     then have "negligible (S - (\<Union>i \<in> C. cball(a i)(r i)) \<union> (\<Union>i \<in> C. sphere (a i) (r i)))"
```
```   519       by (rule negligible_Un [OF neg])
```
```   520     then show "negligible (S - (\<Union>i\<in>C. ball (a i) (r i)))"
```
```   521       by (rule negligible_subset) force
```
```   522   qed (use C in auto)
```
```   523 qed
```
```   524
```
```   525
```
```   526 lemma negligible_eq_zero_density_alt:
```
```   527      "negligible S \<longleftrightarrow>
```
```   528       (\<forall>x \<in> S. \<forall>e > 0.
```
```   529         \<exists>d U. 0 < d \<and> d \<le> e \<and> S \<inter> ball x d \<subseteq> U \<and>
```
```   530               U \<in> lmeasurable \<and> measure lebesgue U < e * measure lebesgue (ball x d))"
```
```   531      (is "_ = (\<forall>x \<in> S. \<forall>e > 0. ?Q x e)")
```
```   532 proof (intro iffI ballI allI impI)
```
```   533   fix x and e :: real
```
```   534   assume "negligible S" and "x \<in> S" and "e > 0"
```
```   535   then
```
```   536   show "\<exists>d U. 0 < d \<and> d \<le> e \<and> S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and>
```
```   537               measure lebesgue U < e * measure lebesgue (ball x d)"
```
```   538     apply (rule_tac x=e in exI)
```
```   539     apply (rule_tac x="S \<inter> ball x e" in exI)
```
```   540     apply (auto simp: negligible_imp_measurable negligible_Int negligible_imp_measure0 zero_less_measure_iff)
```
```   541     done
```
```   542 next
```
```   543   assume R [rule_format]: "\<forall>x \<in> S. \<forall>e > 0. ?Q x e"
```
```   544   let ?\<mu> = "measure lebesgue"
```
```   545   have "\<exists>U. openin (top_of_set S) U \<and> z \<in> U \<and> negligible U"
```
```   546     if "z \<in> S" for z
```
```   547   proof (intro exI conjI)
```
```   548     show "openin (top_of_set S) (S \<inter> ball z 1)"
```
```   549       by (simp add: openin_open_Int)
```
```   550     show "z \<in> S \<inter> ball z 1"
```
```   551       using \<open>z \<in> S\<close> by auto
```
```   552     show "negligible (S \<inter> ball z 1)"
```
```   553     proof (clarsimp simp: negligible_outer_le)
```
```   554       fix e :: "real"
```
```   555       assume "e > 0"
```
```   556       let ?K = "{(x,d). x \<in> S \<and> 0 < d \<and> ball x d \<subseteq> ball z 1 \<and>
```
```   557                      (\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and>
```
```   558                          ?\<mu> U < e / ?\<mu> (ball z 1) * ?\<mu> (ball x d))}"
```
```   559       obtain C where "countable C" and Csub: "C \<subseteq> ?K"
```
```   560         and pwC: "pairwise (\<lambda>i j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C"
```
```   561         and negC: "negligible((S \<inter> ball z 1) - (\<Union>i \<in> C. ball (fst i) (snd i)))"
```
```   562       proof (rule Vitali_covering_theorem_balls [of "S \<inter> ball z 1" ?K fst snd])
```
```   563         fix x and d :: "real"
```
```   564         assume x: "x \<in> S \<inter> ball z 1" and "d > 0"
```
```   565         obtain k where "k > 0" and k: "ball x k \<subseteq> ball z 1"
```
```   566           by (meson Int_iff open_ball openE x)
```
```   567         let ?\<epsilon> = "min (e / ?\<mu> (ball z 1) / 2) (min (d / 2) k)"
```
```   568         obtain r U where r: "r > 0" "r \<le> ?\<epsilon>" and U: "S \<inter> ball x r \<subseteq> U" "U \<in> lmeasurable"
```
```   569           and mU: "?\<mu> U < ?\<epsilon> * ?\<mu> (ball x r)"
```
```   570           using R [of x ?\<epsilon>] \<open>d > 0\<close> \<open>e > 0\<close> \<open>k > 0\<close> x by auto
```
```   571         show "\<exists>i. i \<in> ?K \<and> x \<in> ball (fst i) (snd i) \<and> snd i < d"
```
```   572         proof (rule exI [of _ "(x,r)"], simp, intro conjI exI)
```
```   573           have "ball x r \<subseteq> ball x k"
```
```   574             using r by (simp add: ball_subset_ball_iff)
```
```   575           also have "\<dots> \<subseteq> ball z 1"
```
```   576             using ball_subset_ball_iff k by auto
```
```   577           finally show "ball x r \<subseteq> ball z 1" .
```
```   578           have "?\<epsilon> * ?\<mu> (ball x r) \<le> e * content (ball x r) / content (ball z 1)"
```
```   579             using r \<open>e > 0\<close> by (simp add: ord_class.min_def divide_simps)
```
```   580           with mU show "?\<mu> U < e * content (ball x r) / content (ball z 1)"
```
```   581             by auto
```
```   582         qed (use r U x in auto)
```
```   583       qed
```
```   584       have "\<exists>U. case p of (x,d) \<Rightarrow> S \<inter> ball x d \<subseteq> U \<and>
```
```   585                         U \<in> lmeasurable \<and> ?\<mu> U < e / ?\<mu> (ball z 1) * ?\<mu> (ball x d)"
```
```   586         if "p \<in> C" for p
```
```   587         using that Csub by auto
```
```   588       then obtain U where U:
```
```   589                 "\<And>p. p \<in> C \<Longrightarrow>
```
```   590                        case p of (x,d) \<Rightarrow> S \<inter> ball x d \<subseteq> U p \<and>
```
```   591                         U p \<in> lmeasurable \<and> ?\<mu> (U p) < e / ?\<mu> (ball z 1) * ?\<mu> (ball x d)"
```
```   592         by (rule that [OF someI_ex])
```
```   593       let ?T = "((S \<inter> ball z 1) - (\<Union>(x,d)\<in>C. ball x d)) \<union> \<Union>(U ` C)"
```
```   594       show "\<exists>T. S \<inter> ball z 1 \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
```
```   595       proof (intro exI conjI)
```
```   596         show "S \<inter> ball z 1 \<subseteq> ?T"
```
```   597           using U by fastforce
```
```   598         { have Um: "U i \<in> lmeasurable" if "i \<in> C" for i
```
```   599             using that U by blast
```
```   600           have lee: "?\<mu> (\<Union>i\<in>I. U i) \<le> e" if "I \<subseteq> C" "finite I" for I
```
```   601           proof -
```
```   602             have "?\<mu> (\<Union>(x,d)\<in>I. ball x d) \<le> ?\<mu> (ball z 1)"
```
```   603               apply (rule measure_mono_fmeasurable)
```
```   604               using \<open>I \<subseteq> C\<close> \<open>finite I\<close> Csub by (force simp: prod.case_eq_if sets.finite_UN)+
```
```   605             then have le1: "(?\<mu> (\<Union>(x,d)\<in>I. ball x d) / ?\<mu> (ball z 1)) \<le> 1"
```
```   606               by simp
```
```   607             have "?\<mu> (\<Union>i\<in>I. U i) \<le> (\<Sum>i\<in>I. ?\<mu> (U i))"
```
```   608               using that U by (blast intro: measure_UNION_le)
```
```   609             also have "\<dots> \<le> (\<Sum>(x,r)\<in>I. e / ?\<mu> (ball z 1) * ?\<mu> (ball x r))"
```
```   610               by (rule sum_mono) (use \<open>I \<subseteq> C\<close> U in force)
```
```   611             also have "\<dots> = (e / ?\<mu> (ball z 1)) * (\<Sum>(x,r)\<in>I. ?\<mu> (ball x r))"
```
```   612               by (simp add: case_prod_app prod.case_distrib sum_distrib_left)
```
```   613             also have "\<dots> = e * (?\<mu> (\<Union>(x,r)\<in>I. ball x r) / ?\<mu> (ball z 1))"
```
```   614               apply (subst measure_UNION')
```
```   615               using that pwC by (auto simp: case_prod_unfold elim: pairwise_mono)
```
```   616             also have "\<dots> \<le> e"
```
```   617               by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \<open>e > 0\<close> le1)
```
```   618             finally show ?thesis .
```
```   619           qed
```
```   620           have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
```
```   621             using \<open>e > 0\<close> Um lee
```
```   622             by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>])
```
```   623         }
```
```   624         moreover have "?\<mu> ?T = ?\<mu> (\<Union>(U ` C))"
```
```   625         proof (rule measure_negligible_symdiff [OF \<open>\<Union>(U ` C) \<in> lmeasurable\<close>])
```
```   626           show "negligible((\<Union>(U ` C) - ?T) \<union> (?T - \<Union>(U ` C)))"
```
```   627             by (force intro!: negligible_subset [OF negC])
```
```   628         qed
```
```   629         ultimately show "?T \<in> lmeasurable"  "?\<mu> ?T \<le> e"
```
```   630           by (simp_all add: fmeasurable.Un negC negligible_imp_measurable split_def)
```
```   631       qed
```
```   632     qed
```
```   633   qed
```
```   634   with locally_negligible_alt show "negligible S"
```
```   635     by metis
```
```   636 qed
```
```   637
```
```   638 proposition negligible_eq_zero_density:
```
```   639    "negligible S \<longleftrightarrow>
```
```   640     (\<forall>x\<in>S. \<forall>r>0. \<forall>e>0. \<exists>d. 0 < d \<and> d \<le> r \<and>
```
```   641                    (\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and> measure lebesgue U < e * measure lebesgue (ball x d)))"
```
```   642 proof -
```
```   643   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)"
```
```   644   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)"
```
```   645     if "x \<in> S" for x
```
```   646   proof (intro iffI allI impI)
```
```   647     fix r :: "real" and e :: "real"
```
```   648     assume L [rule_format]: "\<forall>e>0. \<exists>d>0. d \<le> e \<and> ?Q x d e" and "r > 0" "e > 0"
```
```   649     show "\<exists>d>0. d \<le> r \<and> ?Q x d e"
```
```   650       using L [of "min r e"] apply (rule ex_forward)
```
```   651       using \<open>r > 0\<close> \<open>e > 0\<close>  by (auto intro: less_le_trans elim!: ex_forward)
```
```   652   qed auto
```
```   653   then show ?thesis
```
```   654     by (force simp: negligible_eq_zero_density_alt)
```
```   655 qed
```
```   656
```
```   657 end
```