# HG changeset patch # User hoelzl # Date 1475228139 -7200 # Node ID 4359400adfe7afd29f771ec0bcb2bba795c257f0 # Parent 2aa42596edc3b3756d7f4fa922c55c2ae30a5aab 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) diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Analysis.thy --- 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 diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Complete_Measure.thy --- 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 \ sets M \ measure (completion M) S = measure M S" + unfolding measure_def by auto + lemma emeasure_completion_UN: "range S \ sets (completion M) \ emeasure (completion M) (\i::nat. (S i)) = emeasure M (\i. main_part M (S i))" diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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 \: "\ division_of S" shows lmeasurable_division: "S \ lmeasurable" (is ?l) - and content_divsion: "(\k\\. measure lebesgue k) = measure lebesgue S" (is ?m) + and content_division: "(\k\\. measure lebesgue k) = measure lebesgue S" (is ?m) proof - { fix d1 d2 assume *: "d1 \ \" "d2 \ \" "d1 \ 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 \Negligibility of a Lipschitz image of a negligible set\ + +lemma measure_eq_0_null_sets: "S \ null_sets M \ measure M S = 0" + by (auto simp: measure_def null_sets_def) + +text\The bound will be eliminated by a sort of onion argument\ +lemma locally_Lipschitz_negl_bounded: + fixes f :: "'M::euclidean_space \ 'N::euclidean_space" + assumes MleN: "DIM('M) \ DIM('N)" "0 < B" "bounded S" "negligible S" + and lips: "\x. x \ S + \ \T. open T \ x \ T \ + (\y \ S \ T. norm(f y - f x) \ 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 \ lmeasurable" + using \negligible S\ by (simp add: negligible_iff_null_sets fmeasurableI_null_sets) + have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)" + using \0 < e\ \0 < B\ by (simp add: divide_simps) + obtain T + where "open T" "S \ T" "T \ lmeasurable" + and "measure lebesgue T \ measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)" + by (rule lmeasurable_outer_open [OF \S \ lmeasurable\ e22]) + then have T: "measure lebesgue T \ e / 2 / (2 * B * DIM('M)) ^ DIM('N)" + using \negligible S\ by (simp add: negligible_iff_null_sets measure_eq_0_null_sets) + have "\r. 0 < r \ r \ 1/2 \ + (x \ S \ (\y. norm(y - x) < r + \ y \ T \ (y \ S \ norm(f y - f x) \ B * norm(y - x))))" + for x + proof (cases "x \ S") + case True + obtain U where "open U" "x \ U" and U: "\y. y \ S \ U \ norm(f y - f x) \ B * norm(y - x)" + using lips [OF \x \ S\] by auto + have "x \ T \ U" + using \S \ T\ \x \ U\ \x \ S\ by auto + then obtain \ where "0 < \" "ball x \ \ T \ U" + by (metis \open T\ \open U\ openE open_Int) + then show ?thesis + apply (rule_tac x="min (1/2) \" 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: "\x. 0 < R x \ R x \ 1/2" + and RT: "\x y. \x \ S; norm(y - x) < R x\ \ y \ T" + and RB: "\x y. \x \ S; y \ S; norm(y - x) < R x\ \ norm(f y - f x) \ B * norm(y - x)" + by metis+ + then have gaugeR: "gauge (\x. ball x (R x))" + by (simp add: gauge_def) + obtain c where c: "S \ cbox (-c *\<^sub>R One) (c *\<^sub>R One)" "box (-c *\<^sub>R One:: 'M) (c *\<^sub>R One) \ {}" + proof - + obtain B where B: "\x. x \ S \ norm x \ B" + using \bounded S\ 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 \ where "countable \" + and Dsub: "\\ \ cbox (-c *\<^sub>R One) (c *\<^sub>R One)" + and cbox: "\K. K \ \ \ interior K \ {} \ (\c d. K = cbox c d)" + and pw: "pairwise (\A B. interior A \ interior B = {}) \" + and Ksub: "\K. K \ \ \ \x \ S \ K. K \ (\x. ball x (R x)) x" + and exN: "\u v. cbox u v \ \ \ \n. \i \ Basis. v \ i - u \ i = (2*c) / 2^n" + and "S \ \\" + using covering_lemma [OF c gaugeR] by force + have "\u v z. K = cbox u v \ box u v \ {} \ z \ S \ z \ cbox u v \ + cbox u v \ ball z (R z)" if "K \ \" for K + proof - + obtain u v where "K = cbox u v" + using \K \ \\ 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: "\K. K \ \ \ + K = cbox (uf K) (vf K) \ box (uf K) (vf K) \ {} \ zf K \ S \ + zf K \ cbox (uf K) (vf K) \ cbox (uf K) (vf K) \ ball (zf K) (R (zf K))" + by metis + define prj1 where "prj1 \ \x::'M. x \ (SOME i. i \ Basis)" + define fbx where "fbx \ \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 \ \" 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) \ i" if "X \ \" "i \ Basis" for X i + proof - + have "cbox (uf X) (vf X) \ \" + using uvz \X \ \\ by auto + with exN obtain n where "\i. i \ Basis \ vf X \ i - uf X \ i = (2*c) / 2^n" + by blast + then show ?thesis + by (simp add: \i \ Basis\ SOME_Basis inner_diff prj1_def) + qed + have countbl: "countable (fbx ` \)" + using \countable \\ by blast + have "(\k\fbx`\'. measure lebesgue k) \ e / 2" if "\' \ \" "finite \'" for \' + proof - + have BM_ge0: "0 \ B * (DIM('M) * prj1 (vf X - uf X))" if "X \ \'" for X + using \0 < B\ \\' \ \\ that vu_pos by fastforce + have "{} \ \'" + using cbox \\' \ \\ interior_empty by blast + have "(\k\fbx`\'. measure lebesgue k) \ setsum (measure lebesgue o fbx) \'" + by (rule setsum_image_le [OF \finite \'\]) (force simp: fbx_def) + also have "\ \ (\X\\'. (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X)" + proof (rule setsum_mono) + fix X assume "X \ \'" + then have "X \ \" using \\' \ \\ by blast + then have ufvf: "cbox (uf X) (vf X) = X" + using uvz by blast + have "prj1 (vf X - uf X) ^ DIM('M) = (\i::'M \ Basis. prj1 (vf X - uf X))" + by (rule setprod_constant [symmetric]) + also have "\ = (\i\Basis. vf X \ i - uf X \ i)" + using prj1_idem [OF \X \ \\] by (auto simp: algebra_simps intro: setprod.cong) + finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\i\Basis. vf X \ i - uf X \ i)" . + have "uf X \ cbox (uf X) (vf X)" "vf X \ cbox (uf X) (vf X)" + using uvz [OF \X \ \\] by (force simp: mem_box)+ + moreover have "cbox (uf X) (vf X) \ ball (zf X) (1/2)" + by (meson R12 order_trans subset_ball uvz [OF \X \ \\]) + ultimately have "uf X \ ball (zf X) (1/2)" "vf X \ ball (zf X) (1/2)" + by auto + then have "dist (vf X) (uf X) \ 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) \ 1" + unfolding prj1_def dist_norm using Basis_le_norm SOME_Basis order_trans by fastforce + have 0: "0 \ prj1 (vf X - uf X)" + using \X \ \\ prj1_def vu_pos by fastforce + have "(measure lebesgue \ fbx) X \ (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))" + apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \X \ \'\ setprod_constant) + apply (simp add: power_mult_distrib \0 < B\ prj1_eq [symmetric]) + using MleN 0 1 uvz \X \ \\ + apply (fastforce simp add: box_ne_empty power_decreasing) + done + also have "\ = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" + by (subst (3) ufvf[symmetric]) simp + finally show "(measure lebesgue \ fbx) X \ (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" . + qed + also have "\ = (2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \'" + by (simp add: setsum_distrib_left) + also have "\ \ e / 2" + proof - + have div: "\' division_of \\'" + apply (auto simp: \finite \'\ \{} \ \'\ division_of_def) + using cbox that apply blast + using pairwise_subset [OF pw \\' \ \\] unfolding pairwise_def apply force+ + done + have le_meaT: "measure lebesgue (\\') \ measure lebesgue T" + proof (rule measure_mono_fmeasurable [OF _ _ \T : lmeasurable\]) + show "(\\') \ sets lebesgue" + using div lmeasurable_division by auto + have "\\' \ \\" + using \\' \ \\ by blast + also have "... \ T" + proof (clarify) + fix x D + assume "x \ D" "D \ \" + show "x \ T" + using Ksub [OF \D \ \\] + by (metis \x \ D\ Int_iff dist_norm mem_ball norm_minus_commute subsetD RT) + qed + finally show "\\' \ T" . + qed + have "setsum (measure lebesgue) \' = setsum content \'" + using \\' \ \\ cbox by (force intro: setsum.cong) + then have "(2 * B * DIM('M)) ^ DIM('N) * setsum (measure lebesgue) \' = + (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\\')" + using content_division [OF div] by auto + also have "\ \ (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T" + apply (rule mult_left_mono [OF le_meaT]) + using \0 < B\ + apply (simp add: algebra_simps) + done + also have "\ \ e / 2" + using T \0 < B\ by (simp add: field_simps) + finally show ?thesis . + qed + finally show ?thesis . + qed + then have e2: "setsum (measure lebesgue) \ \ e / 2" if "\ \ fbx ` \" "finite \" for \ + by (metis finite_subset_image that) + show "\W\lmeasurable. f ` S \ W \ measure lebesgue W < e" + proof (intro bexI conjI) + have "\X\\. f y \ fbx X" if "y \ S" for y + proof - + obtain X where "y \ X" "X \ \" + using \S \ \\\ \y \ S\ by auto + then have y: "y \ ball(zf X) (R(zf X))" + using uvz by fastforce + have conj_le_eq: "z - b \ y \ y \ z + b \ abs(y - z) \ b" for z y b::real + by auto + have yin: "y \ cbox (uf X) (vf X)" and zin: "(zf X) \ cbox (uf X) (vf X)" + using uvz \X \ \\ \y \ X\ by auto + have "norm (y - zf X) \ (\i\Basis. \(y - zf X) \ i\)" + by (rule norm_le_l1) + also have "\ \ real DIM('M) * prj1 (vf X - uf X)" + proof (rule setsum_bounded_above) + fix j::'M assume j: "j \ Basis" + show "\(y - zf X) \ j\ \ prj1 (vf X - uf X)" + using yin zin j + by (fastforce simp add: mem_box prj1_idem [OF \X \ \\ j] inner_diff_left) + qed + finally have nole: "norm (y - zf X) \ DIM('M) * prj1 (vf X - uf X)" + by simp + have fle: "\f y \ i - f(zf X) \ i\ \ B * DIM('M) * prj1 (vf X - uf X)" if "i \ Basis" for i + proof - + have "\f y \ i - f (zf X) \ i\ = \(f y - f (zf X)) \ i\" + by (simp add: algebra_simps) + also have "\ \ norm (f y - f (zf X))" + by (simp add: Basis_le_norm that) + also have "\ \ B * norm(y - zf X)" + by (metis uvz RB \X \ \\ dist_commute dist_norm mem_ball \y \ S\ y) + also have "\ \ B * real DIM('M) * prj1 (vf X - uf X)" + using \0 < B\ 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 \X \ \\) + qed + then show "f ` S \ (\D\\. fbx D)" by auto + next + have 1: "\D. D \ \ \ fbx D \ lmeasurable" + by (auto simp: fbx_def) + have 2: "I' \ \ \ finite I' \ measure lebesgue (\D\I'. fbx D) \ e/2" for I' + by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def) + have 3: "0 \ e/2" + using \0 by auto + show "(\D\\. fbx D) \ lmeasurable" + by (intro fmeasurable_UN_bound[OF \countable \\ 1 2 3]) + have "measure lebesgue (\D\\. fbx D) \ e/2" + by (intro measure_UN_bound[OF \countable \\ 1 2 3]) + then show "measure lebesgue (\D\\. fbx D) < e" + using \0 < e\ by linarith + qed +qed + +proposition negligible_locally_Lipschitz_image: + fixes f :: "'M::euclidean_space \ 'N::euclidean_space" + assumes MleN: "DIM('M) \ DIM('N)" "negligible S" + and lips: "\x. x \ S + \ \T B. open T \ x \ T \ + (\y \ S \ T. norm(f y - f x) \ B * norm(y - x))" + shows "negligible (f ` S)" +proof - + let ?S = "\n. ({x \ S. norm x \ n \ + (\T. open T \ x \ T \ + (\y\S \ T. norm (f y - f x) \ (real n + 1) * norm (y - x)))})" + have negfn: "f ` ?S n \ 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 \negligible S\]) + have "S = (\n. ?S n)" + proof (intro set_eqI iffI) + fix x assume "x \ S" + with lips obtain T B where T: "open T" "x \ T" + and B: "\y. y \ S \ T \ norm(f y - f x) \ B * norm(y - x)" + by metis+ + have no: "norm (f y - f x) \ (nat \max B (norm x)\ + 1) * norm (y - x)" if "y \ S \ T" for y + proof - + have "B * norm(y - x) \ (nat \max B (norm x)\ + 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 \ ?S (nat (ceiling (max B (norm x))))" + apply (simp add: \x \ S \, rule) + using real_nat_ceiling_ge max.bounded_iff apply blast + using T no + apply (force simp: algebra_simps) + done + then show "x \ (\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 \ 'N::euclidean_space" + assumes MleN: "DIM('M) \ DIM('N)" "negligible S" + and diff_f: "f differentiable_on S" + shows "negligible (f ` S)" +proof - + have "\T B. open T \ x \ T \ (\y \ S \ T. norm(f y - f x) \ B * norm(y - x))" + if "x \ S" for x + proof - + obtain f' where "linear f'" + and f': "\e. e>0 \ + \d>0. \y\S. norm (y - x) < d \ + norm (f y - f x - f' (y - x)) \ e * norm (y - x)" + using diff_f \x \ S\ + by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt) + obtain B where "B > 0" and B: "\x. norm (f' x) \ B * norm x" + using linear_bounded_pos \linear f'\ by blast + obtain d where "d>0" + and d: "\y. \y \ S; norm (y - x) < d\ \ + norm (f y - f x - f' (y - x)) \ norm (y - x)" + using f' [of 1] by (force simp:) + have *: "norm (f y - f x) \ (B + 1) * norm (y - x)" + if "y \ S" "norm (y - x) < d" for y + proof - + have "norm (f y - f x) -B * norm (y - x) \ norm (f y - f x) - norm (f' (y - x))" + by (simp add: B) + also have "\ \ norm (f y - f x - f' (y - x))" + by (rule norm_triangle_ineq2) + also have "... \ 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 \d>0\ + 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 \ 'N::euclidean_space" + assumes MlessN: "DIM('M) < DIM('N)" and diff_f: "f differentiable_on S" + shows "negligible (f ` S)" +proof - + have "x \ DIM('M) \ x \ DIM('N)" for x + using MlessN by linarith + obtain lift :: "'M * real \ 'N" and drop :: "'N \ 'M * real" and j :: 'N + where "linear lift" "linear drop" and dropl [simp]: "\z. drop (lift z) = z" + and "j \ Basis" and j: "\x. lift(x,0) \ j = 0" + using lowerdim_embeddings [OF MlessN] by metis + have "negligible {x. x\j = 0}" + by (metis \j \ Basis\ negligible_standard_hyperplane) + then have neg0S: "negligible ((\x. lift (x, 0)) ` S)" + apply (rule negligible_subset) + by (simp add: image_subsetI j) + have diff_f': "f \ fst \ drop differentiable_on (\x. lift (x, 0)) ` S" + using diff_f + apply (clarsimp simp add: differentiable_on_def) + apply (intro differentiable_chain_within linear_imp_differentiable [OF \linear drop\] + linear_imp_differentiable [OF fst_linear]) + apply (force simp: image_comp o_def) + done + have "f = (f o fst o drop o (\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 :: "_ \ 'a :: {banach, second_countable_topology}" shows "set_integrable M k f \ norm (LINT x:k|M. f x) \ LINT x:k|M. norm (f x)" diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Lebesgue_Measure.thy --- 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 \Lebesgue measure\ 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 \Every right continuous and nondecreasing function gives rise to a measure\ @@ -986,4 +986,92 @@ "compact S \ (\c x. \(c *\<^sub>R x) \ S; 0 \ c; x \ S\ \ c = 1) \ S \ null_sets lebesgue" using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed) +lemma outer_regular_lborel: + assumes B: "B \ fmeasurable lborel" "0 < (e::real)" + shows "\U. open U \ B \ U \ emeasure lborel U \ emeasure lborel B + e" +proof - + let ?\ = "emeasure lborel" + let ?B = "\n::nat. ball 0 n :: 'a set" + have B[measurable]: "B \ sets borel" + using B by auto + let ?e = "\n. e*((1/2)^Suc n)" + have "\n. \U. open U \ ?B n \ B \ U \ ?\ (U - B) < ?e n" + proof + fix n :: nat + let ?A = "density lborel (indicator (?B n))" + have emeasure_A: "X \ sets borel \ emeasure ?A X = ?\ (?B n \ X)" for X + by (auto simp add: emeasure_density borel_measurable_indicator indicator_inter_arith[symmetric]) + + have finite_A: "emeasure ?A (space ?A) \ \" + 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 \ U \ open U}. emeasure ?A U)" + using \0 by (auto simp: outer_regular[OF _ finite_A B, symmetric]) + then obtain U where U: "B \ U" "open U" "?\ (?B n \ B) + ?e n > ?\ (?B n \ U)" + unfolding INF_less_iff by (auto simp: emeasure_A) + moreover + { have "?\ ((?B n \ U) - B) = ?\ ((?B n \ U) - (?B n \ B))" + using U by (intro arg_cong[where f="?\"]) auto + also have "\ = ?\ (?B n \ U) - ?\ (?B n \ B)" + using U A.emeasure_finite[of B] + by (intro emeasure_Diff) (auto simp del: A.emeasure_finite simp: emeasure_A) + also have "\ < ?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 "?\ ((?B n \ U) - B) < ?e n" . } + ultimately show "\U. open U \ ?B n \ B \ U \ ?\ (U - B) < ?e n" + by (intro exI[of _ "?B n \ U"]) auto + qed + then obtain U + where U: "\n. open (U n)" "\n. ?B n \ B \ U n" "\n. ?\ (U n - B) < ?e n" + by metis + then show ?thesis + proof (intro exI conjI) + { fix x assume "x \ B" + moreover + have "\n. norm x < real n" + by (simp add: reals_Archimedean2) + then guess n .. + ultimately have "x \ (\n. U n)" + using U(2)[of n] by auto } + note * = this + then show "open (\n. U n)" "B \ (\n. U n)" + using U(1,2) by auto + have "?\ (\n. U n) = ?\ (B \ (\n. U n - B))" + using * U(2) by (intro arg_cong[where ?f="?\"]) auto + also have "\ = ?\ B + ?\ (\n. U n - B)" + using U(1) by (intro plus_emeasure[symmetric]) auto + also have "\ \ ?\ B + (\n. ?\ (U n - B))" + using U(1) by (intro add_mono emeasure_subadditive_countably) auto + also have "\ \ ?\ B + (\n. ennreal (?e n))" + using U(3) by (intro add_mono suminf_le) (auto intro: less_imp_le) + also have "(\n. ennreal (?e n)) = ennreal (e * 1)" + using \0 by (intro suminf_ennreal_eq sums_mult power_half_series) auto + finally show "emeasure lborel (\n. U n) \ emeasure lborel B + ennreal e" + by simp + qed +qed + +lemma lmeasurable_outer_open: + assumes S: "S \ lmeasurable" and "0 < e" + obtains T where "open T" "S \ T" "T \ lmeasurable" "measure lebesgue T \ measure lebesgue S + e" +proof - + obtain S' where S': "S \ S'" "S' \ sets borel" "emeasure lborel S' = emeasure lebesgue S" + using completion_upper[of S lborel] S by auto + then have f_S': "S' \ fmeasurable lborel" + using S by (auto simp: fmeasurable_def) + from outer_regular_lborel[OF this \0] guess U .. note U = this + show thesis + proof (rule that) + show "open U" "S \ U" "U \ lmeasurable" + using f_S' U S' by (auto simp: fmeasurable_def less_top[symmetric] top_unique) + then have "U \ fmeasurable lborel" + by (auto simp: fmeasurable_def) + with S U \0 show "measure lebesgue U \ measure lebesgue S + e" + unfolding S'(3) by (simp add: emeasure_eq_measure2 ennreal_plus[symmetric] del: ennreal_plus) + qed +qed + end diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Analysis/Measure_Space.thy --- 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 \ sets M \ b \ sets M \ a \ b = {} \ emeasure M a + emeasure M b = emeasure M (a \ b)" using additiveD[OF emeasure_additive] .. +lemma emeasure_Union: + "A \ sets M \ B \ sets M \ emeasure M (A \ B) = emeasure M A + emeasure M (B - A)" + using plus_emeasure[of A M "B - A"] by auto + lemma setsum_emeasure: "F`I \ sets M \ disjoint_family_on F I \ finite I \ (\i\I. emeasure M (F i)) = emeasure M (\i\I. F i)" @@ -1749,6 +1753,42 @@ "finite F \ (\S. S \ F \ S \ sets M) \ measure M (\F) \ (\S\F. measure M S)" using measure_UNION_le[of F "\x. x" M] by simp +lemma + assumes "countable I" and I: "\i. i \ I \ A i \ fmeasurable M" + and bound: "\I'. I' \ I \ finite I' \ measure M (\i\I'. A i) \ B" and "0 \ B" + shows fmeasurable_UN_bound: "(\i\I. A i) \ fmeasurable M" (is ?fm) + and measure_UN_bound: "measure M (\i\I. A i) \ B" (is ?m) +proof - + have "?fm \ ?m" + proof cases + assume "I = {}" with \0 \ B\ show ?thesis by simp + next + assume "I \ {}" + have "(\i\I. A i) = (\i. (\n\i. A (from_nat_into I n)))" + by (subst range_from_nat_into[symmetric, OF \I \ {}\ \countable I\]) auto + then have "emeasure M (\i\I. A i) = emeasure M (\i. (\n\i. A (from_nat_into I n)))" by simp + also have "\ = (SUP i. emeasure M (\n\i. A (from_nat_into I n)))" + using I \I \ {}\[THEN from_nat_into] by (intro SUP_emeasure_incseq[symmetric]) (fastforce simp: incseq_Suc_iff)+ + also have "\ \ B" + proof (intro SUP_least) + fix i :: nat + have "emeasure M (\n\i. A (from_nat_into I n)) = measure M (\n\i. A (from_nat_into I n))" + using I \I \ {}\[THEN from_nat_into] by (intro emeasure_eq_measure2 fmeasurable.finite_UN) auto + also have "\ = measure M (\n\from_nat_into I ` {..i}. A n)" + by simp + also have "\ \ B" + by (intro ennreal_leI bound) (auto intro: from_nat_into[OF \I \ {}\]) + finally show "emeasure M (\n\i. A (from_nat_into I n)) \ ennreal B" . + qed + finally have *: "emeasure M (\i\I. A i) \ B" . + then have ?fm + using I \countable I\ by (intro fmeasurableI conjI) (auto simp: less_top[symmetric] top_unique) + with * \0\B\ show ?thesis + by (simp add: emeasure_eq_measure2) + qed + then show ?fm ?m by auto +qed + subsection \Measure spaces with @{term "emeasure M (space M) < \"}\ locale finite_measure = sigma_finite_measure M for M + diff -r 2aa42596edc3 -r 4359400adfe7 src/HOL/Library/Extended_Real.thy --- 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) \ -\ \ (\b>-\. \i\I. b \ f i)" + unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less) + +lemma INF_ereal_add_left: + assumes "I \ {}" "c \ -\" "\x. x \ I \ 0 \ f x" + shows "(INF i:I. f i + c :: ereal) = (INF i:I. f i) + c" +proof - + have "(INF i:I. f i) \ -\" + unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto + then show ?thesis + by (subst continuous_at_Inf_mono[where f="\x. x + c"]) + (auto simp: mono_def ereal_add_mono \I \ {}\ \c \ -\\ continuous_at_imp_continuous_at_within continuous_at) +qed + +lemma INF_ereal_add_right: + assumes "I \ {}" "c \ -\" "\x. x \ I \ 0 \ 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 \ ereal" + assumes nonneg: "\i. i \ I \ 0 \ f i" "\i. i \ I \ 0 \ g i" + assumes directed: "\i j. i \ I \ j \ I \ \k\I. f i + g j \ 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 \ {}" + show ?thesis + proof (rule antisym) + show "(INF i:I. f i) + (INF i:I. g i) \ (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) \ (INF i:I. (INF j:I. f i + g j))" + using directed by (intro INF_greatest) (blast intro: INF_lower2) + also have "\ = (INF i:I. f i + (INF i:I. g i))" + using nonneg by (intro INF_cong refl INF_ereal_add_right \I \ {}\) (auto simp: INF_eq_minf intro!: exI[of _ 0]) + also have "\ = (INF i:I. f i) + (INF i:I. g i)" + using nonneg by (intro INF_ereal_add_left \I \ {}\) (auto simp: INF_eq_minf intro!: exI[of _ 0]) + finally show "(INF i:I. f i + g i) \ (INF i:I. f i) + (INF i:I. g i)" . + qed +qed + lemma INF_ereal_add: fixes f :: "nat \ ereal" assumes "decseq f" "decseq g"