(* 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_iff1 ‹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