src/HOL/Analysis/Vitali_Covering_Theorem.thy
 author haftmann Sun Nov 18 18:07:51 2018 +0000 (8 months ago) changeset 69313 b021008c5397 parent 68833 fde093888c16 child 69683 8b3458ca0762 permissions -rw-r--r--
removed legacy input syntax
 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@68833 ` 5` ```section%important \Vitali Covering Theorem and an Application to Negligibility\ ``` 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@68833 ` 12` ```lemma%important stretch_Galois: ``` lp15@67996 ` 13` ``` fixes x :: "real^'n" ``` lp15@67996 ` 14` ``` shows "(\k. m k \ 0) \ ((y = (\ k. m k * x\$k)) \ (\ k. y\$k / m k) = x)" ``` ak2110@68833 ` 15` ``` by%unimportant auto ``` lp15@67996 ` 16` ak2110@68833 ` 17` ```lemma%important lambda_swap_Galois: ``` lp15@67996 ` 18` ``` "(x = (\ i. y \$ Fun.swap m n id i) \ (\ i. x \$ Fun.swap m n id i) = y)" ``` ak2110@68833 ` 19` ``` by%unimportant (auto; simp add: pointfree_idE vec_eq_iff) ``` lp15@67996 ` 20` ak2110@68833 ` 21` ```lemma%important lambda_add_Galois: ``` lp15@67996 ` 22` ``` fixes x :: "real^'n" ``` lp15@67996 ` 23` ``` 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)" ``` ak2110@68833 ` 24` ``` by%unimportant (safe; simp add: vec_eq_iff) ``` lp15@67996 ` 25` lp15@67996 ` 26` ak2110@68833 ` 27` ```lemma%important Vitali_covering_lemma_cballs_balls: ``` lp15@67996 ` 28` ``` fixes a :: "'a \ 'b::euclidean_space" ``` lp15@67996 ` 29` ``` assumes "\i. i \ K \ 0 < r i \ r i \ B" ``` lp15@67996 ` 30` ``` obtains C where "countable C" "C \ K" ``` lp15@67996 ` 31` ``` "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 32` ``` "\i. i \ K \ \j. j \ C \ ``` lp15@67996 ` 33` ``` \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 34` ``` cball (a i) (r i) \ ball (a j) (5 * r j)" ``` ak2110@68833 ` 35` ```proof%unimportant (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]: "\i. i \ K \ 0 < r i" ``` lp15@67996 ` 44` ``` using assms by auto ``` lp15@67996 ` 45` ``` let ?djnt = "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j)))" ``` lp15@67996 ` 46` ``` have "\C. \n. (C n \ K \ ``` lp15@67996 ` 47` ``` (\i \ C n. B/2 ^ n \ r i) \ ?djnt (C n) \ ``` lp15@67996 ` 48` ``` (\i \ K. B/2 ^ n < r i ``` lp15@67996 ` 49` ``` \ (\j. j \ C n \ ``` lp15@67996 ` 50` ``` \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 51` ``` cball (a i) (r i) \ ball (a j) (5 * r j)))) \ (C n \ 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 \ {i \ K. B/2 ^ Suc n < r i \ (\j\C. disjnt (cball(a i)(r i)) (cball (a j) (r j)))}" ``` lp15@67996 ` 55` ``` let ?cover_ar = "\i j. \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 56` ``` cball (a i) (r i) \ ball (a j) (5 * r j)" ``` lp15@67996 ` 57` ``` assume "C \ K" ``` lp15@67996 ` 58` ``` and Ble: "\i\C. B/2 ^ n \ r i" ``` lp15@67996 ` 59` ``` and djntC: "?djnt C" ``` lp15@67996 ` 60` ``` and cov_n: "\i\K. B/2 ^ n < r i \ (\j. j \ C \ ?cover_ar i j)" ``` lp15@67996 ` 61` ``` have *: "\C\chains {C. C \ D \ ?djnt C}. \C \ {C. C \ D \ ?djnt C}" ``` lp15@67996 ` 62` ``` proof (clarsimp simp: chains_def) ``` lp15@67996 ` 63` ``` fix C ``` lp15@67996 ` 64` ``` assume C: "C \ {C. C \ D \ ?djnt C}" and "chain\<^sub>\ C" ``` lp15@67996 ` 65` ``` show "\C \ D \ ?djnt (\C)" ``` lp15@67996 ` 66` ``` unfolding pairwise_def ``` lp15@67996 ` 67` ``` proof (intro ballI conjI impI) ``` lp15@67996 ` 68` ``` show "\C \ D" ``` lp15@67996 ` 69` ``` using C by blast ``` lp15@67996 ` 70` ``` next ``` lp15@67996 ` 71` ``` fix x y ``` lp15@67996 ` 72` ``` assume "x \ \C" and "y \ \C" and "x \ y" ``` lp15@67996 ` 73` ``` then obtain X Y where XY: "x \ X" "X \ C" "y \ Y" "Y \ C" ``` lp15@67996 ` 74` ``` by blast ``` lp15@67996 ` 75` ``` then consider "X \ Y" | "Y \ X" ``` lp15@67996 ` 76` ``` by (meson \chain\<^sub>\ C\ 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 \x \ y\ 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 \x \ y\ 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 \ D" and djntE: "?djnt E" and maximalE: "\X. \X \ D; ?djnt X; E \ X\ \ X = E" ``` lp15@67996 ` 90` ``` using Zorn_Lemma [OF *] by safe blast ``` lp15@67996 ` 91` ``` show "\L. (L \ K \ ``` lp15@67996 ` 92` ``` (\i\L. B/2 ^ Suc n \ r i) \ ?djnt L \ ``` lp15@67996 ` 93` ``` (\i\K. B/2 ^ Suc n < r i \ (\j. j \ L \ ?cover_ar i j))) \ C \ L" ``` lp15@67996 ` 94` ``` proof (intro exI conjI ballI) ``` lp15@67996 ` 95` ``` show "C \ E \ K" ``` lp15@67996 ` 96` ``` using D_def \C \ K\ \E \ D\ by blast ``` lp15@67996 ` 97` ``` show "B/2 ^ Suc n \ r i" if i: "i \ C \ E" for i ``` lp15@67996 ` 98` ``` using i ``` lp15@67996 ` 99` ``` proof ``` lp15@67996 ` 100` ``` assume "i \ C" ``` lp15@67996 ` 101` ``` have "B/2 ^ Suc n \ B/2 ^ n" ``` lp15@67996 ` 102` ``` using \B > 0\ by (simp add: divide_simps) ``` lp15@67996 ` 103` ``` also have "\ \ r i" ``` lp15@67996 ` 104` ``` using Ble \i \ C\ by blast ``` lp15@67996 ` 105` ``` finally show ?thesis . ``` lp15@67996 ` 106` ``` qed (use D_def \E \ D\ in auto) ``` lp15@67996 ` 107` ``` show "?djnt (C \ E)" ``` lp15@67996 ` 108` ``` using D_def \C \ K\ \E \ D\ 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 \ K" ``` lp15@67996 ` 113` ``` show "B/2 ^ Suc n < r i \ (\j. j \ C \ E \ ?cover_ar i j)" ``` lp15@67996 ` 114` ``` proof (cases "r i \ B/2^n") ``` lp15@67996 ` 115` ``` case False ``` lp15@67996 ` 116` ``` then show ?thesis ``` lp15@67996 ` 117` ``` using cov_n \i \ K\ by auto ``` lp15@67996 ` 118` ``` next ``` lp15@67996 ` 119` ``` case True ``` lp15@67996 ` 120` ``` have "cball (a i) (r i) \ ball (a j) (5 * r j)" ``` lp15@67996 ` 121` ``` if less: "B/2 ^ Suc n < r i" and j: "j \ C \ E" ``` lp15@67996 ` 122` ``` and nondis: "\ 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 \ r i" "dist (a j) x \ r j" ``` lp15@67996 ` 125` ``` using nondis by (force simp: disjnt_def) ``` lp15@67996 ` 126` ``` have "dist (a i) (a j) \ dist (a i) x + dist x (a j)" ``` lp15@67996 ` 127` ``` by (simp add: dist_triangle) ``` lp15@67996 ` 128` ``` also have "\ \ 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 \ C" ``` lp15@67996 ` 136` ``` have "B/2^n < 2 * r j" ``` lp15@67996 ` 137` ``` using Ble True \j \ C\ less by auto ``` lp15@67996 ` 138` ``` with aij True show "cball (a i) (r i) \ 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 \ E" ``` lp15@67996 ` 142` ``` then have "B/2 ^ n < 2 * r j" ``` lp15@67996 ` 143` ``` using D_def \E \ D\ 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) \ 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 "\j. j \ C \ E \ \ 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: "\ ?thesis" ``` lp15@67996 ` 154` ``` show ?thesis ``` lp15@67996 ` 155` ``` proof (cases "i \ 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 \ D" ``` lp15@67996 ` 160` ``` by (simp add: True \E \ D\) ``` lp15@67996 ` 161` ``` show "pairwise (\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 \i \ K\ 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 \i \ K\) ``` lp15@67996 ` 170` ``` qed ``` lp15@67996 ` 171` ``` qed ``` lp15@67996 ` 172` ``` ultimately ``` lp15@67996 ` 173` ``` show "B/2 ^ Suc n < r i \ ``` lp15@67996 ` 174` ``` (\j. j \ C \ E \ ``` lp15@67996 ` 175` ``` \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 176` ``` cball (a i) (r i) \ 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: "\n. F n \ K" ``` lp15@67996 ` 182` ``` and Fle: "\n i. i \ F n \ B/2 ^ n \ r i" ``` lp15@67996 ` 183` ``` and Fdjnt: "\n. ?djnt (F n)" ``` lp15@67996 ` 184` ``` and FF: "\n i. \i \ K; B/2 ^ n < r i\ ``` lp15@67996 ` 185` ``` \ \j. j \ F n \ \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 186` ``` cball (a i) (r i) \ ball (a j) (5 * r j)" ``` lp15@67996 ` 187` ``` and inc: "\n. F n \ 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 \ K" and pw: "pairwise (\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 "\i. cball(a i)(r i)"]) ``` lp15@67996 ` 196` ``` show "countable ((\i. cball (a i) (r i)) ` I)" ``` lp15@67996 ` 197` ``` proof (rule countable_disjoint_nonempty_interior_subsets) ``` lp15@67996 ` 198` ``` show "disjoint ((\i. cball (a i) (r i)) ` I)" ``` lp15@67996 ` 199` ``` by (auto simp: dest: pairwiseD [OF pw] intro: pairwise_imageI) ``` lp15@67996 ` 200` ``` show "\S. \S \ (\i. cball (a i) (r i)) ` I; interior S = {}\ \ S = {}" ``` lp15@67996 ` 201` ``` using \I \ K\ ``` lp15@67996 ` 202` ``` by (auto simp: not_less [symmetric]) ``` lp15@67996 ` 203` ``` qed ``` lp15@67996 ` 204` ``` next ``` lp15@67996 ` 205` ``` have "\x y. \x \ I; y \ I; a x = a y; r x = r y\ \ x = y" ``` lp15@67996 ` 206` ``` using pw \I \ K\ 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 (\i. cball (a i) (r i)) I" ``` lp15@67996 ` 210` ``` using \I \ K\ 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)) \ K" ``` lp15@67996 ` 214` ``` using FK by blast ``` lp15@67996 ` 215` ``` moreover show "pairwise (\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>\ (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 \ K" ``` lp15@67996 ` 224` ``` then obtain n where "(1/2) ^ n < r i / B" ``` lp15@67996 ` 225` ``` using \B > 0\ assms real_arch_pow_inv by fastforce ``` lp15@67996 ` 226` ``` then have B2: "B/2 ^ n < r i" ``` lp15@67996 ` 227` ``` using \B > 0\ by (simp add: divide_simps) ``` lp15@67996 ` 228` ``` have "0 < r i" "r i \ B" ``` lp15@67996 ` 229` ``` by (auto simp: \i \ K\ assms) ``` lp15@67996 ` 230` ``` show "\j. j \ (Union(range F)) \ ``` lp15@67996 ` 231` ``` \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 232` ``` cball (a i) (r i) \ ball (a j) (5 * r j)" ``` lp15@67996 ` 233` ``` using FF [OF \i \ K\ B2] by auto ``` lp15@67996 ` 234` ``` qed ``` lp15@67996 ` 235` ```qed ``` lp15@67996 ` 236` ak2110@68833 ` 237` ```subsection%important\Vitali covering theorem\ ``` lp15@67996 ` 238` ak2110@68833 ` 239` ```lemma%unimportant Vitali_covering_lemma_cballs: ``` lp15@67996 ` 240` ``` fixes a :: "'a \ 'b::euclidean_space" ``` lp15@67996 ` 241` ``` assumes S: "S \ (\i\K. cball (a i) (r i))" ``` lp15@67996 ` 242` ``` and r: "\i. i \ K \ 0 < r i \ r i \ B" ``` lp15@67996 ` 243` ``` obtains C where "countable C" "C \ K" ``` lp15@67996 ` 244` ``` "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 245` ``` "S \ (\i\C. cball (a i) (5 * r i))" ``` ak2110@68833 ` 246` ```proof%unimportant - ``` lp15@67996 ` 247` ``` obtain C where C: "countable C" "C \ K" ``` lp15@67996 ` 248` ``` "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 249` ``` and cov: "\i. i \ K \ \j. j \ C \ \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 250` ``` cball (a i) (r i) \ 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 "(\i\K. cball (a i) (r i)) \ (\i\C. cball (a i) (5 * r i))" ``` lp15@67996 ` 255` ``` using cov subset_iff by fastforce ``` lp15@67996 ` 256` ``` with S show "S \ (\i\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@68833 ` 261` ```lemma%important Vitali_covering_lemma_balls: ``` lp15@67996 ` 262` ``` fixes a :: "'a \ 'b::euclidean_space" ``` lp15@67996 ` 263` ``` assumes S: "S \ (\i\K. ball (a i) (r i))" ``` lp15@67996 ` 264` ``` and r: "\i. i \ K \ 0 < r i \ r i \ B" ``` lp15@67996 ` 265` ``` obtains C where "countable C" "C \ K" ``` lp15@67996 ` 266` ``` "pairwise (\i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C" ``` lp15@67996 ` 267` ``` "S \ (\i\C. ball (a i) (5 * r i))" ``` ak2110@68833 ` 268` ```proof%unimportant - ``` lp15@67996 ` 269` ``` obtain C where C: "countable C" "C \ K" ``` lp15@67996 ` 270` ``` and pw: "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 271` ``` and cov: "\i. i \ K \ \j. j \ C \ \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 272` ``` cball (a i) (r i) \ 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 "(\i\K. ball (a i) (r i)) \ (\i\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 \ (\i\C. ball (a i) (5 * r i))" ``` lp15@67996 ` 280` ``` by blast ``` lp15@67996 ` 281` ``` show "pairwise (\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@68833 ` 288` ```proposition%important Vitali_covering_theorem_cballs: ``` lp15@67996 ` 289` ``` fixes a :: "'a \ 'n::euclidean_space" ``` lp15@67996 ` 290` ``` assumes r: "\i. i \ K \ 0 < r i" ``` lp15@67996 ` 291` ``` and S: "\x d. \x \ S; 0 < d\ ``` lp15@67996 ` 292` ``` \ \i. i \ K \ x \ cball (a i) (r i) \ r i < d" ``` lp15@67996 ` 293` ``` obtains C where "countable C" "C \ K" ``` lp15@67996 ` 294` ``` "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 295` ``` "negligible(S - (\i \ C. cball (a i) (r i)))" ``` ak2110@68833 ` 296` ```proof%unimportant - ``` lp15@67996 ` 297` ``` let ?\ = "measure lebesgue" ``` lp15@67996 ` 298` ``` have *: "\C. countable C \ C \ K \ ``` lp15@67996 ` 299` ``` pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C \ ``` lp15@67996 ` 300` ``` negligible(S - (\i \ C. cball (a i) (r i)))" ``` lp15@67996 ` 301` ``` if r01: "\i. i \ K \ 0 < r i \ r i \ 1" ``` lp15@67996 ` 302` ``` and Sd: "\x d. \x \ S; 0 < d\ \ \i. i \ K \ x \ cball (a i) (r i) \ r i < d" ``` lp15@67996 ` 303` ``` for K r and a :: "'a \ 'n" ``` lp15@67996 ` 304` ``` proof - ``` lp15@67996 ` 305` ``` obtain C where C: "countable C" "C \ K" ``` lp15@67996 ` 306` ``` and pwC: "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 307` ``` and cov: "\i. i \ K \ \j. j \ C \ \ disjnt (cball (a i) (r i)) (cball (a j) (r j)) \ ``` lp15@67996 ` 308` ``` cball (a i) (r i) \ 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: "\x y. \x \ C; y \ C; a x = a y; r x = r y\ \ x = y" ``` lp15@67996 ` 311` ``` using \C \ K\ 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 - (\i\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 - (\i\C. cball (a i) (r i))) \ 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 \ {i \ C. \ disjnt (ball(a i) (5 * r i)) (cbox l u)}" ``` lp15@67996 ` 324` ``` then have "D \ C" ``` lp15@67996 ` 325` ``` by auto ``` lp15@67996 ` 326` ``` have "countable D" ``` lp15@67996 ` 327` ``` unfolding D_def using \countable C\ by simp ``` lp15@67996 ` 328` ``` have UD: "(\i\D. cball (a i) (r i)) \ lmeasurable" ``` lp15@67996 ` 329` ``` proof (rule fmeasurableI2) ``` lp15@67996 ` 330` ``` show "cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One) \ lmeasurable" ``` lp15@67996 ` 331` ``` by blast ``` lp15@67996 ` 332` ``` have "y \ cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One)" ``` lp15@67996 ` 333` ``` if "i \ C" and x: "x \ cbox l u" and ai: "dist (a i) y \ 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 \ Basis" ``` lp15@67996 ` 342` ``` then have xyj: "\x \ j - y \ j\ \ dist y x" ``` lp15@67996 ` 343` ``` by (metis Basis_le_norm dist_commute dist_norm inner_diff_left) ``` lp15@67996 ` 344` ``` have "l \ j \ x \ j" ``` lp15@67996 ` 345` ``` using \j \ Basis\ mem_box \x \ cbox l u\ by blast ``` lp15@67996 ` 346` ``` also have "\ \ y \ j + 6 * r i" ``` lp15@67996 ` 347` ``` using d6 xyj by (auto simp: algebra_simps) ``` lp15@67996 ` 348` ``` also have "\ \ y \ j + 6" ``` lp15@67996 ` 349` ``` using r01 [of i] \C \ K\ \i \ C\ by auto ``` lp15@67996 ` 350` ``` finally have l: "l \ j \ y \ j + 6" . ``` lp15@67996 ` 351` ``` have "y \ j \ x \ j + 6 * r i" ``` lp15@67996 ` 352` ``` using d6 xyj by (auto simp: algebra_simps) ``` lp15@67996 ` 353` ``` also have "\ \ u \ j + 6 * r i" ``` lp15@67996 ` 354` ``` using j x by (auto simp: mem_box) ``` lp15@67996 ` 355` ``` also have "\ \ u \ j + 6" ``` lp15@67996 ` 356` ``` using r01 [of i] \C \ K\ \i \ C\ by auto ``` lp15@67996 ` 357` ``` finally have u: "y \ j \ u \ j + 6" . ``` lp15@67996 ` 358` ``` show "l \ j \ y \ j + 6 \ y \ j \ u \ j + 6" ``` lp15@67996 ` 359` ``` using l u by blast ``` lp15@67996 ` 360` ``` qed ``` lp15@67996 ` 361` ``` qed ``` lp15@67996 ` 362` ``` then show "(\i\D. cball (a i) (r i)) \ 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 "(\i\D. cball (a i) (r i)) \ sets lebesgue" ``` lp15@67996 ` 365` ``` using \countable D\ by auto ``` lp15@67996 ` 366` ``` qed ``` lp15@67996 ` 367` ``` obtain D1 where "D1 \ D" "finite D1" ``` lp15@67996 ` 368` ``` and measD1: "?\ (\i\D. cball (a i) (r i)) - e / 5 ^ DIM('n) < ?\ (\i\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 ((\i. cball (a i) (r i)) ` D)" ``` lp15@67996 ` 371` ``` using \countable D\ by auto ``` lp15@67996 ` 372` ``` show "\d. d \ (\i. cball (a i) (r i)) ` D \ d \ lmeasurable" ``` lp15@67996 ` 373` ``` by auto ``` lp15@67996 ` 374` ``` show "\D'. \D' \ (\i. cball (a i) (r i)) ` D; finite D'\ \ ?\ (\D') \ ?\ (\i\D. cball (a i) (r i))" ``` lp15@67996 ` 375` ``` by (fastforce simp add: intro!: measure_mono_fmeasurable UD) ``` lp15@67996 ` 376` ``` qed (use \e > 0\ in \auto dest: finite_subset_image\) ``` lp15@67996 ` 377` ``` show "\T. (S - (\i\C. cball (a i) (r i))) \ ``` lp15@67996 ` 378` ``` cbox l u \ T \ T \ lmeasurable \ ?\ T \ e" ``` lp15@67996 ` 379` ``` proof (intro exI conjI) ``` lp15@67996 ` 380` ``` show "(S - (\i\C. cball (a i) (r i))) \ cbox l u \ (\i\D - D1. ball (a i) (5 * r i))" ``` lp15@67996 ` 381` ``` proof clarify ``` lp15@67996 ` 382` ``` fix x ``` lp15@67996 ` 383` ``` assume x: "x \ cbox l u" "x \ S" "x \ (\i\C. cball (a i) (r i))" ``` lp15@67996 ` 384` ``` have "closed (\i\D1. cball (a i) (r i))" ``` lp15@67996 ` 385` ``` using \finite D1\ by blast ``` lp15@67996 ` 386` ``` moreover have "x \ (\j\D1. cball (a j) (r j))" ``` lp15@67996 ` 387` ``` using x \D1 \ D\ unfolding D_def by blast ``` lp15@67996 ` 388` ``` ultimately obtain q where "q > 0" and q: "ball x q \ - (\i\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 \ K" and xi: "x \ cball (a i) (r i)" and ri: "r i < q/2" ``` lp15@67996 ` 391` ``` using Sd [OF \x \ S\] \q > 0\ half_gt_zero by blast ``` lp15@67996 ` 392` ``` then obtain j where "j \ C" ``` lp15@67996 ` 393` ``` and nondisj: "\ disjnt (cball (a i) (r i)) (cball (a j) (r j))" ``` lp15@67996 ` 394` ``` and sub5j: "cball (a i) (r i) \ ball (a j) (5 * r j)" ``` lp15@67996 ` 395` ``` using cov [OF \i \ K\] by metis ``` lp15@67996 ` 396` ``` show "x \ (\i\D - D1. ball (a i) (5 * r i))" ``` lp15@67996 ` 397` ``` proof ``` lp15@67996 ` 398` ``` show "j \ D - D1" ``` lp15@67996 ` 399` ``` proof ``` lp15@67996 ` 400` ``` show "j \ D" ``` lp15@67996 ` 401` ``` using \j \ C\ sub5j \x \ cbox l u\ xi by (auto simp: D_def disjnt_def) ``` lp15@67996 ` 402` ``` obtain y where yi: "dist (a i) y \ r i" and yj: "dist (a j) y \ r j" ``` lp15@67996 ` 403` ``` using disjnt_def nondisj by fastforce ``` lp15@67996 ` 404` ``` have "dist x y \ 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 "\ < q" ``` lp15@67996 ` 407` ``` using ri by linarith ``` lp15@67996 ` 408` ``` finally have "y \ ball x q" ``` lp15@67996 ` 409` ``` by simp ``` lp15@67996 ` 410` ``` with yj q show "j \ D1" ``` lp15@67996 ` 411` ``` by (auto simp: disjoint_UN_iff) ``` lp15@67996 ` 412` ``` qed ``` lp15@67996 ` 413` ``` show "x \ 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: "?\ (\i\D2. ball (a i) (5 * r i)) \ e" ``` lp15@67996 ` 418` ``` if D2: "D2 \ D - D1" and "finite D2" for D2 ``` lp15@67996 ` 419` ``` proof - ``` lp15@67996 ` 420` ``` have rgt0: "0 < r i" if "i \ D2" for i ``` lp15@67996 ` 421` ``` using \C \ K\ D_def \i \ D2\ D2 r01 ``` lp15@67996 ` 422` ``` by (simp add: subset_iff) ``` lp15@67996 ` 423` ``` then have inj: "inj_on (\i. ball (a i) (5 * r i)) D2" ``` lp15@67996 ` 424` ``` using \C \ K\ D2 by (fastforce simp: inj_on_def D_def ball_eq_ball_iff intro: ar_injective) ``` lp15@67996 ` 425` ``` have "?\ (\i\D2. ball (a i) (5 * r i)) \ sum (?\) ((\i. ball (a i) (5 * r i)) ` D2)" ``` lp15@67996 ` 426` ``` using that by (force intro: measure_Union_le) ``` lp15@67996 ` 427` ``` also have "\ = (\i\D2. ?\ (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 "\ = (\i\D2. 5 ^ DIM('n) * ?\ (ball (a i) (r i)))" ``` lp15@67996 ` 430` ``` proof (rule sum.cong [OF refl]) ``` lp15@67996 ` 431` ``` fix i ``` lp15@67996 ` 432` ``` assume "i \ D2" ``` lp15@67996 ` 433` ``` show "?\ (ball (a i) (5 * r i)) = 5 ^ DIM('n) * ?\ (ball (a i) (r i))" ``` lp15@67996 ` 434` ``` using rgt0 [OF \i \ D2\] by (simp add: content_ball) ``` lp15@67996 ` 435` ``` qed ``` lp15@67996 ` 436` ``` also have "\ = (\i\D2. ?\ (ball (a i) (r i))) * 5 ^ DIM('n)" ``` lp15@67996 ` 437` ``` by (simp add: sum_distrib_left mult.commute) ``` lp15@67996 ` 438` ``` finally have "?\ (\i\D2. ball (a i) (5 * r i)) \ (\i\D2. ?\ (ball (a i) (r i))) * 5 ^ DIM('n)" . ``` lp15@67996 ` 439` ``` moreover have "(\i\D2. ?\ (ball (a i) (r i))) \ e / 5 ^ DIM('n)" ``` lp15@67996 ` 440` ``` proof - ``` lp15@67996 ` 441` ``` have D12_dis: "((\x\D1. cball (a x) (r x)) \ (\x\D2. cball (a x) (r x))) \ {}" ``` lp15@67996 ` 442` ``` proof clarify ``` lp15@67996 ` 443` ``` fix w d1 d2 ``` lp15@67996 ` 444` ``` assume "d1 \ D1" "w d1 d2 \ cball (a d1) (r d1)" "d2 \ D2" "w d1 d2 \ cball (a d2) (r d2)" ``` lp15@67996 ` 445` ``` then show "w d1 d2 \ {}" ``` lp15@67996 ` 446` ``` by (metis DiffE disjnt_iff subsetCE D2 \D1 \ D\ \D \ C\ pairwiseD [OF pwC, of d1 d2]) ``` lp15@67996 ` 447` ``` qed ``` lp15@67996 ` 448` ``` have inj: "inj_on (\i. cball (a i) (r i)) D2" ``` lp15@67996 ` 449` ``` using rgt0 D2 \D \ C\ by (force simp: inj_on_def cball_eq_cball_iff intro!: ar_injective) ``` lp15@67996 ` 450` ``` have ds: "disjoint ((\i. cball (a i) (r i)) ` D2)" ``` lp15@67996 ` 451` ``` using D2 \D \ C\ by (auto intro: pairwiseI pairwiseD [OF pwC]) ``` lp15@67996 ` 452` ``` have "(\i\D2. ?\ (ball (a i) (r i))) = (\i\D2. ?\ (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 "\ = sum ?\ ((\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 "\ = ?\ (\i\D2. cball (a i) (r i))" ``` lp15@67996 ` 457` ``` by (auto intro: measure_Union' [symmetric] ds simp add: \finite D2\) ``` lp15@67996 ` 458` ``` finally have "?\ (\i\D1. cball (a i) (r i)) + (\i\D2. ?\ (ball (a i) (r i))) = ``` lp15@67996 ` 459` ``` ?\ (\i\D1. cball (a i) (r i)) + ?\ (\i\D2. cball (a i) (r i))" ``` lp15@67996 ` 460` ``` by simp ``` lp15@67996 ` 461` ``` also have "\ = ?\ (\i \ D1 \ D2. cball (a i) (r i))" ``` lp15@67996 ` 462` ``` using D12_dis by (simp add: measure_Un3 \finite D1\ \finite D2\ fmeasurable.finite_UN) ``` lp15@67996 ` 463` ``` also have "\ \ ?\ (\i\D. cball (a i) (r i))" ``` lp15@67996 ` 464` ``` using D2 \D1 \ D\ by (fastforce intro!: measure_mono_fmeasurable [OF _ _ UD] \finite D1\ \finite D2\) ``` lp15@67996 ` 465` ``` finally have "?\ (\i\D1. cball (a i) (r i)) + (\i\D2. ?\ (ball (a i) (r i))) \ ?\ (\i\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: \countable D\) ``` lp15@67996 ` 474` ``` show "(\i\D - D1. ball (a i) (5 * r i)) \ lmeasurable" ``` lp15@67996 ` 475` ``` using \e > 0\ by (auto simp: fmeasurable_UN_bound [OF co _ 3]) ``` lp15@67996 ` 476` ``` show "?\ (\i\D - D1. ball (a i) (5 * r i)) \ e" ``` lp15@67996 ` 477` ``` using \e > 0\ 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' \ {i \ K. r i \ 1}" ``` lp15@67996 ` 484` ``` have 1: "\i. i \ K' \ 0 < r i \ r i \ 1" ``` lp15@67996 ` 485` ``` using K'_def r by auto ``` lp15@67996 ` 486` ``` have 2: "\i. i \ K' \ x \ cball (a i) (r i) \ r i < d" ``` lp15@67996 ` 487` ``` if "x \ S \ 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' \ 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@68833 ` 496` ```proposition%important Vitali_covering_theorem_balls: ``` lp15@67996 ` 497` ``` fixes a :: "'a \ 'b::euclidean_space" ``` lp15@67996 ` 498` ``` assumes S: "\x d. \x \ S; 0 < d\ \ \i. i \ K \ x \ ball (a i) (r i) \ r i < d" ``` lp15@67996 ` 499` ``` obtains C where "countable C" "C \ K" ``` lp15@67996 ` 500` ``` "pairwise (\i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C" ``` lp15@67996 ` 501` ``` "negligible(S - (\i \ C. ball (a i) (r i)))" ``` ak2110@68833 ` 502` ```proof%unimportant - ``` lp15@67996 ` 503` ``` have 1: "\i. i \ {i \ K. 0 < r i} \ x \ cball (a i) (r i) \ r i < d" ``` lp15@67996 ` 504` ``` if xd: "x \ 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 \ K" ``` lp15@67996 ` 507` ``` and pw: "pairwise (\i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C" ``` lp15@67996 ` 508` ``` and neg: "negligible(S - (\i \ C. cball (a i) (r i)))" ``` lp15@67996 ` 509` ``` by (rule Vitali_covering_theorem_cballs [of "{i \ K. 0 < r i}" r S a, OF _ 1]) auto ``` lp15@67996 ` 510` ``` show thesis ``` lp15@67996 ` 511` ``` proof ``` lp15@67996 ` 512` ``` show "pairwise (\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 (\i\C. sphere (a i) (r i))" ``` lp15@67996 ` 517` ``` by (auto intro: negligible_sphere \countable C\) ``` lp15@67996 ` 518` ``` then have "negligible (S - (\i \ C. cball(a i)(r i)) \ (\i \ C. sphere (a i) (r i)))" ``` lp15@67996 ` 519` ``` by (rule negligible_Un [OF neg]) ``` lp15@67996 ` 520` ``` then show "negligible (S - (\i\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@68833 ` 526` ```lemma%unimportant negligible_eq_zero_density_alt: ``` lp15@67996 ` 527` ``` "negligible S \ ``` lp15@67996 ` 528` ``` (\x \ S. \e > 0. ``` lp15@67996 ` 529` ``` \d U. 0 < d \ d \ e \ S \ ball x d \ U \ ``` lp15@67996 ` 530` ``` U \ lmeasurable \ measure lebesgue U < e * measure lebesgue (ball x d))" ``` lp15@67996 ` 531` ``` (is "_ = (\x \ S. \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 \ S" and "e > 0" ``` lp15@67996 ` 535` ``` then ``` lp15@67996 ` 536` ``` show "\d U. 0 < d \ d \ e \ S \ ball x d \ U \ U \ lmeasurable \ ``` 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 \ 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]: "\x \ S. \e > 0. ?Q x e" ``` lp15@67996 ` 544` ``` let ?\ = "measure lebesgue" ``` lp15@67996 ` 545` ``` have "\U. openin (subtopology euclidean S) U \ z \ U \ negligible U" ``` lp15@67996 ` 546` ``` if "z \ S" for z ``` lp15@67996 ` 547` ``` proof (intro exI conjI) ``` lp15@67996 ` 548` ``` show "openin (subtopology euclidean S) (S \ ball z 1)" ``` lp15@67996 ` 549` ``` by (simp add: openin_open_Int) ``` lp15@67996 ` 550` ``` show "z \ S \ ball z 1" ``` lp15@67996 ` 551` ``` using \z \ S\ by auto ``` lp15@67996 ` 552` ``` show "negligible (S \ 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 \ S \ 0 < d \ ball x d \ ball z 1 \ ``` lp15@67996 ` 557` ``` (\U. S \ ball x d \ U \ U \ lmeasurable \ ``` lp15@67996 ` 558` ``` ?\ U < e / ?\ (ball z 1) * ?\ (ball x d))}" ``` lp15@67996 ` 559` ``` obtain C where "countable C" and Csub: "C \ ?K" ``` lp15@67996 ` 560` ``` and pwC: "pairwise (\i j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C" ``` lp15@67996 ` 561` ``` and negC: "negligible((S \ ball z 1) - (\i \ C. ball (fst i) (snd i)))" ``` lp15@67996 ` 562` ``` proof (rule Vitali_covering_theorem_balls [of "S \ ball z 1" ?K fst snd]) ``` lp15@67996 ` 563` ``` fix x and d :: "real" ``` lp15@67996 ` 564` ``` assume x: "x \ S \ ball z 1" and "d > 0" ``` lp15@67996 ` 565` ``` obtain k where "k > 0" and k: "ball x k \ ball z 1" ``` lp15@67996 ` 566` ``` by (meson Int_iff open_ball openE x) ``` lp15@67996 ` 567` ``` let ?\ = "min (e / ?\ (ball z 1) / 2) (min (d / 2) k)" ``` lp15@67996 ` 568` ``` obtain r U where r: "r > 0" "r \ ?\" and U: "S \ ball x r \ U" "U \ lmeasurable" ``` lp15@67996 ` 569` ``` and mU: "?\ U < ?\ * ?\ (ball x r)" ``` lp15@67996 ` 570` ``` using R [of x ?\] \d > 0\ \e > 0\ \k > 0\ x by auto ``` lp15@67996 ` 571` ``` show "\i. i \ ?K \ x \ ball (fst i) (snd i) \ snd i < d" ``` lp15@67996 ` 572` ``` proof (rule exI [of _ "(x,r)"], simp, intro conjI exI) ``` lp15@67996 ` 573` ``` have "ball x r \ ball x k" ``` lp15@67996 ` 574` ``` using r by (simp add: ball_subset_ball_iff) ``` lp15@67996 ` 575` ``` also have "\ \ ball z 1" ``` lp15@67996 ` 576` ``` using ball_subset_ball_iff k by auto ``` lp15@67996 ` 577` ``` finally show "ball x r \ ball z 1" . ``` lp15@67996 ` 578` ``` have "?\ * ?\ (ball x r) \ e * content (ball x r) / content (ball z 1)" ``` lp15@67996 ` 579` ``` using r \e > 0\ by (simp add: ord_class.min_def divide_simps) ``` lp15@67996 ` 580` ``` with mU show "?\ 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 "\U. case p of (x,d) \ S \ ball x d \ U \ ``` lp15@67996 ` 585` ``` U \ lmeasurable \ ?\ U < e / ?\ (ball z 1) * ?\ (ball x d)" ``` lp15@67996 ` 586` ``` if "p \ C" for p ``` lp15@67996 ` 587` ``` using that Csub by auto ``` lp15@67996 ` 588` ``` then obtain U where U: ``` lp15@67996 ` 589` ``` "\p. p \ C \ ``` lp15@67996 ` 590` ``` case p of (x,d) \ S \ ball x d \ U p \ ``` lp15@67996 ` 591` ``` U p \ lmeasurable \ ?\ (U p) < e / ?\ (ball z 1) * ?\ (ball x d)" ``` lp15@67996 ` 592` ``` by (rule that [OF someI_ex]) ``` lp15@67996 ` 593` ``` let ?T = "((S \ ball z 1) - (\(x,d)\C. ball x d)) \ \(U ` C)" ``` lp15@67996 ` 594` ``` show "\T. S \ ball z 1 \ T \ T \ lmeasurable \ ?\ T \ e" ``` lp15@67996 ` 595` ``` proof (intro exI conjI) ``` lp15@67996 ` 596` ``` show "S \ ball z 1 \ ?T" ``` lp15@67996 ` 597` ``` using U by fastforce ``` lp15@67996 ` 598` ``` { have Um: "U i \ lmeasurable" if "i \ C" for i ``` lp15@67996 ` 599` ``` using that U by blast ``` lp15@67996 ` 600` ``` have lee: "?\ (\i\I. U i) \ e" if "I \ C" "finite I" for I ``` lp15@67996 ` 601` ``` proof - ``` lp15@67996 ` 602` ``` have "?\ (\(x,d)\I. ball x d) \ ?\ (ball z 1)" ``` lp15@67996 ` 603` ``` apply (rule measure_mono_fmeasurable) ``` lp15@67996 ` 604` ``` using \I \ C\ \finite I\ Csub by (force simp: prod.case_eq_if sets.finite_UN)+ ``` lp15@67996 ` 605` ``` then have le1: "(?\ (\(x,d)\I. ball x d) / ?\ (ball z 1)) \ 1" ``` lp15@67996 ` 606` ``` by simp ``` lp15@67996 ` 607` ``` have "?\ (\i\I. U i) \ (\i\I. ?\ (U i))" ``` lp15@67996 ` 608` ``` using that U by (blast intro: measure_UNION_le) ``` lp15@67996 ` 609` ``` also have "\ \ (\(x,r)\I. e / ?\ (ball z 1) * ?\ (ball x r))" ``` lp15@67996 ` 610` ``` by (rule sum_mono) (use \I \ C\ U in force) ``` lp15@67996 ` 611` ``` also have "\ = (e / ?\ (ball z 1)) * (\(x,r)\I. ?\ (ball x r))" ``` lp15@67996 ` 612` ``` by (simp add: case_prod_app prod.case_distrib sum_distrib_left) ``` lp15@67996 ` 613` ``` also have "\ = e * (?\ (\(x,r)\I. ball x r) / ?\ (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 "\ \ e" ``` lp15@67996 ` 617` ``` by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \e > 0\ le1) ``` lp15@67996 ` 618` ``` finally show ?thesis . ``` lp15@67996 ` 619` ``` qed ``` haftmann@69313 ` 620` ``` have "\(U ` C) \ lmeasurable" "?\ (\(U ` C)) \ e" ``` lp15@67996 ` 621` ``` using \e > 0\ Um lee ``` lp15@67996 ` 622` ``` by(auto intro!: fmeasurable_UN_bound [OF \countable C\] measure_UN_bound [OF \countable C\]) ``` lp15@67996 ` 623` ``` } ``` haftmann@69313 ` 624` ``` moreover have "?\ ?T = ?\ (\(U ` C))" ``` haftmann@69313 ` 625` ``` proof (rule measure_negligible_symdiff [OF \\(U ` C) \ lmeasurable\]) ``` haftmann@69313 ` 626` ``` show "negligible((\(U ` C) - ?T) \ (?T - \(U ` C)))" ``` lp15@67996 ` 627` ``` by (force intro!: negligible_subset [OF negC]) ``` lp15@67996 ` 628` ``` qed ``` lp15@67996 ` 629` ``` ultimately show "?T \ lmeasurable" "?\ ?T \ 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@68833 ` 638` ```proposition%important negligible_eq_zero_density: ``` lp15@67996 ` 639` ``` "negligible S \ ``` lp15@67996 ` 640` ``` (\x\S. \r>0. \e>0. \d. 0 < d \ d \ r \ ``` lp15@67996 ` 641` ``` (\U. S \ ball x d \ U \ U \ lmeasurable \ measure lebesgue U < e * measure lebesgue (ball x d)))" ``` ak2110@68833 ` 642` ```proof%unimportant - ``` lp15@67996 ` 643` ``` let ?Q = "\x d e. \U. S \ ball x d \ U \ U \ lmeasurable \ measure lebesgue U < e * content (ball x d)" ``` lp15@67996 ` 644` ``` have "(\e>0. \d>0. d \ e \ ?Q x d e) = (\r>0. \e>0. \d>0. d \ r \ ?Q x d e)" ``` lp15@67996 ` 645` ``` if "x \ 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]: "\e>0. \d>0. d \ e \ ?Q x d e" and "r > 0" "e > 0" ``` lp15@67996 ` 649` ``` show "\d>0. d \ r \ ?Q x d e" ``` lp15@67996 ` 650` ``` using L [of "min r e"] apply (rule ex_forward) ``` lp15@67996 ` 651` ``` using \r > 0\ \e > 0\ 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 ```