Quelle Vitali_Covering_Theorem.thy Sprache: Isabelle

(*  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
  "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 \
                        \<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_right_pos \<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

quality99%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.