--- 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
--- 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>
--- 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)
--- 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"
--- 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)
--- 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)