# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1575292923 -3600
# Node ID a8ccea88b7250a9b4624a8ea9e892448f1ce3c02
# Parent  6695aeae8ec99ca36776a4b1b4ea3ba56c2f028b
Flattened dependency tree of HOL-Analysis

diff -r 6695aeae8ec9 -r a8ccea88b725 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Mon Dec 02 10:31:51 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Mon Dec 02 14:22:03 2019 +0100
@@ -504,11 +504,12 @@
           have neg: "negligible (frontier (f' x ` ball 0 1))"
             using deriv has_derivative_linear \<open>x \<in> S\<close>
             by (auto intro!: negligible_convex_frontier [OF convex_linear_image])
-          have 0: "0 < e * unit_ball_vol (real CARD('n))"
-            using  \<open>e > 0\<close> by simp
+          let ?unit_vol = "content (ball (0 :: real ^ 'n :: {finite, wellorder}) 1)"
+          have 0: "0 < e * ?unit_vol"
+            using \<open>e > 0\<close> by (simp add: content_ball_pos)
           obtain k where "k > 0" and k:
                   "\<And>U. \<lbrakk>U \<in> lmeasurable; \<And>y. y \<in> U \<Longrightarrow> \<exists>z. z \<in> f' x ` ball 0 1 \<and> dist z y < k\<rbrakk>
-                        \<Longrightarrow> ?\<mu> U < ?\<mu> (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))"
+                        \<Longrightarrow> ?\<mu> U < ?\<mu> (f' x ` ball 0 1) + e * ?unit_vol"
             using measure_semicontinuous_with_hausdist_explicit [OF bo neg 0] by blast
           obtain l where "l > 0" and l: "ball x l \<subseteq> T"
             using \<open>x \<in> S\<close> \<open>open T\<close> \<open>S \<subseteq> T\<close> openE by blast
@@ -577,17 +578,18 @@
             have "?\<mu> (f ` (S \<inter> ball x r)) = ?\<mu> (?rfs) * r ^ CARD('n)"
               using \<open>r > 0\<close> fsb
               by (simp add: measure_linear_image measure_translation_subtract measurable_translation_subtract field_simps cong: image_cong_simp)
-            also have "\<dots> \<le> (\<bar>det (matrix (f' x))\<bar> * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))) * r ^ CARD('n)"
+            also have "\<dots> \<le> (\<bar>det (matrix (f' x))\<bar> * ?unit_vol + e * ?unit_vol) * r ^ CARD('n)"
             proof -
-              have "?\<mu> (?rfs) < ?\<mu> (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))"
+              have "?\<mu> (?rfs) < ?\<mu> (f' x ` ball 0 1) + e * ?unit_vol"
                 using rfs_mble by (force intro: k dest!: ex_lessK)
-              then have "?\<mu> (?rfs) < \<bar>det (matrix (f' x))\<bar> * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))"
-                by (simp add: lin measure_linear_image [of "f' x"] content_ball)
+              then have "?\<mu> (?rfs) < \<bar>det (matrix (f' x))\<bar> * ?unit_vol + e * ?unit_vol"
+                by (simp add: lin measure_linear_image [of "f' x"])
               with \<open>r > 0\<close> show ?thesis
                 by auto
             qed
             also have "\<dots> \<le> (B + e) * ?\<mu> (ball x r)"
-              using bounded [OF \<open>x \<in> S\<close>] \<open>r > 0\<close> by (simp add: content_ball algebra_simps)
+              using bounded [OF \<open>x \<in> S\<close>] \<open>r > 0\<close>
+              by (simp add: algebra_simps content_ball_conv_unit_ball[of r] content_ball_pos)
             finally show "?\<mu> (f ` (S \<inter> ball x r)) \<le> (B + e) * ?\<mu> (ball x r)" .
           qed
         qed
@@ -1453,9 +1455,11 @@
               by (simp add: abs_diff_le_iff abs_minus_commute)
           qed (use \<open>e > 0\<close> in auto)
           also have "\<dots> < e * content (cball ?x' (min d r))"
-            using \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> by auto
+            using \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> by (auto intro: content_cball_pos)
           also have "\<dots> = e * content (ball x (min d r))"
-            using \<open>r > 0\<close> \<open>d > 0\<close> by (simp add: content_cball content_ball)
+            using \<open>r > 0\<close> \<open>d > 0\<close> content_ball_conv_unit_ball[of "min d r" "inv T x"]
+                  content_ball_conv_unit_ball[of "min d r" x]
+            by (simp add: content_cball_conv_ball)
           finally show "measure lebesgue ?W < e * content (ball x (min d r))" .
       qed
     qed
diff -r 6695aeae8ec9 -r a8ccea88b725 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Dec 02 10:31:51 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Dec 02 14:22:03 2019 +0100
@@ -230,6 +230,61 @@
 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
   using cball_divide_subset one_le_numeral by blast
 
+lemma cball_scale:
+  assumes "a \<noteq> 0"
+  shows   "(\<lambda>x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\<bar>a\<bar> * r)"
+proof -
+  have 1: "(\<lambda>x. a *\<^sub>R x) ` cball c r \<subseteq> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)" if "a \<noteq> 0" for a r and c :: 'a
+  proof safe
+    fix x
+    assume x: "x \<in> cball c r"
+    have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
+      by (auto simp: dist_norm)
+    also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
+      by (simp add: algebra_simps)
+    finally show "a *\<^sub>R x \<in> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+      using that x by (auto simp: dist_norm)
+  qed
+
+  have "cball (a *\<^sub>R c) (\<bar>a\<bar> * r) = (\<lambda>x. a *\<^sub>R x) ` (\<lambda>x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+    unfolding image_image using assms by simp
+  also have "\<dots> \<subseteq> (\<lambda>x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\<bar>inverse a\<bar> * (\<bar>a\<bar> * r))"
+    using assms by (intro image_mono 1) auto
+  also have "\<dots> = (\<lambda>x. a *\<^sub>R x) ` cball c r"
+    using assms by (simp add: algebra_simps)
+  finally have "cball (a *\<^sub>R c) (\<bar>a\<bar> * r) \<subseteq> (\<lambda>x. a *\<^sub>R x) ` cball c r" .
+  moreover from assms have "(\<lambda>x. a *\<^sub>R x) ` cball c r \<subseteq> cball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+    by (intro 1) auto
+  ultimately show ?thesis by blast
+qed
+
+lemma ball_scale:
+  assumes "a \<noteq> 0"
+  shows   "(\<lambda>x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\<bar>a\<bar> * r)"
+proof -
+  have 1: "(\<lambda>x. a *\<^sub>R x) ` ball c r \<subseteq> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)" if "a \<noteq> 0" for a r and c :: 'a
+  proof safe
+    fix x
+    assume x: "x \<in> ball c r"
+    have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
+      by (auto simp: dist_norm)
+    also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
+      by (simp add: algebra_simps)
+    finally show "a *\<^sub>R x \<in> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+      using that x by (auto simp: dist_norm)
+  qed
+
+  have "ball (a *\<^sub>R c) (\<bar>a\<bar> * r) = (\<lambda>x. a *\<^sub>R x) ` (\<lambda>x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+    unfolding image_image using assms by simp
+  also have "\<dots> \<subseteq> (\<lambda>x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\<bar>inverse a\<bar> * (\<bar>a\<bar> * r))"
+    using assms by (intro image_mono 1) auto
+  also have "\<dots> = (\<lambda>x. a *\<^sub>R x) ` ball c r"
+    using assms by (simp add: algebra_simps)
+  finally have "ball (a *\<^sub>R c) (\<bar>a\<bar> * r) \<subseteq> (\<lambda>x. a *\<^sub>R x) ` ball c r" .
+  moreover from assms have "(\<lambda>x. a *\<^sub>R x) ` ball c r \<subseteq> ball (a *\<^sub>R c) (\<bar>a\<bar> * r)"
+    by (intro 1) auto
+  ultimately show ?thesis by blast
+qed
 
 subsection \<open>Limit Points\<close>
 
diff -r 6695aeae8ec9 -r a8ccea88b725 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Dec 02 10:31:51 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Dec 02 14:22:03 2019 +0100
@@ -1561,6 +1561,15 @@
 lemma measurable_convex: "\<lbrakk>convex S; bounded S\<rbrakk> \<Longrightarrow> S \<in> lmeasurable"
   by (simp add: measurable_Jordan negligible_convex_frontier)
 
+lemma content_cball_conv_ball: "content (cball c r) = content (ball c r)"
+proof -
+  have "ball c r - cball c r \<union> (cball c r - ball c r) = sphere c r"
+    by auto
+  hence "measure lebesgue (cball c r) = measure lebesgue (ball c r)"
+    using negligible_sphere[of c r] by (intro measure_negligible_symdiff) simp_all
+  thus ?thesis by simp
+qed
+
 subsection\<open>Negligibility of image under non-injective linear map\<close>
 
 lemma negligible_Union_nat:
@@ -2902,6 +2911,41 @@
 
 subsection\<open>Transformation of measure by linear maps\<close>
 
+lemma emeasure_lebesgue_ball_conv_unit_ball:
+  fixes c :: "'a :: euclidean_space"
+  assumes "r \<ge> 0"
+  shows "emeasure lebesgue (ball c r) =
+           ennreal (r ^ DIM('a)) * emeasure lebesgue (ball (0 :: 'a) 1)"
+proof (cases "r = 0")
+  case False
+  with assms have r: "r > 0" by auto
+  have "emeasure lebesgue ((\<lambda>x. c + x) ` (\<lambda>x. r *\<^sub>R x) ` ball (0 :: 'a) 1) =
+          r ^ DIM('a) * emeasure lebesgue (ball (0 :: 'a) 1)"
+    unfolding image_image using emeasure_lebesgue_affine[of r c "ball 0 1"] assms
+    by (simp add: add_ac)
+  also have "(\<lambda>x. r *\<^sub>R x) ` ball 0 1 = ball (0 :: 'a) r"
+    using r by (subst ball_scale) auto
+  also have "(\<lambda>x. c + x) ` \<dots> = ball c r"
+    by (subst image_add_ball) (simp_all add: algebra_simps)
+  finally show ?thesis by simp
+qed auto
+
+lemma content_ball_conv_unit_ball:
+  fixes c :: "'a :: euclidean_space"
+  assumes "r \<ge> 0"
+  shows "content (ball c r) = r ^ DIM('a) * content (ball (0 :: 'a) 1)"
+proof -
+  have "ennreal (content (ball c r)) = emeasure lebesgue (ball c r)"
+    using emeasure_lborel_ball_finite[of c r] by (subst emeasure_eq_ennreal_measure) auto
+  also have "\<dots> = ennreal (r ^ DIM('a)) * emeasure lebesgue (ball (0 :: 'a) 1)"
+    using assms by (intro emeasure_lebesgue_ball_conv_unit_ball) auto
+  also have "\<dots> = ennreal (r ^ DIM('a) * content (ball (0::'a) 1))"
+    using emeasure_lborel_ball_finite[of "0::'a" 1] assms
+    by (subst emeasure_eq_ennreal_measure) (auto simp: ennreal_mult')
+  finally show ?thesis 
+    using assms by (subst (asm) ennreal_inj) auto
+qed
+
 lemma measurable_linear_image_interval:
    "linear f \<Longrightarrow> f ` (cbox a b) \<in> lmeasurable"
   by (metis bounded_linear_image linear_linear bounded_cbox closure_bounded_linear_image closure_cbox compact_closure lmeasurable_compact)
diff -r 6695aeae8ec9 -r a8ccea88b725 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Dec 02 10:31:51 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Dec 02 14:22:03 2019 +0100
@@ -128,6 +128,44 @@
   using emeasure_mono[of s "cbox a b" lborel]
   by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
 
+lemma content_ball_pos:
+  assumes "r > 0"
+  shows   "content (ball c r) > 0"
+proof -
+  from rational_boxes[OF assms, of c] obtain a b where ab: "c \<in> box a b" "box a b \<subseteq> ball c r"
+    by auto
+  from ab have "0 < content (box a b)"
+    by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def)
+  have "emeasure lborel (box a b) \<le> emeasure lborel (ball c r)"
+    using ab by (intro emeasure_mono) auto
+  also have "emeasure lborel (box a b) = ennreal (content (box a b))"
+    using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto
+  also have "emeasure lborel (ball c r) = ennreal (content (ball c r))"
+    using emeasure_lborel_ball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto
+  finally show ?thesis
+    using \<open>content (box a b) > 0\<close> by simp
+qed
+
+lemma content_cball_pos:
+  assumes "r > 0"
+  shows   "content (cball c r) > 0"
+proof -
+  from rational_boxes[OF assms, of c] obtain a b where ab: "c \<in> box a b" "box a b \<subseteq> ball c r"
+    by auto
+  from ab have "0 < content (box a b)"
+    by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def)
+  have "emeasure lborel (box a b) \<le> emeasure lborel (ball c r)"
+    using ab by (intro emeasure_mono) auto
+  also have "\<dots> \<le> emeasure lborel (cball c r)"
+    by (intro emeasure_mono) auto
+  also have "emeasure lborel (box a b) = ennreal (content (box a b))"
+    using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto
+  also have "emeasure lborel (cball c r) = ennreal (content (cball c r))"
+    using emeasure_lborel_cball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto
+  finally show ?thesis
+    using \<open>content (box a b) > 0\<close> by simp
+qed
+
 lemma content_split:
   fixes a :: "'a::euclidean_space"
   assumes "k \<in> Basis"
diff -r 6695aeae8ec9 -r a8ccea88b725 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Dec 02 10:31:51 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Dec 02 14:22:03 2019 +0100
@@ -823,6 +823,34 @@
   using emeasure_lborel_cbox[of x x] nonempty_Basis
   by (auto simp del: emeasure_lborel_cbox nonempty_Basis)
 
+lemma emeasure_lborel_cbox_finite: "emeasure lborel (cbox a b) < \<infinity>"
+  by (auto simp: emeasure_lborel_cbox_eq)
+
+lemma emeasure_lborel_box_finite: "emeasure lborel (box a b) < \<infinity>"
+  by (auto simp: emeasure_lborel_box_eq)
+
+lemma emeasure_lborel_ball_finite: "emeasure lborel (ball c r) < \<infinity>"
+proof -
+  have "bounded (ball c r)" by simp
+  from bounded_subset_cbox_symmetric[OF this] obtain a where a: "ball c r \<subseteq> cbox (-a) a"
+    by auto
+  hence "emeasure lborel (ball c r) \<le> emeasure lborel (cbox (-a) a)"
+    by (intro emeasure_mono) auto
+  also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq)
+  finally show ?thesis .
+qed
+
+lemma emeasure_lborel_cball_finite: "emeasure lborel (cball c r) < \<infinity>"
+proof -
+  have "bounded (cball c r)" by simp
+  from bounded_subset_cbox_symmetric[OF this] obtain a where a: "cball c r \<subseteq> cbox (-a) a"
+    by auto
+  hence "emeasure lborel (cball c r) \<le> emeasure lborel (cbox (-a) a)"
+    by (intro emeasure_mono) auto
+  also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq)
+  finally show ?thesis .
+qed
+
 lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel"
   and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel"
   by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
diff -r 6695aeae8ec9 -r a8ccea88b725 src/HOL/Analysis/Vitali_Covering_Theorem.thy
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Mon Dec 02 10:31:51 2019 +0100
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Mon Dec 02 14:22:03 2019 +0100
@@ -5,7 +5,7 @@
 section  \<open>Vitali Covering Theorem and an Application to Negligibility\<close>
 
 theory Vitali_Covering_Theorem
-  imports Ball_Volume "HOL-Library.Permutations"
+  imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Permutations"
 
 begin
 
@@ -428,10 +428,10 @@
                 by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
               also have "\<dots> = (\<Sum>i\<in>D2. 5 ^ DIM('n) * ?\<mu> (ball (a i) (r i)))"
               proof (rule sum.cong [OF refl])
-                fix i
-                assume "i \<in> D2"
-                show "?\<mu> (ball (a i) (5 * r i)) = 5 ^ DIM('n) * ?\<mu> (ball (a i) (r i))"
-                  using rgt0 [OF \<open>i \<in> D2\<close>] by (simp add: content_ball)
+                fix i assume "i \<in> D2"
+                thus "?\<mu> (ball (a i) (5 * r i)) = 5 ^ DIM('n) * ?\<mu> (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 "\<dots> = (\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) * 5 ^ DIM('n)"
                 by (simp add: sum_distrib_left mult.commute)
@@ -450,7 +450,7 @@
                 have ds: "disjoint ((\<lambda>i. cball (a i) (r i)) ` D2)"
                   using D2 \<open>D \<subseteq> C\<close> by (auto intro: pairwiseI pairwiseD [OF pwC])
                 have "(\<Sum>i\<in>D2. ?\<mu> (ball (a i) (r i))) = (\<Sum>i\<in>D2. ?\<mu> (cball (a i) (r i)))"
-                  using rgt0 by (simp add: content_ball content_cball less_eq_real_def)
+                  by (simp add: content_cball_conv_ball)
                 also have "\<dots> = sum ?\<mu> ((\<lambda>i. cball (a i) (r i)) ` D2)"
                   by (simp add: comm_monoid_add_class.sum.reindex [OF inj])
                 also have "\<dots> = ?\<mu> (\<Union>i\<in>D2. cball (a i) (r i))"
@@ -537,7 +537,8 @@
               measure lebesgue U < e * measure lebesgue (ball x d)"
     apply (rule_tac x=e in exI)
     apply (rule_tac x="S \<inter> ball x e" in exI)
-    apply (auto simp: negligible_imp_measurable negligible_Int negligible_imp_measure0 zero_less_measure_iff)
+    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]: "\<forall>x \<in> S. \<forall>e > 0. ?Q x e"
@@ -567,7 +568,7 @@
         let ?\<epsilon> = "min (e / ?\<mu> (ball z 1) / 2) (min (d / 2) k)"
         obtain r U where r: "r > 0" "r \<le> ?\<epsilon>" and U: "S \<inter> ball x r \<subseteq> U" "U \<in> lmeasurable"
           and mU: "?\<mu> U < ?\<epsilon> * ?\<mu> (ball x r)"
-          using R [of x ?\<epsilon>] \<open>d > 0\<close> \<open>e > 0\<close> \<open>k > 0\<close> x by auto
+          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 "\<exists>i. i \<in> ?K \<and> x \<in> ball (fst i) (snd i) \<and> snd i < d"
         proof (rule exI [of _ "(x,r)"], simp, intro conjI exI)
           have "ball x r \<subseteq> ball x k"
@@ -576,7 +577,7 @@
             using ball_subset_ball_iff k by auto
           finally show "ball x r \<subseteq> ball z 1" .
           have "?\<epsilon> * ?\<mu> (ball x r) \<le> 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)
+            using r \<open>e > 0\<close> by (simp add: ord_class.min_def field_split_simps content_ball_pos)
           with mU show "?\<mu> U < e * content (ball x r) / content (ball z 1)"
             by auto
         qed (use r U x in auto)
@@ -603,7 +604,7 @@
               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: "(?\<mu> (\<Union>(x,d)\<in>I. ball x d) / ?\<mu> (ball z 1)) \<le> 1"
-              by simp
+              by (simp add: content_ball_pos)
             have "?\<mu> (\<Union>i\<in>I. U i) \<le> (\<Sum>i\<in>I. ?\<mu> (U i))"
               using that U by (blast intro: measure_UNION_le)
             also have "\<dots> \<le> (\<Sum>(x,r)\<in>I. e / ?\<mu> (ball z 1) * ?\<mu> (ball x r))"
@@ -648,7 +649,7 @@
     assume L [rule_format]: "\<forall>e>0. \<exists>d>0. d \<le> e \<and> ?Q x d e" and "r > 0" "e > 0"
     show "\<exists>d>0. d \<le> r \<and> ?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)
+      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)