HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
--- a/src/HOL/Analysis/Analysis.thy Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Analysis.thy Fri Sep 30 11:35:39 2016 +0200
@@ -1,6 +1,5 @@
theory Analysis
imports
- Regularity
Lebesgue_Integral_Substitution
Embed_Measure
Complete_Measure
--- a/src/HOL/Analysis/Complete_Measure.thy Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy Fri Sep 30 11:35:39 2016 +0200
@@ -199,6 +199,9 @@
qed
qed
+lemma measure_completion[simp]: "S \<in> sets M \<Longrightarrow> measure (completion M) S = measure M S"
+ unfolding measure_def by auto
+
lemma emeasure_completion_UN:
"range S \<subseteq> sets (completion M) \<Longrightarrow>
emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 30 11:35:39 2016 +0200
@@ -962,7 +962,7 @@
lemma
assumes \<D>: "\<D> division_of S"
shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
- and content_divsion: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
+ and content_division: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
proof -
{ fix d1 d2 assume *: "d1 \<in> \<D>" "d2 \<in> \<D>" "d1 \<noteq> d2"
then obtain a b c d where "d1 = cbox a b" "d2 = cbox c d"
@@ -1133,6 +1133,368 @@
not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
intro: eq_refl antisym less_imp_le)
+subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
+
+lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
+ by (auto simp: measure_def null_sets_def)
+
+text\<open>The bound will be eliminated by a sort of onion argument\<close>
+lemma locally_Lipschitz_negl_bounded:
+ fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+ assumes MleN: "DIM('M) \<le> DIM('N)" "0 < B" "bounded S" "negligible S"
+ and lips: "\<And>x. x \<in> S
+ \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and>
+ (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
+ shows "negligible (f ` S)"
+ unfolding negligible_iff_null_sets
+proof (clarsimp simp: completion.null_sets_outer)
+ fix e::real
+ assume "0 < e"
+ have "S \<in> lmeasurable"
+ using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets fmeasurableI_null_sets)
+ have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)"
+ using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
+ obtain T
+ where "open T" "S \<subseteq> T" "T \<in> lmeasurable"
+ and "measure lebesgue T \<le> measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+ by (rule lmeasurable_outer_open [OF \<open>S \<in> lmeasurable\<close> e22])
+ then have T: "measure lebesgue T \<le> e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+ using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets measure_eq_0_null_sets)
+ have "\<exists>r. 0 < r \<and> r \<le> 1/2 \<and>
+ (x \<in> S \<longrightarrow> (\<forall>y. norm(y - x) < r
+ \<longrightarrow> y \<in> T \<and> (y \<in> S \<longrightarrow> norm(f y - f x) \<le> B * norm(y - x))))"
+ for x
+ proof (cases "x \<in> S")
+ case True
+ obtain U where "open U" "x \<in> U" and U: "\<And>y. y \<in> S \<inter> U \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
+ using lips [OF \<open>x \<in> S\<close>] by auto
+ have "x \<in> T \<inter> U"
+ using \<open>S \<subseteq> T\<close> \<open>x \<in> U\<close> \<open>x \<in> S\<close> by auto
+ then obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T \<inter> U"
+ by (metis \<open>open T\<close> \<open>open U\<close> openE open_Int)
+ then show ?thesis
+ apply (rule_tac x="min (1/2) \<epsilon>" in exI)
+ apply (simp del: divide_const_simps)
+ apply (intro allI impI conjI)
+ apply (metis dist_commute dist_norm mem_ball subsetCE)
+ by (metis Int_iff subsetCE U dist_norm mem_ball norm_minus_commute)
+ next
+ case False
+ then show ?thesis
+ by (rule_tac x="1/4" in exI) auto
+ qed
+ then obtain R where R12: "\<And>x. 0 < R x \<and> R x \<le> 1/2"
+ and RT: "\<And>x y. \<lbrakk>x \<in> S; norm(y - x) < R x\<rbrakk> \<Longrightarrow> y \<in> T"
+ and RB: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; norm(y - x) < R x\<rbrakk> \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
+ by metis+
+ then have gaugeR: "gauge (\<lambda>x. ball x (R x))"
+ by (simp add: gauge_def)
+ obtain c where c: "S \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)" "box (-c *\<^sub>R One:: 'M) (c *\<^sub>R One) \<noteq> {}"
+ proof -
+ obtain B where B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
+ using \<open>bounded S\<close> bounded_iff by blast
+ show ?thesis
+ apply (rule_tac c = "abs B + 1" in that)
+ using norm_bound_Basis_le Basis_le_norm
+ apply (fastforce simp: box_eq_empty mem_box dest!: B intro: order_trans)+
+ done
+ qed
+ obtain \<D> where "countable \<D>"
+ and Dsub: "\<Union>\<D> \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)"
+ and cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
+ and pw: "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
+ and Ksub: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> (\<lambda>x. ball x (R x)) x"
+ and exN: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (2*c) / 2^n"
+ and "S \<subseteq> \<Union>\<D>"
+ using covering_lemma [OF c gaugeR] by force
+ have "\<exists>u v z. K = cbox u v \<and> box u v \<noteq> {} \<and> z \<in> S \<and> z \<in> cbox u v \<and>
+ cbox u v \<subseteq> ball z (R z)" if "K \<in> \<D>" for K
+ proof -
+ obtain u v where "K = cbox u v"
+ using \<open>K \<in> \<D>\<close> cbox by blast
+ with that show ?thesis
+ apply (rule_tac x=u in exI)
+ apply (rule_tac x=v in exI)
+ apply (metis Int_iff interior_cbox cbox Ksub)
+ done
+ qed
+ then obtain uf vf zf
+ where uvz: "\<And>K. K \<in> \<D> \<Longrightarrow>
+ K = cbox (uf K) (vf K) \<and> box (uf K) (vf K) \<noteq> {} \<and> zf K \<in> S \<and>
+ zf K \<in> cbox (uf K) (vf K) \<and> cbox (uf K) (vf K) \<subseteq> ball (zf K) (R (zf K))"
+ by metis
+ define prj1 where "prj1 \<equiv> \<lambda>x::'M. x \<bullet> (SOME i. i \<in> Basis)"
+ define fbx where "fbx \<equiv> \<lambda>D. cbox (f(zf D) - (B * DIM('M) * (prj1(vf D - uf D))) *\<^sub>R One::'N)
+ (f(zf D) + (B * DIM('M) * prj1(vf D - uf D)) *\<^sub>R One)"
+ have vu_pos: "0 < prj1 (vf X - uf X)" if "X \<in> \<D>" for X
+ using uvz [OF that] by (simp add: prj1_def box_ne_empty SOME_Basis inner_diff_left)
+ have prj1_idem: "prj1 (vf X - uf X) = (vf X - uf X) \<bullet> i" if "X \<in> \<D>" "i \<in> Basis" for X i
+ proof -
+ have "cbox (uf X) (vf X) \<in> \<D>"
+ using uvz \<open>X \<in> \<D>\<close> by auto
+ with exN obtain n where "\<And>i. i \<in> Basis \<Longrightarrow> vf X \<bullet> i - uf X \<bullet> i = (2*c) / 2^n"
+ by blast
+ then show ?thesis
+ by (simp add: \<open>i \<in> Basis\<close> SOME_Basis inner_diff prj1_def)
+ qed
+ have countbl: "countable (fbx ` \<D>)"
+ using \<open>countable \<D>\<close> by blast
+ have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e / 2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
+ proof -
+ have BM_ge0: "0 \<le> B * (DIM('M) * prj1 (vf X - uf X))" if "X \<in> \<D>'" for X
+ using \<open>0 < B\<close> \<open>\<D>' \<subseteq> \<D>\<close> that vu_pos by fastforce
+ have "{} \<notin> \<D>'"
+ using cbox \<open>\<D>' \<subseteq> \<D>\<close> interior_empty by blast
+ have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> setsum (measure lebesgue o fbx) \<D>'"
+ by (rule setsum_image_le [OF \<open>finite \<D>'\<close>]) (force simp: fbx_def)
+ also have "\<dots> \<le> (\<Sum>X\<in>\<D>'. (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X)"
+ proof (rule setsum_mono)
+ fix X assume "X \<in> \<D>'"
+ then have "X \<in> \<D>" using \<open>\<D>' \<subseteq> \<D>\<close> by blast
+ then have ufvf: "cbox (uf X) (vf X) = X"
+ using uvz by blast
+ have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
+ by (rule setprod_constant [symmetric])
+ also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
+ using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: setprod.cong)
+ finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
+ have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
+ using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
+ moreover have "cbox (uf X) (vf X) \<subseteq> ball (zf X) (1/2)"
+ by (meson R12 order_trans subset_ball uvz [OF \<open>X \<in> \<D>\<close>])
+ ultimately have "uf X \<in> ball (zf X) (1/2)" "vf X \<in> ball (zf X) (1/2)"
+ by auto
+ then have "dist (vf X) (uf X) \<le> 1"
+ unfolding mem_ball
+ by (metis dist_commute dist_triangle_half_l dual_order.order_iff_strict)
+ then have 1: "prj1 (vf X - uf X) \<le> 1"
+ unfolding prj1_def dist_norm using Basis_le_norm SOME_Basis order_trans by fastforce
+ have 0: "0 \<le> prj1 (vf X - uf X)"
+ using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
+ have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
+ apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> setprod_constant)
+ apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
+ using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
+ apply (fastforce simp add: box_ne_empty power_decreasing)
+ done
+ also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
+ by (subst (3) ufvf[symmetric]) simp
+ finally show "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
+ qed
+ also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \<D>'"
+ by (simp add: setsum_distrib_left)
+ also have "\<dots> \<le> e / 2"
+ proof -
+ have div: "\<D>' division_of \<Union>\<D>'"
+ apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
+ using cbox that apply blast
+ using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
+ done
+ have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
+ proof (rule measure_mono_fmeasurable [OF _ _ \<open>T : lmeasurable\<close>])
+ show "(\<Union>\<D>') \<in> sets lebesgue"
+ using div lmeasurable_division by auto
+ have "\<Union>\<D>' \<subseteq> \<Union>\<D>"
+ using \<open>\<D>' \<subseteq> \<D>\<close> by blast
+ also have "... \<subseteq> T"
+ proof (clarify)
+ fix x D
+ assume "x \<in> D" "D \<in> \<D>"
+ show "x \<in> T"
+ using Ksub [OF \<open>D \<in> \<D>\<close>]
+ by (metis \<open>x \<in> D\<close> Int_iff dist_norm mem_ball norm_minus_commute subsetD RT)
+ qed
+ finally show "\<Union>\<D>' \<subseteq> T" .
+ qed
+ have "setsum (measure lebesgue) \<D>' = setsum content \<D>'"
+ using \<open>\<D>' \<subseteq> \<D>\<close> cbox by (force intro: setsum.cong)
+ then have "(2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \<D>' =
+ (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\<Union>\<D>')"
+ using content_division [OF div] by auto
+ also have "\<dots> \<le> (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
+ apply (rule mult_left_mono [OF le_meaT])
+ using \<open>0 < B\<close>
+ apply (simp add: algebra_simps)
+ done
+ also have "\<dots> \<le> e / 2"
+ using T \<open>0 < B\<close> by (simp add: field_simps)
+ finally show ?thesis .
+ qed
+ finally show ?thesis .
+ qed
+ then have e2: "setsum (measure lebesgue) \<G> \<le> e / 2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
+ by (metis finite_subset_image that)
+ show "\<exists>W\<in>lmeasurable. f ` S \<subseteq> W \<and> measure lebesgue W < e"
+ proof (intro bexI conjI)
+ have "\<exists>X\<in>\<D>. f y \<in> fbx X" if "y \<in> S" for y
+ proof -
+ obtain X where "y \<in> X" "X \<in> \<D>"
+ using \<open>S \<subseteq> \<Union>\<D>\<close> \<open>y \<in> S\<close> by auto
+ then have y: "y \<in> ball(zf X) (R(zf X))"
+ using uvz by fastforce
+ have conj_le_eq: "z - b \<le> y \<and> y \<le> z + b \<longleftrightarrow> abs(y - z) \<le> b" for z y b::real
+ by auto
+ have yin: "y \<in> cbox (uf X) (vf X)" and zin: "(zf X) \<in> cbox (uf X) (vf X)"
+ using uvz \<open>X \<in> \<D>\<close> \<open>y \<in> X\<close> by auto
+ have "norm (y - zf X) \<le> (\<Sum>i\<in>Basis. \<bar>(y - zf X) \<bullet> i\<bar>)"
+ by (rule norm_le_l1)
+ also have "\<dots> \<le> real DIM('M) * prj1 (vf X - uf X)"
+ proof (rule setsum_bounded_above)
+ fix j::'M assume j: "j \<in> Basis"
+ show "\<bar>(y - zf X) \<bullet> j\<bar> \<le> prj1 (vf X - uf X)"
+ using yin zin j
+ by (fastforce simp add: mem_box prj1_idem [OF \<open>X \<in> \<D>\<close> j] inner_diff_left)
+ qed
+ finally have nole: "norm (y - zf X) \<le> DIM('M) * prj1 (vf X - uf X)"
+ by simp
+ have fle: "\<bar>f y \<bullet> i - f(zf X) \<bullet> i\<bar> \<le> B * DIM('M) * prj1 (vf X - uf X)" if "i \<in> Basis" for i
+ proof -
+ have "\<bar>f y \<bullet> i - f (zf X) \<bullet> i\<bar> = \<bar>(f y - f (zf X)) \<bullet> i\<bar>"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<le> norm (f y - f (zf X))"
+ by (simp add: Basis_le_norm that)
+ also have "\<dots> \<le> B * norm(y - zf X)"
+ by (metis uvz RB \<open>X \<in> \<D>\<close> dist_commute dist_norm mem_ball \<open>y \<in> S\<close> y)
+ also have "\<dots> \<le> B * real DIM('M) * prj1 (vf X - uf X)"
+ using \<open>0 < B\<close> by (simp add: nole)
+ finally show ?thesis .
+ qed
+ show ?thesis
+ by (rule_tac x=X in bexI)
+ (auto simp: fbx_def prj1_idem mem_box conj_le_eq inner_add inner_diff fle \<open>X \<in> \<D>\<close>)
+ qed
+ then show "f ` S \<subseteq> (\<Union>D\<in>\<D>. fbx D)" by auto
+ next
+ have 1: "\<And>D. D \<in> \<D> \<Longrightarrow> fbx D \<in> lmeasurable"
+ by (auto simp: fbx_def)
+ have 2: "I' \<subseteq> \<D> \<Longrightarrow> finite I' \<Longrightarrow> measure lebesgue (\<Union>D\<in>I'. fbx D) \<le> e/2" for I'
+ by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def)
+ have 3: "0 \<le> e/2"
+ using \<open>0<e\<close> by auto
+ show "(\<Union>D\<in>\<D>. fbx D) \<in> lmeasurable"
+ by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
+ have "measure lebesgue (\<Union>D\<in>\<D>. fbx D) \<le> e/2"
+ by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
+ then show "measure lebesgue (\<Union>D\<in>\<D>. fbx D) < e"
+ using \<open>0 < e\<close> by linarith
+ qed
+qed
+
+proposition negligible_locally_Lipschitz_image:
+ fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+ assumes MleN: "DIM('M) \<le> DIM('N)" "negligible S"
+ and lips: "\<And>x. x \<in> S
+ \<Longrightarrow> \<exists>T B. open T \<and> x \<in> T \<and>
+ (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
+ shows "negligible (f ` S)"
+proof -
+ let ?S = "\<lambda>n. ({x \<in> S. norm x \<le> n \<and>
+ (\<exists>T. open T \<and> x \<in> T \<and>
+ (\<forall>y\<in>S \<inter> T. norm (f y - f x) \<le> (real n + 1) * norm (y - x)))})"
+ have negfn: "f ` ?S n \<in> null_sets lebesgue" for n::nat
+ unfolding negligible_iff_null_sets[symmetric]
+ apply (rule_tac B = "real n + 1" in locally_Lipschitz_negl_bounded)
+ by (auto simp: MleN bounded_iff intro: negligible_subset [OF \<open>negligible S\<close>])
+ have "S = (\<Union>n. ?S n)"
+ proof (intro set_eqI iffI)
+ fix x assume "x \<in> S"
+ with lips obtain T B where T: "open T" "x \<in> T"
+ and B: "\<And>y. y \<in> S \<inter> T \<Longrightarrow> norm(f y - f x) \<le> B * norm(y - x)"
+ by metis+
+ have no: "norm (f y - f x) \<le> (nat \<lceil>max B (norm x)\<rceil> + 1) * norm (y - x)" if "y \<in> S \<inter> T" for y
+ proof -
+ have "B * norm(y - x) \<le> (nat \<lceil>max B (norm x)\<rceil> + 1) * norm (y - x)"
+ by (meson max.cobounded1 mult_right_mono nat_ceiling_le_eq nat_le_iff_add norm_ge_zero order_trans)
+ then show ?thesis
+ using B order_trans that by blast
+ qed
+ have "x \<in> ?S (nat (ceiling (max B (norm x))))"
+ apply (simp add: \<open>x \<in> S \<close>, rule)
+ using real_nat_ceiling_ge max.bounded_iff apply blast
+ using T no
+ apply (force simp: algebra_simps)
+ done
+ then show "x \<in> (\<Union>n. ?S n)" by force
+ qed auto
+ then show ?thesis
+ by (rule ssubst) (auto simp: image_Union negligible_iff_null_sets intro: negfn)
+qed
+
+corollary negligible_differentiable_image_negligible:
+ fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+ assumes MleN: "DIM('M) \<le> DIM('N)" "negligible S"
+ and diff_f: "f differentiable_on S"
+ shows "negligible (f ` S)"
+proof -
+ have "\<exists>T B. open T \<and> x \<in> T \<and> (\<forall>y \<in> S \<inter> T. norm(f y - f x) \<le> B * norm(y - x))"
+ if "x \<in> S" for x
+ proof -
+ obtain f' where "linear f'"
+ and f': "\<And>e. e>0 \<Longrightarrow>
+ \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
+ norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
+ using diff_f \<open>x \<in> S\<close>
+ by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
+ obtain B where "B > 0" and B: "\<forall>x. norm (f' x) \<le> B * norm x"
+ using linear_bounded_pos \<open>linear f'\<close> by blast
+ obtain d where "d>0"
+ and d: "\<And>y. \<lbrakk>y \<in> S; norm (y - x) < d\<rbrakk> \<Longrightarrow>
+ norm (f y - f x - f' (y - x)) \<le> norm (y - x)"
+ using f' [of 1] by (force simp:)
+ have *: "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
+ if "y \<in> S" "norm (y - x) < d" for y
+ proof -
+ have "norm (f y - f x) -B * norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
+ by (simp add: B)
+ also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
+ by (rule norm_triangle_ineq2)
+ also have "... \<le> norm (y - x)"
+ by (rule d [OF that])
+ finally show ?thesis
+ by (simp add: algebra_simps)
+ qed
+ show ?thesis
+ apply (rule_tac x="ball x d" in exI)
+ apply (rule_tac x="B+1" in exI)
+ using \<open>d>0\<close>
+ apply (auto simp: dist_norm norm_minus_commute intro!: *)
+ done
+ qed
+ with negligible_locally_Lipschitz_image assms show ?thesis by metis
+qed
+
+corollary negligible_differentiable_image_lowdim:
+ fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
+ assumes MlessN: "DIM('M) < DIM('N)" and diff_f: "f differentiable_on S"
+ shows "negligible (f ` S)"
+proof -
+ have "x \<le> DIM('M) \<Longrightarrow> x \<le> DIM('N)" for x
+ using MlessN by linarith
+ obtain lift :: "'M * real \<Rightarrow> 'N" and drop :: "'N \<Rightarrow> 'M * real" and j :: 'N
+ where "linear lift" "linear drop" and dropl [simp]: "\<And>z. drop (lift z) = z"
+ and "j \<in> Basis" and j: "\<And>x. lift(x,0) \<bullet> j = 0"
+ using lowerdim_embeddings [OF MlessN] by metis
+ have "negligible {x. x\<bullet>j = 0}"
+ by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
+ then have neg0S: "negligible ((\<lambda>x. lift (x, 0)) ` S)"
+ apply (rule negligible_subset)
+ by (simp add: image_subsetI j)
+ have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
+ using diff_f
+ apply (clarsimp simp add: differentiable_on_def)
+ apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
+ linear_imp_differentiable [OF fst_linear])
+ apply (force simp: image_comp o_def)
+ done
+ have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
+ by (simp add: o_def)
+ then show ?thesis
+ apply (rule ssubst)
+ apply (subst image_comp [symmetric])
+ apply (metis negligible_differentiable_image_negligible order_refl diff_f' neg0S)
+ done
+qed
+
lemma set_integral_norm_bound:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Sep 30 11:35:39 2016 +0200
@@ -8,7 +8,7 @@
section \<open>Lebesgue measure\<close>
theory Lebesgue_Measure
- imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests
+ imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity
begin
subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
@@ -986,4 +986,92 @@
"compact S \<Longrightarrow> (\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1) \<Longrightarrow> S \<in> null_sets lebesgue"
using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed)
+lemma outer_regular_lborel:
+ assumes B: "B \<in> fmeasurable lborel" "0 < (e::real)"
+ shows "\<exists>U. open U \<and> B \<subseteq> U \<and> emeasure lborel U \<le> emeasure lborel B + e"
+proof -
+ let ?\<mu> = "emeasure lborel"
+ let ?B = "\<lambda>n::nat. ball 0 n :: 'a set"
+ have B[measurable]: "B \<in> sets borel"
+ using B by auto
+ let ?e = "\<lambda>n. e*((1/2)^Suc n)"
+ have "\<forall>n. \<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n"
+ proof
+ fix n :: nat
+ let ?A = "density lborel (indicator (?B n))"
+ have emeasure_A: "X \<in> sets borel \<Longrightarrow> emeasure ?A X = ?\<mu> (?B n \<inter> X)" for X
+ by (auto simp add: emeasure_density borel_measurable_indicator indicator_inter_arith[symmetric])
+
+ have finite_A: "emeasure ?A (space ?A) \<noteq> \<infinity>"
+ using emeasure_bounded_finite[of "?B n"] by (auto simp add: emeasure_A)
+ interpret A: finite_measure ?A
+ by rule fact
+ have "emeasure ?A B + ?e n > (INF U:{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
+ using \<open>0<e\<close> by (auto simp: outer_regular[OF _ finite_A B, symmetric])
+ then obtain U where U: "B \<subseteq> U" "open U" "?\<mu> (?B n \<inter> B) + ?e n > ?\<mu> (?B n \<inter> U)"
+ unfolding INF_less_iff by (auto simp: emeasure_A)
+ moreover
+ { have "?\<mu> ((?B n \<inter> U) - B) = ?\<mu> ((?B n \<inter> U) - (?B n \<inter> B))"
+ using U by (intro arg_cong[where f="?\<mu>"]) auto
+ also have "\<dots> = ?\<mu> (?B n \<inter> U) - ?\<mu> (?B n \<inter> B)"
+ using U A.emeasure_finite[of B]
+ by (intro emeasure_Diff) (auto simp del: A.emeasure_finite simp: emeasure_A)
+ also have "\<dots> < ?e n"
+ using U(1,2,3) A.emeasure_finite[of B]
+ by (subst minus_less_iff_ennreal)
+ (auto simp del: A.emeasure_finite simp: emeasure_A less_top ac_simps intro!: emeasure_mono)
+ finally have "?\<mu> ((?B n \<inter> U) - B) < ?e n" . }
+ ultimately show "\<exists>U. open U \<and> ?B n \<inter> B \<subseteq> U \<and> ?\<mu> (U - B) < ?e n"
+ by (intro exI[of _ "?B n \<inter> U"]) auto
+ qed
+ then obtain U
+ where U: "\<And>n. open (U n)" "\<And>n. ?B n \<inter> B \<subseteq> U n" "\<And>n. ?\<mu> (U n - B) < ?e n"
+ by metis
+ then show ?thesis
+ proof (intro exI conjI)
+ { fix x assume "x \<in> B"
+ moreover
+ have "\<exists>n. norm x < real n"
+ by (simp add: reals_Archimedean2)
+ then guess n ..
+ ultimately have "x \<in> (\<Union>n. U n)"
+ using U(2)[of n] by auto }
+ note * = this
+ then show "open (\<Union>n. U n)" "B \<subseteq> (\<Union>n. U n)"
+ using U(1,2) by auto
+ have "?\<mu> (\<Union>n. U n) = ?\<mu> (B \<union> (\<Union>n. U n - B))"
+ using * U(2) by (intro arg_cong[where ?f="?\<mu>"]) auto
+ also have "\<dots> = ?\<mu> B + ?\<mu> (\<Union>n. U n - B)"
+ using U(1) by (intro plus_emeasure[symmetric]) auto
+ also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ?\<mu> (U n - B))"
+ using U(1) by (intro add_mono emeasure_subadditive_countably) auto
+ also have "\<dots> \<le> ?\<mu> B + (\<Sum>n. ennreal (?e n))"
+ using U(3) by (intro add_mono suminf_le) (auto intro: less_imp_le)
+ also have "(\<Sum>n. ennreal (?e n)) = ennreal (e * 1)"
+ using \<open>0<e\<close> by (intro suminf_ennreal_eq sums_mult power_half_series) auto
+ finally show "emeasure lborel (\<Union>n. U n) \<le> emeasure lborel B + ennreal e"
+ by simp
+ qed
+qed
+
+lemma lmeasurable_outer_open:
+ assumes S: "S \<in> lmeasurable" and "0 < e"
+ obtains T where "open T" "S \<subseteq> T" "T \<in> lmeasurable" "measure lebesgue T \<le> measure lebesgue S + e"
+proof -
+ obtain S' where S': "S \<subseteq> S'" "S' \<in> sets borel" "emeasure lborel S' = emeasure lebesgue S"
+ using completion_upper[of S lborel] S by auto
+ then have f_S': "S' \<in> fmeasurable lborel"
+ using S by (auto simp: fmeasurable_def)
+ from outer_regular_lborel[OF this \<open>0<e\<close>] guess U .. note U = this
+ show thesis
+ proof (rule that)
+ show "open U" "S \<subseteq> U" "U \<in> lmeasurable"
+ using f_S' U S' by (auto simp: fmeasurable_def less_top[symmetric] top_unique)
+ then have "U \<in> fmeasurable lborel"
+ by (auto simp: fmeasurable_def)
+ with S U \<open>0<e\<close> show "measure lebesgue U \<le> measure lebesgue S + e"
+ unfolding S'(3) by (simp add: emeasure_eq_measure2 ennreal_plus[symmetric] del: ennreal_plus)
+ qed
+qed
+
end
--- a/src/HOL/Analysis/Measure_Space.thy Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Sep 30 11:35:39 2016 +0200
@@ -472,6 +472,10 @@
"a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
using additiveD[OF emeasure_additive] ..
+lemma emeasure_Union:
+ "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
+ using plus_emeasure[of A M "B - A"] by auto
+
lemma setsum_emeasure:
"F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
(\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
@@ -1749,6 +1753,42 @@
"finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> sets M) \<Longrightarrow> measure M (\<Union>F) \<le> (\<Sum>S\<in>F. measure M S)"
using measure_UNION_le[of F "\<lambda>x. x" M] by simp
+lemma
+ assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> fmeasurable M"
+ and bound: "\<And>I'. I' \<subseteq> I \<Longrightarrow> finite I' \<Longrightarrow> measure M (\<Union>i\<in>I'. A i) \<le> B" and "0 \<le> B"
+ shows fmeasurable_UN_bound: "(\<Union>i\<in>I. A i) \<in> fmeasurable M" (is ?fm)
+ and measure_UN_bound: "measure M (\<Union>i\<in>I. A i) \<le> B" (is ?m)
+proof -
+ have "?fm \<and> ?m"
+ proof cases
+ assume "I = {}" with \<open>0 \<le> B\<close> show ?thesis by simp
+ next
+ assume "I \<noteq> {}"
+ have "(\<Union>i\<in>I. A i) = (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))"
+ by (subst range_from_nat_into[symmetric, OF \<open>I \<noteq> {}\<close> \<open>countable I\<close>]) auto
+ then have "emeasure M (\<Union>i\<in>I. A i) = emeasure M (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))" by simp
+ also have "\<dots> = (SUP i. emeasure M (\<Union>n\<le>i. A (from_nat_into I n)))"
+ using I \<open>I \<noteq> {}\<close>[THEN from_nat_into] by (intro SUP_emeasure_incseq[symmetric]) (fastforce simp: incseq_Suc_iff)+
+ also have "\<dots> \<le> B"
+ proof (intro SUP_least)
+ fix i :: nat
+ have "emeasure M (\<Union>n\<le>i. A (from_nat_into I n)) = measure M (\<Union>n\<le>i. A (from_nat_into I n))"
+ using I \<open>I \<noteq> {}\<close>[THEN from_nat_into] by (intro emeasure_eq_measure2 fmeasurable.finite_UN) auto
+ also have "\<dots> = measure M (\<Union>n\<in>from_nat_into I ` {..i}. A n)"
+ by simp
+ also have "\<dots> \<le> B"
+ by (intro ennreal_leI bound) (auto intro: from_nat_into[OF \<open>I \<noteq> {}\<close>])
+ finally show "emeasure M (\<Union>n\<le>i. A (from_nat_into I n)) \<le> ennreal B" .
+ qed
+ finally have *: "emeasure M (\<Union>i\<in>I. A i) \<le> B" .
+ then have ?fm
+ using I \<open>countable I\<close> by (intro fmeasurableI conjI) (auto simp: less_top[symmetric] top_unique)
+ with * \<open>0\<le>B\<close> show ?thesis
+ by (simp add: emeasure_eq_measure2)
+ qed
+ then show ?fm ?m by auto
+qed
+
subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
locale finite_measure = sigma_finite_measure M for M +
--- a/src/HOL/Library/Extended_Real.thy Fri Sep 30 14:05:51 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Sep 30 11:35:39 2016 +0200
@@ -2106,6 +2106,50 @@
apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
done
+lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
+ unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less)
+
+lemma INF_ereal_add_left:
+ assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
+ shows "(INF i:I. f i + c :: ereal) = (INF i:I. f i) + c"
+proof -
+ have "(INF i:I. f i) \<noteq> -\<infinity>"
+ unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
+ then show ?thesis
+ by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
+ (auto simp: mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at)
+qed
+
+lemma INF_ereal_add_right:
+ assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
+ shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)"
+ using INF_ereal_add_left[OF assms] by (simp add: ac_simps)
+
+lemma INF_ereal_add_directed:
+ fixes f g :: "'a \<Rightarrow> ereal"
+ assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
+ assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<ge> f k + g k"
+ shows "(INF i:I. f i + g i) = (INF i:I. f i) + (INF i:I. g i)"
+proof cases
+ assume "I = {}" then show ?thesis
+ by (simp add: top_ereal_def)
+next
+ assume "I \<noteq> {}"
+ show ?thesis
+ proof (rule antisym)
+ show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)"
+ by (rule INF_greatest; intro ereal_add_mono INF_lower)
+ next
+ have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))"
+ using directed by (intro INF_greatest) (blast intro: INF_lower2)
+ also have "\<dots> = (INF i:I. f i + (INF i:I. g i))"
+ using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
+ also have "\<dots> = (INF i:I. f i) + (INF i:I. g i)"
+ using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
+ finally show "(INF i:I. f i + g i) \<le> (INF i:I. f i) + (INF i:I. g i)" .
+ qed
+qed
+
lemma INF_ereal_add:
fixes f :: "nat \<Rightarrow> ereal"
assumes "decseq f" "decseq g"