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