(* Title: HOL/Analysis/Vitali_Covering_Theorem.thy
Authors: LC Paulson, based on material from HOL Light
*)
section \<open>Vitali Covering Theorem and an Application to Negligibility\<close>
theory Vitali_Covering_Theorem
imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Permutations"
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 $ Fun.swap m n id i) \ (\ i. x $ Fun.swap m n id 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 \
\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
cball (a i) (r i) \<subseteq> 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 \
(\<forall>i \<in> C n. B/2 ^ n \<le> r i) \<and> ?djnt (C n) \<and>
(\<forall>i \<in> K. B/2 ^ n < r i
\<longrightarrow> (\<exists>j. j \<in> C n \<and>
\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)))) \<and> (C n \<subseteq> 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) \<subseteq> 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\<^sub>\ 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 \<open>chain\<^sub>\<subseteq> C\<close> chain_subset_def)
then show "disjnt (cball (a x) (r x)) (cball (a y) (r y))"
proof cases
case 1
with C XY \<open>x \<noteq> y\<close> show ?thesis
unfolding pairwise_def by blast
next
case 2
with C XY \<open>x \<noteq> y\<close> 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 \
(\<forall>i\<in>L. B/2 ^ Suc n \<le> r i) \<and> ?djnt L \<and>
(\<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"
proof (intro exI conjI ballI)
show "C \ E \ K"
using D_def \<open>C \<subseteq> K\<close> \<open>E \<subseteq> D\<close> 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 \<open>B > 0\<close> by (simp add: field_split_simps)
also have "\ \ r i"
using Ble \<open>i \<in> C\<close> by blast
finally show ?thesis .
qed (use D_def \<open>E \<subseteq> D\<close> in auto)
show "?djnt (C \ E)"
using D_def \<open>C \<subseteq> K\<close> \<open>E \<subseteq> D\<close> 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 \<open>i \<in> K\<close> 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 \<open>j \<in> C\<close> 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 \<open>E \<subseteq> D\<close> 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 \<open>E \<subseteq> D\<close>)
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 \<open>i \<in> K\<close> assms by fastforce
next
case False
with that show ?thesis
by (auto simp: D_def disjnt_def \<open>i \<in> K\<close>)
qed
qed
ultimately
show "B/2 ^ Suc n < r i \
(\<exists>j. j \<in> C \<union> E \<and>
\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
cball (a i) (r i) \<subseteq> 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\
\<Longrightarrow> \<exists>j. j \<in> F n \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
cball (a i) (r i) \<subseteq> 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 \<open>I \<subseteq> K\<close>
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 \<open>I \<subseteq> K\<close> 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 \<open>I \<subseteq> K\<close> 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\<^sub>\ (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 \<open>B > 0\<close> assms real_arch_pow_inv by fastforce
then have B2: "B/2 ^ n < r i"
using \<open>B > 0\<close> by (simp add: field_split_simps)
have "0 < r i" "r i \ B"
by (auto simp: \<open>i \<in> K\<close> assms)
show "\j. j \ (Union(range F)) \
\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
using FF [OF \<open>i \<in> K\<close> B2] by auto
qed
qed
subsection\<open>Vitali covering theorem\<close>
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) \<subseteq> 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) \<subseteq> 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\
\<Longrightarrow> \<exists>i. i \<in> K \<and> x \<in> cball (a i) (r i) \<and> 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 ?\<mu> = "measure lebesgue"
have *: "\C. countable C \ C \ K \
pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C \<and>
negligible(S - (\<Union>i \<in> 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) \<subseteq> 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 \<open>C \<subseteq> K\<close> 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 \<open>countable C\<close> by simp
have UD: "(\i\D. cball (a i) (r i)) \ lmeasurable"
proof (rule fmeasurableI2)
show "cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>R One) \ lmeasurable"
by blast
have "y \ cbox (l - 6 *\<^sub>R One) (u + 6 *\<^sub>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 \<open>j \<in> Basis\<close> mem_box \<open>x \<in> cbox l u\<close> 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] \<open>C \<subseteq> K\<close> \<open>i \<in> C\<close> 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] \<open>C \<subseteq> K\<close> \<open>i \<in> C\<close> 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 *\<^sub>R One) (u + 6 *\<^sub>R One)"
by (force simp: D_def disjnt_def)
show "(\i\D. cball (a i) (r i)) \ sets lebesgue"
using \<open>countable D\<close> 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 \<open>countable D\<close> 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 \<open>e > 0\<close> in \<open>auto dest: finite_subset_image\<close>)
show "\T. (S - (\i\C. cball (a i) (r i))) \
cbox l u \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> 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 \<open>finite D1\<close> by blast
moreover have "x \ (\j\D1. cball (a j) (r j))"
using x \<open>D1 \<subseteq> D\<close> 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 \<open>x \<in> S\<close>] \<open>q > 0\<close> 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 \<open>i \<in> K\<close>] by metis
show "x \ (\i\D - D1. ball (a i) (5 * r i))"
proof
show "j \ D - D1"
proof
show "j \ D"
using \<open>j \<in> C\<close> sub5j \<open>x \<in> cbox l u\<close> 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 \<open>C \<subseteq> K\<close> D_def \<open>i \<in> D2\<close> D2 r01
by (simp add: subset_iff)
then have inj: "inj_on (\i. ball (a i) (5 * r i)) D2"
using \<open>C \<subseteq> K\<close> 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 \<open>D1 \<subseteq> D\<close> \<open>D \<subseteq> C\<close> pairwiseD [OF pwC, of d1 d2])
qed
have inj: "inj_on (\i. cball (a i) (r i)) D2"
using rgt0 D2 \<open>D \<subseteq> C\<close> 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 \<open>D \<subseteq> C\<close> 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))) =
?\<mu> (\<Union>i\<in>D1. cball (a i) (r i)) + ?\<mu> (\<Union>i\<in>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 \<open>finite D1\<close> \<open>finite D2\<close> fmeasurable.finite_UN)
also have "\ \ ?\ (\i\D. cball (a i) (r i))"
using D2 \<open>D1 \<subseteq> D\<close> by (fastforce intro!: measure_mono_fmeasurable [OF _ _ UD] \<open>finite D1\<close> \<open>finite D2\<close>)
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: \<open>countable D\<close>)
show "(\i\D - D1. ball (a i) (5 * r i)) \ lmeasurable"
using \<open>e > 0\<close> by (auto simp: fmeasurable_UN_bound [OF co _ 3])
show "?\ (\i\D - D1. ball (a i) (5 * r i)) \ e"
using \<open>e > 0\<close> by (auto simp: measure_UN_bound [OF co _ 3])
qed
qed
qed
qed (use C pwC in auto)
qed
define K' where "K' \<equiv> {i \<in> K. r i \<le> 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 \<open>countable C\<close>)
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 \
(\<forall>x \<in> S. \<forall>e > 0.
\<exists>d U. 0 < d \<and> d \<le> e \<and> S \<inter> ball x d \<subseteq> U \<and>
U \<in> lmeasurable \<and> 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 ?\<mu> = "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 \<open>z \<in> S\<close> 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 \
(\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and>
?\<mu> U < e / ?\<mu> (ball z 1) * ?\<mu> (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 ?\<epsilon> = "min (e / ?\<mu> (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 ?\<epsilon>] \<open>d > 0\<close> \<open>e > 0\<close> \<open>k > 0\<close> 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 \<open>e > 0\<close> 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 \<in> lmeasurable \<and> ?\<mu> U < e / ?\<mu> (ball z 1) * ?\<mu> (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) \<Rightarrow> S \<inter> ball x d \<subseteq> U p \<and>
U p \<in> lmeasurable \<and> ?\<mu> (U p) < e / ?\<mu> (ball z 1) * ?\<mu> (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 \<open>I \<subseteq> C\<close> \<open>finite I\<close> 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 \<open>I \<subseteq> C\<close> 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 \<open>e > 0\<close> le1)
finally show ?thesis .
qed
have "\(U ` C) \ lmeasurable" "?\ (\(U ` C)) \ e"
using \<open>e > 0\<close> Um lee
by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>])
}
moreover have "?\ ?T = ?\ (\(U ` C))"
proof (rule measure_negligible_symdiff [OF \<open>\<Union>(U ` C) \<in> lmeasurable\<close>])
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 \
(\<forall>x\<in>S. \<forall>r>0. \<forall>e>0. \<exists>d. 0 < d \<and> d \<le> r \<and>
(\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and> 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 \<open>r > 0\<close> \<open>e > 0\<close> 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
¤ Dauer der Verarbeitung: 0.35 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
