(* Title: HOL/Analysis/Change_Of_Vars.thy Authors: LC Paulson, based on material from HOL Light
*)
section\<open>Change of Variables Theorems\<close>
theory Change_Of_Vars imports Vitali_Covering_Theorem Determinants
begin
subsection \<open>Measurable Shear and Stretch\<close>
proposition fixes a :: "real^'n" assumes"m \ n" and ab_ne: "cbox a b \ {}" and an: "0 \ a$n" shows measurable_shear_interval: "(\x. \ i. if i = m then x$m + x$n else x$i) ` (cbox a b) \ lmeasurable"
(is"?f ` _ \ _") and measure_shear_interval: "measure lebesgue ((\x. \ i. if i = m then x$m + x$n else x$i) ` cbox a b)
= measure lebesgue (cbox a b)" (is "?Q") proof - have lin: "linear ?f" by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps) show fab: "?f ` cbox a b \ lmeasurable" by (simp add: lin measurable_linear_image_interval) let ?c = "\ i. if i = m then b$m + b$n else b$i" let ?mn = "axis m 1 - axis n (1::real)" have eq1: "measure lebesgue (cbox a ?c)
= measure lebesgue (?f ` cbox a b)
+ measure lebesgue (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a$m})
+ measure lebesgue (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m})" proof (rule measure_Un3_negligible) show"cbox a ?c \ {x. ?mn \ x \ a$m} \ lmeasurable" "cbox a ?c \ {x. ?mn \ x \ b$m} \ lmeasurable" by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex) have"negligible {x. ?mn \ x = a$m}" by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) moreoverhave"?f ` cbox a b \ (cbox a ?c \ {x. ?mn \ x \ a $ m}) \ {x. ?mn \ x = a$m}" using\<open>m \<noteq> n\<close> antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') ultimatelyshow"negligible ((?f ` cbox a b) \ (cbox a ?c \ {x. ?mn \ x \ a $ m}))" by (rule negligible_subset) have"negligible {x. ?mn \ x = b$m}" by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) moreoverhave"(?f ` cbox a b) \ (cbox a ?c \ {x. ?mn \ x \ b$m}) \ {x. ?mn \ x = b$m}" using\<open>m \<noteq> n\<close> antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') ultimatelyshow"negligible (?f ` cbox a b \ (cbox a ?c \ {x. ?mn \ x \ b$m}))" by (rule negligible_subset) have"negligible {x. ?mn \ x = b$m}" by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) moreoverhave"(cbox a ?c \ {x. ?mn \ x \ a $ m} \ (cbox a ?c \ {x. ?mn \ x \ b$m})) \ {x. ?mn \ x = b$m}" using\<open>m \<noteq> n\<close> ab_ne apply (clarsimp simp: algebra_simps mem_box_cart inner_axis') by (smt (verit, ccfv_SIG) interval_ne_empty_cart(1)) ultimatelyshow"negligible (cbox a ?c \ {x. ?mn \ x \ a $ m} \ (cbox a ?c \ {x. ?mn \ x \ b$m}))" by (rule negligible_subset) show"?f ` cbox a b \ cbox a ?c \ {x. ?mn \ x \ a $ m} \ cbox a ?c \ {x. ?mn \ x \ b$m} = cbox a ?c" (is "?lhs = _") proof show"?lhs \ cbox a ?c" by (auto simp: mem_box_cart add_mono) (meson add_increasing2 an order_trans) show"cbox a ?c \ ?lhs" apply (clarsimp simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF \m \n\]) by (smt (verit, del_insts) mem_box_cart(2) vec_lambda_beta) qed qed (fact fab) let ?d = "\ i. if i = m then a $ m - b $ m else 0" have eq2: "measure lebesgue (cbox a ?c \ {x. ?mn \ x \ a $ m}) + measure lebesgue (cbox a ?c \ {x. ?mn \ x \ b$m})
= measure lebesgue (cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i))" proof (rule measure_translate_add[of "cbox a ?c \ {x. ?mn \ x \ a$m}" "cbox a ?c \{x. ?mn \ x \ b$m}" "(\ i. if i = m then a$m - b$m else 0)" "cbox a (\ i. if i = m then a$m + b$n else b$i)"]) show"(cbox a ?c \ {x. ?mn \ x \ a$m}) \ lmeasurable" "cbox a ?c \ {x. ?mn \ x \ b$m} \ lmeasurable" by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex) have"\x. \x $ n + a $ m \ x $ m\ \<Longrightarrow> x \<in> (+) (\<chi> i. if i = m then a $ m - b $ m else 0) ` {x. x $ n + b $ m \<le> x $ m}" using\<open>m \<noteq> n\<close> by (rule_tac x="x - (\ i. if i = m then a$m - b$m else 0)" in image_eqI)
(simp_all add: mem_box_cart) thenhave imeq: "(+) ?d ` {x. b $ m \ ?mn \ x} = {x. a $ m \ ?mn \ x}" using\<open>m \<noteq> n\<close> by (auto simp: mem_box_cart inner_axis' algebra_simps) have"\x. \0 \ a $ n; x $ n + a $ m \ x $ m; \<forall>i. i \<noteq> m \<longrightarrow> a $ i \<le> x $ i \<and> x $ i \<le> b $ i\<rbrakk> \<Longrightarrow> a $ m \<le> x $ m" using\<open>m \<noteq> n\<close> by force thenhave"(+) ?d ` (cbox a ?c \ {x. b $ m \ ?mn \ x})
= cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i) \<inter> {x. a $ m \<le> ?mn \<bullet> x}" using an ab_ne apply (simp add: cbox_translation [symmetric] translation_Int interval_ne_empty_cart imeq) apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib) by (metis (full_types) add_mono mult_2_right) thenshow"cbox a ?c \ {x. ?mn \ x \ a $ m} \
(+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x}) =
cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i)" (is "?lhs = ?rhs") using an \<open>m \<noteq> n\<close> apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib, force) apply (drule_tac x=n in spec)+ by (meson ab_ne add_mono_thms_linordered_semiring(3) dual_order.trans interval_ne_empty_cart(1)) have"negligible{x. ?mn \ x = a$m}" by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) moreoverhave"(cbox a ?c \ {x. ?mn \ x \ a $ m} \
(+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x})) \<subseteq> {x. ?mn \<bullet> x = a$m}" using\<open>m \<noteq> n\<close> antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') ultimatelyshow"negligible (cbox a ?c \ {x. ?mn \ x \ a $ m} \
(+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x}))" by (rule negligible_subset) qed have ac_ne: "cbox a ?c \ {}" by (smt (verit, del_insts) ab_ne an interval_ne_empty_cart(1) vec_lambda_beta) have ax_ne: "cbox a (\ i. if i = m then a $ m + b $ n else b $ i) \ {}" using ab_ne an by (smt (verit, ccfv_threshold) interval_ne_empty_cart(1) vec_lambda_beta) have eq3: "measure lebesgue (cbox a ?c) = measure lebesgue (cbox a (\ i. if i = m then a$m + b$n else b$i)) + measure lebesgue (cbox a b)" by (simp add: content_cbox_if_cart ab_ne ac_ne ax_ne algebra_simps prod.delta_remove
if_distrib [of "\u. u - z" for z] prod.remove) show ?Q using eq1 eq2 eq3 by (simp add: algebra_simps) qed
proposition fixes S :: "(real^'n) set" assumes"S \ lmeasurable" shows measurable_stretch: "((\x. \ k. m k * x$k) ` S) \ lmeasurable" (is "?f ` S \ _") and measure_stretch: "measure lebesgue ((\x. \ k. m k * x$k) ` S) = \prod m UNIV\* measure lebesgue S"
(is"?MEQ") proof - have"(?f ` S) \ lmeasurable \ ?MEQ" proof (cases "\k. m k \ 0") case True have m0: "0 < \prod m UNIV\" using True by simp have"(indicat_real (?f ` S) has_integral \prod m UNIV\ * measure lebesgue S) UNIV" proof (clarsimp simp add: has_integral_alt [where i=UNIV]) fix e :: "real" assume"e > 0" have"(indicat_real S has_integral (measure lebesgue S)) UNIV" using assms lmeasurable_iff_has_integral by blast thenobtain B where"B>0" and B: "\a b. ball 0 B \ cbox a b \ \<exists>z. (indicat_real S has_integral z) (cbox a b) \<and> \<bar>z - measure lebesgue S\<bar> < e / \<bar>prod m UNIV\<bar>" by (simp add: has_integral_alt [where i=UNIV]) (metis (full_types) divide_pos_pos m0 m0 \<open>e > 0\<close>) show"\B>0. \a b. ball 0 B \ cbox a b \
(\<exists>z. (indicat_real (?f ` S) has_integral z) (cbox a b) \<and> \<bar>z - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e)" proof (intro exI conjI allI) let ?C = "Max (range (\k. \m k\)) * B" show"?C > 0" using True \<open>B > 0\<close> by (simp add: Max_gr_iff) show"ball 0 ?C \ cbox u v \
(\<exists>z. (indicat_real (?f ` S) has_integral z) (cbox u v) \<and> \<bar>z - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e)" for u v proof assume uv: "ball 0 ?C \ cbox u v" with\<open>?C > 0\<close> have cbox_ne: "cbox u v \<noteq> {}" using centre_in_ball by blast let ?\<alpha> = "\<lambda>k. u$k / m k" let ?\<beta> = "\<lambda>k. v$k / m k" have invm0: "\k. inverse (m k) \ 0" using True by auto have"ball 0 B \ (\x. \ k. x $ k / m k) ` ball 0 ?C" proof clarsimp fix x :: "real^'n" assume x: "norm x < B" have [simp]: "\Max (range (\k. \m k\))\ = Max (range (\k. \m k\))" by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI) have"norm (\ k. m k * x $ k) \ norm (Max (range (\k. \m k\)) *\<^sub>R x)" by (rule norm_le_componentwise_cart) (auto simp: abs_mult intro: mult_right_mono) alsohave"\ < ?C" using x \<open>0 < (MAX k. \<bar>m k\<bar>) * B\<close> \<open>0 < B\<close> zero_less_mult_pos2 by fastforce finallyhave"norm (\ k. m k * x $ k) < ?C" . thenshow"x \ (\x. \ k. x $ k / m k) ` ball 0 ?C" using stretch_Galois [of "inverse \ m"] True by (auto simp: image_iff field_simps) qed thenhave Bsub: "ball 0 B \ cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k))" using cbox_ne uv image_stretch_interval_cart [of "inverse \ m" u v, symmetric] by (force simp: field_simps) obtain z where zint: "(indicat_real S has_integral z) (cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k)))" and zless: "\z - measure lebesgue S\ < e / \prod m UNIV\" using B [OF Bsub] by blast have ind: "indicat_real (?f ` S) = (\x. indicator S (\ k. x$k / m k))" using True stretch_Galois [of m] by (force simp: indicator_def) show"\z. (indicat_real (?f ` S) has_integral z) (cbox u v) \ \<bar>z - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e" proof (simp add: ind, intro conjI exI) have"((\x. indicat_real S (\ k. x $ k/ m k)) has_integral z *\<^sub>R \prod m UNIV\)
((\<lambda>x. \<chi> k. x $ k * m k) ` cbox (\<chi> k. min (?\<alpha> k) (?\<beta> k)) (\<chi> k. max (?\<alpha> k) (?\<beta> k)))" using True has_integral_stretch_cart [OF zint, of "inverse \ m"] by (simp add: field_simps prod_dividef) moreoverhave"((\x. \ k. x $ k * m k) ` cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k))) = cbox u v" using True image_stretch_interval_cart [of "inverse \ m" u v, symmetric]
image_stretch_interval_cart [of "\k. 1" u v, symmetric] \cbox u v \ {}\ by (simp add: field_simps image_comp o_def) ultimatelyshow"((\x. indicat_real S (\ k. x $ k/ m k)) has_integral z *\<^sub>R \prod m UNIV\) (cbox u v)" by simp have"\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\
= \<bar>prod m UNIV\<bar> * \<bar>z - measure lebesgue S\<bar>" by (metis (no_types, opaque_lifting) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib') alsohave"\ < e" using zless True by (simp add: field_simps) finallyshow"\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\ < e" . qed qed qed qed thenshow ?thesis by (auto simp: has_integral_integrable integral_unique lmeasure_integral_UNIV measurable_integrable) next case False thenobtain k where"m k = 0"and prm: "prod m UNIV = 0" by auto have nfS: "negligible (?f ` S)" by (rule negligible_subset [OF negligible_standard_hyperplane_cart]) (use\<open>m k = 0\<close> in auto) thenshow ?thesis by (simp add: negligible_iff_measure prm) qed thenshow"(?f ` S) \ lmeasurable" ?MEQ by metis+ qed
proposition fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes"linear f""S \ lmeasurable" shows measurable_linear_image: "(f ` S) \ lmeasurable" and measure_linear_image: "measure lebesgue (f ` S) = \det (matrix f)\ * measure lebesgue S" (is "?Q f S") proof - have"\S \ lmeasurable. (f ` S) \ lmeasurable \ ?Q f S" proof (rule induct_linear_elementary [OF \<open>linear f\<close>]; intro ballI) fix f g and S :: "(real,'n) vec set" assume"linear f"and"linear g" and f [rule_format]: "\S \ lmeasurable. f ` S \ lmeasurable \ ?Q f S" and g [rule_format]: "\S \ lmeasurable. g ` S \ lmeasurable \ ?Q g S" and S: "S \ lmeasurable" thenhave gS: "g ` S \ lmeasurable" by blast show"(f \ g) ` S \ lmeasurable \ ?Q (f \ g) S" using f [OF gS] g [OF S] matrix_compose [OF \<open>linear g\<close> \<open>linear f\<close>] by (simp add: o_def image_comp abs_mult det_mul) next fix f :: "real^'n::_ \ real^'n::_" and i and S :: "(real^'n::_) set" assume"linear f"and 0: "\x. f x $ i = 0" and "S \ lmeasurable" thenhave"\ inj f" by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component) have detf: "det (matrix f) = 0" using\<open>\<not> inj f\<close> det_nz_iff_inj[OF \<open>linear f\<close>] by blast show"f ` S \ lmeasurable \ ?Q f S" proof show"f ` S \ lmeasurable" using lmeasurable_iff_indicator_has_integral \<open>linear f\<close> \<open>\<not> inj f\<close> negligible_UNIV negligible_linear_singular_image by blast have"measure lebesgue (f ` S) = 0" by (meson \<open>\<not> inj f\<close> \<open>linear f\<close> negligible_imp_measure0 negligible_linear_singular_image) alsohave"\ = \det (matrix f)\ * measure lebesgue S" by (simp add: detf) finallyshow"?Q f S" . qed next fix c and S :: "(real^'n::_) set" assume"S \ lmeasurable" show"(\a. \ i. c i * a $ i) ` S \ lmeasurable \ ?Q (\a. \ i. c i * a $ i) S" proof show"(\a. \ i. c i * a $ i) ` S \ lmeasurable" by (simp add: \<open>S \<in> lmeasurable\<close> measurable_stretch) show"?Q (\a. \ i. c i * a $ i) S" by (simp add: measure_stretch [OF \<open>S \<in> lmeasurable\<close>, of c] axis_def matrix_def det_diagonal) qed next fix m :: "'n"and n :: "'n"and S :: "(real, 'n) vec set" assume"m \ n" and "S \ lmeasurable" let ?h = "\v::(real, 'n) vec. \ i. v $ Transposition.transpose m n i" have lin: "linear ?h" by (rule linearI) (simp_all add: plus_vec_def scaleR_vec_def) have meq: "measure lebesgue ((\v::(real, 'n) vec. \ i. v $ Transposition.transpose m n i) ` cbox a b)
= measure lebesgue (cbox a b)" for a b proof (cases "cbox a b = {}") case True thenshow ?thesis by simp next case False thenhave him: "?h ` (cbox a b) \ {}" by blast have eq: "?h ` (cbox a b) = cbox (?h a) (?h b)" by (auto simp: image_iff lambda_swap_Galois mem_box_cart) (metis transpose_involutory)+ show ?thesis using him prod.permute [OF permutes_swap_id, where S=UNIV and g="\i. (b - a)$i", symmetric] by (simp add: eq content_cbox_cart False) qed have"(\ i j. if Transposition.transpose m n i = j then 1 else 0) = (\ i j. if j = Transposition.transpose m n i then 1 else (0::real))" by (auto intro!: Cart_lambda_cong) thenhave"matrix ?h = transpose(\ i j. mat 1 $ i $ Transposition.transpose m n j)" by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def) thenhave 1: "\det (matrix ?h)\ = 1" by (simp add: det_permute_columns permutes_swap_id sign_swap_id abs_mult) show"?h ` S \ lmeasurable \ ?Q ?h S" using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force next fix m n :: "'n"and S :: "(real, 'n) vec set" assume"m \ n" and "S \ lmeasurable" let ?h = "\v::(real, 'n) vec. \ i. if i = m then v $ m + v $ n else v $ i" have lin: "linear ?h" by (rule linearI) (auto simp: algebra_simps plus_vec_def scaleR_vec_def vec_eq_iff)
consider "m < n" | " n < m" using\<open>m \<noteq> n\<close> less_linear by blast thenhave 1: "det(matrix ?h) = 1" proof cases assume"m < n" have *: "matrix ?h $ i $ j = (0::real)"if"j < i"for i j :: 'n proof - have"axis j 1 = (\ n. if n = j then 1 else (0::real))" using axis_def by blast thenhave"(\ p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)" using\<open>j < i\<close> axis_def \<open>m < n\<close> by auto with\<open>m < n\<close> show ?thesis by (auto simp: matrix_def axis_def cong: if_cong) qed show ?thesis using\<open>m \<noteq> n\<close> by (subst det_upperdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong) next assume"n < m" have *: "matrix ?h $ i $ j = (0::real)"if"j > i"for i j :: 'n proof - have"axis j 1 = (\ n. if n = j then 1 else (0::real))" using axis_def by blast thenhave"(\ p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)" using\<open>j > i\<close> axis_def \<open>m > n\<close> by auto with\<open>m > n\<close> show ?thesis by (auto simp: matrix_def axis_def cong: if_cong) qed show ?thesis using\<open>m \<noteq> n\<close> by (subst det_lowerdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong) qed have meq: "measure lebesgue (?h ` (cbox a b)) = measure lebesgue (cbox a b)"for a b proof (cases "cbox a b = {}") case True thenshow ?thesis by simp next case False thenhave ne: "(+) (\ i. if i = n then - a $ n else 0) ` cbox a b \ {}" by auto let ?v = "\ i. if i = n then - a $ n else 0" have"?h ` cbox a b
= (+) (\<chi> i. if i = m \<or> i = n then a $ n else 0) ` ?h ` (+) ?v ` (cbox a b)" using\<open>m \<noteq> n\<close> unfolding image_comp o_def by (force simp: vec_eq_iff) thenhave"measure lebesgue (?h ` (cbox a b))
= measure lebesgue ((\<lambda>v. \<chi> i. if i = m then v $ m + v $ n else v $ i) `
(+) ?v ` cbox a b)" by (rule ssubst) (rule measure_translation) alsohave"\ = measure lebesgue ((\v. \ i. if i = m then v $ m + v $ n else v $ i) ` cbox (?v +a) (?v + b))" by (metis (no_types, lifting) cbox_translation) alsohave"\ = measure lebesgue ((+) ?v ` cbox a b)" apply (subst measure_shear_interval) using\<open>m \<noteq> n\<close> ne apply auto apply (simp add: cbox_translation) by (metis cbox_borel cbox_translation measure_completion sets_lborel) alsohave"\ = measure lebesgue (cbox a b)" by (rule measure_translation) finallyshow ?thesis . qed show"?h ` S \ lmeasurable \ ?Q ?h S" using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force qed with assms show"(f ` S) \ lmeasurable" "?Q f S" by metis+ qed
lemma fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes f: "orthogonal_transformation f"and S: "S \ lmeasurable" shows measurable_orthogonal_image: "f ` S \ lmeasurable" and measure_orthogonal_image: "measure lebesgue (f ` S) = measure lebesgue S" proof - have"linear f" by (simp add: f orthogonal_transformation_linear) thenshow"f ` S \ lmeasurable" by (metis S measurable_linear_image) show"measure lebesgue (f ` S) = measure lebesgue S" by (simp add: measure_linear_image \<open>linear f\<close> S f) qed
proposition measure_semicontinuous_with_hausdist_explicit: assumes"bounded S"and neg: "negligible(frontier S)"and"e > 0" obtains d where"d > 0" "\T. \T \ lmeasurable; \y. y \ T \ \x. x \ S \ dist x y < d\ \<Longrightarrow> measure lebesgue T < measure lebesgue S + e" proof (cases "S = {}") case True with that \<open>e > 0\<close> show ?thesis by force next case False thenhave frS: "frontier S \ {}" using\<open>bounded S\<close> frontier_eq_empty not_bounded_UNIV by blast have"S \ lmeasurable" by (simp add: \<open>bounded S\<close> measurable_Jordan neg) have null: "(frontier S) \ null_sets lebesgue" by (metis neg negligible_iff_null_sets) have"frontier S \ lmeasurable" and mS0: "measure lebesgue (frontier S) = 0" using neg negligible_imp_measurable negligible_iff_measure by blast+ with\<open>e > 0\<close> sets_lebesgue_outer_open obtain U where"open U" and U: "frontier S \ U" "U - frontier S \ lmeasurable" "emeasure lebesgue (U - frontier S) < e" by (metis fmeasurableD) with null have"U \ lmeasurable" by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel) have"measure lebesgue (U - frontier S) = measure lebesgue U" using mS0 by (simp add: \<open>U \<in> lmeasurable\<close> fmeasurableD measure_Diff_null_set null) with U have mU: "measure lebesgue U < e" by (simp add: emeasure_eq_measure2 ennreal_less_iff) show ?thesis proof have"U \ UNIV" using\<open>U \<in> lmeasurable\<close> by auto thenhave"- U \ {}" by blast with\<open>open U\<close> \<open>frontier S \<subseteq> U\<close> show "setdist (frontier S) (- U) > 0" by (auto simp: \<open>bounded S\<close> open_closed compact_frontier_bounded setdist_gt_0_compact_closed frS) fix T assume"T \ lmeasurable" and T: "\t. t \ T \ \y. y \ S \ dist y t < setdist (frontier S) (- U)" thenhave"measure lebesgue T - measure lebesgue S \ measure lebesgue (T - S)" by (simp add: \<open>S \<in> lmeasurable\<close> measure_diff_le_measure_setdiff) alsohave"\ \ measure lebesgue U" proof - have"T - S \ U" proof clarify fix x assume"x \ T" and "x \ S" thenobtain y where"y \ S" and y: "dist y x < setdist (frontier S) (- U)" using T by blast have"closed_segment x y \ frontier S \ {}" using connected_Int_frontier \<open>x \<notin> S\<close> \<open>y \<in> S\<close> by blast thenobtain z where z: "z \ closed_segment x y" "z \ frontier S" by auto with y have"dist z x < setdist(frontier S) (- U)" by (auto simp: dist_commute dest!: dist_in_closed_segment) with z have False if"x \ -U" using setdist_le_dist [OF \<open>z \<in> frontier S\<close> that] by auto thenshow"x \ U" by blast qed thenshow ?thesis by (simp add: \<open>S \<in> lmeasurable\<close> \<open>T \<in> lmeasurable\<close> \<open>U \<in> lmeasurable\<close> fmeasurableD measure_mono_fmeasurable sets.Diff) qed finallyhave"measure lebesgue T - measure lebesgue S \ measure lebesgue U" . with mU show"measure lebesgue T < measure lebesgue S + e" by linarith qed qed
proposition fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ lmeasurable" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and int: "(\x. \det (matrix (f' x))\) integrable_on S" and bounded: "\x. x \ S \ \det (matrix (f' x))\ \ B" shows measurable_bounded_differentiable_image: "f ` S \ lmeasurable" and measure_bounded_differentiable_image: "measure lebesgue (f ` S) \ B * measure lebesgue S" (is "?M") proof - have"f ` S \ lmeasurable \ measure lebesgue (f ` S) \ B * measure lebesgue S" proof (cases "B < 0") case True thenhave"S = {}" by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI) thenshow ?thesis by auto next case False thenhave"B \ 0" by arith let ?\<mu> = "measure lebesgue" have f_diff: "f differentiable_on S" using deriv by (auto simp: differentiable_on_def differentiable_def) have eps: "f ` S \ lmeasurable" "?\ (f ` S) \ (B+e) * ?\ S" (is "?ME") if"e > 0"for e proof - have eps_d: "f ` S \ lmeasurable" "?\ (f ` S) \ (B+e) * (?\ S + d)" (is "?MD") if"d > 0"for d proof - obtain T where T: "open T""S \ T" and TS: "(T-S) \ lmeasurable" and "emeasure lebesgue (T-S) < ennreal d" using S \<open>d > 0\<close> sets_lebesgue_outer_open by blast thenhave"?\ (T-S) < d" by (metis emeasure_eq_measure2 ennreal_leI not_less) with S T TS have"T \ lmeasurable" and Tless: "?\ T < ?\ S + d" by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D) have"\r. 0 < r \ r < d \ ball x r \ T \ f ` (S \ ball x r) \ lmeasurable \
?\<mu> (f ` (S \<inter> ball x r)) \<le> (B + e) * ?\<mu> (ball x r)" if"x \ S" "d > 0" for x d proof - have lin: "linear (f' x)" and lim0: "((\y. (f y - (f x + f' x (y - x))) /\<^sub>R norm(y - x)) \ 0) (at x within S)" using deriv \<open>x \<in> S\<close> by (auto simp: has_derivative_within bounded_linear.linear field_simps) have bo: "bounded (f' x ` ball 0 1)" by (simp add: bounded_linear_image linear_linear lin) 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]) 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: "\U. \U \ lmeasurable; \y. y \ U \ \z. z \ f' x ` ball 0 1 \ dist z y < k\ \<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 \ T" using\<open>x \<in> S\<close> \<open>open T\<close> \<open>S \<subseteq> T\<close> openE by blast obtain\<zeta> where "0 < \<zeta>" and\<zeta>: "\<And>y. \<lbrakk>y \<in> S; y \<noteq> x; dist y x < \<zeta>\<rbrakk> \<Longrightarrow> norm (f y - (f x + f' x (y - x))) / norm (y - x) < k" using lim0 \<open>k > 0\<close> by (simp add: Lim_within) (auto simp add: field_simps)
define r where"r \ min (min l (\/2)) (min 1 (d/2))" show ?thesis proof (intro exI conjI) show"r > 0""r < d" using\<open>l > 0\<close> \<open>\<zeta> > 0\<close> \<open>d > 0\<close> by (auto simp: r_def) have"r \ l" by (auto simp: r_def) with l show"ball x r \ T" by auto have ex_lessK: "\x' \ ball 0 1. dist (f' x x') ((f y - f x) /\<^sub>R r) < k" if"y \ S" and "dist x y < r" for y proof (cases "y = x") case True with lin linear_0 \<open>k > 0\<close> that show ?thesis by (rule_tac x=0 in bexI) (auto simp: linear_0) next case False thenshow ?thesis proof (rule_tac x="(y - x) /\<^sub>R r" in bexI) have"f' x ((y - x) /\<^sub>R r) = f' x (y - x) /\<^sub>R r" by (simp add: lin linear_scale) thenhave"dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) = norm (f' x (y - x) /\<^sub>R r - (f y - f x) /\<^sub>R r)" by (simp add: dist_norm) alsohave"\ = norm (f' x (y - x) - (f y - f x)) / r" using\<open>r > 0\<close> by (simp add: divide_simps scale_right_diff_distrib [symmetric]) alsohave"\ \ norm (f y - (f x + f' x (y - x))) / norm (y - x)" using that \<open>r > 0\<close> False by (simp add: field_split_simps dist_norm norm_minus_commute mult_right_mono) alsohave"\ < k" using that \<open>0 < \<zeta>\<close> by (simp add: dist_commute r_def \<zeta> [OF \<open>y \<in> S\<close> False]) finallyshow"dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) < k" . show"(y - x) /\<^sub>R r \ ball 0 1" using that \<open>r > 0\<close> by (simp add: dist_norm divide_simps norm_minus_commute) qed qed let ?rfs = "(\x. x /\<^sub>R r) ` (+) (- f x) ` f ` (S \ ball x r)" have rfs_mble: "?rfs \ lmeasurable" proof (rule bounded_set_imp_lmeasurable) have"f differentiable_on S \ ball x r" using f_diff by (auto simp: fmeasurableD differentiable_on_subset) with S show"?rfs \ sets lebesgue" by (auto simp: sets.Int intro!: lebesgue_sets_translation differentiable_image_in_sets_lebesgue) let ?B = "(\(x, y). x + y) ` (f' x ` ball 0 1 \ ball 0 k)" have"bounded ?B" by (simp add: bounded_plus [OF bo]) moreoverhave"?rfs \ ?B" apply (auto simp: dist_norm image_iff dest!: ex_lessK) by (metis (no_types, opaque_lifting) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball) ultimatelyshow"bounded (?rfs)" by (rule bounded_subset) qed thenhave"(\x. r *\<^sub>R x) ` ?rfs \ lmeasurable" by (simp add: measurable_linear_image) with\<open>r > 0\<close> have "(+) (- f x) ` f ` (S \<inter> ball x r) \<in> lmeasurable" by (simp add: image_comp o_def) thenhave"(+) (f x) ` (+) (- f x) ` f ` (S \ ball x r) \ lmeasurable" using measurable_translation by blast thenshow fsb: "f ` (S \ ball x r) \ lmeasurable" by (simp add: image_comp o_def) have"?\ (f ` (S \ ball x r)) = ?\ (?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) alsohave"\ \ (\det (matrix (f' x))\ * ?unit_vol + e * ?unit_vol) * r ^ CARD('n)" proof - have"?\ (?rfs) < ?\ (f' x ` ball 0 1) + e * ?unit_vol" using rfs_mble by (force intro: k dest!: ex_lessK) thenhave"?\ (?rfs) < \det (matrix (f' x))\ * ?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 alsohave"\ \ (B + e) * ?\ (ball x r)" 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) finallyshow"?\ (f ` (S \ ball x r)) \ (B + e) * ?\ (ball x r)" . qed qed thenobtain r where
r0d: "\x d. \x \ S; d > 0\ \ 0 < r x d \ r x d < d" and rT: "\x d. \x \ S; d > 0\ \ ball x (r x d) \ T" and r: "\x d. \x \ S; d > 0\ \
(f ` (S \<inter> ball x (r x d))) \<in> lmeasurable \<and>
?\<mu> (f ` (S \<inter> ball x (r x d))) \<le> (B + e) * ?\<mu> (ball x (r x d))" by metis obtain C where"countable C"and Csub: "C \ {(x,r x t) |x t. x \ S \ 0 < t}" and pwC: "pairwise (\i j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C" and negC: "negligible(S - (\i \ C. ball (fst i) (snd i)))" apply (rule Vitali_covering_theorem_balls [of S "{(x,r x t) |x t. x \ S \ 0 < t}" fst snd]) apply auto by (metis dist_eq_0_iff r0d) let ?UB = "(\(x,s) \ C. ball x s)" have eq: "f ` (S \ ?UB) = (\(x,s) \ C. f ` (S \ ball x s))" by auto have mle: "?\ (\(x,s) \ K. f ` (S \ ball x s)) \ (B + e) * (?\ S + d)" (is "?l \?r") if"K \ C" and "finite K" for K proof - have gt0: "b > 0"if"(a, b) \ K" for a b using Csub that \<open>K \<subseteq> C\<close> r0d by auto have inj: "inj_on (\(x, y). ball x y) K" by (force simp: inj_on_def ball_eq_ball_iff dest: gt0) have disjnt: "disjoint ((\(x, y). ball x y) ` K)" using pwC that pairwise_image pairwise_mono by fastforce have"?l \ (\i\K. ?\ (case i of (x, s) \ f ` (S \ ball x s)))" proof (rule measure_UNION_le [OF \<open>finite K\<close>], clarify) fix x r assume"(x,r) \ K" thenhave"x \ S" using Csub \<open>K \<subseteq> C\<close> by auto show"f ` (S \ ball x r) \ sets lebesgue" by (meson Int_lower1 S differentiable_on_subset f_diff fmeasurableD lmeasurable_ball order_refl sets.Int differentiable_image_in_sets_lebesgue) qed alsohave"\ \ (\(x,s) \ K. (B + e) * ?\ (ball x s))" using Csub r \<open>K \<subseteq> C\<close> by (intro sum_mono) auto alsohave"\ = (B + e) * (\(x,s) \ K. ?\ (ball x s))" by (simp add: prod.case_distrib sum_distrib_left) alsohave"\ = (B + e) * sum ?\ ((\(x, y). ball x y) ` K)" using\<open>B \<ge> 0\<close> \<open>e > 0\<close> by (simp add: inj sum.reindex prod.case_distrib) alsohave"\ = (B + e) * ?\ (\(x,s) \ K. ball x s)" using\<open>B \<ge> 0\<close> \<open>e > 0\<close> that by (subst measure_Union') (auto simp: disjnt measure_Union') alsohave"\ \ (B + e) * ?\ T" using\<open>B \<ge> 0\<close> \<open>e > 0\<close> that apply simp using measure_mono_fmeasurable [OF _ _ \<open>T \<in> lmeasurable\<close>] Csub rT by (smt (verit) SUP_least measure_nonneg measure_notin_sets mem_Collect_eq old.prod.case subset_iff) alsohave"\ \ (B + e) * (?\ S + d)" using\<open>B \<ge> 0\<close> \<open>e > 0\<close> Tless by simp finallyshow ?thesis . qed have fSUB_mble: "(f ` (S \ ?UB)) \ lmeasurable" unfolding eq using Csub r False \<open>e > 0\<close> that by (auto simp: intro!: fmeasurable_UN_bound [OF \<open>countable C\<close> _ mle]) have fSUB_meas: "?\ (f ` (S \ ?UB)) \ (B + e) * (?\ S + d)" (is "?MUB") unfolding eq using Csub r False \<open>e > 0\<close> that by (auto simp: intro!: measure_UN_bound [OF \<open>countable C\<close> _ mle]) have neg: "negligible ((f ` (S \ ?UB) - f ` S) \ (f ` S - f ` (S \ ?UB)))" proof (rule negligible_subset [OF negligible_differentiable_image_negligible [OF order_refl negC, where f=f]]) show"f differentiable_on S - (\i\C. ball (fst i) (snd i))" by (meson DiffE differentiable_on_subset subsetI f_diff) qed force show"f ` S \ lmeasurable" by (rule lmeasurable_negligible_symdiff [OF fSUB_mble neg]) show ?MD using fSUB_meas measure_negligible_symdiff [OF fSUB_mble neg] by simp qed show"f ` S \ lmeasurable" using eps_d [of 1] by simp show ?ME proof (rule field_le_epsilon) fix\<delta> :: real assume"0 < \" thenshow"?\ (f ` S) \ (B + e) * ?\ S + \" using eps_d [of "\ / (B+e)"] \e > 0\ \B \ 0\ by (auto simp: divide_simps mult_ac) qed qed show ?thesis proof (cases "?\ S = 0") case True with eps have"?\ (f ` S) = 0" by (metis mult_zero_right not_le zero_less_measure_iff) thenshow ?thesis using eps [of 1] by (simp add: True) next case False have"?\ (f ` S) \ B * ?\ S" proof (rule field_le_epsilon) fix e :: real assume"e > 0" thenshow"?\ (f ` S) \ B * ?\ S + e" using eps [of "e / ?\ S"] False by (auto simp: algebra_simps zero_less_measure_iff) qed with eps [of 1] show ?thesis by auto qed qed thenshow"f ` S \ lmeasurable" ?M by blast+ qed
lemma m_diff_image_weak: fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ lmeasurable" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and int: "(\x. \det (matrix (f' x))\) integrable_on S" shows"f ` S \ lmeasurable \ measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" proof - let ?\<mu> = "measure lebesgue" have aint_S: "(\x. \det (matrix (f' x))\) absolutely_integrable_on S" using int unfolding absolutely_integrable_on_def by auto
define m where"m \ integral S (\x. \det (matrix (f' x))\)" have *: "f ` S \ lmeasurable" "?\ (f ` S) \ m + e * ?\ S" if"e > 0"for e proof -
define T where"T \ \n. {x \ S. n * e \ \det (matrix (f' x))\ \ \<bar>det (matrix (f' x))\<bar> < (Suc n) * e}" have meas_t: "T n \ lmeasurable" for n proof - have *: "(\x. \det (matrix (f' x))\) \ borel_measurable (lebesgue_on S)" using aint_S by (simp add: S borel_measurable_restrict_space_iff fmeasurableD set_integrable_def) have [intro]: "x \ sets (lebesgue_on S) \ x \ sets lebesgue" for x using S sets_restrict_space_subset by blast have"{x \ S. real n * e \ \det (matrix (f' x))\} \ sets lebesgue" using * by (auto simp: borel_measurable_iff_halfspace_ge space_restrict_space) thenhave 1: "{x \ S. real n * e \ \det (matrix (f' x))\} \ lmeasurable" using S by (simp add: fmeasurableI2) have"{x \ S. \det (matrix (f' x))\ < (1 + real n) * e} \ sets lebesgue" using * by (auto simp: borel_measurable_iff_halfspace_less space_restrict_space) thenhave 2: "{x \ S. \det (matrix (f' x))\ < (1 + real n) * e} \ lmeasurable" using S by (simp add: fmeasurableI2) show ?thesis using fmeasurable.Int [OF 1 2] by (simp add: T_def Int_def cong: conj_cong) qed have aint_T: "\k. (\x. \det (matrix (f' x))\) absolutely_integrable_on T k" using set_integrable_subset [OF aint_S] meas_t T_def by blast have Seq: "S = (\n. T n)" apply (auto simp: T_def) apply (rule_tac x = "nat \\det (matrix (f' x))\ / e\" in exI) by (smt (verit, del_insts) divide_nonneg_nonneg floor_eq_iff of_nat_nat pos_divide_less_eq that zero_le_floor) have meas_ft: "f ` T n \ lmeasurable" for n proof (rule measurable_bounded_differentiable_image) show"T n \ lmeasurable" by (simp add: meas_t) next fix x :: "(real,'n) vec" assume"x \ T n" show"(f has_derivative f' x) (at x within T n)" by (metis (no_types, lifting) \<open>x \<in> T n\<close> deriv has_derivative_subset mem_Collect_eq subsetI T_def) show"\det (matrix (f' x))\ \ (Suc n) * e" using\<open>x \<in> T n\<close> T_def by auto next show"(\x. \det (matrix (f' x))\) integrable_on T n" using aint_T absolutely_integrable_on_def by blast qed have disT: "disjoint (range T)" unfolding disjoint_def proof clarsimp show"T m \ T n = {}" if "T m \ T n" for m n using that proof (induction m n rule: linorder_less_wlog) case (less m n) with\<open>e > 0\<close> show ?case unfolding T_def proof (clarsimp simp add: Collect_conj_eq [symmetric]) fix x assume"e > 0""m < n""n * e \ \det (matrix (f' x))\" "\det (matrix (f' x))\ < (1 + real m) * e" thenhave"n < 1 + real m" by (metis (no_types, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_left_pos) thenshow"False" using less.hyps by linarith qed qed auto qed have injT: "inj_on T ({n. T n \ {}})" unfolding inj_on_def proof clarsimp show"m = n"if"T m = T n""T n \ {}" for m n using that proof (induction m n rule: linorder_less_wlog) case (less m n) have False if"T n \ T m" "x \ T n" for x using\<open>e > 0\<close> \<open>m < n\<close> that apply (auto simp: T_def mult.commute intro: less_le_trans dest!: subsetD) by (smt (verit, best) mult_less_cancel_left_disj nat_less_real_le) thenshow ?case using less.prems by blast qed auto qed have sum_eq_Tim: "(\k\n. f (T k)) = sum f (T ` {..n})" if "f {} = 0" for f :: "_ \ real" and n proof (subst sum.reindex_nontrivial) fix i j assume"i \ {..n}" "j \ {..n}" "i \ j" "T i = T j" with that injT [unfolded inj_on_def] show"f (T i) = 0" by simp metis qed (use atMost_atLeast0 in auto) let ?B = "m + e * ?\ S" have"(\k\n. ?\ (f ` T k)) \ ?B" for n proof - have"(\k\n. ?\ (f ` T k)) \ (\k\n. ((k+1) * e) * ?\(T k))" proof (rule sum_mono [OF measure_bounded_differentiable_image]) show"(f has_derivative f' x) (at x within T k)"if"x \ T k" for k x using that unfolding T_def by (blast intro: deriv has_derivative_subset) show"(\x. \det (matrix (f' x))\) integrable_on T k" for k using absolutely_integrable_on_def aint_T by blast show"\det (matrix (f' x))\ \ real (k + 1) * e" if "x \ T k" for k x using T_def that by auto qed (use meas_t in auto) alsohave"\ \ (\k\n. (k * e) * ?\(T k)) + (\k\n. e * ?\(T k))" by (simp add: algebra_simps sum.distrib) alsohave"\ \ ?B" proof (rule add_mono) have"(\k\n. real k * e * ?\ (T k)) = (\k\n. integral (T k) (\x. k * e))" by (simp add: lmeasure_integral [OF meas_t]
flip: integral_mult_right integral_mult_left) alsohave"\ \ (\k\n. integral (T k) (\x. (abs (det (matrix (f' x))))))" proof (rule sum_mono) fix k assume"k \ {..n}" show"integral (T k) (\x. k * e) \ integral (T k) (\x. \det (matrix (f' x))\)" proof (rule integral_le [OF integrable_on_const [OF meas_t]]) show"(\x. \det (matrix (f' x))\) integrable_on T k" using absolutely_integrable_on_def aint_T by blast next fix x assume"x \ T k" show"k * e \ \det (matrix (f' x))\" using\<open>x \<in> T k\<close> T_def by blast qed qed alsohave"\ = sum (\T. integral T (\x. \det (matrix (f' x))\)) (T ` {..n})" by (auto intro: sum_eq_Tim) alsohave"\ = integral (\k\n. T k) (\x. \det (matrix (f' x))\)" proof (rule integral_unique [OF has_integral_Union, symmetric]) fix S assume"S \ T ` {..n}" thenshow"((\x. \det (matrix (f' x))\) has_integral integral S (\x. \det (matrix (f' x))\)) S" using absolutely_integrable_on_def aint_T by blast next show"pairwise (\S S'. negligible (S \ S')) (T ` {..n})" using disT unfolding disjnt_iff by (auto simp: pairwise_def intro!: empty_imp_negligible) qed auto alsohave"\ \ m" unfolding m_def proof (rule integral_subset_le) have"(\x. \det (matrix (f' x))\) absolutely_integrable_on (\k\n. T k)" proof (rule set_integrable_subset [OF aint_S]) show"\ (T ` {..n}) \ sets lebesgue" by (intro measurable meas_t fmeasurableD) qed (force simp: Seq) thenshow"(\x. \det (matrix (f' x))\) integrable_on (\k\n. T k)" using absolutely_integrable_on_def by blast qed (use Seq int in auto) finallyshow"(\k\n. real k * e * ?\ (T k)) \ m" . next have"(\k\n. ?\ (T k)) = sum ?\ (T ` {..n})" by (auto intro: sum_eq_Tim) alsohave"\ = ?\ (\k\n. T k)" using S disT by (auto simp: pairwise_def meas_t intro: measure_Union' [symmetric]) alsohave"\ \ ?\ S" using S by (auto simp: Seq intro: meas_t fmeasurableD measure_mono_fmeasurable) finallyhave"(\k\n. ?\ (T k)) \ ?\ S" . thenshow"(\k\n. e * ?\ (T k)) \ e * ?\ S" by (metis less_eq_real_def ordered_comm_semiring_class.comm_mult_left_mono sum_distrib_left that) qed finallyshow"(\k\n. ?\ (f ` T k)) \ ?B" . qed moreoverhave"measure lebesgue (\k\n. f ` T k) \ (\k\n. ?\ (f ` T k))" for n by (simp add: fmeasurableD meas_ft measure_UNION_le) ultimatelyhave B_ge_m: "?\ (\k\n. (f ` T k)) \ ?B" for n by (meson order_trans) have"(\n. f ` T n) \ lmeasurable" by (rule fmeasurable_countable_Union [OF meas_ft B_ge_m]) moreoverhave"?\ (\n. f ` T n) \ m + e * ?\ S" by (rule measure_countable_Union_le [OF meas_ft B_ge_m]) ultimatelyshow"f ` S \ lmeasurable" "?\ (f ` S) \ m + e * ?\ S" by (auto simp: Seq image_Union) qed show ?thesis proof show"f ` S \ lmeasurable" using * linordered_field_no_ub by blast let ?x = "m - ?\ (f ` S)" have False if"?\ (f ` S) > integral S (\x. \det (matrix (f' x))\)" proof - have ml: "m < ?\ (f ` S)" using m_def that by blast thenhave"?\ S \ 0" using"*"(2) bgauge_existence_lemma by fastforce with ml have 0: "0 < - (m - ?\ (f ` S))/2 / ?\ S" using that zero_less_measure_iff by force thenshow ?thesis using * [OF 0] that by (auto simp: field_split_simps m_def split: if_split_asm) qed thenshow"?\ (f ` S) \ integral S (\x. \det (matrix (f' x))\)" by fastforce qed qed
theorem fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" assumes S: "S \ sets lebesgue" and deriv: "\x. x \ S \ (f has_derivative f' x) (at x within S)" and int: "(\x. \det (matrix (f' x))\) integrable_on S" shows measurable_differentiable_image: "f ` S \ lmeasurable" and measure_differentiable_image: "measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" (is "?M") proof - let ?I = "\n::nat. cbox (vec (-n)) (vec n) \ S" let ?\<mu> = "measure lebesgue" have"x \ cbox (vec (- real (nat \norm x\))) (vec (real (nat \norm x\)))" for x :: "real^'n::_" apply (simp add: mem_box_cart) by (smt (verit, best) component_le_norm_cart le_of_int_ceiling) thenhave Seq: "S = (\n. ?I n)" by blast have fIn: "f ` ?I n \ lmeasurable" and mfIn: "?\ (f ` ?I n) \ integral S (\x. \det (matrix (f' x))\)" (is ?MN) for n proof - haveIn: "?I n \ lmeasurable" by (simp add: S bounded_Int bounded_set_imp_lmeasurable sets.Int) moreoverhave"\x. x \ ?I n \ (f has_derivative f' x) (at x within ?I n)" by (meson Int_iff deriv has_derivative_subset subsetI) moreoverhave int_In: "(\x. \det (matrix (f' x))\) integrable_on ?I n" by (metis (mono_tags) Int_commute int integrable_altD(1) integrable_restrict_Int) ultimatelyhave"f ` ?I n \ lmeasurable" "?\ (f ` ?I n) \ integral (?I n) (\x. \det (matrix (f' x))\)" using m_diff_image_weak by metis+ moreoverhave"integral (?I n) (\x. \det (matrix (f' x))\) \ integral S (\x. \det (matrix (f' x))\)" by (simp add: int_In int integral_subset_le) ultimatelyshow"f ` ?I n \ lmeasurable" ?MN by auto qed have"?I k \ ?I n" if "k \ n" for k n by (rule Int_mono) (use that in\<open>auto simp: subset_interval_imp_cart\<close>) thenhave"(\k\n. f ` ?I k) = f ` ?I n" for n by (fastforce simp add:) with mfIn have"?\ (\k\n. f ` ?I k) \ integral S (\x. \det (matrix (f' x))\)" for n by simp thenhave"(\n. f ` ?I n) \ lmeasurable" "?\ (\n. f ` ?I n) \ integral S (\x. \det (matrix (f' x))\)" by (rule fmeasurable_countable_Union [OF fIn] measure_countable_Union_le [OF fIn])+ thenshow"f ` S \ lmeasurable" ?M by (metis Seq image_UN)+ qed
lemma borel_measurable_simple_function_limit_increasing: fixes f :: "'a::euclidean_space \ real" shows"(f \ borel_measurable lebesgue \ (\x. 0 \ f x)) \
(\<exists>g. (\<forall>n x. 0 \<le> g n x \<and> g n x \<le> f x) \<and> (\<forall>n x. g n x \<le> (g(Suc n) x)) \<and>
(\<forall>n. g n \<in> borel_measurable lebesgue) \<and> (\<forall>n. finite(range (g n))) \<and>
(\<forall>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x))"
(is"?lhs = ?rhs") proof assume f: ?lhs have leb_f: "{x. a \ f x \ f x < b} \ sets lebesgue" for a b proof - have"{x. a \ f x \ f x < b} = {x. f x < b} - {x. f x < a}" by auto alsohave"\ \ sets lebesgue" using borel_measurable_vimage_halfspace_component_lt [of f UNIV] f by auto finallyshow ?thesis . qed have"g n x \ f x" if inc_g: "\n x. 0 \ g n x \ g n x \ g (Suc n) x" and meas_g: "\n. g n \ borel_measurable lebesgue" and fin: "\n. finite(range (g n))" and lim: "\x. (\n. g n x) \ f x" for g n x proof - have"\r>0. \N. \n\N. dist (g n x) (f x) \ r" if "g n x > f x" proof - have g: "g n x \ g (N + n) x" for N by (rule transitive_stepwise_le) (use inc_g in auto) have"\m\N. g n x - f x \ dist (g m x) (f x)" for N proof show"N \ N + n \ g n x - f x \ dist (g (N + n) x) (f x)" using g [of N] by (auto simp: dist_norm) qed with that show ?thesis using diff_gt_0_iff_gt by blast qed with lim show ?thesis unfolding lim_sequentially by (meson less_le_not_le not_le_imp_less) qed moreover let ?\<Omega> = "\<lambda>n k. indicator {y. k/2^n \<le> f y \<and> f y < (k+1)/2^n}" let ?g = "\n x. (\k::real | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x)" have"\g. (\n x. 0 \ g n x \ g n x \ (g(Suc n) x)) \
(\<forall>n. g n \<in> borel_measurable lebesgue) \<and> (\<forall>n. finite(range (g n))) \<and>(\<forall>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x)" proof (intro exI allI conjI) show"0 \ ?g n x" for n x proof (clarify intro!: ordered_comm_monoid_add_class.sum_nonneg) fix k::real assume"k \ \" and k: "\k\ \ 2 ^ (2*n)" show"0 \ k/2^n * ?\ n k x" using f \<open>k \<in> \<int>\<close> apply (clarsimp simp: indicator_def field_split_simps Ints_def) by (smt (verit) int_less_real_le mult_nonneg_nonneg of_int_0 zero_le_power) qed show"?g n x \ ?g (Suc n) x" for n x proof - have"?g n x =
(\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n).
k/2^n * (indicator {y. k/2^n \<le> f y \<and> f y < (k+1/2)/2^n} x +
indicator {y. (k+1/2)/2^n \<le> f y \<and> f y < (k+1)/2^n} x))" by (rule sum.cong [OF refl]) (simp add: indicator_def field_split_simps) alsohave"\ = (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. k/2^n \ f y \f y < (k+1/2)/2^n} x) +
(\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n \<le> f y \<and> f y < (k+1)/2^n} x)" by (simp add: comm_monoid_add_class.sum.distrib algebra_simps) alsohave"\ = (\k | k \ \ \ \k\ \ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k)/2 ^ Suc n \ f y \ f y < (2 * k+1)/2 ^ Suc n} x) +
(\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \<le> f y \<and> f y < ((2 * k+1) + 1)/2 ^ Suc n} x)" by (force simp: field_simps indicator_def intro: sum.cong) alsohave"\ \ (\k | k \ \ \ \k\ \ 2 ^ (2 * Suc n). k/2 ^ Suc n * (indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x))"
(is"?a + _ \ ?b") proof - have *: "\sum f I \ sum h I; a + sum h I \ b\ \ a + sum f I \ b" for I a b f and h :: "real\real" by linarith let ?h = "\k. (2*k+1)/2 ^ Suc n *
(indicator {y. (2 * k+1)/2 ^ Suc n \<le> f y \<and> f y < ((2*k+1) + 1)/2 ^ Suc n} x)" show ?thesis proof (rule *) show"(\k | k \ \ \ \k\ \ 2 ^ (2*n).
2 * k/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \<le> f y \<and> f y < (2 * k+1 + 1)/2 ^ Suc n} x) \<le> sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}" by (rule sum_mono) (simp add: indicator_def field_split_simps) next have\<alpha>: "?a = (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)" by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex) have\<beta>: "sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
= (\<Sum>k \<in> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)" by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex) have 0: "(*) 2 ` {k \ \. P k} \ (\x. 2 * x + 1) ` {k \ \. P k} = {}" for P :: "real \ bool" proof - have"2 * i \ 2 * j + 1" for i j :: int by arith thus ?thesis unfolding Ints_def by auto (use of_int_eq_iff in fastforce) qed have"?a + sum ?h {k \ \. \k\ \ 2 ^ (2*n)}
= (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)" unfolding\<alpha> \<beta> using finite_abs_int_segment [of "2 ^ (2*n)"] by (subst sum_Un) (auto simp: 0) alsohave"\ \ ?b" proof (rule sum_mono2) show"finite {k::real. k \ \ \ \k\ \ 2 ^ (2 * Suc n)}" by (rule finite_abs_int_segment) show"(*) 2 ` {k::real. k \ \ \ \k\ \ 2^(2*n)} \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2^(2*n)} \ {k \ \. \k\ \ 2 ^ (2 * Suc n)}" apply (clarsimp simp: image_subset_iff) using one_le_power [of "2::real""2*n"] by linarith have *: "\x \ (S \ T) - U; \x. x \ S \ x \ U; \x. x \ T \ x \ U\ \ P x" for S T U P by blast have"0 \ b" if "b \ \" "f x * (2 * 2^n) < b + 1" for b by (smt (verit, ccfv_SIG) Ints_cases f int_le_real_less mult_nonneg_nonneg of_int_add one_le_power that) thenshow"0 \ b/2 ^ Suc n * indicator {y. b/2 ^ Suc n \ f y \ f y < (b + 1)/2 ^ Suc n} x" if"b \ {k \ \. \k\ \ 2 ^ (2 * Suc n)} -
((*) 2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})" for b using that by (simp add: indicator_def divide_simps) qed finallyshow"?a + sum ?h {k \ \. \k\ \ 2 ^ (2*n)} \ ?b" . qed qed finallyshow ?thesis . qed show"?g n \ borel_measurable lebesgue" for n apply (intro borel_measurable_indicator borel_measurable_times borel_measurable_sum) using leb_f sets_restrict_UNIV by auto show"finite (range (?g n))"for n proof - have"(\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) \<in> (\<lambda>k. k/2^n) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}" for x proof (cases "\k. k \ \ \ \k\ \ 2 ^ (2*n) \ k/2^n \ f x \ f x < (k+1)/2^n") case True thenshow ?thesis by (blast intro: indicator_sum_eq) next case False thenhave"(\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) = 0" by auto thenshow ?thesis by force qed thenhave"range (?g n) \ ((\k. (k/2^n)) ` {k. k \ \ \ \k\ \ 2 ^ (2*n)})" by auto moreoverhave"finite ((\k::real. (k/2^n)) ` {k \ \. \k\ \ 2 ^ (2*n)})" by (intro finite_imageI finite_abs_int_segment) ultimatelyshow ?thesis by (rule finite_subset) qed show"(\n. ?g n x) \ f x" for x proof (clarsimp simp add: lim_sequentially) fix e::real assume"e > 0" obtain N1 where N1: "2 ^ N1 > abs(f x)" using real_arch_pow by fastforce obtain N2 where N2: "(1/2) ^ N2 < e" using real_arch_pow_inv \<open>e > 0\<close> by fastforce have"dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) (f x) < e" if "N1 + N2 \ n" for n proof - let ?m = "real_of_int \2^n * f x\" have"\?m\ \ 2^n * 2^N1" using N1 apply (simp add: f) by (meson floor_mono le_floor_iff less_le_not_le mult_le_cancel_left_pos zero_less_numeral zero_less_power) alsohave"\ \ 2 ^ (2*n)" by (metis that add_leD1 add_le_cancel_left mult.commute mult_2_right one_less_numeral_iff
power_add power_increasing_iff semiring_norm(76)) finallyhave m_le: "\?m\ \ 2 ^ (2*n)" . have"?m/2^n \ f x" "f x < (?m + 1)/2^n" by (auto simp: mult.commute pos_divide_le_eq mult_imp_less_div_pos) thenhave eq: "dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) (f x)
= dist (?m/2^n) (f x)" by (subst indicator_sum_eq [of ?m]) (auto simp: m_le) have"\2^n\ * \?m/2^n - f x\ = \2^n * (?m/2^n - f x)\" by (simp add: abs_mult) alsohave"\ < 2 ^ N2 * e" using N2 by (simp add: divide_simps mult.commute) linarith alsohave"\ \ \2^n\ * e" using that \<open>e > 0\<close> by auto finallyshow ?thesis using eq by (simp add: dist_real_def) qed thenshow"\no. \n\no. dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k * ?\ n k x/2^n) (f x) < e" by force qed qed ultimatelyshow ?rhs by metis next assume RHS: ?rhs with borel_measurable_simple_function_limit [of f UNIV, unfolded lebesgue_on_UNIV_eq] show ?lhs by (blast intro: order_trans) qed
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.32Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
