Quelle  Vitali_Covering_Theorem.thy

(*  Title:      HOL/Analysis/Vitali_Covering_Theorem.thy
  Authors: LC Paulson, based on material from HOL Light
*)

section  ‹Vitali Covering Theorem and an Application to Negligibility›

theory Vitali_Covering_Theorem
imports
  "HOL-Combinatorics.Permutations"
  Equivalence_Lebesgue_Henstock_Integration
begin

lemma stretch_Galois:
  fixes x :: "real^'n"
  shows "(∧k. m k ≠ 0) ==> ((y = (χ k. m k * x$k)) ⟷ (χ k. y$k / m k) = x)"
  by auto

lemma lambda_swap_Galois:
   "(x = (χ i. y $ Transposition.transpose m n i) ⟷ (χ i. x $ Transposition.transpose m n i) = y)"
  by (auto; simp add: pointfree_idE vec_eq_iff)

lemma lambda_add_Galois:
  fixes x :: "real^'n"
  shows "m ≠ n ==> (x = (χ i. if i = m then y$m + y$n else y$i) ⟷ (χ i. if i = m then x$m - x$n else x$i) = y)"
  by (safe; simp add: vec_eq_iff)


lemma Vitali_covering_lemma_cballs_balls:
  fixes a :: "'a ==> 'b::euclidean_space"
  assumes "∧i. i ∈ K ==> 0 < r i ∧ r i ≤ B"
  obtains C where "countable C" "C ⊆ K"
     "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
     "∧i. i ∈ K ==> ∃j. j ∈ C ∧
                        ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                        cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
proof (cases "K = {}")
  case True
  with that show ?thesis
    by auto
next
  case False
  then have "B > 0"
    using assms less_le_trans by auto
  have rgt0[simp]: "∧i. i ∈ K ==> 0 < r i"
    using assms by auto
  let ?djnt = "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j)))"
  have "∃C. ∀n. (C n ⊆ K ∧
             (∀i ∈ C n. B/2 ^ n ≤ r i) ∧ ?djnt (C n) ∧
             (∀i ∈ K. B/2 ^ n < r i
                 ⟶ (∃j. j ∈ C n ∧
                         ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                         cball (a i) (r i) ⊆ ball (a j) (5 * r j)))) ∧ (C n ⊆ C(Suc n))"
  proof (rule dependent_nat_choice, safe)
    fix C n
    define D where "D ≡ {i ∈ K. B/2 ^ Suc n < r i ∧ (∀j∈C. disjnt (cball(a i)(r i)) (cball (a j) (r j)))}"
    let ?cover_ar = "λi j. ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                             cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
    assume "C ⊆ K"
      and Ble: "∀i∈C. B/2 ^ n ≤ r i"
      and djntC: "?djnt C"
      and cov_n: "∀i∈K. B/2 ^ n < r i ⟶ (∃j. j ∈ C ∧ ?cover_ar i j)"
    have *: "∀C∈chains {C. C ⊆ D ∧ ?djnt C}. ∪C ∈ {C. C ⊆ D ∧ ?djnt C}"
    proof (clarsimp simp: chains_def)
      fix C
      assume C: "C ⊆ {C. C ⊆ D ∧ ?djnt C}" and "chain🪙⊆ C"
      show "∪C ⊆ D ∧ ?djnt (∪C)"
        unfolding pairwise_def
      proof (intro ballI conjI impI)
        show "∪C ⊆ D"
          using C by blast
      next
        fix x y
        assume "x ∈ ∪C" and "y ∈ ∪C" and "x ≠ y"
        then obtain X Y where XY: "x ∈ X" "X ∈ C" "y ∈ Y" "Y ∈ C"
          by blast
        then consider "X ⊆ Y" | "Y ⊆ X"
          by (meson ‹chain🪙⊆ C› chain_subset_def)
        then show "disjnt (cball (a x) (r x)) (cball (a y) (r y))"
        proof cases
          case 1
          with C XY ‹x ≠ y› show ?thesis
            unfolding pairwise_def by blast
        next
          case 2
          with C XY ‹x ≠ y› show ?thesis
            unfolding pairwise_def by blast
        qed
      qed
    qed
    obtain E where "E ⊆ D" and djntE: "?djnt E" and maximalE: "∧X. [X ⊆ D; ?djnt X; E ⊆ X] ==> X = E"
      using Zorn_Lemma [OF *] by safe blast
    show "∃L. (L ⊆ K ∧
               (∀i∈L. B/2 ^ Suc n ≤ r i) ∧ ?djnt L ∧
               (∀i∈K. B/2 ^ Suc n < r i ⟶ (∃j. j ∈ L ∧ ?cover_ar i j))) ∧ C ⊆ L"
    proof (intro exI conjI ballI)
      show "C ∪ E ⊆ K"
        using D_def ‹C ⊆ K› ‹E ⊆ D› by blast
      show "B/2 ^ Suc n ≤ r i" if i: "i ∈ C ∪ E" for i
        using i
      proof
        assume "i ∈ C"
        have "B/2 ^ Suc n ≤ B/2 ^ n"
          using ‹B > 0› by (simp add: field_split_simps)
        also have "… ≤ r i"
          using Ble ‹i ∈ C› by blast
        finally show ?thesis .
      qed (use D_def ‹E ⊆ D› in auto)
      show "?djnt (C ∪ E)"
        using D_def ‹C ⊆ K› ‹E ⊆ D› djntC djntE
        unfolding pairwise_def disjnt_def by blast
    next
      fix i
      assume "i ∈ K"
      show "B/2 ^ Suc n < r i ⟶ (∃j. j ∈ C ∪ E ∧ ?cover_ar i j)"
      proof (cases "r i ≤ B/2^n")
        case False
        then show ?thesis
          using cov_n ‹i ∈ K› by auto
      next
        case True
        have "cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
          if less: "B/2 ^ Suc n < r i" and j: "j ∈ C ∪ E"
            and nondis: "¬ disjnt (cball (a i) (r i)) (cball (a j) (r j))" for j
        proof -
          obtain x where x: "dist (a i) x ≤ r i" "dist (a j) x ≤ r j"
            using nondis by (force simp: disjnt_def)
          have "dist (a i) (a j) ≤ dist (a i) x + dist x (a j)"
            by (simp add: dist_triangle)
          also have "… ≤ r i + r j"
            by (metis add_mono_thms_linordered_semiring(1) dist_commute x)
          finally have aij: "dist (a i) (a j) + r i < 5 * r j" if "r i < 2 * r j"
            using that by auto
          show ?thesis
            using j
          proof
            assume "j ∈ C"
            have "B/2^n < 2 * r j"
              using Ble True ‹j ∈ C› less by auto
            with aij True show "cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
              by (simp add: cball_subset_ball_iff)
          next
            assume "j ∈ E"
            then have "B/2 ^ n < 2 * r j"
              using D_def ‹E ⊆ D› by auto
            with True have "r i < 2 * r j"
              by auto
            with aij show "cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
              by (simp add: cball_subset_ball_iff)
          qed
        qed
      moreover have "∃j. j ∈ C ∪ E ∧ ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j))"
        if "B/2 ^ Suc n < r i"
      proof (rule classical)
        assume NON: "¬ ?thesis"
        show ?thesis
        proof (cases "i ∈ D")
          case True
          have "insert i E = E"
          proof (rule maximalE)
            show "insert i E ⊆ D"
              by (simp add: True ‹E ⊆ D›)
            show "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) (insert i E)"
              using False NON by (auto simp: pairwise_insert djntE disjnt_sym)
          qed auto
          then show ?thesis
            using ‹i ∈ K› assms by fastforce
        next
          case False
          with that show ?thesis
            by (auto simp: D_def disjnt_def ‹i ∈ K›)
        qed
      qed
      ultimately
      show "B/2 ^ Suc n < r i ⟶
            (∃j. j ∈ C ∪ E ∧
                 ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                 cball (a i) (r i) ⊆ ball (a j) (5 * r j))"
        by blast
      qed
    qed auto
  qed (use assms in force)
  then obtain F where FK: "∧n. F n ⊆ K"
               and Fle: "∧n i. i ∈ F n ==> B/2 ^ n ≤ r i"
               and Fdjnt:  "∧n. ?djnt (F n)"
               and FF:  "∧n i. [i ∈ K; B/2 ^ n < r i]
                        ==> ∃j. j ∈ F n ∧ ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                                cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
               and inc:  "∧n. F n ⊆ F(Suc n)"
    by (force simp: all_conj_distrib)
  show thesis
  proof
    have *: "countable I"
      if "I ⊆ K" and pw: "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) I" for I
    proof -
      show ?thesis
      proof (rule countable_image_inj_on [of "λi. cball(a i)(r i)"])
        show "countable ((λi. cball (a i) (r i)) ` I)"
        proof (rule countable_disjoint_nonempty_interior_subsets)
          show "disjoint ((λi. cball (a i) (r i)) ` I)"
            by (auto simp: dest: pairwiseD [OF pw] intro: pairwise_imageI)
          show "∧S. [S ∈ (λi. cball (a i) (r i)) ` I; interior S = {}] ==> S = {}"
            using ‹I ⊆ K›
            by (auto simp: not_less [symmetric])
        qed
      next
        have "∧x y. [x ∈ I; y ∈ I; a x = a y; r x = r y] ==> x = y"
          using pw ‹I ⊆ K› assms
          apply (clarsimp simp: pairwise_def disjnt_def)
          by (metis assms centre_in_cball subsetD empty_iff inf.idem less_eq_real_def)
        then show "inj_on (λi. cball (a i) (r i)) I"
          using ‹I ⊆ K› by (fastforce simp: inj_on_def cball_eq_cball_iff dest: assms)
      qed
    qed
    show "(Union(range F)) ⊆ K"
      using FK by blast
    moreover show "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) (Union(range F))"
    proof (rule pairwise_chain_Union)
      show "chain🪙⊆ (range F)"
        unfolding chain_subset_def by clarify (meson inc lift_Suc_mono_le linear subsetCE)
    qed (use Fdjnt in blast)
    ultimately show "countable (Union(range F))"
      by (blast intro: *)
  next
    fix i assume "i ∈ K"
    then obtain n where "(1/2) ^ n < r i / B"
      using  ‹B > 0› assms real_arch_pow_inv by fastforce
    then have B2: "B/2 ^ n < r i"
      using ‹B > 0› by (simp add: field_split_simps)
    have "0 < r i" "r i ≤ B"
      by (auto simp: ‹i ∈ K› assms)
    show "∃j. j ∈ (Union(range F)) ∧
          ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
          cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
      using FF [OF ‹i ∈ K› B2] by auto
  qed
qed

subsection‹Vitali covering theorem›

lemma Vitali_covering_lemma_cballs:
  fixes a :: "'a ==> 'b::euclidean_space"
  assumes S: "S ⊆ (∪i∈K. cball (a i) (r i))"
      and r: "∧i. i ∈ K ==> 0 < r i ∧ r i ≤ B"
  obtains C where "countable C" "C ⊆ K"
     "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
     "S ⊆ (∪i∈C. cball (a i) (5 * r i))"
proof -
  obtain C where C: "countable C" "C ⊆ K"
                    "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
           and cov: "∧i. i ∈ K ==> ∃j. j ∈ C ∧ ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                        cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
    by (rule Vitali_covering_lemma_cballs_balls [OF r, where a=a]) (blast intro: that)+
  show ?thesis
  proof
    have "(∪i∈K. cball (a i) (r i)) ⊆ (∪i∈C. cball (a i) (5 * r i))"
      using cov subset_iff by fastforce
    with S show "S ⊆ (∪i∈C. cball (a i) (5 * r i))"
      by blast
  qed (use C in auto)
qed

lemma Vitali_covering_lemma_balls:
  fixes a :: "'a ==> 'b::euclidean_space"
  assumes S: "S ⊆ (∪i∈K. ball (a i) (r i))"
      and r: "∧i. i ∈ K ==> 0 < r i ∧ r i ≤ B"
  obtains C where "countable C" "C ⊆ K"
     "pairwise (λi j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
     "S ⊆ (∪i∈C. ball (a i) (5 * r i))"
proof -
  obtain C where C: "countable C" "C ⊆ K"
           and pw:  "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
           and cov: "∧i. i ∈ K ==> ∃j. j ∈ C ∧ ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                        cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
    by (rule Vitali_covering_lemma_cballs_balls [OF r, where a=a]) (blast intro: that)+
  show ?thesis
  proof
    have "(∪i∈K. ball (a i) (r i)) ⊆ (∪i∈C. ball (a i) (5 * r i))"
      using cov subset_iff
      by clarsimp (meson less_imp_le mem_ball mem_cball subset_eq)
    with S show "S ⊆ (∪i∈C. ball (a i) (5 * r i))"
      by blast
    show "pairwise (λi j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
      using pw
      by (clarsimp simp: pairwise_def) (meson ball_subset_cball disjnt_subset1 disjnt_subset2)
  qed (use C in auto)
qed


theorem Vitali_covering_theorem_cballs:
  fixes a :: "'a ==> 'n::euclidean_space"
  assumes r: "∧i. i ∈ K ==> 0 < r i"
      and S: "∧x d. [x ∈ S; 0 < d]
                     ==> ∃i. i ∈ K ∧ x ∈ cball (a i) (r i) ∧ r i < d"
  obtains C where "countable C" "C ⊆ K"
     "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
     "negligible(S - (∪i ∈ C. cball (a i) (r i)))"
proof -
  let ?μ = "measure lebesgue"
  have *: "∃C. countable C ∧ C ⊆ K ∧
            pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C ∧
            negligible(S - (∪i ∈ C. cball (a i) (r i)))"
    if r01: "∧i. i ∈ K ==> 0 < r i ∧ r i ≤ 1"
       and Sd: "∧x d. [x ∈ S; 0 < d] ==> ∃i. i ∈ K ∧ x ∈ cball (a i) (r i) ∧ r i < d"
     for K r and a :: "'a ==> 'n"
  proof -
    obtain C where C: "countable C" "C ⊆ K"
      and pwC: "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
      and cov: "∧i. i ∈ K ==> ∃j. j ∈ C ∧ ¬ disjnt (cball (a i) (r i)) (cball (a j) (r j)) ∧
                        cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
      by (rule Vitali_covering_lemma_cballs_balls [of K r 1 a]) (auto simp: r01)
    have ar_injective: "∧x y. [x ∈ C; y ∈ C; a x = a y; r x = r y] ==> x = y"
      using ‹C ⊆ K› pwC cov
      by (force simp: pairwise_def disjnt_def)
    show ?thesis
    proof (intro exI conjI)
      show "negligible (S - (∪i∈C. cball (a i) (r i)))"
      proof (clarsimp simp: negligible_on_intervals [of "S-T" for T])
        fix l u
        show "negligible ((S - (∪i∈C. cball (a i) (r i))) ∩ cbox l u)"
          unfolding negligible_outer_le
        proof (intro allI impI)
          fix e::real
          assume "e > 0"
          define D where "D ≡ {i ∈ C. ¬ disjnt (ball(a i) (5 * r i)) (cbox l u)}"
          then have "D ⊆ C"
            by auto
          have "countable D"
            unfolding D_def using ‹countable C› by simp
          have UD: "(∪i∈D. cball (a i) (r i)) ∈ lmeasurable"
          proof (rule fmeasurableI2)
            show "cbox (l - 6 *🪙R One) (u + 6 *🪙R One) ∈ lmeasurable"
              by blast
            have "y ∈ cbox (l - 6 *🪙R One) (u + 6 *🪙R One)"
              if "i ∈ C" and x: "x ∈ cbox l u" and ai: "dist (a i) y ≤ r i" "dist (a i) x < 5 * r i"
              for i x y
            proof -
              have d6: "dist y x < 6 * r i"
                using dist_triangle3 [of y x "a i"] that by linarith
              show ?thesis
              proof (clarsimp simp: mem_box algebra_simps)
                fix j::'n
                assume j: "j ∈ Basis"
                then have xyj: "∣x ∙ j - y ∙ j∣ ≤ dist y x"
                  by (metis Basis_le_norm dist_commute dist_norm inner_diff_left)
                have "l ∙ j ≤ x ∙ j"
                  using ‹j ∈ Basis› mem_box ‹x ∈ cbox l u› by blast
                also have "… ≤ y ∙ j + 6 * r i"
                  using d6 xyj by (auto simp: algebra_simps)
                also have "… ≤ y ∙ j + 6"
                  using r01 [of i] ‹C ⊆ K› ‹i ∈ C› by auto
                finally have l: "l ∙ j ≤ y ∙ j + 6" .
                have "y ∙ j ≤ x ∙ j + 6 * r i"
                  using d6 xyj by (auto simp: algebra_simps)
                also have "… ≤ u ∙ j + 6 * r i"
                  using j  x by (auto simp: mem_box)
                also have "… ≤ u ∙ j + 6"
                  using r01 [of i] ‹C ⊆ K› ‹i ∈ C› by auto
                finally have u: "y ∙ j ≤ u ∙ j + 6" .
                show "l ∙ j ≤ y ∙ j + 6 ∧ y ∙ j ≤ u ∙ j + 6"
                  using l u by blast
              qed
            qed
            then show "(∪i∈D. cball (a i) (r i)) ⊆ cbox (l - 6 *🪙R One) (u + 6 *🪙R One)"
              by (force simp: D_def disjnt_def)
            show "(∪i∈D. cball (a i) (r i)) ∈ sets lebesgue"
              using ‹countable D› by auto
          qed
          obtain D1 where "D1 ⊆ D" "finite D1"
            and measD1: "?μ (∪i∈D. cball (a i) (r i)) - e / 5 ^ DIM('n) < ?μ (∪i∈D1. cball (a i) (r i))"
          proof (rule measure_countable_Union_approachable [where e = "e / 5 ^ (DIM('n))"])
            show "countable ((λi. cball (a i) (r i)) ` D)"
              using ‹countable D› by auto
            show "∧d. d ∈ (λi. cball (a i) (r i)) ` D ==> d ∈ lmeasurable"
              by auto
            show "∧D'. [D' ⊆ (λi. cball (a i) (r i)) ` D; finite D'] ==> ?μ (∪D') ≤ ?μ (∪i∈D. cball (a i) (r i))"
              by (fastforce simp add: intro!: measure_mono_fmeasurable UD)
          qed (use ‹e > 0› in ‹auto dest: finite_subset_image›)
          show "∃T. (S - (∪i∈C. cball (a i) (r i))) ∩
                    cbox l u ⊆ T ∧ T ∈ lmeasurable ∧ ?μ T ≤ e"
          proof (intro exI conjI)
            show "(S - (∪i∈C. cball (a i) (r i))) ∩ cbox l u ⊆ (∪i∈D - D1. ball (a i) (5 * r i))"
            proof clarify
              fix x
              assume x: "x ∈ cbox l u" "x ∈ S" "x ∉ (∪i∈C. cball (a i) (r i))"
              have "closed (∪i∈D1. cball (a i) (r i))"
                using ‹finite D1› by blast
              moreover have "x ∉ (∪j∈D1. cball (a j) (r j))"
                using x ‹D1 ⊆ D› unfolding D_def by blast
              ultimately obtain q where "q > 0" and q: "ball x q ⊆ - (∪i∈D1. cball (a i) (r i))"
                by (metis (no_types, lifting) ComplI open_contains_ball closed_def)
              obtain i where "i ∈ K" and xi: "x ∈ cball (a i) (r i)" and ri: "r i < q/2"
                using Sd [OF ‹x ∈ S›] ‹q > 0› half_gt_zero by blast
              then obtain j where "j ∈ C"
                             and nondisj: "¬ disjnt (cball (a i) (r i)) (cball (a j) (r j))"
                             and sub5j:  "cball (a i) (r i) ⊆ ball (a j) (5 * r j)"
                using cov [OF ‹i ∈ K›] by metis
              show "x ∈ (∪i∈D - D1. ball (a i) (5 * r i))"
              proof
                show "j ∈ D - D1"
                proof
                  show "j ∈ D"
                    using ‹j ∈ C› sub5j ‹x ∈ cbox l u› xi by (auto simp: D_def disjnt_def)
                  obtain y where yi: "dist (a i) y ≤ r i" and yj: "dist (a j) y ≤ r j"
                    using disjnt_def nondisj by fastforce
                  have "dist x y ≤ r i + r i"
                    by (metis add_mono dist_commute dist_triangle_le mem_cball xi yi)
                  also have "… < q"
                    using ri by linarith
                  finally have "y ∈ ball x q"
                    by simp
                  with yj q show "j ∉ D1"
                    by (auto simp: disjoint_UN_iff)
                qed
                show "x ∈ ball (a j) (5 * r j)"
                  using xi sub5j by blast
              qed
            qed
            have 3: "?μ (∪i∈D2. ball (a i) (5 * r i)) ≤ e"
              if D2: "D2 ⊆ D - D1" and "finite D2" for D2
            proof -
              have rgt0: "0 < r i" if "i ∈ D2" for i
                using ‹C ⊆ K› D_def ‹i ∈ D2› D2 r01
                by (simp add: subset_iff)
              then have inj: "inj_on (λi. ball (a i) (5 * r i)) D2"
                using ‹C ⊆ K› D2 by (fastforce simp: inj_on_def D_def ball_eq_ball_iff intro: ar_injective)
              have "?μ (∪i∈D2. ball (a i) (5 * r i)) ≤ sum (?μ) ((λi. ball (a i) (5 * r i)) ` D2)"
                using that by (force intro: measure_Union_le)
              also have "… = (∑i∈D2. ?μ (ball (a i) (5 * r i)))"
                by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
              also have "… = (∑i∈D2. 5 ^ DIM('n) * ?μ (ball (a i) (r i)))"
              proof (rule sum.cong [OF refl])
                fix i assume "i ∈ D2"
                thus "?μ (ball (a i) (5 * r i)) = 5 ^ DIM('n) * ?μ (ball (a i) (r i))"
                  using content_ball_conv_unit_ball[of "5 * r i" "a i"]
                        content_ball_conv_unit_ball[of "r i" "a i"] rgt0[of i] by auto
              qed
              also have "… = (∑i∈D2. ?μ (ball (a i) (r i))) * 5 ^ DIM('n)"
                by (simp add: sum_distrib_left mult.commute)
              finally have "?μ (∪i∈D2. ball (a i) (5 * r i)) ≤ (∑i∈D2. ?μ (ball (a i) (r i))) * 5 ^ DIM('n)" .
              moreover have "(∑i∈D2. ?μ (ball (a i) (r i))) ≤ e / 5 ^ DIM('n)"
              proof -
                have D12_dis: "((∪x∈D1. cball (a x) (r x)) ∩ (∪x∈D2. cball (a x) (r x))) ≤ {}"
                proof clarify
                  fix w d1 d2
                  assume "d1 ∈ D1" "w d1 d2 ∈ cball (a d1) (r d1)" "d2 ∈ D2" "w d1 d2 ∈ cball (a d2) (r d2)"
                  then show "w d1 d2 ∈ {}"
                    by (metis DiffE disjnt_iff subsetCE D2 ‹D1 ⊆ D› ‹D ⊆ C› pairwiseD [OF pwC, of d1 d2])
                qed
                have inj: "inj_on (λi. cball (a i) (r i)) D2"
                  using rgt0 D2 ‹D ⊆ C› by (force simp: inj_on_def cball_eq_cball_iff intro!: ar_injective)
                have ds: "disjoint ((λi. cball (a i) (r i)) ` D2)"
                  using D2 ‹D ⊆ C› by (auto intro: pairwiseI pairwiseD [OF pwC])
                have "(∑i∈D2. ?μ (ball (a i) (r i))) = (∑i∈D2. ?μ (cball (a i) (r i)))"
                  by (simp add: content_cball_conv_ball)
                also have "… = sum ?μ ((λi. cball (a i) (r i)) ` D2)"
                  by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
                also have "… = ?μ (∪i∈D2. cball (a i) (r i))"
                  by (auto intro: measure_Union' [symmetric] ds simp add: ‹finite D2›)
                finally have "?μ (∪i∈D1. cball (a i) (r i)) + (∑i∈D2. ?μ (ball (a i) (r i))) =
                              ?μ (∪i∈D1. cball (a i) (r i)) + ?μ (∪i∈D2. cball (a i) (r i))"
                  by simp
                also have "… = ?μ (∪i ∈ D1 ∪ D2. cball (a i) (r i))"
                  using D12_dis by (simp add: measure_Un3 ‹finite D1› ‹finite D2› fmeasurable.finite_UN)
                also have "… ≤ ?μ (∪i∈D. cball (a i) (r i))"
                  using D2 ‹D1 ⊆ D› by (fastforce intro!: measure_mono_fmeasurable [OF _ _ UD] ‹finite D1› ‹finite D2›)
                finally have "?μ (∪i∈D1. cball (a i) (r i)) + (∑i∈D2. ?μ (ball (a i) (r i))) ≤ ?μ (∪i∈D. cball (a i) (r i))" .
                with measD1 show ?thesis
                  by simp
              qed
                ultimately show ?thesis
                  by (simp add: field_split_simps)
            qed
            have co: "countable (D - D1)"
              by (simp add: ‹countable D›)
            show "(∪i∈D - D1. ball (a i) (5 * r i)) ∈ lmeasurable"
              using ‹e > 0› by (auto simp: fmeasurable_UN_bound [OF co _ 3])
            show "?μ (∪i∈D - D1. ball (a i) (5 * r i)) ≤ e"
              using ‹e > 0› by (auto simp: measure_UN_bound [OF co _ 3])
          qed
        qed
      qed
    qed (use C pwC in auto)
  qed
  define K' where "K' ≡ {i ∈ K. r i ≤ 1}"
  have 1: "∧i. i ∈ K' ==> 0 < r i ∧ r i ≤ 1"
    using K'_def r by auto
  have 2: "∃i. i ∈ K' ∧ x ∈ cball (a i) (r i) ∧ r i < d"
    if "x ∈ S ∧ 0 < d" for x d
    using that by (auto simp: K'_def dest!: S [where d = "min d 1"])
  have "K' ⊆ K"
    using K'_def by auto
  then show thesis
    using * [OF 1 2] that by fastforce
qed


theorem Vitali_covering_theorem_balls:
  fixes a :: "'a ==> 'b::euclidean_space"
  assumes S: "∧x d. [x ∈ S; 0 < d] ==> ∃i. i ∈ K ∧ x ∈ ball (a i) (r i) ∧ r i < d"
  obtains C where "countable C" "C ⊆ K"
     "pairwise (λi j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
     "negligible(S - (∪i ∈ C. ball (a i) (r i)))"
proof -
  have 1: "∃i. i ∈ {i ∈ K. 0 < r i} ∧ x ∈ cball (a i) (r i) ∧ r i < d"
         if xd: "x ∈ S" "d > 0" for x d
    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))
  obtain C where C: "countable C" "C ⊆ K"
             and pw: "pairwise (λi j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
             and neg: "negligible(S - (∪i ∈ C. cball (a i) (r i)))"
    by (rule Vitali_covering_theorem_cballs [of "{i ∈ K. 0 < r i}" r S a, OF _ 1]) auto
  show thesis
  proof
    show "pairwise (λi j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
      apply (rule pairwise_mono [OF pw])
      apply (auto simp: disjnt_def)
      by (meson disjoint_iff_not_equal less_imp_le mem_cball)
    have "negligible (∪i∈C. sphere (a i) (r i))"
      by (auto intro: negligible_sphere ‹countable C›)
    then have "negligible (S - (∪i ∈ C. cball(a i)(r i)) ∪ (∪i ∈ C. sphere (a i) (r i)))"
      by (rule negligible_Un [OF neg])
    then show "negligible (S - (∪i∈C. ball (a i) (r i)))"
      by (rule negligible_subset) force
  qed (use C in auto)
qed


lemma negligible_eq_zero_density_alt:
     "negligible S ⟷
      (∀x ∈ S. ∀e > 0.
        ∃d U. 0 < d ∧ d ≤ e ∧ S ∩ ball x d ⊆ U ∧
              U ∈ lmeasurable ∧ measure lebesgue U < e * measure lebesgue (ball x d))"
     (is "_ = (∀x ∈ S. ∀e > 0. ?Q x e)")
proof (intro iffI ballI allI impI)
  fix x and e :: real
  assume "negligible S" and "x ∈ S" and "e > 0"
  then
  show "∃d U. 0 < d ∧ d ≤ e ∧ S ∩ ball x d ⊆ U ∧ U ∈ lmeasurable ∧
              measure lebesgue U < e * measure lebesgue (ball x d)"
    apply (rule_tac x=e in exI)
    apply (rule_tac x="S ∩ ball x e" in exI)
    apply (auto simp: negligible_imp_measurable negligible_Int negligible_imp_measure0 zero_less_measure_iff
                intro: mult_pos_pos content_ball_pos)
    done
next
  assume R [rule_format]: "∀x ∈ S. ∀e > 0. ?Q x e"
  let ?μ = "measure lebesgue"
  have "∃U. openin (top_of_set S) U ∧ z ∈ U ∧ negligible U"
    if "z ∈ S" for z
  proof (intro exI conjI)
    show "openin (top_of_set S) (S ∩ ball z 1)"
      by (simp add: openin_open_Int)
    show "z ∈ S ∩ ball z 1"
      using ‹z ∈ S› by auto
    show "negligible (S ∩ ball z 1)"
    proof (clarsimp simp: negligible_outer_le)
      fix e :: "real"
      assume "e > 0"
      let ?K = "{(x,d). x ∈ S ∧ 0 < d ∧ ball x d ⊆ ball z 1 ∧
                     (∃U. S ∩ ball x d ⊆ U ∧ U ∈ lmeasurable ∧
                         ?μ U < e / ?μ (ball z 1) * ?μ (ball x d))}"
      obtain C where "countable C" and Csub: "C ⊆ ?K"
        and pwC: "pairwise (λi j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C"
        and negC: "negligible((S ∩ ball z 1) - (∪i ∈ C. ball (fst i) (snd i)))"
      proof (rule Vitali_covering_theorem_balls [of "S ∩ ball z 1" ?K fst snd])
        fix x and d :: "real"
        assume x: "x ∈ S ∩ ball z 1" and "d > 0"
        obtain k where "k > 0" and k: "ball x k ⊆ ball z 1"
          by (meson Int_iff open_ball openE x)
        let ?ε = "min (e / ?μ (ball z 1) / 2) (min (d / 2) k)"
        obtain r U where r: "r > 0" "r ≤ ?ε" and U: "S ∩ ball x r ⊆ U" "U ∈ lmeasurable"
          and mU: "?μ U < ?ε * ?μ (ball x r)"
          using R [of x ?ε] ‹d > 0› ‹e > 0› ‹k > 0› x by (auto simp: content_ball_pos)
        show "∃i. i ∈ ?K ∧ x ∈ ball (fst i) (snd i) ∧ snd i < d"
        proof (rule exI [of _ "(x,r)"], simp, intro conjI exI)
          have "ball x r ⊆ ball x k"
            using r by (simp add: ball_subset_ball_iff)
          also have "… ⊆ ball z 1"
            using ball_subset_ball_iff k by auto
          finally show "ball x r ⊆ ball z 1" .
          have "?ε * ?μ (ball x r) ≤ e * content (ball x r) / content (ball z 1)"
            using r ‹e > 0› by (simp add: ord_class.min_def field_split_simps content_ball_pos)
          with mU show "?μ U < e * content (ball x r) / content (ball z 1)"
            by auto
        qed (use r U x in auto)
      qed
      have "∃U. case p of (x,d) ==> S ∩ ball x d ⊆ U ∧
                        U ∈ lmeasurable ∧ ?μ U < e / ?μ (ball z 1) * ?μ (ball x d)"
        if "p ∈ C" for p
        using that Csub unfolding case_prod_unfold by blast
      then obtain U where U:
                "∧p. p ∈ C ==>
                       case p of (x,d) ==> S ∩ ball x d ⊆ U p ∧
                        U p ∈ lmeasurable ∧ ?μ (U p) < e / ?μ (ball z 1) * ?μ (ball x d)"
        by (rule that [OF someI_ex])
      let ?T = "((S ∩ ball z 1) - (∪(x,d)∈C. ball x d)) ∪ ∪(U ` C)"
      show "∃T. S ∩ ball z 1 ⊆ T ∧ T ∈ lmeasurable ∧ ?μ T ≤ e"
      proof (intro exI conjI)
        show "S ∩ ball z 1 ⊆ ?T"
          using U by fastforce
        { have Um: "U i ∈ lmeasurable" if "i ∈ C" for i
            using that U by blast
          have lee: "?μ (∪i∈I. U i) ≤ e" if "I ⊆ C" "finite I" for I
          proof -
            have "?μ (∪(x,d)∈I. ball x d) ≤ ?μ (ball z 1)"
              apply (rule measure_mono_fmeasurable)
              using ‹I ⊆ C› ‹finite I› Csub by (force simp: prod.case_eq_if sets.finite_UN)+
            then have le1: "(?μ (∪(x,d)∈I. ball x d) / ?μ (ball z 1)) ≤ 1"
              by (simp add: content_ball_pos)
            have "?μ (∪i∈I. U i) ≤ (∑i∈I. ?μ (U i))"
              using that U by (blast intro: measure_UNION_le)
            also have "… ≤ (∑(x,r)∈I. e / ?μ (ball z 1) * ?μ (ball x r))"
              by (rule sum_mono) (use ‹I ⊆ C› U in force)
            also have "… = (e / ?μ (ball z 1)) * (∑(x,r)∈I. ?μ (ball x r))"
              by (simp add: case_prod_app prod.case_distrib sum_distrib_left)
            also have "… = e * (?μ (∪(x,r)∈I. ball x r) / ?μ (ball z 1))"
              apply (subst measure_UNION')
              using that pwC by (auto simp: case_prod_unfold elim: pairwise_mono)
            also have "… ≤ e"
              by (metis mult.commute mult.left_neutral mult_le_cancel_right_pos ‹e > 0› le1)
            finally show ?thesis .
          qed
          have "∪(U ` C) ∈ lmeasurable" "?μ (∪(U ` C)) ≤ e"
            using ‹e > 0› Um lee
            by(auto intro!: fmeasurable_UN_bound [OF ‹countable C›] measure_UN_bound [OF ‹countable C›])
        }
        moreover have "?μ ?T = ?μ (∪(U ` C))"
        proof (rule measure_negligible_symdiff [OF ‹∪(U ` C) ∈ lmeasurable›])
          show "negligible((∪(U ` C) - ?T) ∪ (?T - ∪(U ` C)))"
            by (force intro!: negligible_subset [OF negC])
        qed
        ultimately show "?T ∈ lmeasurable"  "?μ ?T ≤ e"
          by (simp_all add: fmeasurable.Un negC negligible_imp_measurable split_def)
      qed
    qed
  qed
  with locally_negligible_alt show "negligible S"
    by metis
qed

proposition negligible_eq_zero_density:
   "negligible S ⟷
    (∀x∈S. ∀r>0. ∀e>0. ∃d. 0 < d ∧ d ≤ r ∧
                   (∃U. S ∩ ball x d ⊆ U ∧ U ∈ lmeasurable ∧ measure lebesgue U < e * measure lebesgue (ball x d)))"
proof -
  let ?Q = "λx d e. ∃U. S ∩ ball x d ⊆ U ∧ U ∈ lmeasurable ∧ measure lebesgue U < e * content (ball x d)"
  have "(∀e>0. ∃d>0. d ≤ e ∧ ?Q x d e) = (∀r>0. ∀e>0. ∃d>0. d ≤ r ∧ ?Q x d e)"
    if "x ∈ S" for x
  proof (intro iffI allI impI)
    fix r :: "real" and e :: "real"
    assume L [rule_format]: "∀e>0. ∃d>0. d ≤ e ∧ ?Q x d e" and "r > 0" "e > 0"
    show "∃d>0. d ≤ r ∧ ?Q x d e"
      using L [of "min r e"] apply (rule ex_forward)
      using ‹r > 0› ‹e > 0›  by (auto intro: less_le_trans elim!: ex_forward simp: content_ball_pos)
  qed auto
  then show ?thesis
    by (force simp: negligible_eq_zero_density_alt)
qed

end