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