# HG changeset patch # User paulson # Date 1524000948 -3600 # Node ID 73a5a33486ee2400ee0701d632dee57af52864c3 # Parent ae76012879c600481edd49774089d5bcd9994643 Change of variables proof diff -r ae76012879c6 -r 73a5a33486ee src/HOL/Analysis/Change_Of_Vars.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Tue Apr 17 22:35:48 2018 +0100 @@ -0,0 +1,3974 @@ +theory Change_Of_Vars + imports "HOL-Analysis.Vitali_Covering_Theorem" "HOL-Analysis.Determinants" + +begin + +subsection\Induction on matrix row operations\ + +lemma induct_matrix_row_operations: + fixes P :: "(real^'n, 'n::finite) vec \ bool" + assumes zero_row: "\A i. row i A = 0 \ P A" + and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" + and swap_cols: "\A m n. \P A; m \ n\ \ P(\ i j. A $ i $ Fun.swap m n id j)" + and row_op: "\A m n c. \P A; m \ n\ + \ P(\ i. if i = m then row m A + c *\<^sub>R row n A else row i A)" + shows "P A" +proof - + have "P A" if "(\i j. \j \ -K; i \ j\ \ A$i$j = 0)" for A K + proof - + have "finite K" + by simp + then show ?thesis using that + proof (induction arbitrary: A rule: finite_induct) + case empty + with diagonal show ?case + by simp + next + case (insert k K) + note insertK = insert + have "P A" if kk: "A$k$k \ 0" + and 0: "\i j. \j \ - insert k K; i \ j\ \ A$i$j = 0" + "\i. \i \ -L; i \ k\ \ A$i$k = 0" for A L + proof - + have "finite L" + by simp + then show ?thesis using 0 kk + proof (induction arbitrary: A rule: finite_induct) + case (empty B) + show ?case + proof (rule insertK) + fix i j + assume "i \ - K" "j \ i" + show "B $ j $ i = 0" + using \j \ i\ \i \ - K\ empty + by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff) + qed + next + case (insert l L B) + show ?case + proof (cases "k = l") + case True + with insert show ?thesis + by auto + next + case False + let ?C = "\ i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B" + have 1: "\j \ - insert k K; i \ j\ \ ?C $ i $ j = 0" for j i + by (auto simp: insert.prems(1) row_def) + have 2: "?C $ i $ k = 0" + if "i \ - L" "i \ k" for i + proof (cases "i=l") + case True + with that insert.prems show ?thesis + by (simp add: row_def) + next + case False + with that show ?thesis + by (simp add: insert.prems(2) row_def) + qed + have 3: "?C $ k $ k \ 0" + by (auto simp: insert.prems row_def \k \ l\) + have PC: "P ?C" + using insert.IH [OF 1 2 3] by auto + have eqB: "(\ i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B" + using \k \ l\ by (simp add: vec_eq_iff row_def) + show ?thesis + using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \k \ l\ + by (simp add: cong: if_cong) + qed + qed + qed + then have nonzero_hyp: "P A" + if kk: "A$k$k \ 0" and zeroes: "\i j. j \ - insert k K \ i\j \ A$i$j = 0" for A + by (auto simp: intro!: kk zeroes) + show ?case + proof (cases "row k A = 0") + case True + with zero_row show ?thesis by auto + next + case False + then obtain l where l: "A$k$l \ 0" + by (auto simp: row_def zero_vec_def vec_eq_iff) + show ?thesis + proof (cases "k = l") + case True + with l nonzero_hyp insert.prems show ?thesis + by blast + next + case False + have *: "A $ i $ Fun.swap k l id j = 0" if "j \ k" "j \ K" "i \ j" for i j + using False l insert.prems that + by (auto simp: swap_def insert split: if_split_asm) + have "P (\ i j. (\ i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)" + by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *) + moreover + have "(\ i j. (\ i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A" + by (metis (no_types, lifting) id_apply o_apply swap_id_idempotent vec_lambda_unique vec_lambda_unique) + ultimately show ?thesis + by simp + qed + qed + qed + qed + then show ?thesis + by blast +qed + +lemma induct_matrix_elementary: + fixes P :: "(real^'n, 'n::finite) vec \ bool" + assumes mult: "\A B. \P A; P B\ \ P(A ** B)" + and zero_row: "\A i. row i A = 0 \ P A" + and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" + and swap1: "\m n. m \ n \ P(\ i j. mat 1 $ i $ Fun.swap m n id j)" + and idplus: "\m n c. m \ n \ P(\ i j. if i = m \ j = n then c else of_bool (i = j))" + shows "P A" +proof - + have swap: "P (\ i j. A $ i $ Fun.swap m n id j)" (is "P ?C") + if "P A" "m \ n" for A m n + proof - + have "A ** (\ i j. mat 1 $ i $ Fun.swap m n id j) = ?C" + by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove) + then show ?thesis + using mult swap1 that by metis + qed + have row: "P (\ i. if i = m then row m A + c *\<^sub>R row n A else row i A)" (is "P ?C") + if "P A" "m \ n" for A m n c + proof - + let ?B = "\ i j. if i = m \ j = n then c else of_bool (i = j)" + have "?B ** A = ?C" + using \m \ n\ unfolding matrix_matrix_mult_def row_def of_bool_def + by (auto simp: vec_eq_iff if_distrib [of "\x. x * y" for y] sum.remove cong: if_cong) + then show ?thesis + by (rule subst) (auto simp: that mult idplus) + qed + show ?thesis + by (rule induct_matrix_row_operations [OF zero_row diagonal swap row]) +qed + +lemma induct_matrix_elementary_alt: + fixes P :: "(real^'n, 'n::finite) vec \ bool" + assumes mult: "\A B. \P A; P B\ \ P(A ** B)" + and zero_row: "\A i. row i A = 0 \ P A" + and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" + and swap1: "\m n. m \ n \ P(\ i j. mat 1 $ i $ Fun.swap m n id j)" + and idplus: "\m n. m \ n \ P(\ i j. of_bool (i = m \ j = n \ i = j))" + shows "P A" +proof - + have *: "P (\ i j. if i = m \ j = n then c else of_bool (i = j))" + if "m \ n" for m n c + proof (cases "c = 0") + case True + with diagonal show ?thesis by auto + next + case False + then have eq: "(\ i j. if i = m \ j = n then c else of_bool (i = j)) = + (\ i j. if i = j then (if j = n then inverse c else 1) else 0) ** + (\ i j. of_bool (i = m \ j = n \ i = j)) ** + (\ i j. if i = j then if j = n then c else 1 else 0)" + using \m \ n\ + apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\x. y * x" for y] cong: if_cong) + apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong) + done + show ?thesis + apply (subst eq) + apply (intro mult idplus that) + apply (auto intro: diagonal) + done + qed + show ?thesis + by (rule induct_matrix_elementary) (auto intro: assms *) +qed + +lemma induct_linear_elementary: + fixes f :: "real^'n \ real^'n" + assumes "linear f" + and comp: "\f g. \linear f; linear g; P f; P g\ \ P(f \ g)" + and zeroes: "\f i. \linear f; \x. (f x) $ i = 0\ \ P f" + and const: "\c. P(\x. \ i. c i * x$i)" + and swap: "\m n::'n. m \ n \ P(\x. \ i. x $ Fun.swap m n id i)" + and idplus: "\m n::'n. m \ n \ P(\x. \ i. if i = m then x$m + x$n else x$i)" + shows "P f" +proof - + have "P (( *v) A)" for A + proof (rule induct_matrix_elementary_alt) + fix A B + assume "P (( *v) A)" and "P (( *v) B)" + then show "P (( *v) (A ** B))" + by (metis (no_types, lifting) comp linear_compose matrix_compose matrix_eq matrix_vector_mul matrix_vector_mul_linear) + next + fix A :: "((real, 'n) vec, 'n) vec" and i + assume "row i A = 0" + then show "P (( *v) A)" + by (metis inner_zero_left matrix_vector_mul_component matrix_vector_mul_linear row_def vec_eq_iff vec_lambda_beta zeroes) + next + fix A :: "((real, 'n) vec, 'n) vec" + assume 0: "\i j. i \ j \ A $ i $ j = 0" + have "A $ i $ i * x $ i = (\j\UNIV. A $ i $ j * x $ j)" for x :: "(real, 'n) vec" and i :: "'n" + by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i]) + then have "(\x. \ i. A $ i $ i * x $ i) = (( *v) A)" + by (auto simp: 0 matrix_vector_mult_def) + then show "P (( *v) A)" + using const [of "\i. A $ i $ i"] by simp + next + fix m n :: "'n" + assume "m \ n" + have eq: "(\j\UNIV. if i = Fun.swap m n id j then x $ j else 0) = + (\j\UNIV. if j = Fun.swap m n id i then x $ j else 0)" + for i and x :: "(real, 'n) vec" + unfolding swap_def by (rule sum.cong) auto + have "(\x::real^'n. \ i. x $ Fun.swap m n id i) = (( *v) (\ i j. if i = Fun.swap m n id j then 1 else 0))" + by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\x. x * y" for y] cong: if_cong) + with swap [OF \m \ n\] show "P (( *v) (\ i j. mat 1 $ i $ Fun.swap m n id j))" + by (simp add: mat_def matrix_vector_mult_def) + next + fix m n :: "'n" + assume "m \ n" + then have "x $ m + x $ n = (\j\UNIV. of_bool (j = n \ m = j) * x $ j)" for x :: "(real, 'n) vec" + by (auto simp: of_bool_def if_distrib [of "\x. x * y" for y] sum.remove cong: if_cong) + then have "(\x::real^'n. \ i. if i = m then x $ m + x $ n else x $ i) = + (( *v) (\ i j. of_bool (i = m \ j = n \ i = j)))" + unfolding matrix_vector_mult_def of_bool_def + by (auto simp: vec_eq_iff if_distrib [of "\x. x * y" for y] cong: if_cong) + then show "P (( *v) (\ i j. of_bool (i = m \ j = n \ i = j)))" + using idplus [OF \m \ n\] by simp + qed + then show ?thesis + by (metis \linear f\ matrix_vector_mul) +qed + + +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 (force simp: plus_vec_def scaleR_vec_def algebra_simps intro: linearI) + 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 \ {x. ?mn \ x \ a$m}) + + measure lebesgue (cbox a ?c \ {x. ?mn \ x \ 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 \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) + moreover have "?f ` cbox a b \ (cbox a ?c \ {x. ?mn \ x \ a $ m}) \ {x. ?mn \ x = a$m}" + using \m \ n\ antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') + ultimately show "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 \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) + moreover have "(?f ` cbox a b) \ (cbox a ?c \ {x. ?mn \ x \ b$m}) \ {x. ?mn \ x = b$m}" + using \m \ n\ antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') + ultimately show "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 \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) + moreover have "(cbox a ?c \ {x. ?mn \ x \ a $ m} \ (cbox a ?c \ {x. ?mn \ x \ b$m})) \ {x. ?mn \ x = b$m}" + using \m \ n\ ab_ne + apply (auto simp: algebra_simps mem_box_cart inner_axis') + apply (drule_tac x=m in spec)+ + apply simp + done + ultimately show "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 (auto simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF \m \ n\]) + apply (auto simp: mem_box_cart split: if_split_asm) + done + 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 (\ 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\ + \ x \ (+) (\ i. if i = m then a $ m - b $ m else 0) ` {x. x $ n + b $ m \ x $ m}" + using \m \ n\ + 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) + then have imeq: "(+) ?d ` {x. b $ m \ ?mn \ x} = {x. a $ m \ ?mn \ x}" + using \m \ n\ by (auto simp: mem_box_cart inner_axis' algebra_simps) + have "\x. \0 \ a $ n; x $ n + a $ m \ x $ m; + \i. i \ m \ a $ i \ x $ i \ x $ i \ b $ i\ + \ a $ m \ x $ m" + using \m \ n\ by force + then have "(+) ?d ` (cbox a ?c \ {x. b $ m \ ?mn \ x}) + = cbox a (\ i. if i = m then a $ m + b $ n else b $ i) \ {x. a $ m \ ?mn \ 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) + then show "cbox a ?c \ {x. ?mn \ x \ a $ m} \ + (+) ?d ` (cbox a ?c \ {x. b $ m \ ?mn \ x}) = + cbox a (\ i. if i = m then a $ m + b $ n else b $ i)" (is "?lhs = ?rhs") + using an \m \ n\ + 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 \m \ n\ axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane) + moreover have "(cbox a ?c \ {x. ?mn \ x \ a $ m} \ + (+) ?d ` (cbox a ?c \ {x. b $ m \ ?mn \ x})) \ {x. ?mn \ x = a$m}" + using \m \ n\ antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis') + ultimately show "negligible (cbox a ?c \ {x. ?mn \ x \ a $ m} \ + (+) ?d ` (cbox a ?c \ {x. b $ m \ ?mn \ x}))" + by (rule negligible_subset) + qed + have ac_ne: "cbox a ?c \ {}" + using ab_ne an + by (clarsimp simp: interval_eq_empty_cart) (meson add_less_same_cancel1 le_less_linear less_le_trans) + have ax_ne: "cbox a (\ i. if i = m then a $ m + b $ n else b $ i) \ {}" + using ab_ne an + by (clarsimp simp: interval_eq_empty_cart) (meson add_less_same_cancel1 le_less_linear less_le_trans) + 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 + then obtain B where "B>0" + and B: "\a b. ball 0 B \ cbox a b \ + \z. (indicat_real S has_integral z) (cbox a b) \ + \z - measure lebesgue S\ < e / \prod m UNIV\" + by (simp add: has_integral_alt [where i=UNIV]) (metis (full_types) divide_pos_pos m0 m0 \e > 0\) + show "\B>0. \a b. ball 0 B \ cbox a b \ + (\z. (indicat_real (?f ` S) has_integral z) (cbox a b) \ + \z - \prod m UNIV\ * measure lebesgue S\ < e)" + proof (intro exI conjI allI) + let ?C = "Max (range (\k. \m k\)) * B" + show "?C > 0" + using True \B > 0\ by (simp add: Max_gr_iff) + show "ball 0 ?C \ cbox u v \ + (\z. (indicat_real (?f ` S) has_integral z) (cbox u v) \ + \z - \prod m UNIV\ * measure lebesgue S\ < e)" for u v + proof + assume uv: "ball 0 ?C \ cbox u v" + with \?C > 0\ have cbox_ne: "cbox u v \ {}" + using centre_in_ball by blast + let ?\ = "\k. u$k / m k" + let ?\ = "\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) vec" + 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) + also have "\ < ?C" + using x by simp (metis \B > 0\ \?C > 0\ mult.commute real_mult_less_iff1 zero_less_mult_pos) + finally have "norm (\ k. m k * x $ k) < ?C" . + then show "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 + then have 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) \ + \z - \prod m UNIV\ * measure lebesgue S\ < 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\) + ((\x. \ k. x $ k * m k) ` cbox (\ k. min (?\ k) (?\ k)) (\ k. max (?\ k) (?\ k)))" + using True has_integral_stretch_cart [OF zint, of "inverse \ m"] + by (simp add: field_simps prod_dividef) + moreover have "((\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) + ultimately show "((\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\ + = \prod m UNIV\ * \z - measure lebesgue S\" + by (metis (no_types, hide_lams) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib') + also have "\ < e" + using zless True by (simp add: field_simps) + finally show "\z *\<^sub>R \prod m UNIV\ - \prod m UNIV\ * measure lebesgue S\ < e" . + qed + qed + qed + qed + then show ?thesis + by (auto simp: has_integral_integrable integral_unique lmeasure_integral_UNIV measurable_integrable) + next + case False + then obtain 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 \m k = 0\ in auto) + then have "(?f ` S) \ lmeasurable" + by (simp add: negligible_iff_measure) + with nfS show ?thesis + by (simp add: prm negligible_iff_measure0) + qed + then show "(?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 \linear f\]; 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" + then have 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 \linear g\ \linear f\] + by (simp add: o_def image_comp abs_mult det_mul) + next + fix f :: "(real, 'n) vec \ (real, 'n) vec" and i and S :: "(real, 'n) vec set" + assume "linear f" and 0: "\x. f x $ i = 0" and "S \ lmeasurable" + then have "\ inj f" + by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component) + have detf: "det (matrix f) = 0" + by (metis "0" \linear f\ invertible_det_nz invertible_right_inverse matrix_right_invertible_surjective matrix_vector_mul surjE vec_component) + show "f ` S \ lmeasurable \ ?Q f S" + proof + show "f ` S \ lmeasurable" + using lmeasurable_iff_indicator_has_integral \linear f\ \\ inj f\ negligible_UNIV negligible_linear_singular_image by blast + have "measure lebesgue (f ` S) = 0" + by (meson \\ inj f\ \linear f\ negligible_imp_measure0 negligible_linear_singular_image) + also have "\ = \det (matrix f)\ * measure lebesgue S" + by (simp add: detf) + finally show "?Q f S" . + qed + next + fix c and S :: "(real, 'n) vec 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: \S \ lmeasurable\ measurable_stretch) + show "?Q (\a. \ i. c i * a $ i) S" + by (simp add: measure_stretch [OF \S \ lmeasurable\, 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 $ Fun.swap m n id i" + have lin: "linear ?h" + by (simp add: plus_vec_def scaleR_vec_def linearI) + have meq: "measure lebesgue ((\v::(real, 'n) vec. \ i. v $ Fun.swap m n id i) ` cbox a b) + = measure lebesgue (cbox a b)" for a b + proof (cases "cbox a b = {}") + case True then show ?thesis + by simp + next + case False + then have 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 swap_id_eq)+ + 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 Fun.swap m n id i = j then 1 else 0) = (\ i j. if j = Fun.swap m n id i then 1 else (0::real))" + by (auto intro!: Cart_lambda_cong) + then have "matrix ?h = transpose(\ i j. mat 1 $ i $ Fun.swap m n id j)" + by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def) + then have 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" + proof + show "?h ` S \ lmeasurable" "?Q ?h S" + using measure_linear_sufficient [OF lin \S \ lmeasurable\] meq 1 by force+ + 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. if i = m then v $ m + v $ n else v $ i" + have lin: "linear ?h" + by (auto simp: algebra_simps plus_vec_def scaleR_vec_def vec_eq_iff intro: linearI) + consider "m < n" | " n < m" + using \m \ n\ less_linear by blast + then have 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 + then have "(\ p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)" + using \j < i\ axis_def \m < n\ by auto + with \m < n\ show ?thesis + by (auto simp: matrix_def axis_def cong: if_cong) + qed + show ?thesis + using \m \ n\ 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 + then have "(\ p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)" + using \j > i\ axis_def \m > n\ by auto + with \m > n\ show ?thesis + by (auto simp: matrix_def axis_def cong: if_cong) + qed + show ?thesis + using \m \ n\ + 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 then show ?thesis by simp + next + case False + then have 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 + = (+) (\ i. if i = m \ i = n then a $ n else 0) ` ?h ` (+) ?v ` (cbox a b)" + using \m \ n\ unfolding image_comp o_def by (force simp: vec_eq_iff) + then have "measure lebesgue (?h ` (cbox a b)) + = measure lebesgue ((\v. \ i. if i = m then v $ m + v $ n else v $ i) ` + (+) ?v ` cbox a b)" + by (rule ssubst) (rule measure_translation) + also have "\ = 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) + also have "\ = measure lebesgue ((+) (\ i. if i = n then - a $ n else 0) ` cbox a b)" + apply (subst measure_shear_interval) + using \m \ n\ ne apply auto + apply (simp add: cbox_translation) + by (metis cbox_borel cbox_translation measure_completion sets_lborel) + also have "\ = measure lebesgue (cbox a b)" + by (rule measure_translation) + finally show ?thesis . + qed + show "?h ` S \ lmeasurable \ ?Q ?h S" + using measure_linear_sufficient [OF lin \S \ lmeasurable\] 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) + then show "f ` S \ lmeasurable" + by (metis S measurable_linear_image) + show "measure lebesgue (f ` S) = measure lebesgue S" + by (simp add: measure_linear_image \linear f\ S f) +qed + +lemma sets_lebesgue_inner_closed: + assumes "S \ sets lebesgue" "e > 0" + obtains T where "closed T" "T \ S" "S-T \ lmeasurable" "measure lebesgue (S - T) < e" +proof - + have "-S \ sets lebesgue" + using assms by (simp add: Compl_in_sets_lebesgue) + then obtain T where "open T" "-S \ T" + and T: "(T - -S) \ lmeasurable" "measure lebesgue (T - -S) < e" + using lmeasurable_outer_open assms by blast + show thesis + proof + show "closed (-T)" + using \open T\ by blast + show "-T \ S" + using \- S \ T\ by auto + show "S - ( -T) \ lmeasurable" "measure lebesgue (S - (- T)) < e" + using T by (auto simp: Int_commute) + qed +qed + +subsection\@{text F_sigma} and @{text G_delta} sets.\ + +(*https://en.wikipedia.org/wiki/F\_set*) +inductive fsigma :: "'a::topological_space set \ bool" where + "(\n::nat. closed (F n)) \ fsigma (UNION UNIV F)" + +inductive gdelta :: "'a::topological_space set \ bool" where + "(\n::nat. open (F n)) \ gdelta (INTER UNIV F)" + + +lemma fsigma_Union_compact: + fixes S :: "'a::{real_normed_vector,heine_borel} set" + shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = UNION UNIV F)" +proof safe + assume "fsigma S" + then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = UNION UNIV F" + by (meson fsigma.cases image_subsetI mem_Collect_eq) + then have "\D::nat \ 'a set. range D \ Collect compact \ UNION UNIV D = F i" for i + using closed_Union_compact_subsets [of "F i"] + by (metis image_subsetI mem_Collect_eq range_subsetD) + then obtain D :: "nat \ nat \ 'a set" + where D: "\i. range (D i) \ Collect compact \ UNION UNIV (D i) = F i" + by metis + let ?DD = "\n. (\(i,j). D i j) (prod_decode n)" + show "\F::nat \ 'a set. range F \ Collect compact \ S = UNION UNIV F" + proof (intro exI conjI) + show "range ?DD \ Collect compact" + using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair) + show "S = UNION UNIV ?DD" + proof + show "S \ UNION UNIV ?DD" + using D F + by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq) + show "UNION UNIV ?DD \ S" + using D F by fastforce + qed + qed +next + fix F :: "nat \ 'a set" + assume "range F \ Collect compact" and "S = UNION UNIV F" + then show "fsigma (UNION UNIV F)" + by (simp add: compact_imp_closed fsigma.intros image_subset_iff) +qed + +lemma gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" +proof (induction rule: gdelta.induct) + case (1 F) + have "- INTER UNIV F = (\i. -(F i))" + by auto + then show ?case + by (simp add: fsigma.intros closed_Compl 1) +qed + +lemma fsigma_imp_gdelta: "fsigma S \ gdelta (- S)" +proof (induction rule: fsigma.induct) + case (1 F) + have "- UNION UNIV F = (\i. -(F i))" + by auto + then show ?case + by (simp add: 1 gdelta.intros open_closed) +qed + + + +lemma gdelta_complement: "gdelta(- S) \ fsigma S" + using fsigma_imp_gdelta gdelta_imp_fsigma by force + + +text\A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\ +lemma lebesgue_set_almost_fsigma: + assumes "S \ sets lebesgue" + obtains C T where "fsigma C" "negligible T" "C \ T = S" "disjnt C T" +proof - + { fix n::nat + have "\T. closed T \ T \ S \ S - T \ lmeasurable \ measure lebesgue (S-T) < 1 / Suc n" + using sets_lebesgue_inner_closed [OF assms] + by (metis divide_pos_pos less_numeral_extra(1) of_nat_0_less_iff zero_less_Suc) + } + then obtain F where F: "\n::nat. closed (F n) \ F n \ S \ S - F n \ lmeasurable \ measure lebesgue (S - F n) < 1 / Suc n" + by metis + let ?C = "UNION UNIV F" + show thesis + proof + show "fsigma ?C" + using F by (simp add: fsigma.intros) + show "negligible (S - ?C)" + proof (clarsimp simp add: negligible_outer_le) + fix e :: "real" + assume "0 < e" + then obtain n where n: "1 / Suc n < e" + using nat_approx_posE by metis + show "\T. S - (\x. F x) \ T \ T \ lmeasurable \ measure lebesgue T \ e" + proof (intro exI conjI) + show "measure lebesgue (S - F n) \ e" + by (meson F n less_trans not_le order.asym) + qed (use F in auto) + qed + show "?C \ (S - ?C) = S" + using F by blast + show "disjnt ?C (S - ?C)" + by (auto simp: disjnt_def) + qed +qed + +lemma lebesgue_set_almost_gdelta: + assumes "S \ sets lebesgue" + obtains C T where "gdelta C" "negligible T" "S \ T = C" "disjnt S T" +proof - + have "-S \ sets lebesgue" + using assms Compl_in_sets_lebesgue by blast + then obtain C T where C: "fsigma C" "negligible T" "C \ T = -S" "disjnt C T" + using lebesgue_set_almost_fsigma by metis + show thesis + proof + show "gdelta (-C)" + by (simp add: \fsigma C\ fsigma_imp_gdelta) + show "S \ T = -C" "disjnt S T" + using C by (auto simp: disjnt_def) + qed (use C in auto) +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\ + \ measure lebesgue T < measure lebesgue S + e" +proof (cases "S = {}") + case True + with that \e > 0\ show ?thesis by force +next + case False + then have frS: "frontier S \ {}" + using \bounded S\ frontier_eq_empty not_bounded_UNIV by blast + have "S \ lmeasurable" + by (simp add: \bounded S\ 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 \e > 0\ lmeasurable_outer_open + obtain U where "open U" + and U: "frontier S \ U" "U - frontier S \ lmeasurable" "measure 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: \U \ lmeasurable\ fmeasurableD measure_Diff_null_set null) + with U have mU: "measure lebesgue U < e" + by simp + show ?thesis + proof + have "U \ UNIV" + using \U \ lmeasurable\ by auto + then have "- U \ {}" + by blast + with \open U\ \frontier S \ U\ show "setdist (frontier S) (- U) > 0" + by (auto simp: \bounded S\ 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)" + then have "measure lebesgue T - measure lebesgue S \ measure lebesgue (T - S)" + by (simp add: \S \ lmeasurable\ measure_diff_le_measure_setdiff) + also have "\ \ measure lebesgue U" + proof - + have "T - S \ U" + proof clarify + fix x + assume "x \ T" and "x \ S" + then obtain 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 \x \ S\ \y \ S\ by blast + then obtain 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 \z \ frontier S\ that] by auto + then show "x \ U" + by blast + qed + then show ?thesis + by (simp add: \S \ lmeasurable\ \T \ lmeasurable\ \U \ lmeasurable\ fmeasurableD measure_mono_fmeasurable sets.Diff) + qed + finally have "measure lebesgue T - measure lebesgue S \ measure lebesgue U" . + with mU show "measure lebesgue T < measure lebesgue S + e" + by linarith + qed +qed + +proposition lebesgue_regular_inner: + assumes "S \ sets lebesgue" + obtains K C where "negligible K" "\n::nat. compact(C n)" "S = (\n. C n) \ K" +proof - + have "\T. closed T \ T \ S \ (S - T) \ lmeasurable \ measure lebesgue (S - T) < (1/2)^n" for n + using sets_lebesgue_inner_closed assms + by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power) + then obtain C where clo: "\n. closed (C n)" and subS: "\n. C n \ S" + and mea: "\n. (S - C n) \ lmeasurable" + and less: "\n. measure lebesgue (S - C n) < (1/2)^n" + by metis + have "\F. (\n::nat. compact(F n)) \ (\n. F n) = C m" for m::nat + by (metis clo closed_Union_compact_subsets) + then obtain D :: "[nat,nat] \ 'a set" where D: "\m n. compact(D m n)" "\m. (\n. D m n) = C m" + by metis + let ?C = "from_nat_into (\m. range (D m))" + have "countable (\m. range (D m))" + by blast + have "range (from_nat_into (\m. range (D m))) = (\m. range (D m))" + using range_from_nat_into by simp + then have CD: "\m n. ?C k = D m n" for k + by (metis (mono_tags, lifting) UN_iff rangeE range_eqI) + show thesis + proof + show "negligible (S - (\n. C n))" + proof (clarsimp simp: negligible_outer_le) + fix e :: "real" + assume "e > 0" + then obtain n where n: "(1/2)^n < e" + using real_arch_pow_inv [of e "1/2"] by auto + show "\T. S - (\n. C n) \ T \ T \ lmeasurable \ measure lebesgue T \ e" + proof (intro exI conjI) + show "S - (\n. C n) \ S - C n" + by blast + show "S - C n \ lmeasurable" + by (simp add: mea) + show "measure lebesgue (S - C n) \ e" + using less [of n] n by simp + qed + qed + show "compact (?C n)" for n + using CD D by metis + show "S = (\n. ?C n) \ (S - (\n. C n))" (is "_ = ?rhs") + proof + show "S \ ?rhs" + using D by fastforce + show "?rhs \ S" + using subS D CD by auto (metis Sup_upper range_eqI subsetCE) + qed + qed +qed + + +lemma sets_lebesgue_continuous_image: + assumes T: "T \ sets lebesgue" and contf: "continuous_on S f" + and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" and "T \ S" + shows "f ` T \ sets lebesgue" +proof - + obtain K C where "negligible K" and com: "\n::nat. compact(C n)" and Teq: "T = (\n. C n) \ K" + using lebesgue_regular_inner [OF T] by metis + then have comf: "\n::nat. compact(f ` C n)" + by (metis Un_subset_iff Union_upper \T \ S\ compact_continuous_image contf continuous_on_subset rangeI) + have "((\n. f ` C n) \ f ` K) \ sets lebesgue" + proof (rule sets.Un) + have "K \ S" + using Teq \T \ S\ by blast + show "(\n. f ` C n) \ sets lebesgue" + proof (rule sets.countable_Union) + show "range (\n. f ` C n) \ sets lebesgue" + using borel_compact comf by (auto simp: borel_compact) + qed auto + show "f ` K \ sets lebesgue" + by (simp add: \K \ S\ \negligible K\ negim negligible_imp_sets) + qed + then show ?thesis + by (simp add: Teq image_Un image_Union) +qed + +lemma differentiable_image_in_sets_lebesgue: + fixes f :: "'m::euclidean_space \ 'n::euclidean_space" + assumes S: "S \ sets lebesgue" and dim: "DIM('m) \ DIM('n)" and f: "f differentiable_on S" + shows "f`S \ sets lebesgue" +proof (rule sets_lebesgue_continuous_image [OF S]) + show "continuous_on S f" + by (meson differentiable_imp_continuous_on f) + show "\T. \negligible T; T \ S\ \ negligible (f ` T)" + using differentiable_on_subset f + by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) +qed auto + +lemma sets_lebesgue_on_continuous_image: + assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and contf: "continuous_on S f" + and negim: "\T. \negligible T; T \ S\ \ negligible(f ` T)" + shows "f ` X \ sets (lebesgue_on (f ` S))" +proof - + have "X \ S" + by (metis S X sets.Int_space_eq2 sets_restrict_space_iff) + moreover have "f ` S \ sets lebesgue" + using S contf negim sets_lebesgue_continuous_image by blast + moreover have "f ` X \ sets lebesgue" + by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2) + ultimately show ?thesis + by (auto simp: sets_restrict_space_iff) +qed + +lemma differentiable_image_in_sets_lebesgue_on: + fixes f :: "'m::euclidean_space \ 'n::euclidean_space" + assumes S: "S \ sets lebesgue" and X: "X \ sets (lebesgue_on S)" and dim: "DIM('m) \ DIM('n)" + and f: "f differentiable_on S" + shows "f ` X \ sets (lebesgue_on (f`S))" +proof (rule sets_lebesgue_on_continuous_image [OF S X]) + show "continuous_on S f" + by (meson differentiable_imp_continuous_on f) + show "\T. \negligible T; T \ S\ \ negligible (f ` T)" + using differentiable_on_subset f + by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim]) +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 + then have "S = {}" + by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI) + then show ?thesis + by auto + next + case False + then have "B \ 0" + by arith + let ?\ = "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 "open T" "S \ T" and TS: "(T-S) \ lmeasurable" and "?\ (T-S) < d" + using S \d > 0\ lmeasurable_outer_open by blast + with S 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 \ + ?\ (f ` (S \ ball x r)) \ (B + e) * ?\ (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 \x \ S\ 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 \x \ S\ + by (auto intro!: negligible_convex_frontier [OF convex_linear_image]) + have 0: "0 < e * unit_ball_vol (real CARD('n))" + using \e > 0\ by simp + obtain k where "k > 0" and k: + "\U. \U \ lmeasurable; \y. y \ U \ \z. z \ f' x ` ball 0 1 \ dist z y < k\ + \ ?\ U < ?\ (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))" + using measure_semicontinuous_with_hausdist_explicit [OF bo neg 0] by blast + obtain l where "l > 0" and l: "ball x l \ T" + using \x \ S\ \open T\ \S \ T\ openE by blast + obtain \ where "0 < \" + and \: "\y. \y \ S; y \ x; dist y x < \\ + \ norm (f y - (f x + f' x (y - x))) / norm (y - x) < k" + using lim0 \k > 0\ by (force simp: Lim_within 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 \l > 0\ \\ > 0\ \d > 0\ 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 \k > 0\ that show ?thesis + by (rule_tac x=0 in bexI) (auto simp: linear_0) + next + case False + then show ?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_cmul) + then have "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) + also have "\ = norm (f' x (y - x) - (f y - f x)) / r" + using \r > 0\ by (simp add: real_vector.scale_right_diff_distrib [symmetric] divide_simps) + also have "\ \ norm (f y - (f x + f' x (y - x))) / norm (y - x)" + using that \r > 0\ False by (simp add: algebra_simps divide_simps dist_norm norm_minus_commute mult_right_mono) + also have "\ < k" + using that \0 < \\ by (simp add: dist_commute r_def \ [OF \y \ S\ False]) + finally show "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 \r > 0\ 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]) + moreover have "?rfs \ ?B" + apply (auto simp: dist_norm image_iff dest!: ex_lessK) + by (metis (no_types, hide_lams) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball) + ultimately show "bounded (?rfs)" + by (rule bounded_subset) + qed + then have "(\x. r *\<^sub>R x) ` ?rfs \ lmeasurable" + by (simp add: measurable_linear_image) + with \r > 0\ have "(+) (- f x) ` f ` (S \ ball x r) \ lmeasurable" + by (simp add: image_comp o_def) + then have "(+) (f x) ` (+) (- f x) ` f ` (S \ ball x r) \ lmeasurable" + using measurable_translation by blast + then show 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 \r > 0\ by (simp add: measure_translation measure_linear_image measurable_translation fsb field_simps) + also have "\ \ (\det (matrix (f' x))\ * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))) * r ^ CARD('n)" + proof - + have "?\ (?rfs) < ?\ (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))" + using rfs_mble by (force intro: k dest!: ex_lessK) + then have "?\ (?rfs) < \det (matrix (f' x))\ * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))" + by (simp add: lin measure_linear_image [of "f' x"] content_ball) + with \r > 0\ show ?thesis + by auto + qed + also have "\ \ (B + e) * ?\ (ball x r)" + using bounded [OF \x \ S\] \r > 0\ by (simp add: content_ball algebra_simps) + finally show "?\ (f ` (S \ ball x r)) \ (B + e) * ?\ (ball x r)" . + qed + qed + then obtain 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 \ ball x (r x d))) \ lmeasurable \ + ?\ (f ` (S \ ball x (r x d))) \ (B + e) * ?\ (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 \K \ C\ 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 + apply (clarsimp simp: pairwise_def case_prod_unfold ball_eq_ball_iff) + by (metis subsetD fst_conv snd_conv) + have "?l \ (\i\K. ?\ (case i of (x, s) \ f ` (S \ ball x s)))" + proof (rule measure_UNION_le [OF \finite K\], clarify) + fix x r + assume "(x,r) \ K" + then have "x \ S" + using Csub \K \ C\ 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 + also have "\ \ (\(x,s) \ K. (B + e) * ?\ (ball x s))" + apply (rule sum_mono) + using Csub r \K \ C\ by auto + also have "\ = (B + e) * (\(x,s) \ K. ?\ (ball x s))" + by (simp add: prod.case_distrib sum_distrib_left) + also have "\ = (B + e) * sum ?\ ((\(x, y). ball x y) ` K)" + using \B \ 0\ \e > 0\ by (simp add: inj sum.reindex prod.case_distrib) + also have "\ = (B + e) * ?\ (\(x,s) \ K. ball x s)" + using \B \ 0\ \e > 0\ that + by (subst measure_Union') (auto simp: disjnt measure_Union') + also have "\ \ (B + e) * ?\ T" + using \B \ 0\ \e > 0\ that apply simp + apply (rule measure_mono_fmeasurable [OF _ _ \T \ lmeasurable\]) + using Csub rT by force+ + also have "\ \ (B + e) * (?\ S + d)" + using \B \ 0\ \e > 0\ Tless by simp + finally show ?thesis . + qed + have fSUB_mble: "(f ` (S \ ?UB)) \ lmeasurable" + unfolding eq using Csub r False \e > 0\ that + by (auto simp: intro!: fmeasurable_UN_bound [OF \countable C\ _ mle]) + have fSUB_meas: "?\ (f ` (S \ ?UB)) \ (B + e) * (?\ S + d)" (is "?MUB") + unfolding eq using Csub r False \e > 0\ that + by (auto simp: intro!: measure_UN_bound [OF \countable C\ _ 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 \ :: real + assume "0 < \" + then show "?\ (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) + then show ?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" + then show "?\ (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 + then show "f ` S \ lmeasurable" ?M by blast+ +qed + +lemma + 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 m_diff_image_weak: "f ` S \ lmeasurable \ measure lebesgue (f ` S) \ integral S (\x. \det (matrix (f' x))\)" +proof - + let ?\ = "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))\ \ + \det (matrix (f' x))\ < (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) + then have 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) + then have 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(floor(abs(det(matrix(f' x))) / e))" in exI) + using that apply auto + using of_int_floor_le pos_le_divide_eq apply blast + by (metis add.commute pos_divide_less_eq real_of_int_floor_add_one_gt) + 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) \x \ T n\ deriv has_derivative_within_subset mem_Collect_eq subsetI T_def) + show "\det (matrix (f' x))\ \ (Suc n) * e" + using \x \ T n\ 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 \e > 0\ 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" + then have "n < 1 + real m" + by (metis (no_types, hide_lams) less_le_trans mult.commute not_le real_mult_le_cancel_iff2) + then show "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 \e > 0\ \m < n\ that + apply (auto simp: T_def mult.commute intro: less_le_trans dest!: subsetD) + by (metis add.commute less_le_trans nat_less_real_le not_le real_mult_le_cancel_iff2) + then show ?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_within_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) + also have "\ \ (\k\n. (k * e) * ?\(T k)) + (\k\n. e * ?\(T k))" + by (simp add: algebra_simps sum.distrib) + also have "\ \ ?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] + integral_mult_right [symmetric] integral_mult_left [symmetric] + del: integral_mult_right integral_mult_left) + also have "\ \ (\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 \x \ T k\ T_def by blast + qed + qed + also have "\ = sum (\T. integral T (\x. \det (matrix (f' x))\)) (T ` {..n})" + by (auto intro: sum_eq_Tim) + also have "\ = 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}" + then show "((\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 + also have "\ \ m" + unfolding m_def + proof (rule integral_subset_le) + have "(\x. \det (matrix (f' x))\) absolutely_integrable_on (\k\n. T k)" + apply (rule set_integrable_subset [OF aint_S]) + apply (intro measurable meas_t fmeasurableD) + apply (force simp: Seq) + done + then show "(\x. \det (matrix (f' x))\) integrable_on (\k\n. T k)" + using absolutely_integrable_on_def by blast + qed (use Seq int in auto) + finally show "(\k\n. real k * e * ?\ (T k)) \ m" . + next + have "(\k\n. ?\ (T k)) = sum ?\ (T ` {..n})" + by (auto intro: sum_eq_Tim) + also have "\ = ?\ (\k\n. T k)" + using S disT by (auto simp: pairwise_def meas_t intro: measure_Union' [symmetric]) + also have "\ \ ?\ S" + using S by (auto simp: Seq intro: meas_t fmeasurableD measure_mono_fmeasurable) + finally have "(\k\n. ?\ (T k)) \ ?\ S" . + then show "(\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 + finally show "(\k\n. ?\ (f ` T k)) \ ?B" . + qed + moreover have "measure lebesgue (\k\n. f ` T k) \ (\k\n. ?\ (f ` T k))" for n + by (simp add: fmeasurableD meas_ft measure_UNION_le) + ultimately have 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]) + moreover have "?\ (\n. f ` T n) \ m + e * ?\ S" + by (rule measure_countable_Union_le [OF meas_ft B_ge_m]) + ultimately show "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 + then have "?\ 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 + then show ?thesis + using * [OF 0] that by (auto simp: divide_simps m_def split: if_split_asm) + qed + then show "?\ (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 ?\ = "measure lebesgue" + have "x \ cbox (vec (- real (nat \norm x\))) (vec (real (nat \norm x\)))" for x :: "real^'n::_" + apply (auto simp: mem_box_cart) + apply (metis abs_le_iff component_le_norm_cart minus_le_iff of_nat_ceiling order.trans) + by (meson abs_le_D1 norm_bound_component_le_cart real_nat_ceiling_ge) + then have Seq: "S = (\n. ?I n)" + by auto + have fIn: "f ` ?I n \ lmeasurable" + and mfIn: "?\ (f ` ?I n) \ integral S (\x. \det (matrix (f' x))\)" (is ?MN) for n + proof - + have In: "?I n \ lmeasurable" + by (simp add: S bounded_Int bounded_set_imp_lmeasurable sets.Int) + moreover have "\x. x \ ?I n \ (f has_derivative f' x) (at x within ?I n)" + by (meson Int_iff deriv has_derivative_within_subset subsetI) + moreover have int_In: "(\x. \det (matrix (f' x))\) integrable_on ?I n" + proof - + have "(\x. \det (matrix (f' x))\) absolutely_integrable_on S" + using int absolutely_integrable_integrable_bound by force + then have "(\x. \det (matrix (f' x))\) absolutely_integrable_on ?I n" + by (metis (no_types) Int_lower1 In fmeasurableD inf_commute set_integrable_subset) + then show ?thesis + using absolutely_integrable_on_def by blast + qed + ultimately have "f ` ?I n \ lmeasurable" "?\ (f ` ?I n) \ integral (?I n) (\x. \det (matrix (f' x))\)" + using m_diff_image_weak by metis+ + moreover have "integral (?I n) (\x. \det (matrix (f' x))\) \ integral S (\x. \det (matrix (f' x))\)" + by (simp add: int_In int integral_subset_le) + ultimately show "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 \auto simp: subset_interval_imp_cart\) + then have "(\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 + then have "(\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])+ + then show "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)) \ + (\g. (\n x. 0 \ g n x \ g n x \ f x) \ (\n x. g n x \ (g(Suc n) x)) \ + (\n. g n \ borel_measurable lebesgue) \ (\n. finite(range (g n))) \ + (\x. (\n. g n x) \ 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 + also have "\ \ sets lebesgue" + using borel_measurable_vimage_halfspace_component_lt [of f UNIV] f by auto + finally show ?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 "\na\N. g n x - f x \ dist (g na x) (f x)" for N + apply (rule_tac x="N+n" in exI) + using g [of N] by (auto simp: dist_norm) + with that show ?thesis + using diff_gt_0_iff_gt by blast + qed + with lim show ?thesis + apply (auto simp: lim_sequentially) + by (meson less_le_not_le not_le_imp_less) + qed + moreover + let ?\ = "\n k. indicator {y. k/2^n \ f y \ 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)) \ + (\n. g n \ borel_measurable lebesgue) \ (\n. finite(range (g n))) \(\x. (\n. g n x) \ 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 \k \ \\ apply (auto simp: indicator_def divide_simps Ints_def) + apply (drule spec [where x=x]) + using zero_le_power [of "2::real" n] mult_nonneg_nonneg [of "f x" "2^n"] + by linarith + qed + show "?g n x \ ?g (Suc n) x" for n x + proof - + have "?g n x = + (\k | k \ \ \ \k\ \ 2 ^ (2*n). + k/2^n * (indicator {y. k/2^n \ f y \ f y < (k+1/2)/2^n} x + + indicator {y. (k+1/2)/2^n \ f y \ f y < (k+1)/2^n} x))" + by (rule sum.cong [OF refl]) (simp add: indicator_def divide_simps) + also have "\ = (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. k/2^n \ f y \ f y < (k+1/2)/2^n} x) + + (\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n \ f y \ f y < (k+1)/2^n} x)" + by (simp add: comm_monoid_add_class.sum.distrib algebra_simps) + also have "\ = (\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) + + (\k | k \ \ \ \k\ \ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \ f y \ f y < ((2 * k+1) + 1)/2 ^ Suc n} x)" + by (force simp: field_simps indicator_def intro: sum.cong) + also have "\ \ (\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 \ f y \ 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 \ f y \ f y < (2 * k+1 + 1)/2 ^ Suc n} x) + \ sum ?h {k \ \. \k\ \ 2 ^ (2*n)}" + by (rule sum_mono) (simp add: indicator_def divide_simps) + next + have \: "?a = (\k \ ( *)2 ` {k \ \. \k\ \ 2 ^ (2*n)}. + k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x)" + by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex) + have \: "sum ?h {k \ \. \k\ \ 2 ^ (2*n)} + = (\k \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2 ^ (2*n)}. + k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ 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)} + = (\k \ ( *)2 ` {k \ \. \k\ \ 2 ^ (2*n)} \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2 ^ (2*n)}. + k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \ f y \ f y < (k+1)/2 ^ Suc n} x)" + unfolding \ \ + using finite_abs_int_segment [of "2 ^ (2*n)"] + by (subst sum_Un) (auto simp: 0) + also have "\ \ ?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 auto + 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 + proof - + have "0 \ f x * (2 * 2^n)" + by (simp add: f) + also have "\ < b+1" + by (simp add: that) + finally show "0 \ b" + using \b \ \\ by (auto simp: elim!: Ints_cases) + qed + then show "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 \ \. \k\ \ 2 ^ (2*n)} \ (\x. 2*x + 1) ` {k \ \. \k\ \ 2 ^ (2*n)})" for b + using that by (simp add: indicator_def divide_simps) + qed + finally show "?a + sum ?h {k \ \. \k\ \ 2 ^ (2*n)} \ ?b" . + qed + qed + finally show ?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) + \ (\k. k/2^n) ` {k \ \. \k\ \ 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 + then show ?thesis + by (blast intro: indicator_sum_eq) + next + case False + then have "(\k | k \ \ \ \k\ \ 2 ^ (2*n). k/2^n * ?\ n k x) = 0" + by auto + then show ?thesis by force + qed + then have "range (?g n) \ ((\k. (k/2^n)) ` {k. k \ \ \ \k\ \ 2 ^ (2*n)})" + by auto + moreover have "finite ((\k::real. (k/2^n)) ` {k \ \. \k\ \ 2 ^ (2*n)})" + by (intro finite_imageI finite_abs_int_segment) + ultimately show ?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 \e > 0\ 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) + also have "\ \ 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)) + finally have 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) + then have 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) + also have "\ < 2 ^ N2 * e" + using N2 by (simp add: divide_simps mult.commute) linarith + also have "\ \ \2^n\ * e" + using that \e > 0\ by auto + finally have "dist (?m/2^n) (f x) < e" + by (simp add: dist_norm) + then show ?thesis + using eq by linarith + qed + then show "\no. \n\no. dist (\k | k \ \ \ \k\ \ 2 ^ (2*n). k * ?\ n k x/2^n) (f x) < e" + by force + qed + qed + ultimately show ?rhs + by metis +next + assume RHS: ?rhs + with borel_measurable_simple_function_limit [of f UNIV, unfolded borel_measurable_UNIV_eq] + show ?lhs + by (blast intro: order_trans) +qed + +subsection\Borel measurable Jacobian determinant\ + +lemma lemma_partial_derivatives0: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "linear f" and lim0: "((\x. f x /\<^sub>R norm x) \ 0) (at 0 within S)" + and lb: "\v. v \ 0 \ (\k>0. \e>0. \x. x \ S - {0} \ norm x < e \ k * norm x \ \v \ x\)" + shows "f x = 0" +proof - + have "dim {x. f x = 0} \ DIM('a)" + using dim_subset_UNIV by blast + moreover have False if less: "dim {x. f x = 0} < DIM('a)" + proof - + obtain d where "d \ 0" and d: "\y. f y = 0 \ d \ y = 0" + using orthogonal_to_subspace_exists [OF less] orthogonal_def + by (metis (mono_tags, lifting) mem_Collect_eq span_clauses(1)) + then obtain k where "k > 0" + and k: "\e. e > 0 \ \y. y \ S - {0} \ norm y < e \ k * norm y \ \d \ y\" + using lb by blast + have "\h. \n. ((h n \ S \ h n \ 0 \ k * norm (h n) \ \d \ h n\) \ norm (h n) < 1 / real (Suc n)) \ + norm (h (Suc n)) < norm (h n)" + proof (rule dependent_nat_choice) + show "\y. (y \ S \ y \ 0 \ k * norm y \ \d \ y\) \ norm y < 1 / real (Suc 0)" + by simp (metis DiffE insertCI k not_less not_one_le_zero) + qed (use k [of "min (norm x) (1/(Suc n + 1))" for x n] in auto) + then obtain \ where \: "\n. \ n \ S - {0}" and kd: "\n. k * norm(\ n) \ \d \ \ n\" + and norm_lt: "\n. norm(\ n) < 1/(Suc n)" + by force + let ?\ = "\n. \ n /\<^sub>R norm (\ n)" + have com: "\g. (\n. g n \ sphere (0::'a) 1) + \ \l \ sphere 0 1. \\::nat\nat. strict_mono \ \ (g \ \) \ l" + using compact_sphere compact_def by metis + moreover have "\n. ?\ n \ sphere 0 1" + using \ by auto + ultimately obtain l::'a and \::"nat\nat" + where l: "l \ sphere 0 1" and "strict_mono \" and to_l: "(?\ \ \) \ l" + by meson + moreover have "continuous (at l) (\x. (\d \ x\ - k))" + by (intro continuous_intros) + ultimately have lim_dl: "((\x. (\d \ x\ - k)) \ (?\ \ \)) \ (\d \ l\ - k)" + by (meson continuous_imp_tendsto) + have "\\<^sub>F i in sequentially. 0 \ ((\x. \d \ x\ - k) \ ((\n. \ n /\<^sub>R norm (\ n)) \ \)) i" + using \ kd by (auto simp: divide_simps) + then have "k \ \d \ l\" + using tendsto_lowerbound [OF lim_dl, of 0] by auto + moreover have "d \ l = 0" + proof (rule d) + show "f l = 0" + proof (rule LIMSEQ_unique [of "f \ ?\ \ \"]) + have "isCont f l" + using \linear f\ linear_continuous_at linear_conv_bounded_linear by blast + then show "(f \ (\n. \ n /\<^sub>R norm (\ n)) \ \) \ f l" + unfolding comp_assoc + using to_l continuous_imp_tendsto by blast + have "\ \ 0" + using norm_lt LIMSEQ_norm_0 by metis + with \strict_mono \\ have "(\ \ \) \ 0" + by (metis LIMSEQ_subseq_LIMSEQ) + with lim0 \ have "((\x. f x /\<^sub>R norm x) \ (\ \ \)) \ 0" + by (force simp: tendsto_at_iff_sequentially) + then show "(f \ (\n. \ n /\<^sub>R norm (\ n)) \ \) \ 0" + by (simp add: o_def linear_cmul \linear f\) + qed + qed + ultimately show False + using \k > 0\ by auto + qed + ultimately have dim: "dim {x. f x = 0} = DIM('a)" + by force + then show ?thesis + by (metis (mono_tags, lifting) UNIV_I assms(1) dim_eq_full linear_eq_0_span mem_Collect_eq) +qed + +lemma lemma_partial_derivatives: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "linear f" and lim: "((\x. f (x - a) /\<^sub>R norm (x - a)) \ 0) (at a within S)" + and lb: "\v. v \ 0 \ (\k>0. \e>0. \x \ S - {a}. norm(a - x) < e \ k * norm(a - x) \ \v \ (x - a)\)" + shows "f x = 0" +proof - + have "((\x. f x /\<^sub>R norm x) \ 0) (at 0 within (\x. x-a) ` S)" + using lim by (simp add: Lim_within dist_norm) + then show ?thesis + proof (rule lemma_partial_derivatives0 [OF \linear f\]) + fix v :: "'a" + assume v: "v \ 0" + show "\k>0. \e>0. \x. x \ (\x. x - a) ` S - {0} \ norm x < e \ k * norm x \ \v \ x\" + using lb [OF v] by (force simp: norm_minus_commute) + qed +qed + + +proposition borel_measurable_partial_derivatives: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" + assumes S: "S \ sets lebesgue" + and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + shows "(\x. (matrix(f' x)$m$n)) \ borel_measurable (lebesgue_on S)" +proof - + have contf: "continuous_on S f" + using continuous_on_eq_continuous_within f has_derivative_continuous by blast + have "{x \ S. (matrix (f' x)$m$n) \ b} \ sets lebesgue" for b + proof (rule sets_negligible_symdiff) + let ?T = "{x \ S. \e>0. \d>0. \A. A$m$n < b \ (\i j. A$i$j \ \) \ + (\y \ S. norm(y - x) < d \ norm(f y - f x - A *v (y - x)) \ e * norm(y - x))}" + let ?U = "S \ + (\e \ {e \ \. e > 0}. + \A \ {A. A$m$n < b \ (\i j. A$i$j \ \)}. + \d \ {d \ \. 0 < d}. + S \ (\y \ S. {x \ S. norm(y - x) < d \ norm(f y - f x - A *v (y - x)) \ e * norm(y - x)}))" + have "?T = ?U" + proof (intro set_eqI iffI) + fix x + assume xT: "x \ ?T" + then show "x \ ?U" + proof (clarsimp simp add:) + fix q :: real + assume "q \ \" "q > 0" + then obtain d A where "d > 0" and A: "A $ m $ n < b" "\i j. A $ i $ j \ \" + "\y. \y\S; norm (y - x) < d\ \ norm (f y - f x - A *v (y - x)) \ q * norm (y - x)" + using xT by auto + then obtain \ where "d > \" "\ > 0" "\ \ \" + using Rats_dense_in_real by blast + with A show "\A. A $ m $ n < b \ (\i j. A $ i $ j \ \) \ + (\s. s \ \ \ 0 < s \ (\y\S. norm (y - x) < s \ norm (f y - f x - A *v (y - x)) \ q * norm (y - x)))" + by force + qed + next + fix x + assume xU: "x \ ?U" + then show "x \ ?T" + proof clarsimp + fix e :: "real" + assume "e > 0" + then obtain \ where \: "e > \" "\ > 0" "\ \ \" + using Rats_dense_in_real by blast + with xU obtain A r where "x \ S" and Ar: "A $ m $ n < b" "\i j. A $ i $ j \ \" "r \ \" "r > 0" + and "\y\S. norm (y - x) < r \ norm (f y - f x - A *v (y - x)) \ \ * norm (y - x)" + by (auto simp: split: if_split_asm) + then have "\y\S. norm (y - x) < r \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x)" + by (meson \e > \\ less_eq_real_def mult_right_mono norm_ge_zero order_trans) + then show "\d>0. \A. A $ m $ n < b \ (\i j. A $ i $ j \ \) \ (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" + using \x \ S\ Ar by blast + qed + qed + moreover have "?U \ sets lebesgue" + proof - + have coQ: "countable {e \ \. 0 < e}" + using countable_Collect countable_rat by blast + have ne: "{e \ \. (0::real) < e} \ {}" + using zero_less_one Rats_1 by blast + have coA: "countable {A. A $ m $ n < b \ (\i j. A $ i $ j \ \)}" + proof (rule countable_subset) + show "countable {A. \i j. A $ i $ j \ \}" + using countable_vector [OF countable_vector, of "\i j. \"] by (simp add: countable_rat) + qed blast + have *: "\U \ {} \ closedin (subtopology euclidean S) (S \ \ U)\ + \ closedin (subtopology euclidean S) (S \ \ U)" for U + by fastforce + have eq: "{x::(real,'m)vec. P x \ (Q x \ R x)} = {x. P x \ \ Q x} \ {x. P x \ R x}" for P Q R + by auto + have sets: "S \ (\y\S. {x \ S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x)}) + \ sets lebesgue" for e A d + proof - + have clo: "closedin (subtopology euclidean S) + {x \ S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x)}" + for y + proof - + have cont1: "continuous_on S (\x. norm (y - x))" + and cont2: "continuous_on S (\x. e * norm (y - x) - norm (f y - f x - (A *v y - A *v x)))" + by (force intro: contf continuous_intros)+ + have clo1: "closedin (subtopology euclidean S) {x \ S. d \ norm (y - x)}" + using continuous_closedin_preimage [OF cont1, of "{d..}"] by (simp add: vimage_def Int_def) + have clo2: "closedin (subtopology euclidean S) + {x \ S. norm (f y - f x - (A *v y - A *v x)) \ e * norm (y - x)}" + using continuous_closedin_preimage [OF cont2, of "{0..}"] by (simp add: vimage_def Int_def) + show ?thesis + by (auto simp: eq not_less matrix_vector_mult_diff_distrib intro: clo1 clo2) + qed + show ?thesis + by (rule lebesgue_closedin [of S]) (force intro: * S clo)+ + qed + show ?thesis + by (intro sets sets.Int S sets.countable_UN'' sets.countable_INT'' coQ coA) auto + qed + ultimately show "?T \ sets lebesgue" + by simp + let ?M = "(?T - {x \ S. matrix (f' x) $ m $ n \ b} \ ({x \ S. matrix (f' x) $ m $ n \ b} - ?T))" + let ?\ = "\x v. \\>0. \e>0. \y \ S-{x}. norm (x - y) < e \ \v \ (y - x)\ < \ * norm (x - y)" + have nN: "negligible {x \ S. \v\0. ?\ x v}" + unfolding negligible_eq_zero_density + proof clarsimp + fix x v and r e :: "real" + assume "x \ S" "v \ 0" "r > 0" "e > 0" + and Theta [rule_format]: "?\ x v" + moreover have "(norm v * e / 2) / CARD('m) ^ CARD('m) > 0" + by (simp add: \v \ 0\ \e > 0\) + ultimately obtain d where "d > 0" + and dless: "\y. \y \ S - {x}; norm (x - y) < d\ \ + \v \ (y - x)\ < ((norm v * e / 2) / CARD('m) ^ CARD('m)) * norm (x - y)" + by metis + let ?W = "ball x (min d r) \ {y. \v \ (y - x)\ < (norm v * e/2 * min d r) / CARD('m) ^ CARD('m)}" + have "open {x. \v \ (x - a)\ < b}" for a b + by (intro open_Collect_less continuous_intros) + show "\d>0. d \ r \ + (\U. {x' \ S. \v\0. ?\ x' v} \ ball x d \ U \ + U \ lmeasurable \ measure lebesgue U < e * content (ball x d))" + proof (intro exI conjI) + show "0 < min d r" "min d r \ r" + using \r > 0\ \d > 0\ by auto + show "{x' \ S. \v. v \ 0 \ (\\>0. \e>0. \z\S - {x'}. norm (x' - z) < e \ \v \ (z - x')\ < \ * norm (x' - z))} \ ball x (min d r) \ ?W" + proof (clarsimp simp: dist_norm norm_minus_commute) + fix y :: "(real, 'm) vec" and w :: "(real, 'm) vec" + assume "y \ S" "w \ 0" + and less [rule_format]: + "\\>0. \e>0. \z\S - {y}. norm (y - z) < e \ \w \ (z - y)\ < \ * norm (y - z)" + and d: "norm (y - x) < d" and r: "norm (y - x) < r" + show "\v \ (y - x)\ < norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))" + proof (cases "y = x") + case True + with \r > 0\ \d > 0\ \e > 0\ \v \ 0\ show ?thesis + by simp + next + case False + have "\v \ (y - x)\ < norm v * e / 2 / real (CARD('m) ^ CARD('m)) * norm (x - y)" + apply (rule dless) + using False \y \ S\ d by (auto simp: norm_minus_commute) + also have "\ \ norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))" + using d r \e > 0\ by (simp add: field_simps norm_minus_commute mult_left_mono) + finally show ?thesis . + qed + qed + show "?W \ lmeasurable" + by (simp add: fmeasurable_Int_fmeasurable borel_open) + obtain k::'m where True + by metis + obtain T where T: "orthogonal_transformation T" and v: "v = T(norm v *\<^sub>R axis k (1::real))" + using rotation_rightward_line by metis + define b where "b \ norm v" + have "b > 0" + using \v \ 0\ by (auto simp: b_def) + obtain eqb: "inv T v = b *\<^sub>R axis k (1::real)" and "inj T" "bij T" and invT: "orthogonal_transformation (inv T)" + by (metis UNIV_I b_def T v bij_betw_inv_into_left orthogonal_transformation_inj orthogonal_transformation_bij orthogonal_transformation_inv) + let ?v = "\ i. min d r / CARD('m)" + let ?v' = "\ i. if i = k then (e/2 * min d r) / CARD('m) ^ CARD('m) else min d r" + let ?x' = "inv T x" + let ?W' = "(ball ?x' (min d r) \ {y. \(y - ?x')$k\ < e * min d r / (2 * CARD('m) ^ CARD('m))})" + have abs: "x - e \ y \ y \ x + e \ abs(y - x) \ e" for x y e::real + by auto + have "?W = T ` ?W'" + proof - + have 1: "T ` (ball (inv T x) (min d r)) = ball x (min d r)" + by (simp add: T image_orthogonal_transformation_ball orthogonal_transformation_surj surj_f_inv_f) + have 2: "{y. \v \ (y - x)\ < b * e * min d r / (2 * real CARD('m) ^ CARD('m))} = + T ` {y. \y $ k - ?x' $ k\ < e * min d r / (2 * real CARD('m) ^ CARD('m))}" + proof - + have *: "\T (b *\<^sub>R axis k 1) \ (y - x)\ = b * \inv T y $ k - ?x' $ k\" for y + proof - + have "\T (b *\<^sub>R axis k 1) \ (y - x)\ = \(b *\<^sub>R axis k 1) \ inv T (y - x)\" + by (metis (no_types, hide_lams) b_def eqb invT orthogonal_transformation_def v) + also have "\ = b * \(axis k 1) \ inv T (y - x)\" + using \b > 0\ by (simp add: abs_mult) + also have "\ = b * \inv T y $ k - ?x' $ k\" + using orthogonal_transformation_linear [OF invT] + by (simp add: inner_axis' linear_diff) + finally show ?thesis + by simp + qed + show ?thesis + using v b_def [symmetric] + using \b > 0\ by (simp add: * bij_image_Collect_eq [OF \bij T\] mult_less_cancel_left_pos times_divide_eq_right [symmetric] del: times_divide_eq_right) + qed + show ?thesis + using \b > 0\ by (simp add: image_Int \inj T\ 1 2 b_def [symmetric]) + qed + moreover have "?W' \ lmeasurable" + by (auto intro: fmeasurable_Int_fmeasurable) + ultimately have "measure lebesgue ?W = measure lebesgue ?W'" + by (metis measure_orthogonal_image T) + also have "\ \ measure lebesgue (cbox (?x' - ?v') (?x' + ?v'))" + proof (rule measure_mono_fmeasurable) + show "?W' \ cbox (?x' - ?v') (?x' + ?v')" + apply (clarsimp simp add: mem_box_cart abs dist_norm norm_minus_commute simp del: min_less_iff_conj min.bounded_iff) + by (metis component_le_norm_cart less_eq_real_def le_less_trans vector_minus_component) + qed auto + also have "\ \ e/2 * measure lebesgue (cbox (?x' - ?v) (?x' + ?v))" + proof - + have "cbox (?x' - ?v) (?x' + ?v) \ {}" + using \r > 0\ \d > 0\ by (auto simp: interval_eq_empty_cart divide_less_0_iff) + with \r > 0\ \d > 0\ \e > 0\ show ?thesis + apply (simp add: content_cbox_if_cart mem_box_cart) + apply (auto simp: prod_nonneg) + apply (simp add: abs if_distrib prod.delta_remove prod_constant field_simps power_diff split: if_split_asm) + done + qed + also have "\ \ e/2 * measure lebesgue (cball ?x' (min d r))" + proof (rule mult_left_mono [OF measure_mono_fmeasurable]) + have *: "norm (?x' - y) \ min d r" + if y: "\i. \?x' $ i - y $ i\ \ min d r / real CARD('m)" for y + proof - + have "norm (?x' - y) \ (\i\UNIV. \(?x' - y) $ i\)" + by (rule norm_le_l1_cart) + also have "\ \ real CARD('m) * (min d r / real CARD('m))" + by (rule sum_bounded_above) (use y in auto) + finally show ?thesis + by simp + qed + show "cbox (?x' - ?v) (?x' + ?v) \ cball ?x' (min d r)" + apply (clarsimp simp only: mem_box_cart dist_norm mem_cball intro!: *) + by (simp add: abs_diff_le_iff abs_minus_commute) + qed (use \e > 0\ in auto) + also have "\ < e * content (cball ?x' (min d r))" + using \r > 0\ \d > 0\ \e > 0\ by auto + also have "\ = e * content (ball x (min d r))" + using \r > 0\ \d > 0\ by (simp add: content_cball content_ball) + finally show "measure lebesgue ?W < e * content (ball x (min d r))" . + qed + qed + have *: "(\x. (x \ S) \ (x \ T \ x \ U)) \ (T - U) \ (U - T) \ S" for S T U :: "(real,'m) vec set" + by blast + have MN: "?M \ {x \ S. \v\0. ?\ x v}" + proof (rule *) + fix x + assume x: "x \ {x \ S. \v\0. ?\ x v}" + show "(x \ ?T) \ (x \ {x \ S. matrix (f' x) $ m $ n \ b})" + proof (cases "x \ S") + case True + then have x: "\ ?\ x v" if "v \ 0" for v + using x that by force + show ?thesis + proof (rule iffI; clarsimp) + assume b: "\e>0. \d>0. \A. A $ m $ n < b \ (\i j. A $ i $ j \ \) \ + (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" + (is "\e>0. \d>0. \A. ?\ e d A") + then have "\k. \d>0. \A. ?\ (1 / Suc k) d A" + by (metis (no_types, hide_lams) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff) + then obtain \ A where \: "\k. \ k > 0" + and Ab: "\k. A k $ m $ n < b" + and A: "\k y. \y \ S; norm (y - x) < \ k\ \ + norm (f y - f x - A k *v (y - x)) \ 1/(Suc k) * norm (y - x)" + by metis + have "\i j. \a. (\n. A n $ i $ j) \ a" + proof (intro allI) + fix i j + have vax: "(A n *v axis j 1) $ i = A n $ i $ j" for n + by (metis cart_eq_inner_axis matrix_vector_mul_component) + let ?CA = "{x. Cauchy (\n. (A n) *v x)}" + have "subspace ?CA" + unfolding subspace_def convergent_eq_Cauchy [symmetric] + by (force simp: algebra_simps intro: tendsto_intros) + then have CA_eq: "?CA = span ?CA" + by (metis span_eq) + also have "\ = UNIV" + proof - + have "dim ?CA \ CARD('m)" + by (rule dim_subset_UNIV_cart) + moreover have "False" if less: "dim ?CA < CARD('m)" + proof - + obtain d where "d \ 0" and d: "\y. y \ span ?CA \ orthogonal d y" + using less by (force intro: orthogonal_to_subspace_exists [of ?CA]) + with x [OF \d \ 0\] obtain \ where "\ > 0" + and \: "\e. e > 0 \ \y \ S - {x}. norm (x - y) < e \ \ * norm (x - y) \ \d \ (y - x)\" + by (fastforce simp: not_le Bex_def) + obtain \ z where \Sx: "\i. \ i \ S - {x}" + and \le: "\i. \ * norm(\ i - x) \ \d \ (\ i - x)\" + and \x: "\ \ x" + and z: "(\n. (\ n - x) /\<^sub>R norm (\ n - x)) \ z" + proof - + have "\\. (\i. (\ i \ S - {x} \ + \ * norm(\ i - x) \ \d \ (\ i - x)\ \ norm(\ i - x) < 1/Suc i) \ + norm(\(Suc i) - x) < norm(\ i - x))" + proof (rule dependent_nat_choice) + show "\y. y \ S - {x} \ \ * norm (y - x) \ \d \ (y - x)\ \ norm (y - x) < 1 / Suc 0" + using \ [of 1] by (auto simp: dist_norm norm_minus_commute) + next + fix y i + assume "y \ S - {x} \ \ * norm (y - x) \ \d \ (y - x)\ \ norm (y - x) < 1/Suc i" + then have "min (norm(y - x)) (1/((Suc i) + 1)) > 0" + by auto + then obtain y' where "y' \ S - {x}" and y': "norm (x - y') < min (norm (y - x)) (1/((Suc i) + 1))" + "\ * norm (x - y') \ \d \ (y' - x)\" + using \ by metis + with \ show "\y'. (y' \ S - {x} \ \ * norm (y' - x) \ \d \ (y' - x)\ \ + norm (y' - x) < 1/(Suc (Suc i))) \ norm (y' - x) < norm (y - x)" + by (auto simp: dist_norm norm_minus_commute) + qed + then obtain \ where + \Sx: "\i. \ i \ S - {x}" + and \le: "\i. \ * norm(\ i - x) \ \d \ (\ i - x)\" + and \conv: "\i. norm(\ i - x) < 1/(Suc i)" + by blast + let ?f = "\i. (\ i - x) /\<^sub>R norm (\ i - x)" + have "?f i \ sphere 0 1" for i + using \Sx by auto + then obtain l \ where "l \ sphere 0 1" "strict_mono \" and l: "(?f \ \) \ l" + using compact_sphere [of "0::(real,'m) vec" 1] unfolding compact_def by meson + show thesis + proof + show "(\ \ \) i \ S - {x}" "\ * norm ((\ \ \) i - x) \ \d \ ((\ \ \) i - x)\" for i + using \Sx \le by auto + have "\ \ x" + proof (clarsimp simp add: LIMSEQ_def dist_norm) + fix r :: "real" + assume "r > 0" + with real_arch_invD obtain no where "no \ 0" "real no > 1/r" + by (metis divide_less_0_1_iff not_less_iff_gr_or_eq of_nat_0_eq_iff reals_Archimedean2) + with \conv show "\no. \n\no. norm (\ n - x) < r" + by (metis \r > 0\ add.commute divide_inverse inverse_inverse_eq inverse_less_imp_less less_trans mult.left_neutral nat_le_real_less of_nat_Suc) + qed + with \strict_mono \\ show "(\ \ \) \ x" + by (metis LIMSEQ_subseq_LIMSEQ) + show "(\n. ((\ \ \) n - x) /\<^sub>R norm ((\ \ \) n - x)) \ l" + using l by (auto simp: o_def) + qed + qed + have "isCont (\x. (\d \ x\ - \)) z" + by (intro continuous_intros) + from isCont_tendsto_compose [OF this z] + have lim: "(\y. \d \ ((\ y - x) /\<^sub>R norm (\ y - x))\ - \) \ \d \ z\ - \" + by auto + moreover have "\\<^sub>F i in sequentially. 0 \ \d \ ((\ i - x) /\<^sub>R norm (\ i - x))\ - \" + proof (rule eventuallyI) + fix n + show "0 \ \d \ ((\ n - x) /\<^sub>R norm (\ n - x))\ - \" + using \le [of n] \Sx by (auto simp: abs_mult divide_simps) + qed + ultimately have "\ \ \d \ z\" + using tendsto_lowerbound [where a=0] by fastforce + have "Cauchy (\n. (A n) *v z)" + proof (clarsimp simp add: Cauchy_def) + fix \ :: "real" + assume "0 < \" + then obtain N::nat where "N > 0" and N: "\/2 > 1/N" + by (metis half_gt_zero inverse_eq_divide neq0_conv real_arch_inverse) + show "\M. \m\M. \n\M. dist (A m *v z) (A n *v z) < \" + proof (intro exI allI impI) + fix i j + assume ij: "N \ i" "N \ j" + let ?V = "\i k. A i *v ((\ k - x) /\<^sub>R norm (\ k - x))" + have "\\<^sub>F k in sequentially. dist (\ k) x < min (\ i) (\ j)" + using \x [unfolded tendsto_iff] by (meson min_less_iff_conj \) + then have even: "\\<^sub>F k in sequentially. norm (?V i k - ?V j k) - 2 / N \ 0" + proof (rule eventually_mono, clarsimp) + fix p + assume p: "dist (\ p) x < \ i" "dist (\ p) x < \ j" + let ?C = "\k. f (\ p) - f x - A k *v (\ p - x)" + have "norm ((A i - A j) *v (\ p - x)) = norm (?C j - ?C i)" + by (simp add: algebra_simps) + also have "\ \ norm (?C j) + norm (?C i)" + using norm_triangle_ineq4 by blast + also have "\ \ 1/(Suc j) * norm (\ p - x) + 1/(Suc i) * norm (\ p - x)" + by (metis A Diff_iff \Sx dist_norm p add_mono) + also have "\ \ 1/N * norm (\ p - x) + 1/N * norm (\ p - x)" + apply (intro add_mono mult_right_mono) + using ij \N > 0\ by (auto simp: field_simps) + also have "\ = 2 / N * norm (\ p - x)" + by simp + finally have no_le: "norm ((A i - A j) *v (\ p - x)) \ 2 / N * norm (\ p - x)" . + have "norm (?V i p - ?V j p) = + norm ((A i - A j) *v ((\ p - x) /\<^sub>R norm (\ p - x)))" + by (simp add: algebra_simps) + also have "\ = norm ((A i - A j) *v (\ p - x)) / norm (\ p - x)" + by (simp add: divide_inverse matrix_vector_mult_scaleR) + also have "\ \ 2 / N" + using no_le by (auto simp: divide_simps) + finally show "norm (?V i p - ?V j p) \ 2 / N" . + qed + have "isCont (\w. (norm(A i *v w - A j *v w) - 2 / N)) z" + by (intro continuous_intros) + from isCont_tendsto_compose [OF this z] + have lim: "(\w. norm (A i *v ((\ w - x) /\<^sub>R norm (\ w - x)) - + A j *v ((\ w - x) /\<^sub>R norm (\ w - x))) - 2 / N) + \ norm (A i *v z - A j *v z) - 2 / N" + by auto + have "dist (A i *v z) (A j *v z) \ 2 / N" + using tendsto_upperbound [OF lim even] by (auto simp: dist_norm) + with N show "dist (A i *v z) (A j *v z) < \" + by linarith + qed + qed + then have "d \ z = 0" + using CA_eq d orthogonal_def by auto + then show False + using \0 < \\ \\ \ \d \ z\\ by auto + qed + ultimately show ?thesis + using dim_eq_full by fastforce + qed + finally have "?CA = UNIV" . + then have "Cauchy (\n. (A n) *v axis j 1)" + by auto + then obtain L where "(\n. A n *v axis j 1) \ L" + by (auto simp: Cauchy_convergent_iff convergent_def) + then have "(\x. (A x *v axis j 1) $ i) \ L $ i" + by (rule tendsto_vec_nth) + then show "\a. (\n. A n $ i $ j) \ a" + by (force simp: vax) + qed + then obtain B where B: "\i j. (\n. A n $ i $ j) \ B $ i $ j" + by (auto simp: lambda_skolem) + have lin_df: "linear (f' x)" + and lim_df: "((\y. (1 / norm (y - x)) *\<^sub>R (f y - (f x + f' x (y - x)))) \ 0) (at x within S)" + using \x \ S\ assms by (auto simp: has_derivative_within linear_linear) + moreover have "(matrix (f' x) - B) *v w = 0" for w + proof (rule lemma_partial_derivatives [of "( *v) (matrix (f' x) - B)"]) + show "linear (( *v) (matrix (f' x) - B))" + by (rule matrix_vector_mul_linear) + have "((\y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \ 0) (at x within S)" + using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps) + then show "((\y. (matrix (f' x) - B) *v (y - x) /\<^sub>R norm (y - x)) \ 0) (at x within S)" + proof (rule Lim_transform) + have "((\y. ((f y + B *v x - (f x + B *v y)) /\<^sub>R norm (y - x))) \ 0) (at x within S)" + proof (clarsimp simp add: Lim_within dist_norm) + fix e :: "real" + assume "e > 0" + then obtain q::nat where "q \ 0" and qe2: "1/q < e/2" + by (metis divide_pos_pos inverse_eq_divide real_arch_inverse zero_less_numeral) + let ?g = "\p. sum (\i. sum (\j. abs((A p - B)$i$j)) UNIV) UNIV" + have "(\k. onorm (\y. (A k - B) *v y)) \ 0" + proof (rule Lim_null_comparison) + show "\\<^sub>F k in sequentially. norm (onorm (\y. (A k - B) *v y)) \ ?g k" + proof (rule eventually_sequentiallyI) + fix k :: "nat" + assume "0 \ k" + have "0 \ onorm (( *v) (A k - B))" + by (simp add: linear_linear onorm_pos_le matrix_vector_mul_linear) + then show "norm (onorm (( *v) (A k - B))) \ (\i\UNIV. \j\UNIV. \(A k - B) $ i $ j\)" + by (simp add: onorm_le_matrix_component_sum del: vector_minus_component) + qed + next + show "?g \ 0" + using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum) + qed + with \e > 0\ obtain p where "\n. n \ p \ \onorm (( *v) (A n - B))\ < e/2" + unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral) + then have pqe2: "\onorm (( *v) (A (p + q) - B))\ < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*) + using le_add1 by blast + show "\d>0. \y\S. y \ x \ norm (y - x) < d \ + inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e" + proof (intro exI, safe) + show "0 < \(p + q)" + by (simp add: \) + next + fix y + assume y: "y \ S" "norm (y - x) < \(p + q)" and "y \ x" + have *: "\norm(b - c) < e - d; norm(y - x - b) \ d\ \ norm(y - x - c) < e" + for b c d e x and y:: "real^'n" + using norm_triangle_ineq2 [of "y - x - c" "y - x - b"] by simp + have "norm (f y - f x - B *v (y - x)) < e * norm (y - x)" + proof (rule *) + show "norm (f y - f x - A (p + q) *v (y - x)) \ norm (y - x) / (Suc (p + q))" + using A [OF y] by simp + have "norm (A (p + q) *v (y - x) - B *v (y - x)) \ onorm(\x. (A(p + q) - B) *v x) * norm(y - x)" + by (metis linear_linear matrix_vector_mul_linear matrix_vector_mult_diff_rdistrib onorm) + also have "\ < (e/2) * norm (y - x)" + using \y \ x\ pqe2 by auto + also have "\ \ (e - 1 / (Suc (p + q))) * norm (y - x)" + proof (rule mult_right_mono) + have "1 / Suc (p + q) \ 1 / q" + using \q \ 0\ by (auto simp: divide_simps) + also have "\ < e/2" + using qe2 by auto + finally show "e / 2 \ e - 1 / real (Suc (p + q))" + by linarith + qed auto + finally show "norm (A (p + q) *v (y - x) - B *v (y - x)) < e * norm (y - x) - norm (y - x) / real (Suc (p + q))" + by (simp add: algebra_simps) + qed + then show "inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e" + using \y \ x\ by (simp add: divide_simps algebra_simps) + qed + qed + then show "((\y. (matrix (f' x) - B) *v (y - x) /\<^sub>R + norm (y - x) - (f x + f' x (y - x) - f y) /\<^sub>R norm (y - x)) \ 0) + (at x within S)" + by (simp add: algebra_simps lin_df linear_diff matrix_vector_mul_linear) + qed + qed (use x in \simp; auto simp: not_less\) + ultimately have "f' x = ( *v) B" + by (force simp: algebra_simps) + show "matrix (f' x) $ m $ n \ b" + proof (rule tendsto_upperbound [of "\i. (A i $ m $ n)" _ sequentially]) + show "(\i. A i $ m $ n) \ matrix (f' x) $ m $ n" + by (simp add: B \f' x = ( *v) B\) + show "\\<^sub>F i in sequentially. A i $ m $ n \ b" + by (simp add: Ab less_eq_real_def) + qed auto + next + fix e :: "real" + assume "x \ S" and b: "matrix (f' x) $ m $ n \ b" and "e > 0" + then obtain d where "d>0" + and d: "\y. y\S \ 0 < dist y x \ dist y x < d \ norm (f y - f x - f' x (y - x)) / (norm (y - x)) + < e/2" + using f [OF \x \ S\] unfolding Deriv.has_derivative_at_within Lim_within + by (auto simp: field_simps dest: spec [of _ "e/2"]) + let ?A = "matrix(f' x) - (\ i j. if i = m \ j = n then e / 4 else 0)" + obtain B where BRats: "\i j. B$i$j \ \" and Bo_e6: "onorm(( *v) (?A - B)) < e/6" + using matrix_rational_approximation \e > 0\ + by (metis zero_less_divide_iff zero_less_numeral) + show "\d>0. \A. A $ m $ n < b \ (\i j. A $ i $ j \ \) \ + (\y\S. norm (y - x) < d \ norm (f y - f x - A *v (y - x)) \ e * norm (y - x))" + proof (intro exI conjI ballI allI impI) + show "d>0" + by (rule \d>0\) + show "B $ m $ n < b" + proof - + have "\matrix (( *v) (?A - B)) $ m $ n\ \ onorm (( *v) (?A - B))" + using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis + then show ?thesis + using b Bo_e6 by simp + qed + show "B $ i $ j \ \" for i j + using BRats by auto + show "norm (f y - f x - B *v (y - x)) \ e * norm (y - x)" + if "y \ S" and y: "norm (y - x) < d" for y + proof (cases "y = x") + case True then show ?thesis + by simp + next + case False + have *: "norm(d' - d) \ e/2 \ norm(y - (x + d')) < e/2 \ norm(y - x - d) \ e" for d d' e and x y::"real^'n" + using norm_triangle_le [of "d' - d" "y - (x + d')"] by simp + show ?thesis + proof (rule *) + have split246: "\norm y \ e / 6; norm(x - y) \ e / 4\ \ norm x \ e/2" if "e > 0" for e and x y :: "real^'n" + using norm_triangle_le [of y "x-y" "e/2"] \e > 0\ by simp + have "linear (f' x)" + using True f has_derivative_linear by blast + then have "norm (f' x (y - x) - B *v (y - x)) = norm ((matrix (f' x) - B) *v (y - x))" + by (metis matrix_vector_mul matrix_vector_mult_diff_rdistrib) + also have "\ \ (e * norm (y - x)) / 2" + proof (rule split246) + have "norm ((?A - B) *v (y - x)) / norm (y - x) \ onorm(\x. (?A - B) *v x)" + by (simp add: le_onorm linear_linear matrix_vector_mul_linear) + also have "\ < e/6" + by (rule Bo_e6) + finally have "norm ((?A - B) *v (y - x)) / norm (y - x) < e / 6" . + then show "norm ((?A - B) *v (y - x)) \ e * norm (y - x) / 6" + by (simp add: divide_simps False) + have "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) = norm ((\ i j. if i = m \ j = n then e / 4 else 0) *v (y - x))" + by (simp add: algebra_simps) + also have "\ = norm((e/4) *\<^sub>R (y - x)$n *\<^sub>R axis m (1::real))" + proof - + have "(\j\UNIV. (if i = m \ j = n then e / 4 else 0) * (y $ j - x $ j)) * 4 = e * (y $ n - x $ n) * axis m 1 $ i" for i + proof (cases "i=m") + case True then show ?thesis + by (auto simp: if_distrib [of "\z. z * _"] cong: if_cong) + next + case False then show ?thesis + by (simp add: axis_def) + qed + then have "(\ i j. if i = m \ j = n then e / 4 else 0) *v (y - x) = (e/4) *\<^sub>R (y - x)$n *\<^sub>R axis m (1::real)" + by (auto simp: vec_eq_iff matrix_vector_mult_def) + then show ?thesis + by metis + qed + also have "\ \ e * norm (y - x) / 4" + using \e > 0\ apply (simp add: norm_mult abs_mult) + by (metis component_le_norm_cart vector_minus_component) + finally show "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) \ e * norm (y - x) / 4" . + show "0 < e * norm (y - x)" + by (simp add: False \e > 0\) + qed + finally show "norm (f' x (y - x) - B *v (y - x)) \ (e * norm (y - x)) / 2" . + show "norm (f y - (f x + f' x (y - x))) < (e * norm (y - x)) / 2" + using False d [OF \y \ S\] y by (simp add: dist_norm field_simps) + qed + qed + qed + qed + qed auto + qed + show "negligible ?M" + using negligible_subset [OF nN MN] . + qed + then show ?thesis + by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff assms) +qed + + +theorem borel_measurable_det_Jacobian: + fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" + assumes S: "S \ sets lebesgue" and f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + shows "(\x. det(matrix(f' x))) \ borel_measurable (lebesgue_on S)" + unfolding det_def + by (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S]) + +text\The localisation wrt S uses the same argument for many similar results. +See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.\ +lemma borel_measurable_lebesgue_on_preimage_borel: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "S \ sets lebesgue" + shows "f \ borel_measurable (lebesgue_on S) \ + (\T. T \ sets borel \ {x \ S. f x \ T} \ sets lebesgue)" +proof - + have "{x. (if x \ S then f x else 0) \ T} \ sets lebesgue \ {x \ S. f x \ T} \ sets lebesgue" + if "T \ sets borel" for T + proof (cases "0 \ T") + case True + then have "{x \ S. f x \ T} = {x. (if x \ S then f x else 0) \ T} \ S" + "{x. (if x \ S then f x else 0) \ T} = {x \ S. f x \ T} \ -S" + by auto + then show ?thesis + by (metis (no_types, lifting) Compl_in_sets_lebesgue assms sets.Int sets.Un) + next + case False + then have "{x. (if x \ S then f x else 0) \ T} = {x \ S. f x \ T}" + by auto + then show ?thesis + by auto + qed + then show ?thesis + unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric] + by blast +qed + +lemma sets_lebesgue_almost_borel: + assumes "S \ sets lebesgue" + obtains B N where "B \ sets borel" "negligible N" "B \ N = S" +proof - + obtain T N N' where "S = T \ N" "N \ N'" "N' \ null_sets lborel" "T \ sets borel" + using sets_completionE [OF assms] by auto + then show thesis + by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that) +qed + +lemma double_lebesgue_sets: + assumes S: "S \ sets lebesgue" and T: "T \ sets lebesgue" and fim: "f ` S \ T" + shows "(\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue) \ + f \ borel_measurable (lebesgue_on S) \ + (\U. negligible U \ U \ T \ {x \ S. f x \ U} \ sets lebesgue)" + (is "?lhs \ _ \ ?rhs") + unfolding borel_measurable_lebesgue_on_preimage_borel [OF S] +proof (intro iffI allI conjI impI, safe) + fix V :: "'b set" + assume *: "\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue" + and "V \ sets borel" + then have V: "V \ sets lebesgue" + by simp + have "{x \ S. f x \ V} = {x \ S. f x \ T \ V}" + using fim by blast + also have "{x \ S. f x \ T \ V} \ sets lebesgue" + using T V * le_inf_iff by blast + finally show "{x \ S. f x \ V} \ sets lebesgue" . +next + fix U :: "'b set" + assume "\U. U \ sets lebesgue \ U \ T \ {x \ S. f x \ U} \ sets lebesgue" + "negligible U" "U \ T" + then show "{x \ S. f x \ U} \ sets lebesgue" + using negligible_imp_sets by blast +next + fix U :: "'b set" + assume 1 [rule_format]: "(\T. T \ sets borel \ {x \ S. f x \ T} \ sets lebesgue)" + and 2 [rule_format]: "\U. negligible U \ U \ T \ {x \ S. f x \ U} \ sets lebesgue" + and "U \ sets lebesgue" "U \ T" + then obtain C N where C: "C \ sets borel \ negligible N \ C \ N = U" + using sets_lebesgue_almost_borel + by metis + then have "{x \ S. f x \ C} \ sets lebesgue" + by (blast intro: 1) + moreover have "{x \ S. f x \ N} \ sets lebesgue" + using C \U \ T\ by (blast intro: 2) + moreover have "{x \ S. f x \ C \ N} = {x \ S. f x \ C} \ {x \ S. f x \ N}" + by auto + ultimately show "{x \ S. f x \ U} \ sets lebesgue" + using C by auto +qed + + + +thm integrable_on_subcbox + +proposition measurable_bounded_by_integrable_imp_integrable: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes f: "f \ borel_measurable (lebesgue_on S)" and g: "g integrable_on S" + and normf: "\x. x \ S \ norm(f x) \ g x" and S: "S \ sets lebesgue" + shows "f integrable_on S" +proof (rule integrable_on_all_intervals_integrable_bound [OF _ normf g]) + show "(\x. if x \ S then f x else 0) integrable_on cbox a b" for a b + proof (rule measurable_bounded_lemma) + show "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue" + by (simp add: S borel_measurable_UNIV f) + show "(\x. if x \ S then g x else 0) integrable_on cbox a b" + by (simp add: g integrable_altD(1)) + show "norm (if x \ S then f x else 0) \ (if x \ S then g x else 0)" for x + using normf by simp + qed +qed + + +subsection\Simplest case of Sard's theorem (we don't need continuity of derivative)\ + +lemma Sard_lemma00: + fixes P :: "'b::euclidean_space set" + assumes "a \ 0" and a: "a *\<^sub>R i \ 0" and i: "i \ Basis" + and P: "P \ {x. a *\<^sub>R i \ x = 0}" + and "0 \ m" "0 \ e" + obtains S where "S \ lmeasurable" + and "{z. norm z \ m \ (\t \ P. norm(z - t) \ e)} \ S" + and "measure lebesgue S \ (2 * e) * (2 * m) ^ (DIM('b) - 1)" +proof - + have "a > 0" + using assms by simp + let ?v = "(\j\Basis. (if j = i then e else m) *\<^sub>R j)" + show thesis + proof + have "- e \ x \ i" "x \ i \ e" + if "t \ P" "norm (x - t) \ e" for x t + using \a > 0\ that Basis_le_norm [of i "x-t"] P i + by (auto simp: inner_commute algebra_simps) + moreover have "- m \ x \ j" "x \ j \ m" + if "norm x \ m" "t \ P" "norm (x - t) \ e" "j \ Basis" and "j \ i" + for x t j + using that Basis_le_norm [of j x] by auto + ultimately + show "{z. norm z \ m \ (\t\P. norm (z - t) \ e)} \ cbox (-?v) ?v" + by (auto simp: mem_box) + have *: "\k\Basis. - ?v \ k \ ?v \ k" + using \0 \ m\ \0 \ e\ by (auto simp: inner_Basis) + have 2: "2 ^ DIM('b) = 2 * 2 ^ (DIM('b) - Suc 0)" + by (metis DIM_positive Suc_pred power_Suc) + show "measure lebesgue (cbox (-?v) ?v) \ 2 * e * (2 * m) ^ (DIM('b) - 1)" + using \i \ Basis\ + by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2) + qed blast +qed + +text\As above, but reorienting the vector (HOL Light's @text{GEOM_BASIS_MULTIPLE_TAC})\ +lemma Sard_lemma0: + fixes P :: "(real^'n::{finite,wellorder}) set" + assumes "a \ 0" + and P: "P \ {x. a \ x = 0}" and "0 \ m" "0 \ e" + obtains S where "S \ lmeasurable" + and "{z. norm z \ m \ (\t \ P. norm(z - t) \ e)} \ S" + and "measure lebesgue S \ (2 * e) * (2 * m) ^ (CARD('n) - 1)" +proof - + obtain T and k::'n where T: "orthogonal_transformation T" and a: "a = T (norm a *\<^sub>R axis k (1::real))" + using rotation_rightward_line by metis + have Tinv [simp]: "T (inv T x) = x" for x + by (simp add: T orthogonal_transformation_surj surj_f_inv_f) + obtain S where S: "S \ lmeasurable" + and subS: "{z. norm z \ m \ (\t \ T-`P. norm(z - t) \ e)} \ S" + and mS: "measure lebesgue S \ (2 * e) * (2 * m) ^ (CARD('n) - 1)" + proof (rule Sard_lemma00 [of "norm a" "axis k (1::real)" "T-`P" m e]) + have "norm a *\<^sub>R axis k 1 \ x = 0" if "T x \ P" for x + proof - + have "a \ T x = 0" + using P that by blast + then show ?thesis + by (metis (no_types, lifting) T a orthogonal_orthogonal_transformation orthogonal_def) + qed + then show "T -` P \ {x. norm a *\<^sub>R axis k 1 \ x = 0}" + by auto + qed (use assms T in auto) + show thesis + proof + show "T ` S \ lmeasurable" + using S measurable_orthogonal_image T by blast + have "{z. norm z \ m \ (\t\P. norm (z - t) \ e)} \ T ` {z. norm z \ m \ (\t\T -` P. norm (z - t) \ e)}" + proof clarsimp + fix x t + assume "norm x \ m" "t \ P" "norm (x - t) \ e" + then have "norm (inv T x) \ m" + using orthogonal_transformation_inv [OF T] by (simp add: orthogonal_transformation_norm) + moreover have "\t\T -` P. norm (inv T x - t) \ e" + proof + have "T (inv T x - inv T t) = x - t" + using T linear_diff orthogonal_transformation_def by fastforce + then have "norm (inv T x - inv T t) = norm (x - t)" + by (metis T orthogonal_transformation_norm) + then show "norm (inv T x - inv T t) \ e" + using \norm (x - t) \ e\ by linarith + next + show "inv T t \ T -` P" + using \t \ P\ by force + qed + ultimately show "x \ T ` {z. norm z \ m \ (\t\T -` P. norm (z - t) \ e)}" + by force + qed + then show "{z. norm z \ m \ (\t\P. norm (z - t) \ e)} \ T ` S" + using image_mono [OF subS] by (rule order_trans) + show "measure lebesgue (T ` S) \ 2 * e * (2 * m) ^ (CARD('n) - 1)" + using mS T by (simp add: S measure_orthogonal_image) + qed +qed + +(*As above, but translating the sets (HOL Light's GEN_GEOM_ORIGIN_TAC)*) +lemma Sard_lemma1: + fixes P :: "(real^'n::{finite,wellorder}) set" + assumes P: "dim P < CARD('n)" and "0 \ m" "0 \ e" + obtains S where "S \ lmeasurable" + and "{z. norm(z - w) \ m \ (\t \ P. norm(z - w - t) \ e)} \ S" + and "measure lebesgue S \ (2 * e) * (2 * m) ^ (CARD('n) - 1)" +proof - + obtain a where "a \ 0" "P \ {x. a \ x = 0}" + using lowdim_subset_hyperplane [of P] P span_inc by auto + then obtain S where S: "S \ lmeasurable" + and subS: "{z. norm z \ m \ (\t \ P. norm(z - t) \ e)} \ S" + and mS: "measure lebesgue S \ (2 * e) * (2 * m) ^ (CARD('n) - 1)" + by (rule Sard_lemma0 [OF _ _ \0 \ m\ \0 \ e\]) + show thesis + proof + show "(+)w ` S \ lmeasurable" + by (metis measurable_translation S) + show "{z. norm (z - w) \ m \ (\t\P. norm (z - w - t) \ e)} \ (+)w ` S" + using subS by force + show "measure lebesgue ((+)w ` S) \ 2 * e * (2 * m) ^ (CARD('n) - 1)" + by (metis measure_translation mS) + qed +qed + +lemma Sard_lemma2: + fixes f :: "real^'m::{finite,wellorder} \ real^'n::{finite,wellorder}" + assumes mlen: "CARD('m) \ CARD('n)" (is "?m \ ?n") + and "B > 0" "bounded S" + and derS: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + and rank: "\x. x \ S \ rank(matrix(f' x)) < CARD('n)" + and B: "\x. x \ S \ onorm(f' x) \ B" + shows "negligible(f ` S)" +proof - + have lin_f': "\x. x \ S \ linear(f' x)" + using derS has_derivative_linear by blast + show ?thesis + proof (clarsimp simp add: negligible_outer_le) + fix e :: "real" + assume "e > 0" + obtain c where csub: "S \ cbox (- (vec c)) (vec c)" and "c > 0" + proof - + obtain b where b: "\x. x \ S \ norm x \ b" + using \bounded S\ by (auto simp: bounded_iff) + show thesis + proof + have "- \b\ - 1 \ x $ i \ x $ i \ \b\ + 1" if "x \ S" for x i + using component_le_norm_cart [of x i] b [OF that] by auto + then show "S \ cbox (- vec (\b\ + 1)) (vec (\b\ + 1))" + by (auto simp: mem_box_cart) + qed auto + qed + then have box_cc: "box (- (vec c)) (vec c) \ {}" and cbox_cc: "cbox (- (vec c)) (vec c) \ {}" + by (auto simp: interval_eq_empty_cart) + obtain d where "d > 0" "d \ B" + and d: "(d * 2) * (4 * B) ^ (?n - 1) \ e / (2*c) ^ ?m / ?m ^ ?m" + apply (rule that [of "min B (e / (2*c) ^ ?m / ?m ^ ?m / (4 * B) ^ (?n - 1) / 2)"]) + using \B > 0\ \c > 0\ \e > 0\ + by (simp_all add: divide_simps min_mult_distrib_right) + have "\r. 0 < r \ r \ 1/2 \ + (x \ S + \ (\y. y \ S \ norm(y - x) < r + \ norm(f y - f x - f' x (y - x)) \ d * norm(y - x)))" for x + proof (cases "x \ S") + case True + then obtain r where "r > 0" + and "\y. \y \ S; norm (y - x) < r\ + \ norm (f y - f x - f' x (y - x)) \ d * norm (y - x)" + using derS \d > 0\ by (force simp: has_derivative_within_alt) + then show ?thesis + by (rule_tac x="min r (1/2)" in exI) simp + next + case False + then show ?thesis + by (rule_tac x="1/2" in exI) simp + qed + then obtain r where r12: "\x. 0 < r x \ r x \ 1/2" + and r: "\x y. \x \ S; y \ S; norm(y - x) < r x\ + \ norm(f y - f x - f' x (y - x)) \ d * norm(y - x)" + by metis + then have ga: "gauge (\x. ball x (r x))" + by (auto simp: gauge_def) + obtain \ where \: "countable \" and sub_cc: "\\ \ cbox (- vec c) (vec c)" + and cbox: "\K. K \ \ \ interior K \ {} \ (\u v. K = cbox u v)" + and djointish: "pairwise (\A B. interior A \ interior B = {}) \" + and covered: "\K. K \ \ \ \x \ S \ K. K \ ball x (r x)" + and close: "\u v. cbox u v \ \ \ \n. \i::'m. v $ i - u $ i = 2*c / 2^n" + and covers: "S \ \\" + apply (rule covering_lemma [OF csub box_cc ga]) + apply (auto simp: Basis_vec_def cart_eq_inner_axis [symmetric]) + done + let ?\ = "measure lebesgue" + have "\T. T \ lmeasurable \ f ` (K \ S) \ T \ ?\ T \ e / (2*c) ^ ?m * ?\ K" + if "K \ \" for K + proof - + obtain u v where uv: "K = cbox u v" + using cbox \K \ \\ by blast + then have uv_ne: "cbox u v \ {}" + using cbox that by fastforce + obtain x where x: "x \ S \ cbox u v" "cbox u v \ ball x (r x)" + using \K \ \\ covered uv by blast + then have "dim (range (f' x)) < ?n" + using rank_dim_range [of "matrix (f' x)"] lin_f' rank by fastforce + then obtain T where T: "T \ lmeasurable" + and subT: "{z. norm(z - f x) \ (2 * B) * norm(v - u) \ (\t \ range (f' x). norm(z - f x - t) \ d * norm(v - u))} \ T" + and measT: "?\ T \ (2 * (d * norm(v - u))) * (2 * ((2 * B) * norm(v - u))) ^ (?n - 1)" + (is "_ \ ?DVU") + apply (rule Sard_lemma1 [of "range (f' x)" "(2 * B) * norm(v - u)" "d * norm(v - u)" "f x"]) + using \B > 0\ \d > 0\ by simp_all + show ?thesis + proof (intro exI conjI) + have "f ` (K \ S) \ {z. norm(z - f x) \ (2 * B) * norm(v - u) \ (\t \ range (f' x). norm(z - f x - t) \ d * norm(v - u))}" + unfolding uv + proof (clarsimp simp: mult.assoc, intro conjI) + fix y + assume y: "y \ cbox u v" and "y \ S" + then have "norm (y - x) < r x" + by (metis dist_norm mem_ball norm_minus_commute subsetCE x(2)) + then have le_dyx: "norm (f y - f x - f' x (y - x)) \ d * norm (y - x)" + using r [of x y] x \y \ S\ by blast + have yx_le: "norm (y - x) \ norm (v - u)" + proof (rule norm_le_componentwise_cart) + show "\(y - x) $ i\ \ \(v - u) $ i\" for i + using x y by (force simp: mem_box_cart dest!: spec [where x=i]) + qed + have *: "\norm(y - x - z) \ d; norm z \ B; d \ B\ \ norm(y - x) \ 2 * B" + for x y z :: "real^'n::_" and d B + using norm_triangle_ineq2 [of "y - x" z] by auto + show "norm (f y - f x) \ 2 * (B * norm (v - u))" + proof (rule * [OF le_dyx]) + have "norm (f' x (y - x)) \ onorm (f' x) * norm (y - x)" + using onorm [of "f' x" "y-x"] by (meson IntE lin_f' linear_linear x(1)) + also have "\ \ B * norm (v - u)" + proof (rule mult_mono) + show "onorm (f' x) \ B" + using B x by blast + qed (use \B > 0\ yx_le in auto) + finally show "norm (f' x (y - x)) \ B * norm (v - u)" . + show "d * norm (y - x) \ B * norm (v - u)" + using \B > 0\ by (auto intro: mult_mono [OF \d \ B\ yx_le]) + qed + show "\t. norm (f y - f x - f' x t) \ d * norm (v - u)" + apply (rule_tac x="y-x" in exI) + using \d > 0\ yx_le le_dyx mult_left_mono [where c=d] + by (meson order_trans real_mult_le_cancel_iff2) + qed + with subT show "f ` (K \ S) \ T" by blast + show "?\ T \ e / (2*c) ^ ?m * ?\ K" + proof (rule order_trans [OF measT]) + have "?DVU = (d * 2 * (4 * B) ^ (?n - 1)) * norm (v - u)^?n" + using \c > 0\ + apply (simp add: algebra_simps power_mult_distrib) + by (metis Suc_pred power_Suc zero_less_card_finite) + also have "\ \ (e / (2*c) ^ ?m / (?m ^ ?m)) * norm(v - u) ^ ?n" + by (rule mult_right_mono [OF d]) auto + also have "\ \ e / (2*c) ^ ?m * ?\ K" + proof - + have "u \ ball (x) (r x)" "v \ ball x (r x)" + using box_ne_empty(1) contra_subsetD [OF x(2)] mem_box(2) uv_ne by fastforce+ + moreover have "r x \ 1/2" + using r12 by auto + ultimately have "norm (v - u) \ 1" + using norm_triangle_half_r [of x u 1 v] + by (metis (no_types, hide_lams) dist_commute dist_norm less_eq_real_def less_le_trans mem_ball) + then have "norm (v - u) ^ ?n \ norm (v - u) ^ ?m" + by (simp add: power_decreasing [OF mlen]) + also have "\ \ ?\ K * real (?m ^ ?m)" + proof - + obtain n where n: "\i. v$i - u$i = 2 * c / 2^n" + using close [of u v] \K \ \\ uv by blast + have "norm (v - u) ^ ?m \ (\i\UNIV. \(v - u) $ i\) ^ ?m" + by (intro norm_le_l1_cart power_mono) auto + also have "\ \ (\i\UNIV. v $ i - u $ i) * real CARD('m) ^ CARD('m)" + by (simp add: n field_simps \c > 0\ less_eq_real_def) + also have "\ = ?\ K * real (?m ^ ?m)" + by (simp add: uv uv_ne content_cbox_cart) + finally show ?thesis . + qed + finally have *: "1 / real (?m ^ ?m) * norm (v - u) ^ ?n \ ?\ K" + by (simp add: divide_simps) + show ?thesis + using mult_left_mono [OF *, of "e / (2*c) ^ ?m"] \c > 0\ \e > 0\ by auto + qed + finally show "?DVU \ e / (2*c) ^ ?m * ?\ K" . + qed + qed (use T in auto) + qed + then obtain g where meas_g: "\K. K \ \ \ g K \ lmeasurable" + and sub_g: "\K. K \ \ \ f ` (K \ S) \ g K" + and le_g: "\K. K \ \ \ ?\ (g K) \ e / (2*c)^?m * ?\ K" + by metis + have le_e: "?\ (\i\\. g i) \ e" + if "\ \ \" "finite \" for \ + proof - + have "?\ (\i\\. g i) \ (\i\\. ?\ (g i))" + using meas_g \\ \ \\ by (auto intro: measure_UNION_le [OF \finite \\]) + also have "\ \ (\K\\. e / (2*c) ^ ?m * ?\ K)" + using \\ \ \\ sum_mono [OF le_g] by (meson le_g subsetCE sum_mono) + also have "\ = e / (2*c) ^ ?m * (\K\\. ?\ K)" + by (simp add: sum_distrib_left) + also have "\ \ e" + proof - + have "\ division_of \\" + proof (rule division_ofI) + show "K \ \\" "K \ {}" "\a b. K = cbox a b" if "K \ \" for K + using \K \ \\ covered cbox \\ \ \\ by (auto simp: Union_upper) + show "interior K \ interior L = {}" if "K \ \" and "L \ \" and "K \ L" for K L + by (metis (mono_tags, lifting) \\ \ \\ pairwiseD djointish pairwise_subset that) + qed (use that in auto) + then have "sum ?\ \ \ ?\ (\\)" + by (simp add: content_division) + also have "\ \ ?\ (cbox (- vec c) (vec c) :: (real, 'm) vec set)" + proof (rule measure_mono_fmeasurable) + show "\\ \ cbox (- vec c) (vec c)" + by (meson Sup_subset_mono sub_cc order_trans \\ \ \\) + qed (use \\ division_of \\\ lmeasurable_division in auto) + also have "\ = content (cbox (- vec c) (vec c) :: (real, 'm) vec set)" + by simp + also have "\ \ (2 ^ ?m * c ^ ?m)" + using \c > 0\ by (simp add: content_cbox_if_cart) + finally have "sum ?\ \ \ (2 ^ ?m * c ^ ?m)" . + then show ?thesis + using \e > 0\ \c > 0\ by (auto simp: divide_simps mult_less_0_iff) + qed + finally show ?thesis . + qed + show "\T. f ` S \ T \ T \ lmeasurable \ ?\ T \ e" + proof (intro exI conjI) + show "f ` S \ UNION \ g" + using covers sub_g by force + show "UNION \ g \ lmeasurable" + by (rule fmeasurable_UN_bound [OF \countable \\ meas_g le_e]) + show "?\ (UNION \ g) \ e" + by (rule measure_UN_bound [OF \countable \\ meas_g le_e]) + qed + qed +qed + + +theorem baby_Sard: + fixes f :: "real^'m::{finite,wellorder} \ real^'n::{finite,wellorder}" + assumes mlen: "CARD('m) \ CARD('n)" + and der: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + and rank: "\x. x \ S \ rank(matrix(f' x)) < CARD('n)" + shows "negligible(f ` S)" +proof - + let ?U = "\n. {x \ S. norm(x) \ n \ onorm(f' x) \ real n}" + have "\x. x \ S \ \n. norm x \ real n \ onorm (f' x) \ real n" + by (meson linear order_trans real_arch_simple) + then have eq: "S = (\n. ?U n)" + by auto + have "negligible (f ` ?U n)" for n + proof (rule Sard_lemma2 [OF mlen]) + show "0 < real n + 1" + by auto + show "bounded (?U n)" + using bounded_iff by blast + show "(f has_derivative f' x) (at x within ?U n)" if "x \ ?U n" for x + using der that by (force intro: has_derivative_subset) + qed (use rank in auto) + then show ?thesis + by (subst eq) (simp add: image_Union negligible_Union_nat) +qed + + +subsection\A one-way version of change-of-variables not assuming injectivity. \ + +lemma integral_on_image_ubound_weak: + fixes f :: "real^'n::{finite,wellorder} \ real" + assumes S: "S \ sets lebesgue" + and f: "f \ borel_measurable (lebesgue_on (g ` S))" + and nonneg_fg: "\x. x \ S \ 0 \ f(g x)" + and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and det_int_fg: "(\x. \det (matrix (g' x))\ * f(g x)) integrable_on S" + and meas_gim: "\T. \T \ g ` S; T \ sets lebesgue\ \ {x \ S. g x \ T} \ sets lebesgue" + shows "f integrable_on (g ` S) \ + integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" + (is "_ \ _ \ ?b") +proof - + let ?D = "\x. \det (matrix (g' x))\" + have cont_g: "continuous_on S g" + using der_g has_derivative_continuous_on by blast + have [simp]: "space (lebesgue_on S) = S" + by (simp add: S) + have gS_in_sets_leb: "g ` S \ sets lebesgue" + apply (rule differentiable_image_in_sets_lebesgue) + using der_g by (auto simp: S differentiable_def differentiable_on_def) + obtain h where nonneg_h: "\n x. 0 \ h n x" + and h_le_f: "\n x. x \ S \ h n (g x) \ f (g x)" + and h_inc: "\n x. h n x \ h (Suc n) x" + and h_meas: "\n. h n \ borel_measurable lebesgue" + and fin_R: "\n. finite(range (h n))" + and lim: "\x. x \ g ` S \ (\n. h n x) \ f x" + proof - + let ?f = "\x. if x \ g ` S then f x else 0" + have "?f \ borel_measurable lebesgue \ (\x. 0 \ ?f x)" + by (auto simp: gS_in_sets_leb f nonneg_fg measurable_restrict_space_iff [symmetric]) + then show ?thesis + apply (clarsimp simp add: borel_measurable_simple_function_limit_increasing) + apply (rename_tac h) + by (rule_tac h=h in that) (auto split: if_split_asm) + qed + have h_lmeas: "{t. h n (g t) = y} \ S \ sets lebesgue" for y n + proof - + have "space (lebesgue_on (UNIV::(real,'n) vec set)) = UNIV" + by simp + then have "((h n) -`{y} \ g ` S) \ sets (lebesgue_on (g ` S))" + by (metis Int_commute borel_measurable_vimage h_meas image_eqI inf_top.right_neutral sets_restrict_space space_borel space_completion space_lborel) + then have "({u. h n u = y} \ g ` S) \ sets lebesgue" + using gS_in_sets_leb + by (simp add: integral_indicator fmeasurableI2 sets_restrict_space_iff vimage_def) + then have "{x \ S. g x \ ({u. h n u = y} \ g ` S)} \ sets lebesgue" + using meas_gim[of "({u. h n u = y} \ g ` S)"] by force + moreover have "{t. h n (g t) = y} \ S = {x \ S. g x \ ({u. h n u = y} \ g ` S)}" + by blast + ultimately show ?thesis + by auto + qed + have hint: "h n integrable_on g ` S \ integral (g ` S) (h n) \ integral S (\x. ?D x * h n (g x))" + (is "?INT \ ?lhs \ ?rhs") for n + proof - + let ?R = "range (h n)" + have hn_eq: "h n = (\x. \y\?R. y * indicat_real {x. h n x = y} x)" + by (simp add: indicator_def if_distrib fin_R cong: if_cong) + have yind: "(\t. y * indicator{x. h n x = y} t) integrable_on (g ` S) \ + (integral (g ` S) (\t. y * indicator {x. h n x = y} t)) + \ integral S (\t. \det (matrix (g' t))\ * y * indicator {x. h n x = y} (g t))" + if y: "y \ ?R" for y::real + proof (cases "y=0") + case True + then show ?thesis using gS_in_sets_leb integrable_0 by force + next + case False + with that have "y > 0" + using less_eq_real_def nonneg_h by fastforce + have "(\x. if x \ {t. h n (g t) = y} then ?D x else 0) integrable_on S" + proof (rule measurable_bounded_by_integrable_imp_integrable) + have "(\x. ?D x) \ borel_measurable (lebesgue_on ({t. h n (g t) = y} \ S))" + apply (intro borel_measurable_abs borel_measurable_det_Jacobian [OF h_lmeas, where f=g]) + by (meson der_g IntD2 has_derivative_within_subset inf_le2) + then have "(\x. if x \ {t. h n (g t) = y} \ S then ?D x else 0) \ borel_measurable lebesgue" + by (rule borel_measurable_If_I [OF _ h_lmeas]) + then show "(\x. if x \ {t. h n (g t) = y} then ?D x else 0) \ borel_measurable (lebesgue_on S)" + by (simp add: if_if_eq_conj Int_commute borel_measurable_UNIV [OF S, symmetric]) + show "(\x. ?D x *\<^sub>R f (g x) /\<^sub>R y) integrable_on S" + by (rule integrable_cmul) (use det_int_fg in auto) + show "norm (if x \ {t. h n (g t) = y} then ?D x else 0) \ ?D x *\<^sub>R f (g x) /\<^sub>R y" + if "x \ S" for x + using nonneg_h [of n x] \y > 0\ nonneg_fg [of x] h_le_f [of x n] that + by (auto simp: divide_simps ordered_semiring_class.mult_left_mono) + qed (use S in auto) + then have int_det: "(\t. \det (matrix (g' t))\) integrable_on ({t. h n (g t) = y} \ S)" + using integrable_restrict_Int by force + have "(g ` ({t. h n (g t) = y} \ S)) \ lmeasurable" + apply (rule measurable_differentiable_image [OF h_lmeas]) + apply (blast intro: has_derivative_within_subset [OF der_g]) + apply (rule int_det) + done + moreover have "g ` ({t. h n (g t) = y} \ S) = {x. h n x = y} \ g ` S" + by blast + moreover have "measure lebesgue (g ` ({t. h n (g t) = y} \ S)) + \ integral ({t. h n (g t) = y} \ S) (\t. \det (matrix (g' t))\)" + apply (rule measure_differentiable_image [OF h_lmeas _ int_det]) + apply (blast intro: has_derivative_within_subset [OF der_g]) + done + ultimately show ?thesis + using \y > 0\ integral_restrict_Int [of S "{t. h n (g t) = y}" "\t. \det (matrix (g' t))\ * y"] + apply (simp add: integrable_on_indicator integrable_on_cmult_iff integral_indicator) + apply (simp add: indicator_def if_distrib cong: if_cong) + done + qed + have hn_int: "h n integrable_on g ` S" + apply (subst hn_eq) + using yind by (force intro: integrable_sum [OF fin_R]) + then show ?thesis + proof + have "?lhs = integral (g ` S) (\x. \y\range (h n). y * indicat_real {x. h n x = y} x)" + by (metis hn_eq) + also have "\ = (\y\range (h n). integral (g ` S) (\x. y * indicat_real {x. h n x = y} x))" + by (rule integral_sum [OF fin_R]) (use yind in blast) + also have "\ \ (\y\range (h n). integral S (\u. \det (matrix (g' u))\ * y * indicat_real {x. h n x = y} (g u)))" + using yind by (force intro: sum_mono) + also have "\ = integral S (\u. \y\range (h n). \det (matrix (g' u))\ * y * indicat_real {x. h n x = y} (g u))" + proof (rule integral_sum [OF fin_R, symmetric]) + fix y assume y: "y \ ?R" + with nonneg_h have "y \ 0" + by auto + show "(\u. \det (matrix (g' u))\ * y * indicat_real {x. h n x = y} (g u)) integrable_on S" + proof (rule measurable_bounded_by_integrable_imp_integrable) + have "(\x. indicat_real {x. h n x = y} (g x)) \ borel_measurable (lebesgue_on S)" + using h_lmeas S + by (auto simp: indicator_vimage [symmetric] borel_measurable_indicator_iff sets_restrict_space_iff) + then show "(\u. \det (matrix (g' u))\ * y * indicat_real {x. h n x = y} (g u)) \ borel_measurable (lebesgue_on S)" + by (intro borel_measurable_times borel_measurable_abs borel_measurable_const borel_measurable_det_Jacobian [OF S der_g]) + next + fix x + assume "x \ S" + have "y * indicat_real {x. h n x = y} (g x) \ f (g x)" + by (metis (full_types) \x \ S\ h_le_f indicator_def mem_Collect_eq mult.right_neutral mult_zero_right nonneg_fg) + with \y \ 0\ show "norm (?D x * y * indicat_real {x. h n x = y} (g x)) \ ?D x * f(g x)" + by (simp add: abs_mult mult.assoc mult_left_mono) + qed (use S det_int_fg in auto) + qed + also have "\ = integral S (\T. \det (matrix (g' T))\ * + (\y\range (h n). y * indicat_real {x. h n x = y} (g T)))" + by (simp add: sum_distrib_left mult.assoc) + also have "\ = ?rhs" + by (metis hn_eq) + finally show "integral (g ` S) (h n) \ ?rhs" . + qed + qed + have le: "integral S (\T. \det (matrix (g' T))\ * h n (g T)) \ ?b" for n + proof (rule integral_le) + show "(\T. \det (matrix (g' T))\ * h n (g T)) integrable_on S" + proof (rule measurable_bounded_by_integrable_imp_integrable) + have "(\T. \det (matrix (g' T))\ *\<^sub>R h n (g T)) \ borel_measurable (lebesgue_on S)" + proof (intro borel_measurable_scaleR borel_measurable_abs borel_measurable_det_Jacobian \S \ sets lebesgue\) + have eq: "{x \ S. f x \ a} = (\b \ (f ` S) \ atMost a. {x. f x = b} \ S)" for f and a::real + by auto + have "finite ((\x. h n (g x)) ` S \ {..a})" for a + by (force intro: finite_subset [OF _ fin_R]) + with h_lmeas [of n] show "(\x. h n (g x)) \ borel_measurable (lebesgue_on S)" + apply (simp add: borel_measurable_vimage_halfspace_component_le \S \ sets lebesgue\ sets_restrict_space_iff eq) + by (metis (mono_tags) SUP_inf sets.finite_UN) + qed (use der_g in blast) + then show "(\T. \det (matrix (g' T))\ * h n (g T)) \ borel_measurable (lebesgue_on S)" + by simp + show "norm (?D x * h n (g x)) \ ?D x *\<^sub>R f (g x)" + if "x \ S" for x + by (simp add: h_le_f mult_left_mono nonneg_h that) + qed (use S det_int_fg in auto) + show "?D x * h n (g x) \ ?D x * f (g x)" if "x \ S" for x + by (simp add: \x \ S\ h_le_f mult_left_mono) + show "(\x. ?D x * f (g x)) integrable_on S" + using det_int_fg by blast + qed + have "f integrable_on g ` S \ (\k. integral (g ` S) (h k)) \ integral (g ` S) f" + proof (rule monotone_convergence_increasing) + have "\integral (g ` S) (h n)\ \ integral S (\x. ?D x * f (g x))" for n + proof - + have "\integral (g ` S) (h n)\ = integral (g ` S) (h n)" + using hint by (simp add: integral_nonneg nonneg_h) + also have "\ \ integral S (\x. ?D x * f (g x))" + using hint le by (meson order_trans) + finally show ?thesis . + qed + then show "bounded (range (\k. integral (g ` S) (h k)))" + by (force simp: bounded_iff) + qed (use h_inc lim hint in auto) + moreover have "integral (g ` S) (h n) \ integral S (\x. ?D x * f (g x))" for n + using hint by (blast intro: le order_trans) + ultimately show ?thesis + by (auto intro: Lim_bounded_ereal) +qed + + +lemma integral_on_image_ubound_nonneg: + fixes f :: "real^'n::{finite,wellorder} \ real" + assumes nonneg_fg: "\x. x \ S \ 0 \ f(g x)" + and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and intS: "(\x. \det (matrix (g' x))\ * f(g x)) integrable_on S" + shows "f integrable_on (g ` S) \ integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" + (is "_ \ _ \ ?b") +proof - + let ?D = "\x. det (matrix (g' x))" + define S' where "S' \ {x \ S. ?D x * f(g x) \ 0}" + then have der_gS': "\x. x \ S' \ (g has_derivative g' x) (at x within S')" + by (metis (mono_tags, lifting) der_g has_derivative_within_subset mem_Collect_eq subset_iff) + have "(\x. if x \ S then \?D x\ * f (g x) else 0) integrable_on UNIV" + by (simp add: integrable_restrict_UNIV intS) + then have Df_borel: "(\x. if x \ S then \?D x\ * f (g x) else 0) \ borel_measurable lebesgue" + using integrable_imp_measurable borel_measurable_UNIV_eq by blast + have S': "S' \ sets lebesgue" + proof - + from Df_borel borel_measurable_vimage_open [of _ UNIV] + have "{x. (if x \ S then \?D x\ * f (g x) else 0) \ T} \ sets lebesgue" + if "open T" for T + using that unfolding borel_measurable_UNIV_eq + by (fastforce simp add: dest!: spec) + then have "{x. (if x \ S then \?D x\ * f (g x) else 0) \ -{0}} \ sets lebesgue" + using open_Compl by blast + then show ?thesis + by (simp add: S'_def conj_ac split: if_split_asm cong: conj_cong) + qed + then have gS': "g ` S' \ sets lebesgue" + proof (rule differentiable_image_in_sets_lebesgue) + show "g differentiable_on S'" + using der_g unfolding S'_def differentiable_def differentiable_on_def + by (blast intro: has_derivative_within_subset) + qed auto + have f: "f \ borel_measurable (lebesgue_on (g ` S'))" + proof (clarsimp simp add: borel_measurable_vimage_open) + fix T :: "real set" + assume "open T" + have "{x \ g ` S'. f x \ T} = g ` {x \ S'. f(g x) \ T}" + by blast + moreover have "g ` {x \ S'. f(g x) \ T} \ sets lebesgue" + proof (rule differentiable_image_in_sets_lebesgue) + let ?h = "\x. \?D x\ * f (g x) /\<^sub>R \?D x\" + have "(\x. if x \ S' then \?D x\ * f (g x) else 0) = (\x. if x \ S then \?D x\ * f (g x) else 0)" + by (auto simp: S'_def) + also have "\ \ borel_measurable lebesgue" + by (rule Df_borel) + finally have *: "(\x. \?D x\ * f (g x)) \ borel_measurable (lebesgue_on S')" + by (simp add: borel_measurable_If_D) + have "?h \ borel_measurable (lebesgue_on S')" + by (intro * S' der_gS' borel_measurable_det_Jacobian measurable) (blast intro: der_gS') + moreover have "?h x = f(g x)" if "x \ S'" for x + using that by (auto simp: S'_def) + ultimately have "(\x. f(g x)) \ borel_measurable (lebesgue_on S')" + by (metis (no_types, lifting) measurable_lebesgue_cong) + then show "{x \ S'. f (g x) \ T} \ sets lebesgue" + by (simp add: \S' \ sets lebesgue\ \open T\ borel_measurable_vimage_open sets_restrict_space_iff) + show "g differentiable_on {x \ S'. f (g x) \ T}" + using der_g unfolding S'_def differentiable_def differentiable_on_def + by (blast intro: has_derivative_within_subset) + qed auto + ultimately have "{x \ g ` S'. f x \ T} \ sets lebesgue" + by metis + then show "{x \ g ` S'. f x \ T} \ sets (lebesgue_on (g ` S'))" + by (simp add: \g ` S' \ sets lebesgue\ sets_restrict_space_iff) + qed + have intS': "(\x. \?D x\ * f (g x)) integrable_on S'" + using intS + by (rule integrable_spike_set) (auto simp: S'_def intro: empty_imp_negligible) + have lebS': "{x \ S'. g x \ T} \ sets lebesgue" if "T \ g ` S'" "T \ sets lebesgue" for T + proof - + have "g \ borel_measurable (lebesgue_on S')" + using der_gS' has_derivative_continuous_on S' + by (blast intro: continuous_imp_measurable_on_sets_lebesgue) + moreover have "{x \ S'. g x \ U} \ sets lebesgue" if "negligible U" "U \ g ` S'" for U + proof (intro negligible_imp_sets negligible_differentiable_vimage that) + fix x + assume x: "x \ S'" + then have "linear (g' x)" + using der_gS' has_derivative_linear by blast + with x show "inj (g' x)" + by (auto simp: S'_def det_nz_iff_inj) + qed (use der_gS' in auto) + ultimately show ?thesis + using double_lebesgue_sets [OF S' gS' order_refl] that by blast + qed + have int_gS': "f integrable_on g ` S' \ integral (g ` S') f \ integral S' (\x. \?D x\ * f(g x))" + using integral_on_image_ubound_weak [OF S' f nonneg_fg der_gS' intS' lebS'] S'_def by blast + have "negligible (g ` {x \ S. det(matrix(g' x)) = 0})" + proof (rule baby_Sard, simp_all) + fix x + assume x: "x \ S \ det (matrix (g' x)) = 0" + then show "(g has_derivative g' x) (at x within {x \ S. det (matrix (g' x)) = 0})" + by (metis (no_types, lifting) der_g has_derivative_within_subset mem_Collect_eq subsetI) + then show "rank (matrix (g' x)) < CARD('n)" + using det_nz_iff_inj matrix_vector_mul_linear x + by (fastforce simp add: less_rank_noninjective) + qed + then have negg: "negligible (g ` S - g ` {x \ S. ?D x \ 0})" + by (rule negligible_subset) (auto simp: S'_def) + have null: "g ` {x \ S. ?D x \ 0} - g ` S = {}" + by (auto simp: S'_def) + let ?F = "{x \ S. f (g x) \ 0}" + have eq: "g ` S' = g ` ?F \ g ` {x \ S. ?D x \ 0}" + by (auto simp: S'_def image_iff) + show ?thesis + proof + have "((\x. if x \ g ` ?F then f x else 0) integrable_on g ` {x \ S. ?D x \ 0})" + using int_gS' eq integrable_restrict_Int [where f=f] + by simp + then have "f integrable_on g ` {x \ S. ?D x \ 0}" + by (auto simp: image_iff elim!: integrable_eq) + then show "f integrable_on g ` S" + apply (rule integrable_spike_set [OF _ empty_imp_negligible negligible_subset]) + using negg null by auto + have "integral (g ` S) f = integral (g ` {x \ S. ?D x \ 0}) f" + using negg by (auto intro: negligible_subset integral_spike_set) + also have "\ = integral (g ` {x \ S. ?D x \ 0}) (\x. if x \ g ` ?F then f x else 0)" + by (auto simp: image_iff intro!: integral_cong) + also have "\ = integral (g ` S') f" + using eq integral_restrict_Int by simp + also have "\ \ integral S' (\x. \?D x\ * f(g x))" + by (metis int_gS') + also have "\ \ ?b" + by (rule integral_subset_le [OF _ intS' intS]) (use nonneg_fg S'_def in auto) + finally show "integral (g ` S) f \ ?b" . + qed +qed + + + +lemma absolutely_integrable_on_image_real: + fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and intS: "(\x. \det (matrix (g' x))\ * f(g x)) absolutely_integrable_on S" + shows "f absolutely_integrable_on (g ` S)" +proof - + let ?D = "\x. \det (matrix (g' x))\ * f (g x)" + let ?N = "{x \ S. f (g x) < 0}" and ?P = "{x \ S. f (g x) > 0}" + have eq: "{x. (if x \ S then ?D x else 0) > 0} = {x \ S. ?D x > 0}" + "{x. (if x \ S then ?D x else 0) < 0} = {x \ S. ?D x < 0}" + by auto + have "?D integrable_on S" + using intS absolutely_integrable_on_def by blast + then have "(\x. if x \ S then ?D x else 0) integrable_on UNIV" + by (simp add: integrable_restrict_UNIV) + then have D_borel: "(\x. if x \ S then ?D x else 0) \ borel_measurable (lebesgue_on UNIV)" + using integrable_imp_measurable borel_measurable_UNIV_eq by blast + then have Dlt: "{x \ S. ?D x < 0} \ sets lebesgue" + unfolding borel_measurable_vimage_halfspace_component_lt + by (drule_tac x=0 in spec) (auto simp: eq) + from D_borel have Dgt: "{x \ S. ?D x > 0} \ sets lebesgue" + unfolding borel_measurable_vimage_halfspace_component_gt + by (drule_tac x=0 in spec) (auto simp: eq) + + have dfgbm: "?D \ borel_measurable (lebesgue_on S)" + using intS absolutely_integrable_on_def integrable_imp_measurable by blast + have der_gN: "(g has_derivative g' x) (at x within ?N)" if "x \ ?N" for x + using der_g has_derivative_within_subset that by force + have "(\x. - f x) integrable_on g ` ?N \ + integral (g ` ?N) (\x. - f x) \ integral ?N (\x. \det (matrix (g' x))\ * - f (g x))" + proof (rule integral_on_image_ubound_nonneg [OF _ der_gN]) + have 1: "?D integrable_on {x \ S. ?D x < 0}" + using Dlt + by (auto intro: set_lebesgue_integral_eq_integral [OF set_integrable_subset] intS) + have "uminus \ (\x. \det (matrix (g' x))\ * - f (g x)) integrable_on ?N" + by (simp add: o_def mult_less_0_iff empty_imp_negligible integrable_spike_set [OF 1]) + then show "(\x. \det (matrix (g' x))\ * - f (g x)) integrable_on ?N" + by (simp add: integrable_neg_iff o_def) + qed auto + then have "f integrable_on g ` ?N" + by (simp add: integrable_neg_iff) + moreover have "g ` ?N = {y \ g ` S. f y < 0}" + by auto + ultimately have "f integrable_on {y \ g ` S. f y < 0}" + by simp + then have N: "f absolutely_integrable_on {y \ g ` S. f y < 0}" + by (rule absolutely_integrable_absolutely_integrable_ubound) auto + + have der_gP: "(g has_derivative g' x) (at x within ?P)" if "x \ ?P" for x + using der_g has_derivative_within_subset that by force + have "f integrable_on g ` ?P \ integral (g ` ?P) f \ integral ?P ?D" + proof (rule integral_on_image_ubound_nonneg [OF _ der_gP]) + have "?D integrable_on {x \ S. 0 < ?D x}" + using Dgt + by (auto intro: set_lebesgue_integral_eq_integral [OF set_integrable_subset] intS) + then show "?D integrable_on ?P" + apply (rule integrable_spike_set) + by (auto simp: zero_less_mult_iff empty_imp_negligible) + qed auto + then have "f integrable_on g ` ?P" + by metis + moreover have "g ` ?P = {y \ g ` S. f y > 0}" + by auto + ultimately have "f integrable_on {y \ g ` S. f y > 0}" + by simp + then have P: "f absolutely_integrable_on {y \ g ` S. f y > 0}" + by (rule absolutely_integrable_absolutely_integrable_lbound) auto + have "(\x. if x \ g ` S \ f x < 0 \ x \ g ` S \ 0 < f x then f x else 0) = (\x. if x \ g ` S then f x else 0)" + by auto + then show ?thesis + using absolutely_integrable_Un [OF N P] absolutely_integrable_restrict_UNIV [symmetric, where f=f] + by simp +qed + + +proposition absolutely_integrable_on_image: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and intS: "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S" + shows "f absolutely_integrable_on (g ` S)" + apply (rule absolutely_integrable_componentwise [OF absolutely_integrable_on_image_real [OF der_g]]) + using absolutely_integrable_component [OF intS] by auto + +proposition integral_on_image_ubound: + fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" + assumes"\x. x \ S \ 0 \ f(g x)" + and "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and "(\x. \det (matrix (g' x))\ * f(g x)) integrable_on S" + shows "integral (g ` S) f \ integral S (\x. \det (matrix (g' x))\ * f(g x))" + using integral_on_image_ubound_nonneg [OF assms] by simp + + + +subsection\Change-of-variables theorem\ + +text\The classic change-of-variables theorem. We have two versions with quite general hypotheses, +the first that the transforming function has a continuous inverse, the second that the base set is +Lebesgue measurable.\ +lemma cov_invertible_nonneg_le: + fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and der_h: "\y. y \ T \ (h has_derivative h' y) (at y within T)" + and f0: "\y. y \ T \ 0 \ f y" + and hg: "\x. x \ S \ g x \ T \ h(g x) = x" + and gh: "\y. y \ T \ h y \ S \ g(h y) = y" + and id: "\y. y \ T \ h' y \ g'(h y) = id" + shows "f integrable_on T \ (integral T f) \ b \ + (\x. \det (matrix (g' x))\ * f(g x)) integrable_on S \ + integral S (\x. \det (matrix (g' x))\ * f(g x)) \ b" + (is "?lhs = ?rhs") +proof - + have Teq: "T = g`S" and Seq: "S = h`T" + using hg gh image_iff by fastforce+ + have gS: "g differentiable_on S" + by (meson der_g differentiable_def differentiable_on_def) + let ?D = "\x. \det (matrix (g' x))\ * f (g x)" + show ?thesis + proof + assume ?lhs + then have fT: "f integrable_on T" and intf: "integral T f \ b" + by blast+ + show ?rhs + proof + let ?fgh = "\x. \det (matrix (h' x))\ * (\det (matrix (g' (h x)))\ * f (g (h x)))" + have ddf: "?fgh x = f x" + if "x \ T" for x + proof - + have "matrix (h' x) ** matrix (g' (h x)) = mat 1" + using that id matrix_compose + by (metis der_g gh has_derivative_linear left_inverse_linear matrix_id_mat_1) + then have "\det (matrix (h' x))\ * \det (matrix (g' (h x)))\ = 1" + by (metis abs_1 abs_mult det_I det_mul) + then show ?thesis + by (simp add: gh that) + qed + have "?D integrable_on (h ` T)" + proof (intro set_lebesgue_integral_eq_integral absolutely_integrable_on_image_real) + show "(\x. ?fgh x) absolutely_integrable_on T" + proof (subst absolutely_integrable_on_iff_nonneg) + show "(\x. ?fgh x) integrable_on T" + using ddf fT integrable_eq by force + qed (simp add: zero_le_mult_iff f0 gh) + qed (use der_h in auto) + with Seq show "(\x. ?D x) integrable_on S" + by simp + have "integral S (\x. ?D x) \ integral T (\x. ?fgh x)" + unfolding Seq + proof (rule integral_on_image_ubound) + show "(\x. ?fgh x) integrable_on T" + using ddf fT integrable_eq by force + qed (use f0 gh der_h in auto) + also have "\ = integral T f" + by (force simp: ddf intro: integral_cong) + also have "\ \ b" + by (rule intf) + finally show "integral S (\x. ?D x) \ b" . + qed + next + assume R: ?rhs + then have "f integrable_on g ` S" + using der_g f0 hg integral_on_image_ubound_nonneg by blast + moreover have "integral (g ` S) f \ integral S (\x. ?D x)" + by (rule integral_on_image_ubound [OF f0 der_g]) (use R Teq in auto) + ultimately show ?lhs + using R by (simp add: Teq) + qed +qed + + +lemma cov_invertible_nonneg_eq: + fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" + assumes "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and "\y. y \ T \ (h has_derivative h' y) (at y within T)" + and "\y. y \ T \ 0 \ f y" + and "\x. x \ S \ g x \ T \ h(g x) = x" + and "\y. y \ T \ h y \ S \ g(h y) = y" + and "\y. y \ T \ h' y \ g'(h y) = id" + shows "((\x. \det (matrix (g' x))\ * f(g x)) has_integral b) S \ (f has_integral b) T" + using cov_invertible_nonneg_le [OF assms] + by (simp add: has_integral_iff) (meson eq_iff) + + +lemma cov_invertible_real: + fixes f :: "real^'n::{finite,wellorder} \ real" and g :: "real^'n::_ \ real^'n::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and der_h: "\y. y \ T \ (h has_derivative h' y) (at y within T)" + and hg: "\x. x \ S \ g x \ T \ h(g x) = x" + and gh: "\y. y \ T \ h y \ S \ g(h y) = y" + and id: "\y. y \ T \ h' y \ g'(h y) = id" + shows "(\x. \det (matrix (g' x))\ * f(g x)) absolutely_integrable_on S \ + integral S (\x. \det (matrix (g' x))\ * f(g x)) = b \ + f absolutely_integrable_on T \ integral T f = b" + (is "?lhs = ?rhs") +proof - + have Teq: "T = g`S" and Seq: "S = h`T" + using hg gh image_iff by fastforce+ + let ?DP = "\x. \det (matrix (g' x))\ * f(g x)" and ?DN = "\x. \det (matrix (g' x))\ * -f(g x)" + have "+": "(?DP has_integral b) {x \ S. f (g x) > 0} \ (f has_integral b) {y \ T. f y > 0}" for b + proof (rule cov_invertible_nonneg_eq) + have *: "(\x. f (g x)) -` Y \ {x \ S. f (g x) > 0} + = ((\x. f (g x)) -` Y \ S) \ {x \ S. f (g x) > 0}" for Y + by auto + show "(g has_derivative g' x) (at x within {x \ S. f (g x) > 0})" if "x \ {x \ S. f (g x) > 0}" for x + using that der_g has_derivative_within_subset by fastforce + show "(h has_derivative h' y) (at y within {y \ T. f y > 0})" if "y \ {y \ T. f y > 0}" for y + using that der_h has_derivative_within_subset by fastforce + qed (use gh hg id in auto) + have "-": "(?DN has_integral b) {x \ S. f (g x) < 0} \ ((\x. - f x) has_integral b) {y \ T. f y < 0}" for b + proof (rule cov_invertible_nonneg_eq) + have *: "(\x. - f (g x)) -` y \ {x \ S. f (g x) < 0} + = ((\x. f (g x)) -` uminus ` y \ S) \ {x \ S. f (g x) < 0}" for y + using image_iff by fastforce + show "(g has_derivative g' x) (at x within {x \ S. f (g x) < 0})" if "x \ {x \ S. f (g x) < 0}" for x + using that der_g has_derivative_within_subset by fastforce + show "(h has_derivative h' y) (at y within {y \ T. f y < 0})" if "y \ {y \ T. f y < 0}" for y + using that der_h has_derivative_within_subset by fastforce + qed (use gh hg id in auto) + show ?thesis + proof + assume LHS: ?lhs + have eq: "{x. (if x \ S then ?DP x else 0) > 0} = {x \ S. ?DP x > 0}" + "{x. (if x \ S then ?DP x else 0) < 0} = {x \ S. ?DP x < 0}" + by auto + have "?DP integrable_on S" + using LHS absolutely_integrable_on_def by blast + then have "(\x. if x \ S then ?DP x else 0) integrable_on UNIV" + by (simp add: integrable_restrict_UNIV) + then have D_borel: "(\x. if x \ S then ?DP x else 0) \ borel_measurable (lebesgue_on UNIV)" + using integrable_imp_measurable borel_measurable_UNIV_eq by blast + then have SN: "{x \ S. ?DP x < 0} \ sets lebesgue" + unfolding borel_measurable_vimage_halfspace_component_lt + by (drule_tac x=0 in spec) (auto simp: eq) + from D_borel have SP: "{x \ S. ?DP x > 0} \ sets lebesgue" + unfolding borel_measurable_vimage_halfspace_component_gt + by (drule_tac x=0 in spec) (auto simp: eq) + have "?DP absolutely_integrable_on {x \ S. ?DP x > 0}" + using LHS by (fast intro!: set_integrable_subset [OF _, of _ S] SP) + then have aP: "?DP absolutely_integrable_on {x \ S. f (g x) > 0}" + by (rule absolutely_integrable_spike_set) (auto simp: zero_less_mult_iff empty_imp_negligible) + have "?DP absolutely_integrable_on {x \ S. ?DP x < 0}" + using LHS by (fast intro!: set_integrable_subset [OF _, of _ S] SN) + then have aN: "?DP absolutely_integrable_on {x \ S. f (g x) < 0}" + by (rule absolutely_integrable_spike_set) (auto simp: mult_less_0_iff empty_imp_negligible) + have fN: "f integrable_on {y \ T. f y < 0}" + "integral {y \ T. f y < 0} f = integral {x \ S. f (g x) < 0} ?DP" + using "-" [of "integral {x \ S. f(g x) < 0} ?DN"] aN + by (auto simp: set_lebesgue_integral_eq_integral has_integral_iff integrable_neg_iff) + have faN: "f absolutely_integrable_on {y \ T. f y < 0}" + apply (rule absolutely_integrable_integrable_bound [where g = "\x. - f x"]) + using fN by (auto simp: integrable_neg_iff) + have fP: "f integrable_on {y \ T. f y > 0}" + "integral {y \ T. f y > 0} f = integral {x \ S. f (g x) > 0} ?DP" + using "+" [of "integral {x \ S. f(g x) > 0} ?DP"] aP + by (auto simp: set_lebesgue_integral_eq_integral has_integral_iff integrable_neg_iff) + have faP: "f absolutely_integrable_on {y \ T. f y > 0}" + apply (rule absolutely_integrable_integrable_bound [where g = f]) + using fP by auto + have fa: "f absolutely_integrable_on ({y \ T. f y < 0} \ {y \ T. f y > 0})" + by (rule absolutely_integrable_Un [OF faN faP]) + show ?rhs + proof + have eq: "((if x \ T \ f x < 0 \ x \ T \ 0 < f x then 1 else 0) * f x) + = (if x \ T then 1 else 0) * f x" for x + by auto + show "f absolutely_integrable_on T" + using fa by (simp add: indicator_def set_integrable_def eq) + have [simp]: "{y \ T. f y < 0} \ {y \ T. 0 < f y} = {}" for T and f :: "(real^'n::_) \ real" + by auto + have "integral T f = integral ({y \ T. f y < 0} \ {y \ T. f y > 0}) f" + by (intro empty_imp_negligible integral_spike_set) (auto simp: eq) + also have "\ = integral {y \ T. f y < 0} f + integral {y \ T. f y > 0} f" + using fN fP by simp + also have "\ = integral {x \ S. f (g x) < 0} ?DP + integral {x \ S. 0 < f (g x)} ?DP" + by (simp add: fN fP) + also have "\ = integral ({x \ S. f (g x) < 0} \ {x \ S. 0 < f (g x)}) ?DP" + using aP aN by (simp add: set_lebesgue_integral_eq_integral) + also have "\ = integral S ?DP" + by (intro empty_imp_negligible integral_spike_set) auto + also have "\ = b" + using LHS by simp + finally show "integral T f = b" . + qed + next + assume RHS: ?rhs + have eq: "{x. (if x \ T then f x else 0) > 0} = {x \ T. f x > 0}" + "{x. (if x \ T then f x else 0) < 0} = {x \ T. f x < 0}" + by auto + have "f integrable_on T" + using RHS absolutely_integrable_on_def by blast + then have "(\x. if x \ T then f x else 0) integrable_on UNIV" + by (simp add: integrable_restrict_UNIV) + then have D_borel: "(\x. if x \ T then f x else 0) \ borel_measurable (lebesgue_on UNIV)" + using integrable_imp_measurable borel_measurable_UNIV_eq by blast + then have TN: "{x \ T. f x < 0} \ sets lebesgue" + unfolding borel_measurable_vimage_halfspace_component_lt + by (drule_tac x=0 in spec) (auto simp: eq) + from D_borel have TP: "{x \ T. f x > 0} \ sets lebesgue" + unfolding borel_measurable_vimage_halfspace_component_gt + by (drule_tac x=0 in spec) (auto simp: eq) + have aint: "f absolutely_integrable_on {y. y \ T \ 0 < (f y)}" + "f absolutely_integrable_on {y. y \ T \ (f y) < 0}" + and intT: "integral T f = b" + using set_integrable_subset [of _ T] TP TN RHS + by blast+ + show ?lhs + proof + have fN: "f integrable_on {v \ T. f v < 0}" + using absolutely_integrable_on_def aint by blast + then have DN: "(?DN has_integral integral {y \ T. f y < 0} (\x. - f x)) {x \ S. f (g x) < 0}" + using "-" [of "integral {y \ T. f y < 0} (\x. - f x)"] + by (simp add: has_integral_neg_iff integrable_integral) + have aDN: "?DP absolutely_integrable_on {x \ S. f (g x) < 0}" + apply (rule absolutely_integrable_integrable_bound [where g = ?DN]) + using DN hg by (fastforce simp: abs_mult integrable_neg_iff)+ + have fP: "f integrable_on {v \ T. f v > 0}" + using absolutely_integrable_on_def aint by blast + then have DP: "(?DP has_integral integral {y \ T. f y > 0} f) {x \ S. f (g x) > 0}" + using "+" [of "integral {y \ T. f y > 0} f"] + by (simp add: has_integral_neg_iff integrable_integral) + have aDP: "?DP absolutely_integrable_on {x \ S. f (g x) > 0}" + apply (rule absolutely_integrable_integrable_bound [where g = ?DP]) + using DP hg by (fastforce simp: integrable_neg_iff)+ + have eq: "(if x \ S then 1 else 0) * ?DP x = (if x \ S \ f (g x) < 0 \ x \ S \ f (g x) > 0 then 1 else 0) * ?DP x" for x + by force + have "?DP absolutely_integrable_on ({x \ S. f (g x) < 0} \ {x \ S. f (g x) > 0})" + by (rule absolutely_integrable_Un [OF aDN aDP]) + then show I: "?DP absolutely_integrable_on S" + by (simp add: indicator_def eq set_integrable_def) + have [simp]: "{y \ S. f y < 0} \ {y \ S. 0 < f y} = {}" for S and f :: "(real^'n::_) \ real" + by auto + have "integral S ?DP = integral ({x \ S. f (g x) < 0} \ {x \ S. f (g x) > 0}) ?DP" + by (intro empty_imp_negligible integral_spike_set) auto + also have "\ = integral {x \ S. f (g x) < 0} ?DP + integral {x \ S. 0 < f (g x)} ?DP" + using aDN aDP by (simp add: set_lebesgue_integral_eq_integral) + also have "\ = - integral {y \ T. f y < 0} (\x. - f x) + integral {y \ T. f y > 0} f" + using DN DP by (auto simp: has_integral_iff) + also have "\ = integral ({x \ T. f x < 0} \ {x \ T. 0 < f x}) f" + by (simp add: fN fP) + also have "\ = integral T f" + by (intro empty_imp_negligible integral_spike_set) auto + also have "\ = b" + using intT by simp + finally show "integral S ?DP = b" . + qed + qed +qed + + +lemma cv_inv_version3: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and der_h: "\y. y \ T \ (h has_derivative h' y) (at y within T)" + and hg: "\x. x \ S \ g x \ T \ h(g x) = x" + and gh: "\y. y \ T \ h y \ S \ g(h y) = y" + and id: "\y. y \ T \ h' y \ g'(h y) = id" + shows "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ + integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on T \ integral T f = b" +proof - + let ?D = "\x. \det (matrix (g' x))\ *\<^sub>R f(g x)" + have "((\x. \det (matrix (g' x))\ * f(g x) $ i) absolutely_integrable_on S \ integral S (\x. \det (matrix (g' x))\ * (f(g x) $ i)) = b $ i) \ + ((\x. f x $ i) absolutely_integrable_on T \ integral T (\x. f x $ i) = b $ i)" for i + by (rule cov_invertible_real [OF der_g der_h hg gh id]) + then have "?D absolutely_integrable_on S \ (?D has_integral b) S \ + f absolutely_integrable_on T \ (f has_integral b) T" + unfolding absolutely_integrable_componentwise_iff [where f=f] has_integral_componentwise_iff [of f] + absolutely_integrable_componentwise_iff [where f="?D"] has_integral_componentwise_iff [of ?D] + by (auto simp: all_conj_distrib Basis_vec_def cart_eq_inner_axis [symmetric] + has_integral_iff set_lebesgue_integral_eq_integral) + then show ?thesis + using absolutely_integrable_on_def by blast +qed + + +lemma cv_inv_version4: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S) \ invertible(matrix(g' x))" + and hg: "\x. x \ S \ continuous_on (g ` S) h \ h(g x) = x" + shows "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ + integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" +proof - + have "\x. \h'. x \ S + \ (g has_derivative g' x) (at x within S) \ linear h' \ g' x \ h' = id \ h' \ g' x = id" + using der_g matrix_invertible has_derivative_linear by blast + then obtain h' where h': + "\x. x \ S + \ (g has_derivative g' x) (at x within S) \ + linear (h' x) \ g' x \ (h' x) = id \ (h' x) \ g' x = id" + by metis + show ?thesis + proof (rule cv_inv_version3) + show "\y. y \ g ` S \ (h has_derivative h' (h y)) (at y within g ` S)" + using h' hg + by (force simp: continuous_on_eq_continuous_within intro!: has_derivative_inverse_within) + qed (use h' hg in auto) +qed + + +proposition has_absolute_integral_change_of_variables_invertible: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and hg: "\x. x \ S \ h(g x) = x" + and conth: "continuous_on (g ` S) h" + shows "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b \ + f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" + (is "?lhs = ?rhs") +proof - + let ?S = "{x \ S. invertible (matrix (g' x))}" and ?D = "\x. \det (matrix (g' x))\ *\<^sub>R f(g x)" + have *: "?D absolutely_integrable_on ?S \ integral ?S ?D = b + \ f absolutely_integrable_on (g ` ?S) \ integral (g ` ?S) f = b" + proof (rule cv_inv_version4) + show "(g has_derivative g' x) (at x within ?S) \ invertible (matrix (g' x))" + if "x \ ?S" for x + using der_g that has_derivative_within_subset that by fastforce + show "continuous_on (g ` ?S) h \ h (g x) = x" + if "x \ ?S" for x + using that continuous_on_subset [OF conth] by (simp add: hg image_mono) + qed + have "(g has_derivative g' x) (at x within {x \ S. rank (matrix (g' x)) < CARD('m)})" if "x \ S" for x + by (metis (no_types, lifting) der_g has_derivative_within_subset mem_Collect_eq subsetI that) + then have "negligible (g ` {x \ S. \ invertible (matrix (g' x))})" + by (auto simp: invertible_det_nz det_eq_0_rank intro: baby_Sard) + then have neg: "negligible {x \ g ` S. x \ g ` ?S \ f x \ 0}" + by (auto intro: negligible_subset) + have [simp]: "{x \ g ` ?S. x \ g ` S \ f x \ 0} = {}" + by auto + have "?D absolutely_integrable_on ?S \ integral ?S ?D = b + \ ?D absolutely_integrable_on S \ integral S ?D = b" + apply (intro conj_cong absolutely_integrable_spike_set_eq) + apply(auto simp: integral_spike_set invertible_det_nz empty_imp_negligible neg) + done + moreover + have "f absolutely_integrable_on (g ` ?S) \ integral (g ` ?S) f = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" + by (auto intro!: conj_cong absolutely_integrable_spike_set_eq integral_spike_set neg) + ultimately + show ?thesis + using "*" by blast +qed + + + +lemma has_absolute_integral_change_of_variables_compact: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes "compact S" + and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and inj: "inj_on g S" + shows "((\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ + integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b)" +proof - + obtain h where hg: "\x. x \ S \ h(g x) = x" + using inj by (metis the_inv_into_f_f) + have conth: "continuous_on (g ` S) h" + by (metis \compact S\ continuous_on_inv der_g has_derivative_continuous_on hg) + show ?thesis + by (rule has_absolute_integral_change_of_variables_invertible [OF der_g hg conth]) +qed + + +lemma has_absolute_integral_change_of_variables_compact_family: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes compact: "\n::nat. compact (F n)" + and der_g: "\x. x \ (\n. F n) \ (g has_derivative g' x) (at x within (\n. F n))" + and inj: "inj_on g (\n. F n)" + shows "((\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on (\n. F n) \ + integral (\n. F n) (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on (g ` (\n. F n)) \ integral (g ` (\n. F n)) f = b)" +proof - + let ?D = "\x. \det (matrix (g' x))\ *\<^sub>R f (g x)" + let ?U = "\n. \m\n. F m" + let ?lift = "vec::real\real^1" + have F_leb: "F m \ sets lebesgue" for m + by (simp add: compact borel_compact) + have iff: "(\x. \det (matrix (g' x))\ *\<^sub>R f (g x)) absolutely_integrable_on (?U n) \ + integral (?U n) (\x. \det (matrix (g' x))\ *\<^sub>R f (g x)) = b + \ f absolutely_integrable_on (g ` (?U n)) \ integral (g ` (?U n)) f = b" for n b and f :: "real^'m::_ \ real^'k" + proof (rule has_absolute_integral_change_of_variables_compact) + show "compact (?U n)" + by (simp add: compact compact_UN) + show "(g has_derivative g' x) (at x within (?U n))" + if "x \ ?U n" for x + using that by (blast intro!: has_derivative_within_subset [OF der_g]) + show "inj_on g (?U n)" + using inj by (auto simp: inj_on_def) + qed + show ?thesis + unfolding image_UN + proof safe + assume DS: "?D absolutely_integrable_on (\n. F n)" + and b: "b = integral (\n. F n) ?D" + have DU: "\n. ?D absolutely_integrable_on (?U n)" + "(\n. integral (?U n) ?D) \ integral (\n. F n) ?D" + using integral_countable_UN [OF DS F_leb] by auto + with iff have fag: "f absolutely_integrable_on g ` (?U n)" + and fg_int: "integral (\m\n. g ` F m) f = integral (?U n) ?D" for n + by (auto simp: image_UN) + let ?h = "\x. if x \ (\m. g ` F m) then norm(f x) else 0" + have "(\x. if x \ (\m. g ` F m) then f x else 0) absolutely_integrable_on UNIV" + proof (rule dominated_convergence_absolutely_integrable) + show "(\x. if x \ (\m\k. g ` F m) then f x else 0) absolutely_integrable_on UNIV" for k + unfolding absolutely_integrable_restrict_UNIV + using fag by (simp add: image_UN) + let ?nf = "\n x. if x \ (\m\n. g ` F m) then norm(f x) else 0" + show "?h integrable_on UNIV" + proof (rule monotone_convergence_increasing [THEN conjunct1]) + show "?nf k integrable_on UNIV" for k + using fag + unfolding integrable_restrict_UNIV absolutely_integrable_on_def by (simp add: image_UN) + { fix n + have "(norm \ ?D) absolutely_integrable_on ?U n" + by (intro absolutely_integrable_norm DU) + then have "integral (g ` ?U n) (norm \ f) = integral (?U n) (norm \ ?D)" + using iff [of n "vec \ norm \ f" "integral (?U n) (\x. \det (matrix (g' x))\ *\<^sub>R (?lift \ norm \ f) (g x))"] + unfolding absolutely_integrable_on_1_iff integral_on_1_eq by (auto simp: o_def) + } + moreover have "bounded (range (\k. integral (?U k) (norm \ ?D)))" + unfolding bounded_iff + proof (rule exI, clarify) + fix k + show "norm (integral (?U k) (norm \ ?D)) \ integral (\n. F n) (norm \ ?D)" + unfolding integral_restrict_UNIV [of _ "norm \ ?D", symmetric] + proof (rule integral_norm_bound_integral) + show "(\x. if x \ UNION {..k} F then (norm \ ?D) x else 0) integrable_on UNIV" + "(\x. if x \ (\n. F n) then (norm \ ?D) x else 0) integrable_on UNIV" + using DU(1) DS + unfolding absolutely_integrable_on_def o_def integrable_restrict_UNIV by auto + qed auto + qed + ultimately show "bounded (range (\k. integral UNIV (?nf k)))" + by (simp add: integral_restrict_UNIV image_UN [symmetric] o_def) + next + show "(\k. if x \ (\m\k. g ` F m) then norm (f x) else 0) + \ (if x \ (\m. g ` F m) then norm (f x) else 0)" for x + by (force intro: Lim_eventually eventually_sequentiallyI) + qed auto + next + show "(\k. if x \ (\m\k. g ` F m) then f x else 0) + \ (if x \ (\m. g ` F m) then f x else 0)" for x + proof clarsimp + fix m y + assume "y \ F m" + show "(\k. if \x\{..k}. g y \ g ` F x then f (g y) else 0) \ f (g y)" + using \y \ F m\ by (force intro: Lim_eventually eventually_sequentiallyI [of m]) + qed + qed auto + then show fai: "f absolutely_integrable_on (\m. g ` F m)" + using absolutely_integrable_restrict_UNIV by blast + show "integral ((\x. g ` F x)) f = integral (\n. F n) ?D" + proof (rule LIMSEQ_unique) + show "(\n. integral (?U n) ?D) \ integral (\x. g ` F x) f" + unfolding fg_int [symmetric] + proof (rule integral_countable_UN [OF fai]) + show "g ` F m \ sets lebesgue" for m + proof (rule differentiable_image_in_sets_lebesgue [OF F_leb]) + show "g differentiable_on F m" + by (meson der_g differentiableI UnionI differentiable_on_def differentiable_on_subset rangeI subsetI) + qed auto + qed + next + show "(\n. integral (?U n) ?D) \ integral (\n. F n) ?D" + by (rule DU) + qed + next + assume fs: "f absolutely_integrable_on (\x. g ` F x)" + and b: "b = integral ((\x. g ` F x)) f" + have gF_leb: "g ` F m \ sets lebesgue" for m + proof (rule differentiable_image_in_sets_lebesgue [OF F_leb]) + show "g differentiable_on F m" + using der_g unfolding differentiable_def differentiable_on_def + by (meson Sup_upper UNIV_I UnionI has_derivative_within_subset image_eqI) + qed auto + have fgU: "\n. f absolutely_integrable_on (\m\n. g ` F m)" + "(\n. integral (\m\n. g ` F m) f) \ integral (\m. g ` F m) f" + using integral_countable_UN [OF fs gF_leb] by auto + with iff have DUn: "?D absolutely_integrable_on ?U n" + and D_int: "integral (?U n) ?D = integral (\m\n. g ` F m) f" for n + by (auto simp: image_UN) + let ?h = "\x. if x \ (\n. F n) then norm(?D x) else 0" + have "(\x. if x \ (\n. F n) then ?D x else 0) absolutely_integrable_on UNIV" + proof (rule dominated_convergence_absolutely_integrable) + show "(\x. if x \ ?U k then ?D x else 0) absolutely_integrable_on UNIV" for k + unfolding absolutely_integrable_restrict_UNIV using DUn by simp + let ?nD = "\n x. if x \ ?U n then norm(?D x) else 0" + show "?h integrable_on UNIV" + proof (rule monotone_convergence_increasing [THEN conjunct1]) + show "?nD k integrable_on UNIV" for k + using DUn + unfolding integrable_restrict_UNIV absolutely_integrable_on_def by (simp add: image_UN) + { fix n::nat + have "(norm \ f) absolutely_integrable_on (\m\n. g ` F m)" + apply (rule absolutely_integrable_norm) + using fgU by blast + then have "integral (?U n) (norm \ ?D) = integral (g ` ?U n) (norm \ f)" + using iff [of n "?lift \ norm \ f" "integral (g ` ?U n) (?lift \ norm \ f)"] + unfolding absolutely_integrable_on_1_iff integral_on_1_eq image_UN by (auto simp: o_def) + } + moreover have "bounded (range (\k. integral (g ` ?U k) (norm \ f)))" + unfolding bounded_iff + proof (rule exI, clarify) + fix k + show "norm (integral (g ` ?U k) (norm \ f)) \ integral (g ` (\n. F n)) (norm \ f)" + unfolding integral_restrict_UNIV [of _ "norm \ f", symmetric] + proof (rule integral_norm_bound_integral) + show "(\x. if x \ g ` ?U k then (norm \ f) x else 0) integrable_on UNIV" + "(\x. if x \ g ` (\n. F n) then (norm \ f) x else 0) integrable_on UNIV" + using fgU fs + unfolding absolutely_integrable_on_def o_def integrable_restrict_UNIV + by (auto simp: image_UN) + qed auto + qed + ultimately show "bounded (range (\k. integral UNIV (?nD k)))" + unfolding integral_restrict_UNIV image_UN [symmetric] o_def by simp + next + show "(\k. if x \ ?U k then norm (?D x) else 0) \ (if x \ (\n. F n) then norm (?D x) else 0)" for x + by (force intro: Lim_eventually eventually_sequentiallyI) + qed auto + next + show "(\k. if x \ ?U k then ?D x else 0) \ (if x \ (\n. F n) then ?D x else 0)" for x + proof clarsimp + fix n + assume "x \ F n" + show "(\m. if \j\{..m}. x \ F j then ?D x else 0) \ ?D x" + using \x \ F n\ by (auto intro!: Lim_eventually eventually_sequentiallyI [of n]) + qed + qed auto + then show Dai: "?D absolutely_integrable_on (\n. F n)" + unfolding absolutely_integrable_restrict_UNIV by simp + show "integral (\n. F n) ?D = integral ((\x. g ` F x)) f" + proof (rule LIMSEQ_unique) + show "(\n. integral (\m\n. g ` F m) f) \ integral (\x. g ` F x) f" + by (rule fgU) + show "(\n. integral (\m\n. g ` F m) f) \ integral (\n. F n) ?D" + unfolding D_int [symmetric] by (rule integral_countable_UN [OF Dai F_leb]) + qed + qed +qed + + +proposition has_absolute_integral_change_of_variables: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes S: "S \ sets lebesgue" + and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and inj: "inj_on g S" + shows "(\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S \ + integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" +proof - + obtain C N where "fsigma C" "negligible N" and CNS: "C \ N = S" and "disjnt C N" + using lebesgue_set_almost_fsigma [OF S] . + then obtain F :: "nat \ (real^'m::_) set" + where F: "range F \ Collect compact" and Ceq: "C = Union(range F)" + using fsigma_Union_compact by metis + let ?D = "\x. \det (matrix (g' x))\ *\<^sub>R f (g x)" + have "?D absolutely_integrable_on C \ integral C ?D = b + \ f absolutely_integrable_on (g ` C) \ integral (g ` C) f = b" + unfolding Ceq + proof (rule has_absolute_integral_change_of_variables_compact_family) + fix n x + assume "x \ UNION UNIV F" + then show "(g has_derivative g' x) (at x within UNION UNIV F)" + using Ceq \C \ N = S\ der_g has_derivative_within_subset by blast + next + have "UNION UNIV F \ S" + using Ceq \C \ N = S\ by blast + then show "inj_on g (UNION UNIV F)" + using inj by (meson inj_on_subset) + qed (use F in auto) + moreover + have "?D absolutely_integrable_on C \ integral C ?D = b + \ ?D absolutely_integrable_on S \ integral S ?D = b" + proof (rule conj_cong) + have neg: "negligible {x \ C - S. ?D x \ 0}" "negligible {x \ S - C. ?D x \ 0}" + using CNS by (blast intro: negligible_subset [OF \negligible N\])+ + then show "(?D absolutely_integrable_on C) = (?D absolutely_integrable_on S)" + by (rule absolutely_integrable_spike_set_eq) + show "(integral C ?D = b) \ (integral S ?D = b)" + using integral_spike_set [OF neg] by simp + qed + moreover + have "f absolutely_integrable_on (g ` C) \ integral (g ` C) f = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" + proof (rule conj_cong) + have "g differentiable_on N" + by (metis CNS der_g differentiable_def differentiable_on_def differentiable_on_subset sup.cobounded2) + with \negligible N\ + have neg_gN: "negligible (g ` N)" + by (blast intro: negligible_differentiable_image_negligible) + have neg: "negligible {x \ g ` C - g ` S. f x \ 0}" + "negligible {x \ g ` S - g ` C. f x \ 0}" + using CNS by (blast intro: negligible_subset [OF neg_gN])+ + then show "(f absolutely_integrable_on g ` C) = (f absolutely_integrable_on g ` S)" + by (rule absolutely_integrable_spike_set_eq) + show "(integral (g ` C) f = b) \ (integral (g ` S) f = b)" + using integral_spike_set [OF neg] by simp + qed + ultimately show ?thesis + by simp +qed + + +corollary absolutely_integrable_change_of_variables: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes "S \ sets lebesgue" + and "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and "inj_on g S" + shows "f absolutely_integrable_on (g ` S) + \ (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S" + using assms has_absolute_integral_change_of_variables by blast + +corollary integral_change_of_variables: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes S: "S \ sets lebesgue" + and der_g: "\x. x \ S \ (g has_derivative g' x) (at x within S)" + and inj: "inj_on g S" + and disj: "(f absolutely_integrable_on (g ` S) \ + (\x. \det (matrix (g' x))\ *\<^sub>R f(g x)) absolutely_integrable_on S)" + shows "integral (g ` S) f = integral S (\x. \det (matrix (g' x))\ *\<^sub>R f(g x))" + using has_absolute_integral_change_of_variables [OF S der_g inj] disj + by blast + +lemma has_absolute_integral_change_of_variables_1: + fixes f :: "real \ real^'n::{finite,wellorder}" and g :: "real \ real" + assumes S: "S \ sets lebesgue" + and der_g: "\x. x \ S \ (g has_vector_derivative g' x) (at x within S)" + and inj: "inj_on g S" + shows "(\x. \g' x\ *\<^sub>R f(g x)) absolutely_integrable_on S \ + integral S (\x. \g' x\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" +proof - + let ?lift = "vec :: real \ real^1" + let ?drop = "(\x::real^1. x $ 1)" + have S': "?lift ` S \ sets lebesgue" + by (auto intro: differentiable_image_in_sets_lebesgue [OF S] differentiable_vec) + have "((\x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)" + if "z \ S" for z + using der_g [OF that] + by (simp add: has_vector_derivative_def has_derivative_vector_1) + then have der': "\x. x \ ?lift ` S \ + (?lift \ g \ ?drop has_derivative ( *\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)" + by (auto simp: o_def) + have inj': "inj_on (vec \ g \ ?drop) (vec ` S)" + using inj by (simp add: inj_on_def) + let ?fg = "\x. \g' x\ *\<^sub>R f(g x)" + have "((\x. ?fg x $ i) absolutely_integrable_on S \ ((\x. ?fg x $ i) has_integral b $ i) S + \ (\x. f x $ i) absolutely_integrable_on g ` S \ ((\x. f x $ i) has_integral b $ i) (g ` S))" for i + using has_absolute_integral_change_of_variables [OF S' der' inj', of "\x. ?lift(f (?drop x) $ i)" "?lift (b$i)"] + unfolding integrable_on_1_iff integral_on_1_eq absolutely_integrable_on_1_iff absolutely_integrable_drop absolutely_integrable_on_def + by (auto simp: image_comp o_def integral_vec1_eq has_integral_iff) + then have "?fg absolutely_integrable_on S \ (?fg has_integral b) S + \ f absolutely_integrable_on (g ` S) \ (f has_integral b) (g ` S)" + unfolding has_integral_componentwise_iff [where y=b] + absolutely_integrable_componentwise_iff [where f=f] + absolutely_integrable_componentwise_iff [where f = ?fg] + by (force simp: Basis_vec_def cart_eq_inner_axis) + then show ?thesis + using absolutely_integrable_on_def by blast +qed + + +corollary absolutely_integrable_change_of_variables_1: + fixes f :: "real \ real^'n::{finite,wellorder}" and g :: "real \ real" + assumes S: "S \ sets lebesgue" + and der_g: "\x. x \ S \ (g has_vector_derivative g' x) (at x within S)" + and inj: "inj_on g S" + shows "(f absolutely_integrable_on g ` S \ + (\x. \g' x\ *\<^sub>R f(g x)) absolutely_integrable_on S)" + using has_absolute_integral_change_of_variables_1 [OF assms] by auto + + +subsection\Change of variables for integrals: special case of linear function\ + +lemma has_absolute_integral_change_of_variables_linear: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes "linear g" + shows "(\x. \det (matrix g)\ *\<^sub>R f(g x)) absolutely_integrable_on S \ + integral S (\x. \det (matrix g)\ *\<^sub>R f(g x)) = b + \ f absolutely_integrable_on (g ` S) \ integral (g ` S) f = b" +proof (cases "det(matrix g) = 0") + case True + then have "negligible(g ` S)" + using assms det_nz_iff_inj negligible_linear_singular_image by blast + with True show ?thesis + by (auto simp: absolutely_integrable_on_def integrable_negligible integral_negligible) +next + case False + then obtain h where h: "\x. x \ S \ h (g x) = x" "linear h" + using assms det_nz_iff_inj linear_injective_isomorphism by blast + show ?thesis + proof (rule has_absolute_integral_change_of_variables_invertible) + show "(g has_derivative g) (at x within S)" for x + by (simp add: assms linear_imp_has_derivative) + show "continuous_on (g ` S) h" + using continuous_on_eq_continuous_within has_derivative_continuous linear_imp_has_derivative h by blast + qed (use h in auto) +qed + +lemma absolutely_integrable_change_of_variables_linear: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes "linear g" + shows "(\x. \det (matrix g)\ *\<^sub>R f(g x)) absolutely_integrable_on S + \ f absolutely_integrable_on (g ` S)" + using assms has_absolute_integral_change_of_variables_linear by blast + +lemma absolutely_integrable_on_linear_image: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes "linear g" + shows "f absolutely_integrable_on (g ` S) + \ (f \ g) absolutely_integrable_on S \ det(matrix g) = 0" + unfolding assms absolutely_integrable_change_of_variables_linear [OF assms, symmetric] absolutely_integrable_on_scaleR_iff + by (auto simp: set_integrable_def) + +lemma integral_change_of_variables_linear: + fixes f :: "real^'m::{finite,wellorder} \ real^'n" and g :: "real^'m::_ \ real^'m::_" + assumes "linear g" + and "f absolutely_integrable_on (g ` S) \ (f \ g) absolutely_integrable_on S" + shows "integral (g ` S) f = \det (matrix g)\ *\<^sub>R integral S (f \ g)" +proof - + have "((\x. \det (matrix g)\ *\<^sub>R f (g x)) absolutely_integrable_on S) \ (f absolutely_integrable_on g ` S)" + using absolutely_integrable_on_linear_image assms by blast + moreover + have ?thesis if "((\x. \det (matrix g)\ *\<^sub>R f (g x)) absolutely_integrable_on S)" "(f absolutely_integrable_on g ` S)" + using has_absolute_integral_change_of_variables_linear [OF \linear g\] that + by (auto simp: o_def) + ultimately show ?thesis + using absolutely_integrable_change_of_variables_linear [OF \linear g\] + by blast +qed + +subsection\Change of variable for measure\ + +lemma has_measure_differentiable_image: + fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" + assumes "S \ sets lebesgue" + and "\x. x \ S \ (f has_derivative f' x) (at x within S)" + and "inj_on f S" + shows "f ` S \ lmeasurable \ measure lebesgue (f ` S) = m + \ ((\x. \det (matrix (f' x))\) has_integral m) S" + using has_absolute_integral_change_of_variables [OF assms, of "\x. (1::real^1)" "vec m"] + unfolding absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def + by (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral) + +lemma measurable_differentiable_image_eq: + fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" + assumes "S \ sets lebesgue" + and "\x. x \ S \ (f has_derivative f' x) (at x within S)" + and "inj_on f S" + shows "f ` S \ lmeasurable \ (\x. \det (matrix (f' x))\) integrable_on S" + using has_measure_differentiable_image [OF assms] + by blast + +lemma measurable_differentiable_image_alt: + fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" + assumes "S \ sets lebesgue" + and "\x. x \ S \ (f has_derivative f' x) (at x within S)" + and "inj_on f S" + shows "f ` S \ lmeasurable \ (\x. \det (matrix (f' x))\) absolutely_integrable_on S" + using measurable_differentiable_image_eq [OF assms] + by (simp only: absolutely_integrable_on_iff_nonneg) + +lemma measure_differentiable_image_eq: + fixes f :: "real^'n::{finite,wellorder} \ real^'n::_" + assumes S: "S \ sets lebesgue" + and der_f: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + and inj: "inj_on f S" + and intS: "(\x. \det (matrix (f' x))\) integrable_on S" + shows "measure lebesgue (f ` S) = integral S (\x. \det (matrix (f' x))\)" + using measurable_differentiable_image_eq [OF S der_f inj] + assms has_measure_differentiable_image by blast + +end diff -r ae76012879c6 -r 73a5a33486ee src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Apr 17 18:04:49 2018 +0100 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Apr 17 22:35:48 2018 +0100 @@ -1550,14 +1550,15 @@ assume "0 < e" have "S \ lmeasurable" using \negligible S\ by (simp add: negligible_iff_null_sets fmeasurableI_null_sets) + then have "S \ sets lebesgue" + by blast 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]) + obtain T where "open T" "S \ T" "(T - S) \ lmeasurable" + "measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)" + by (rule lmeasurable_outer_open [OF \S \ sets lebesgue\ 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) + using \negligible S\ by (simp add: measure_Diff_null_set negligible_iff_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))))" @@ -1690,7 +1691,7 @@ 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\]) + proof (rule measure_mono_fmeasurable) show "(\\') \ sets lebesgue" using div lmeasurable_division by auto have "\\' \ \\" @@ -1704,7 +1705,9 @@ by (metis \x \ D\ Int_iff dist_norm mem_ball norm_minus_commute subsetD RT) qed finally show "\\' \ T" . - qed + show "T \ lmeasurable" + using \S \ lmeasurable\ \S \ T\ \T - S \ lmeasurable\ fmeasurable_Diff_D by blast + qed have "sum (measure lebesgue) \' = sum content \'" using \\' \ \\ cbox by (force intro: sum.cong) then have "(2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) \' = @@ -3991,4 +3994,705 @@ (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box) qed +subsection\Various common equivalent forms of function measurability\ + +lemma indicator_sum_eq: + fixes m::real and f :: "'a \ real" + assumes "\m\ \ 2 ^ (2*n)" "m/2^n \ f x" "f x < (m+1)/2^n" "m \ \" + shows "(\k::real | k \ \ \ \k\ \ 2 ^ (2*n). + k/2^n * indicator {y. k/2^n \ f y \ f y < (k+1)/2^n} x) = m/2^n" + (is "sum ?f ?S = _") +proof - + have "sum ?f ?S = sum (\k. k/2^n * indicator {y. k/2^n \ f y \ f y < (k+1)/2^n} x) {m}" + proof (rule comm_monoid_add_class.sum.mono_neutral_right) + show "finite ?S" + by (rule finite_abs_int_segment) + show "{m} \ {k \ \. \k\ \ 2 ^ (2*n)}" + using assms by auto + show "\i\{k \ \. \k\ \ 2 ^ (2*n)} - {m}. ?f i = 0" + using assms by (auto simp: indicator_def Ints_def abs_le_iff divide_simps) + qed + also have "\ = m/2^n" + using assms by (auto simp: indicator_def not_less) + finally show ?thesis . +qed + +lemma measurable_on_sf_limit_lemma1: + fixes f :: "'a::euclidean_space \ real" + assumes "\a b. {x \ S. a \ f x \ f x < b} \ sets (lebesgue_on S)" + obtains g where "\n. g n \ borel_measurable (lebesgue_on S)" + "\n. finite(range (g n))" + "\x. (\n. g n x) \ f x" +proof + show "(\x. sum (\k::real. k/2^n * indicator {y. k/2^n \ f y \ f y < (k+1)/2^n} x) + {k \ \. \k\ \ 2 ^ (2*n)}) \ borel_measurable (lebesgue_on S)" + (is "?g \ _") for n + proof - + have "\k. \k \ \; \k\ \ 2 ^ (2*n)\ + \ Measurable.pred (lebesgue_on S) (\x. k / (2^n) \ f x \ f x < (k+1) / (2^n))" + using assms by (force simp: pred_def space_restrict_space) + then show ?thesis + by (simp add: field_class.field_divide_inverse) + qed + show "finite (range (?g n))" for n + proof - + have "range (?g n) \ (\k. k/2^n) ` {k \ \. \k\ \ 2 ^ (2*n)}" + proof clarify + fix x + show "?g n x \ (\k. k/2^n) ` {k \ \. \k\ \ 2 ^ (2*n)}" + proof (cases "\k::real. k \ \ \ \k\ \ 2 ^ (2*n) \ k/2^n \ (f x) \ (f x) < (k+1)/2^n") + case True + then show ?thesis + apply clarify + by (subst indicator_sum_eq) auto + next + case False + then have "?g n x = 0" by auto + then show ?thesis by force + qed + qed + moreover have "finite ((\k::real. (k/2^n)) ` {k \ \. \k\ \ 2 ^ (2*n)})" + by (simp add: finite_abs_int_segment) + ultimately show ?thesis + using finite_subset by blast + qed + show "(\n. ?g n x) \ f x" for x + proof (rule LIMSEQ_I) + fix e::real + assume "e > 0" + obtain N1 where N1: "\f x\ < 2 ^ N1" + using real_arch_pow by fastforce + obtain N2 where N2: "(1/2) ^ N2 < e" + using real_arch_pow_inv \e > 0\ by force + have "norm (?g n x - f x) < e" if n: "n \ max N1 N2" for n + proof - + define m where "m \ floor(2^n * (f x))" + have "1 \ \2^n\ * e" + using n N2 \e > 0\ less_eq_real_def less_le_trans by (fastforce simp add: divide_simps) + then have *: "\x \ y; y < x + 1\ \ abs(x - y) < \2^n\ * e" for x y::real + by linarith + have "\2^n\ * \m/2^n - f x\ = \2^n * (m/2^n - f x)\" + by (simp add: abs_mult) + also have "\ = \real_of_int \2^n * f x\ - f x * 2^n\" + by (simp add: algebra_simps m_def) + also have "\ < \2^n\ * e" + by (rule *; simp add: mult.commute) + finally have "\2^n\ * \m/2^n - f x\ < \2^n\ * e" . + then have me: "\m/2^n - f x\ < e" + by simp + have "\real_of_int m\ \ 2 ^ (2*n)" + proof (cases "f x < 0") + case True + then have "-\f x\ \ \(2::real) ^ N1\" + using N1 le_floor_iff minus_le_iff by fastforce + with n True have "\real_of_int\f x\\ \ 2 ^ N1" + by linarith + also have "\ \ 2^n" + using n by (simp add: m_def) + finally have "\real_of_int \f x\\ * 2^n \ 2^n * 2^n" + by simp + moreover + have "\real_of_int \2^n * f x\\ \ \real_of_int \f x\\ * 2^n" + proof - + have "\real_of_int \2^n * f x\\ = - (real_of_int \2^n * f x\)" + using True by (simp add: abs_if mult_less_0_iff) + also have "\ \ - (real_of_int (\(2::real) ^ n\ * \f x\))" + using le_mult_floor_Ints [of "(2::real)^n"] by simp + also have "\ \ \real_of_int \f x\\ * 2^n" + using True + by simp + finally show ?thesis . + qed + ultimately show ?thesis + by (metis (no_types, hide_lams) m_def order_trans power2_eq_square power_even_eq) + next + case False + with n N1 have "f x \ 2^n" + by (simp add: not_less) (meson less_eq_real_def one_le_numeral order_trans power_increasing) + moreover have "0 \ m" + using False m_def by force + ultimately show ?thesis + by (metis abs_of_nonneg floor_mono le_floor_iff m_def of_int_0_le_iff power2_eq_square power_mult real_mult_le_cancel_iff1 zero_less_numeral mult.commute zero_less_power) + qed + then have "?g n x = m/2^n" + by (rule indicator_sum_eq) (auto simp: m_def mult.commute divide_simps) + then have "norm (?g n x - f x) = norm (m/2^n - f x)" + by simp + also have "\ < e" + by (simp add: me) + finally show ?thesis . + qed + then show "\no. \n\no. norm (?g n x - f x) < e" + by blast + qed +qed + + +lemma borel_measurable_vimage_halfspace_component_lt: + "f \ borel_measurable (lebesgue_on S) \ + (\a i. i \ Basis \ {x \ S. f x \ i < a} \ sets (lebesgue_on S))" + apply (rule trans [OF borel_measurable_iff_halfspace_less]) + apply (fastforce simp add: space_restrict_space) + done + +lemma borel_measurable_simple_function_limit: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\g. (\n. (g n) \ borel_measurable (lebesgue_on S)) \ + (\n. finite (range (g n))) \ (\x. (\n. g n x) \ f x))" +proof - + have "\g. (\n. (g n) \ borel_measurable (lebesgue_on S)) \ + (\n. finite (range (g n))) \ (\x. (\n. g n x) \ f x)" + if f: "\a i. i \ Basis \ {x \ S. f x \ i < a} \ sets (lebesgue_on S)" + proof - + have "\g. (\n. (g n) \ borel_measurable (lebesgue_on S)) \ + (\n. finite(image (g n) UNIV)) \ + (\x. ((\n. g n x) \ f x \ i))" if "i \ Basis" for i + proof (rule measurable_on_sf_limit_lemma1 [of S "\x. f x \ i"]) + show "{x \ S. a \ f x \ i \ f x \ i < b} \ sets (lebesgue_on S)" for a b + proof - + have "{x \ S. a \ f x \ i \ f x \ i < b} = {x \ S. f x \ i < b} - {x \ S. a > f x \ i}" + by auto + also have "\ \ sets (lebesgue_on S)" + using f that by blast + finally show ?thesis . + qed + qed blast + then obtain g where g: + "\i n. i \ Basis \ g i n \ borel_measurable (lebesgue_on S)" + "\i n. i \ Basis \ finite(range (g i n))" + "\i x. i \ Basis \ ((\n. g i n x) \ f x \ i)" + by metis + show ?thesis + proof (intro conjI allI exI) + show "(\x. \i\Basis. g i n x *\<^sub>R i) \ borel_measurable (lebesgue_on S)" for n + by (intro borel_measurable_sum borel_measurable_scaleR) (auto intro: g) + show "finite (range (\x. \i\Basis. g i n x *\<^sub>R i))" for n + proof - + have "range (\x. \i\Basis. g i n x *\<^sub>R i) \ (\h. \i\Basis. h i *\<^sub>R i) ` PiE Basis (\i. range (g i n))" + proof clarify + fix x + show "(\i\Basis. g i n x *\<^sub>R i) \ (\h. \i\Basis. h i *\<^sub>R i) ` (\\<^sub>E i\Basis. range (g i n))" + by (rule_tac x="\i\Basis. g i n x" in image_eqI) auto + qed + moreover have "finite(PiE Basis (\i. range (g i n)))" + by (simp add: g finite_PiE) + ultimately show ?thesis + by (metis (mono_tags, lifting) finite_surj) + qed + show "(\n. \i\Basis. g i n x *\<^sub>R i) \ f x" for x + proof - + have "(\n. \i\Basis. g i n x *\<^sub>R i) \ (\i\Basis. (f x \ i) *\<^sub>R i)" + by (auto intro!: tendsto_sum tendsto_scaleR g) + moreover have "(\i\Basis. (f x \ i) *\<^sub>R i) = f x" + using euclidean_representation by blast + ultimately show ?thesis + by metis + qed + qed + qed + moreover have "f \ borel_measurable (lebesgue_on S)" + if meas_g: "\n. g n \ borel_measurable (lebesgue_on S)" + and fin: "\n. finite (range (g n))" + and to_f: "\x. (\n. g n x) \ f x" for g + by (rule borel_measurable_LIMSEQ_metric [OF meas_g to_f]) + ultimately show ?thesis + using borel_measurable_vimage_halfspace_component_lt by blast +qed + +lemma borel_measurable_vimage_halfspace_component_ge: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\a i. i \ Basis \ {x \ S. f x \ i \ a} \ sets (lebesgue_on S))" + apply (rule trans [OF borel_measurable_iff_halfspace_ge]) + apply (fastforce simp add: space_restrict_space) + done + +lemma borel_measurable_vimage_halfspace_component_gt: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\a i. i \ Basis \ {x \ S. f x \ i > a} \ sets (lebesgue_on S))" + apply (rule trans [OF borel_measurable_iff_halfspace_greater]) + apply (fastforce simp add: space_restrict_space) + done + +lemma borel_measurable_vimage_halfspace_component_le: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\a i. i \ Basis \ {x \ S. f x \ i \ a} \ sets (lebesgue_on S))" + apply (rule trans [OF borel_measurable_iff_halfspace_le]) + apply (fastforce simp add: space_restrict_space) + done + +lemma + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows borel_measurable_vimage_open_interval: + "f \ borel_measurable (lebesgue_on S) \ + (\a b. {x \ S. f x \ box a b} \ sets (lebesgue_on S))" (is ?thesis1) + and borel_measurable_vimage_open: + "f \ borel_measurable (lebesgue_on S) \ + (\T. open T \ {x \ S. f x \ T} \ sets (lebesgue_on S))" (is ?thesis2) +proof - + have "{x \ S. f x \ box a b} \ sets (lebesgue_on S)" if "f \ borel_measurable (lebesgue_on S)" for a b + proof - + have "S = S \ space lebesgue" + by simp + then have "S \ (f -` box a b) \ sets (lebesgue_on S)" + by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that) + then show ?thesis + by (simp add: Collect_conj_eq vimage_def) + qed + moreover + have "{x \ S. f x \ T} \ sets (lebesgue_on S)" + if T: "\a b. {x \ S. f x \ box a b} \ sets (lebesgue_on S)" "open T" for T + proof - + obtain \ where "countable \" and \: "\X. X \ \ \ \a b. X = box a b" "\\ = T" + using open_countable_Union_open_box that \open T\ by metis + then have eq: "{x \ S. f x \ T} = (\U \ \. {x \ S. f x \ U})" + by blast + have "{x \ S. f x \ U} \ sets (lebesgue_on S)" if "U \ \" for U + using that T \ by blast + then show ?thesis + by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \countable \\]) + qed + moreover + have eq: "{x \ S. f x \ i < a} = {x \ S. f x \ {y. y \ i < a}}" for i a + by auto + have "f \ borel_measurable (lebesgue_on S)" + if "\T. open T \ {x \ S. f x \ T} \ sets (lebesgue_on S)" + by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that) + ultimately show "?thesis1" "?thesis2" + by blast+ +qed + + +lemma borel_measurable_vimage_closed: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\T. closed T \ {x \ S. f x \ T} \ sets (lebesgue_on S))" + (is "?lhs = ?rhs") +proof - + have eq: "{x \ S. f x \ T} = S - {x \ S. f x \ (- T)}" for T + by auto + show ?thesis + apply (simp add: borel_measurable_vimage_open, safe) + apply (simp_all (no_asm) add: eq) + apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open) + apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed) + done +qed + +lemma borel_measurable_vimage_closed_interval: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\a b. {x \ S. f x \ cbox a b} \ sets (lebesgue_on S))" + (is "?lhs = ?rhs") +proof + assume ?lhs then show ?rhs + using borel_measurable_vimage_closed by blast +next + assume RHS: ?rhs + have "{x \ S. f x \ T} \ sets (lebesgue_on S)" if "open T" for T + proof - + obtain \ where "countable \" and \: "\ \ Pow T" "\X. X \ \ \ \a b. X = cbox a b" "\\ = T" + using open_countable_Union_open_cbox that \open T\ by metis + then have eq: "{x \ S. f x \ T} = (\U \ \. {x \ S. f x \ U})" + by blast + have "{x \ S. f x \ U} \ sets (lebesgue_on S)" if "U \ \" for U + using that \ by (metis RHS) + then show ?thesis + by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \countable \\]) + qed + then show ?lhs + by (simp add: borel_measurable_vimage_open) +qed + +lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue" + by auto + +lemma borel_measurable_vimage_borel: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable (lebesgue_on S) \ + (\T. T \ sets borel \ {x \ S. f x \ T} \ sets (lebesgue_on S))" + (is "?lhs = ?rhs") +proof + assume f: ?lhs + then show ?rhs + using measurable_sets [OF f] + by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def) +qed (simp add: borel_measurable_vimage_open_interval) + +lemma lebesgue_measurable_vimage_borel: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "f \ borel_measurable lebesgue" "T \ sets borel" + shows "{x. f x \ T} \ sets lebesgue" + using assms borel_measurable_vimage_borel [of f UNIV] by auto + +lemma borel_measurable_If_I: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes f: "f \ borel_measurable (lebesgue_on S)" and S: "S \ sets lebesgue" + shows "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue" +proof - + have eq: "{x. x \ S} \ {x. f x \ Y} = {x. x \ S} \ {x. f x \ Y} \ S" for Y + by blast + show ?thesis + using f S + apply (simp add: vimage_def in_borel_measurable_borel Ball_def) + apply (elim all_forward imp_forward asm_rl) + apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq) + apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff) + done +qed + +lemma borel_measurable_If_D: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue" + shows "f \ borel_measurable (lebesgue_on S)" + using assms + apply (simp add: in_borel_measurable_borel Ball_def) + apply (elim all_forward imp_forward asm_rl) + apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI) + done + +lemma borel_measurable_UNIV: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "S \ sets lebesgue" + shows "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue \ f \ borel_measurable (lebesgue_on S)" + using assms borel_measurable_If_D borel_measurable_If_I by blast + +lemma borel_measurable_lebesgue_preimage_borel: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + shows "f \ borel_measurable lebesgue \ + (\T. T \ sets borel \ {x. f x \ T} \ sets lebesgue)" + apply (intro iffI allI impI lebesgue_measurable_vimage_borel) + apply (auto simp: in_borel_measurable_borel vimage_def) + done + +subsection\More results on integrability\ + +lemma integrable_on_all_intervals_UNIV: + fixes f :: "'a::euclidean_space \ 'b::banach" + assumes intf: "\a b. f integrable_on cbox a b" + and normf: "\x. norm(f x) \ g x" and g: "g integrable_on UNIV" + shows "f integrable_on UNIV" +proof - +have intg: "(\a b. g integrable_on cbox a b)" + and gle_e: "\e>0. \B>0. \a b c d. + ball 0 B \ cbox a b \ cbox a b \ cbox c d \ + \integral (cbox a b) g - integral (cbox c d) g\ + < e" + using g + by (auto simp: integrable_alt_subset [of _ UNIV] intf) + have le: "norm (integral (cbox a b) f - integral (cbox c d) f) \ \integral (cbox a b) g - integral (cbox c d) g\" + if "cbox a b \ cbox c d" for a b c d + proof - + have "norm (integral (cbox a b) f - integral (cbox c d) f) = norm (integral (cbox c d - cbox a b) f)" + using intf that by (simp add: norm_minus_commute integral_setdiff) + also have "\ \ integral (cbox c d - cbox a b) g" + proof (rule integral_norm_bound_integral [OF _ _ normf]) + show "f integrable_on cbox c d - cbox a b" "g integrable_on cbox c d - cbox a b" + by (meson integrable_integral integrable_setdiff intf intg negligible_setdiff that)+ + qed + also have "\ = integral (cbox c d) g - integral (cbox a b) g" + using intg that by (simp add: integral_setdiff) + also have "\ \ \integral (cbox a b) g - integral (cbox c d) g\" + by simp + finally show ?thesis . + qed + show ?thesis + using gle_e + apply (simp add: integrable_alt_subset [of _ UNIV] intf) + apply (erule imp_forward all_forward ex_forward asm_rl)+ + by (meson not_less order_trans le) +qed + +lemma integrable_on_all_intervals_integrable_bound: + fixes f :: "'a::euclidean_space \ 'b::banach" + assumes intf: "\a b. (\x. if x \ S then f x else 0) integrable_on cbox a b" + and normf: "\x. x \ S \ norm(f x) \ g x" and g: "g integrable_on S" + shows "f integrable_on S" + using integrable_on_all_intervals_UNIV [OF intf, of "(\x. if x \ S then g x else 0)"] + by (simp add: g integrable_restrict_UNIV normf) + +lemma measurable_bounded_lemma: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes f: "f \ borel_measurable lebesgue" and g: "g integrable_on cbox a b" + and normf: "\x. x \ cbox a b \ norm(f x) \ g x" + shows "f integrable_on cbox a b" +proof - + have "g absolutely_integrable_on cbox a b" + by (metis (full_types) add_increasing g le_add_same_cancel1 nonnegative_absolutely_integrable_1 norm_ge_zero normf) + then have "integrable (lebesgue_on (cbox a b)) g" + by (simp add: integrable_restrict_space set_integrable_def) + then have "integrable (lebesgue_on (cbox a b)) f" + proof (rule Bochner_Integration.integrable_bound) + show "AE x in lebesgue_on (cbox a b). norm (f x) \ norm (g x)" + by (rule AE_I2) (auto intro: normf order_trans) + qed (simp add: f measurable_restrict_space1) + then show ?thesis + by (simp add: integrable_on_lebesgue_on) +qed + +proposition measurable_bounded_by_integrable_imp_integrable: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes f: "f \ borel_measurable (lebesgue_on S)" and g: "g integrable_on S" + and normf: "\x. x \ S \ norm(f x) \ g x" and S: "S \ sets lebesgue" + shows "f integrable_on S" +proof (rule integrable_on_all_intervals_integrable_bound [OF _ normf g]) + show "(\x. if x \ S then f x else 0) integrable_on cbox a b" for a b + proof (rule measurable_bounded_lemma) + show "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue" + by (simp add: S borel_measurable_UNIV f) + show "(\x. if x \ S then g x else 0) integrable_on cbox a b" + by (simp add: g integrable_altD(1)) + show "norm (if x \ S then f x else 0) \ (if x \ S then g x else 0)" for x + using normf by simp + qed +qed + +subsection\ Relation between Borel measurability and integrability.\ + +lemma integrable_imp_measurable_weak: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "S \ sets lebesgue" "f integrable_on S" + shows "f \ borel_measurable (lebesgue_on S)" + by (metis (mono_tags, lifting) assms has_integral_implies_lebesgue_measurable borel_measurable_restrict_space_iff integrable_on_def sets.Int_space_eq2) + +lemma integrable_imp_measurable: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "f integrable_on S" + shows "f \ borel_measurable (lebesgue_on S)" +proof - + have "(UNIV::'a set) \ sets lborel" + by simp + then show ?thesis + using assms borel_measurable_If_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast +qed + +proposition negligible_differentiable_vimage: + fixes f :: "'a \ 'a::euclidean_space" + assumes "negligible T" + and f': "\x. x \ S \ inj(f' x)" + and derf: "\x. x \ S \ (f has_derivative f' x) (at x within S)" + shows "negligible {x \ S. f x \ T}" +proof - + define U where + "U \ \n::nat. {x \ S. \y. y \ S \ norm(y - x) < 1/n + \ norm(y - x) \ n * norm(f y - f x)}" + have "negligible {x \ U n. f x \ T}" if "n > 0" for n + proof (subst locally_negligible_alt, clarify) + fix a + assume a: "a \ U n" and fa: "f a \ T" + define V where "V \ {x. x \ U n \ f x \ T} \ ball a (1 / n / 2)" + show "\V. openin (subtopology euclidean {x \ U n. f x \ T}) V \ a \ V \ negligible V" + proof (intro exI conjI) + have noxy: "norm(x - y) \ n * norm(f x - f y)" if "x \ V" "y \ V" for x y + using that unfolding U_def V_def mem_Collect_eq Int_iff mem_ball dist_norm + by (meson norm_triangle_half_r) + then have "inj_on f V" + by (force simp: inj_on_def) + then obtain g where g: "\x. x \ V \ g(f x) = x" + by (metis inv_into_f_f) + have "\T' B. open T' \ f x \ T' \ + (\y\f ` V \ T \ T'. norm (g y - g (f x)) \ B * norm (y - f x))" + if "f x \ T" "x \ V" for x + apply (rule_tac x = "ball (f x) 1" in exI) + using that noxy by (force simp: g) + then have "negligible (g ` (f ` V \ T))" + by (force simp: \negligible T\ negligible_Int intro!: negligible_locally_Lipschitz_image) + moreover have "V \ g ` (f ` V \ T)" + by (force simp: g image_iff V_def) + ultimately show "negligible V" + by (rule negligible_subset) + qed (use a fa V_def that in auto) + qed + with negligible_countable_Union have "negligible (\n \ {0<..}. {x. x \ U n \ f x \ T})" + by auto + moreover have "{x \ S. f x \ T} \ (\n \ {0<..}. {x. x \ U n \ f x \ T})" + proof clarsimp + fix x + assume "x \ S" and "f x \ T" + then obtain inj: "inj(f' x)" and der: "(f has_derivative f' x) (at x within S)" + using assms by metis + moreover have "linear(f' x)" + and eps: "\\. \ > 0 \ \\>0. \y\S. norm (y - x) < \ \ + norm (f y - f x - f' x (y - x)) \ \ * norm (y - x)" + using der by (auto simp: has_derivative_within_alt linear_linear) + ultimately obtain g where "linear g" and g: "g \ f' x = id" + using linear_injective_left_inverse by metis + then obtain B where "B > 0" and B: "\z. B * norm z \ norm(f' x z)" + using linear_invertible_bounded_below_pos \linear (f' x)\ by blast + then obtain i where "i \ 0" and i: "1 / real i < B" + by (metis (full_types) inverse_eq_divide real_arch_invD) + then obtain \ where "\ > 0" + and \: "\y. \y\S; norm (y - x) < \\ \ + norm (f y - f x - f' x (y - x)) \ (B - 1 / real i) * norm (y - x)" + using eps [of "B - 1/i"] by auto + then obtain j where "j \ 0" and j: "inverse (real j) < \" + using real_arch_inverse by blast + have "norm (y - x)/(max i j) \ norm (f y - f x)" + if "y \ S" and less: "norm (y - x) < 1 / (max i j)" for y + proof - + have "1 / real (max i j) < \" + using j \j \ 0\ \0 < \\ + by (auto simp: divide_simps max_mult_distrib_left of_nat_max) + then have "norm (y - x) < \" + using less by linarith + with \ \y \ S\ have le: "norm (f y - f x - f' x (y - x)) \ B * norm (y - x) - norm (y - x)/i" + by (auto simp: algebra_simps) + have *: "\norm(f - f' - y) \ b - c; b \ norm y; d \ c\ \ d \ norm(f - f')" + for b c d and y f f'::'a + using norm_triangle_ineq3 [of "f - f'" y] by simp + show ?thesis + apply (rule * [OF le B]) + using \i \ 0\ \j \ 0\ by (simp add: divide_simps max_mult_distrib_left of_nat_max less_max_iff_disj) + qed + with \x \ S\ \i \ 0\ \j \ 0\ show "\n\{0<..}. x \ U n" + by (rule_tac x="max i j" in bexI) (auto simp: field_simps U_def less_max_iff_disj) +qed + ultimately show ?thesis + by (rule negligible_subset) +qed + +lemma absolutely_integrable_Un: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes S: "f absolutely_integrable_on S" and T: "f absolutely_integrable_on T" + shows "f absolutely_integrable_on (S \ T)" +proof - + have [simp]: "{x. (if x \ A then f x else 0) \ 0} = {x \ A. f x \ 0}" for A + by auto + let ?ST = "{x \ S. f x \ 0} \ {x \ T. f x \ 0}" + have "?ST \ sets lebesgue" + proof (rule Sigma_Algebra.sets.Int) + have "f integrable_on S" + using S absolutely_integrable_on_def by blast + then have "(\x. if x \ S then f x else 0) integrable_on UNIV" + by (simp add: integrable_restrict_UNIV) + then have borel: "(\x. if x \ S then f x else 0) \ borel_measurable (lebesgue_on UNIV)" + using integrable_imp_measurable borel_measurable_UNIV_eq by blast + then show "{x \ S. f x \ 0} \ sets lebesgue" + unfolding borel_measurable_vimage_open + by (rule allE [where x = "-{0}"]) auto + next + have "f integrable_on T" + using T absolutely_integrable_on_def by blast + then have "(\x. if x \ T then f x else 0) integrable_on UNIV" + by (simp add: integrable_restrict_UNIV) + then have borel: "(\x. if x \ T then f x else 0) \ borel_measurable (lebesgue_on UNIV)" + using integrable_imp_measurable borel_measurable_UNIV_eq by blast + then show "{x \ T. f x \ 0} \ sets lebesgue" + unfolding borel_measurable_vimage_open + by (rule allE [where x = "-{0}"]) auto + qed + then have "f absolutely_integrable_on ?ST" + by (rule set_integrable_subset [OF S]) auto + then have Int: "(\x. if x \ ?ST then f x else 0) absolutely_integrable_on UNIV" + using absolutely_integrable_restrict_UNIV by blast + have "(\x. if x \ S then f x else 0) absolutely_integrable_on UNIV" + "(\x. if x \ T then f x else 0) absolutely_integrable_on UNIV" + using S T absolutely_integrable_restrict_UNIV by blast+ + then have "(\x. (if x \ S then f x else 0) + (if x \ T then f x else 0)) absolutely_integrable_on UNIV" + by (rule absolutely_integrable_add) + then have "(\x. ((if x \ S then f x else 0) + (if x \ T then f x else 0)) - (if x \ ?ST then f x else 0)) absolutely_integrable_on UNIV" + using Int by (rule absolutely_integrable_diff) + then have "(\x. if x \ S \ T then f x else 0) absolutely_integrable_on UNIV" + by (rule absolutely_integrable_spike) (auto intro: empty_imp_negligible) + then show ?thesis + unfolding absolutely_integrable_restrict_UNIV . +qed + + + + +subsubsection\Differentiability of inverse function (most basic form)\ + +proposition has_derivative_inverse_within: + fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" + assumes der_f: "(f has_derivative f') (at a within S)" + and cont_g: "continuous (at (f a) within f ` S) g" + and "a \ S" "linear g'" and id: "g' \ f' = id" + and gf: "\x. x \ S \ g(f x) = x" + shows "(g has_derivative g') (at (f a) within f ` S)" +proof - + have [simp]: "g' (f' x) = x" for x + by (simp add: local.id pointfree_idE) + have "bounded_linear f'" + and f': "\e. e>0 \ \d>0. \y\S. norm (y - a) < d \ + norm (f y - f a - f' (y - a)) \ e * norm (y - a)" + using der_f by (auto simp: has_derivative_within_alt) + obtain C where "C > 0" and C: "\x. norm (g' x) \ C * norm x" + using linear_bounded_pos [OF \linear g'\] by metis + obtain B k where "B > 0" "k > 0" + and Bk: "\x. \x \ S; norm(f x - f a) < k\ \ norm(x - a) \ B * norm(f x - f a)" + proof - + obtain B where "B > 0" and B: "\x. B * norm x \ norm (f' x)" + using linear_inj_bounded_below_pos [of f'] \linear g'\ id der_f has_derivative_linear + linear_invertible_bounded_below_pos by blast + then obtain d where "d>0" + and d: "\y. \y \ S; norm (y - a) < d\ \ + norm (f y - f a - f' (y - a)) \ B / 2 * norm (y - a)" + using f' [of "B/2"] by auto + then obtain e where "e > 0" + and e: "\x. \x \ S; norm (f x - f a) < e\ \ norm (g (f x) - g (f a)) < d" + using cont_g by (auto simp: continuous_within_eps_delta dist_norm) + show thesis + proof + show "2/B > 0" + using \B > 0\ by simp + show "norm (x - a) \ 2 / B * norm (f x - f a)" + if "x \ S" "norm (f x - f a) < e" for x + proof - + have xa: "norm (x - a) < d" + using e [OF that] gf by (simp add: \a \ S\ that) + have *: "\norm(y - f') \ B / 2 * norm x; B * norm x \ norm f'\ + \ norm y \ B / 2 * norm x" for y f'::'b and x::'a + using norm_triangle_ineq3 [of y f'] by linarith + show ?thesis + using * [OF d [OF \x \ S\ xa] B] \B > 0\ by (simp add: field_simps) + qed + qed (use \e > 0\ in auto) + qed + show ?thesis + unfolding has_derivative_within_alt + proof (intro conjI impI allI) + show "bounded_linear g'" + using \linear g'\ by (simp add: linear_linear) + next + fix e :: "real" + assume "e > 0" + then obtain d where "d>0" + and d: "\y. \y \ S; norm (y - a) < d\ \ + norm (f y - f a - f' (y - a)) \ e / (B * C) * norm (y - a)" + using f' [of "e / (B * C)"] \B > 0\ \C > 0\ by auto + have "norm (x - a - g' (f x - f a)) \ e * norm (f x - f a)" + if "x \ S" and lt_k: "norm (f x - f a) < k" and lt_dB: "norm (f x - f a) < d/B" for x + proof - + have "norm (x - a) \ B * norm(f x - f a)" + using Bk lt_k \x \ S\ by blast + also have "\ < d" + by (metis \0 < B\ lt_dB mult.commute pos_less_divide_eq) + finally have lt_d: "norm (x - a) < d" . + have "norm (x - a - g' (f x - f a)) \ norm(g'(f x - f a - (f' (x - a))))" + by (simp add: linear_diff [OF \linear g'\] norm_minus_commute) + also have "\ \ C * norm (f x - f a - f' (x - a))" + using C by blast + also have "\ \ e * norm (f x - f a)" + proof - + have "norm (f x - f a - f' (x - a)) \ e / (B * C) * norm (x - a)" + using d [OF \x \ S\ lt_d] . + also have "\ \ (norm (f x - f a) * e) / C" + using \B > 0\ \C > 0\ \e > 0\ by (simp add: field_simps Bk lt_k \x \ S\) + finally show ?thesis + using \C > 0\ by (simp add: field_simps) + qed + finally show ?thesis . + qed + then show "\d>0. \y\f ` S. + norm (y - f a) < d \ + norm (g y - g (f a) - g' (y - f a)) \ e * norm (y - f a)" + apply (rule_tac x="min k (d / B)" in exI) + using \k > 0\ \B > 0\ \d > 0\ \a \ S\ by (auto simp: gf) + qed +qed + end diff -r ae76012879c6 -r 73a5a33486ee src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Apr 17 18:04:49 2018 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Apr 17 22:35:48 2018 +0100 @@ -5069,6 +5069,56 @@ norm (integral (cbox a b) (\x. if x \ s then f x else 0) - integral (cbox c d) (\x. if x \ s then f x else 0)) < e" using assms[unfolded integrable_alt[of f]] by auto +lemma integrable_alt_subset: + fixes f :: "'a::euclidean_space \ 'b::banach" + shows + "f integrable_on S \ + (\a b. (\x. if x \ S then f x else 0) integrable_on cbox a b) \ + (\e>0. \B>0. \a b c d. + ball 0 B \ cbox a b \ cbox a b \ cbox c d + \ norm(integral (cbox a b) (\x. if x \ S then f x else 0) - + integral (cbox c d) (\x. if x \ S then f x else 0)) < e)" + (is "_ = ?rhs") +proof - + let ?g = "\x. if x \ S then f x else 0" + have "f integrable_on S \ + (\a b. ?g integrable_on cbox a b) \ + (\e>0. \B>0. \a b c d. ball 0 B \ cbox a b \ ball 0 B \ cbox c d \ + norm (integral (cbox a b) ?g - integral (cbox c d) ?g) < e)" + by (rule integrable_alt) + also have "\ = ?rhs" + proof - + { fix e :: "real" + assume e: "\e. e>0 \ \B>0. \a b c d. ball 0 B \ cbox a b \ cbox a b \ cbox c d \ + norm (integral (cbox a b) ?g - integral (cbox c d) ?g) < e" + and "e > 0" + obtain B where "B > 0" + and B: "\a b c d. \ball 0 B \ cbox a b; cbox a b \ cbox c d\ \ + norm (integral (cbox a b) ?g - integral (cbox c d) ?g) < e/2" + using \e > 0\ e [of "e/2"] by force + have "\B>0. \a b c d. + ball 0 B \ cbox a b \ ball 0 B \ cbox c d \ + norm (integral (cbox a b) ?g - integral (cbox c d) ?g) < e" + proof (intro exI allI conjI impI) + fix a b c d :: "'a" + let ?\ = "\i\Basis. max (a \ i) (c \ i) *\<^sub>R i" + let ?\ = "\i\Basis. min (b \ i) (d \ i) *\<^sub>R i" + show "norm (integral (cbox a b) ?g - integral (cbox c d) ?g) < e" + if ball: "ball 0 B \ cbox a b \ ball 0 B \ cbox c d" + proof - + have B': "norm (integral (cbox a b \ cbox c d) ?g - integral (cbox x y) ?g) < e/2" + if "cbox a b \ cbox c d \ cbox x y" for x y + using B [of ?\ ?\ x y] ball that by (simp add: Int_interval [symmetric]) + show ?thesis + using B' [of a b] B' [of c d] norm_triangle_half_r by blast + qed + qed (use \B > 0\ in auto)} + then show ?thesis + by force +qed + finally show ?thesis . +qed + lemma integrable_on_subcbox: fixes f :: "'n::euclidean_space \ 'a::banach" assumes intf: "f integrable_on S" diff -r ae76012879c6 -r 73a5a33486ee src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Tue Apr 17 18:04:49 2018 +0100 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue Apr 17 22:35:48 2018 +0100 @@ -1168,29 +1168,27 @@ "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" +proposition outer_regular_lborel_le: + assumes B[measurable]: "B \ sets borel" and "0 < (e::real)" + obtains U where "open U" "B \ U" and "emeasure lborel (U - 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]) + by (auto simp: 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) + using emeasure_bounded_finite[of "?B n"] by (auto simp: 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)" + then obtain U where U: "B \ U" "open U" and muU: "?\ (?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))" @@ -1199,7 +1197,7 @@ 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] + using U muU 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" . } @@ -1209,50 +1207,93 @@ 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) + show ?thesis + proof { fix x assume "x \ B" moreover - have "\n. norm x < real n" - by (simp add: reals_Archimedean2) - then guess n .. + obtain n where "norm x < real n" + using reals_Archimedean2 by blast 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 U by auto + have "?\ (\n. U n - B) \ (\n. ?\ (U n - B))" + using U(1) by (intro emeasure_subadditive_countably) auto + also have "\ \ (\n. ennreal (?e n))" + using U(3) by (intro suminf_le) (auto intro: less_imp_le) + also have "\ = 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" + finally show "emeasure lborel ((\n. U n) - 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" +lemma outer_regular_lborel: + assumes B: "B \ sets borel" and "0 < (e::real)" + obtains U where "open U" "B \ U" "emeasure lborel (U - B) < e" +proof - + obtain U where U: "open U" "B \ U" and "emeasure lborel (U-B) \ e/2" + using outer_regular_lborel_le [OF B, of "e/2"] \e > 0\ + by force + moreover have "ennreal (e/2) < ennreal e" + using \e > 0\ by (simp add: ennreal_lessI) + ultimately have "emeasure lborel (U-B) < e" + by auto + with U show ?thesis + using that by auto +qed + +lemma completion_upper: + assumes A: "A \ sets (completion M)" + obtains A' where "A \ A'" "A' \ sets M" "A' - A \ null_sets (completion M)" + "emeasure (completion M) A = emeasure M A'" proof - - obtain S' where S': "S \ S'" "S' \ sets borel" "emeasure lborel S' = emeasure lebesgue S" + from AE_notin_null_part[OF A] obtain N where N: "N \ null_sets M" "null_part M A \ N" + unfolding eventually_ae_filter using null_part_null_sets[OF A, THEN null_setsD2, THEN sets.sets_into_space] by auto + let ?A' = "main_part M A \ N" + show ?thesis + proof + show "A \ ?A'" + using \null_part M A \ N\ by (subst main_part_null_part_Un[symmetric, OF A]) auto + have "main_part M A \ A" + using assms main_part_null_part_Un by auto + then have "?A' - A \ N" + by blast + with N show "?A' - A \ null_sets (completion M)" + by (blast intro: null_sets_completionI completion.complete_measure_axioms complete_measure.complete2) + show "emeasure (completion M) A = emeasure M (main_part M A \ N)" + using A \N \ null_sets M\ by (simp add: emeasure_Un_null_set) + qed (use A N in auto) +qed + +lemma lmeasurable_outer_open: + assumes S: "S \ sets lebesgue" and "e > 0" + obtains T where "open T" "S \ T" "(T - S) \ lmeasurable" "measure lebesgue (T - S) < e" +proof - + obtain S' where S': "S \ S'" "S' \ sets borel" + and null: "S' - S \ null_sets lebesgue" + and em: "emeasure lebesgue S = emeasure lborel S'" using completion_upper[of S lborel] S by auto - then have f_S': "S' \ fmeasurable lborel" + then have f_S': "S' \ sets borel" using S by (auto simp: fmeasurable_def) - from outer_regular_lborel[OF this \0] guess U .. note U = this + with outer_regular_lborel[OF _ \0] + obtain U where U: "open U" "S' \ U" "emeasure lborel (U - S') < e" + by blast 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) + proof + show "open U" "S \ U" + using f_S' U S' by auto + have "(U - S) = (U - S') \ (S' - S)" + using S' U by auto + then have eq: "emeasure lebesgue (U - S) = emeasure lborel (U - S')" + using null by (simp add: U(1) emeasure_Un_null_set f_S' sets.Diff) + have "(U - S) \ sets lebesgue" + by (simp add: S U(1) sets.Diff) + then show "(U - S) \ lmeasurable" + unfolding fmeasurable_def using U(3) eq less_le_trans by fastforce + with eq U show "measure lebesgue (U - S) < e" + by (metis \U - S \ lmeasurable\ emeasure_eq_measure2 ennreal_leI not_le) qed qed diff -r ae76012879c6 -r 73a5a33486ee src/HOL/Analysis/Vitali_Covering_Theorem.thy --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Tue Apr 17 18:04:49 2018 +0100 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Tue Apr 17 22:35:48 2018 +0100 @@ -629,7 +629,6 @@ by metis qed - proposition negligible_eq_zero_density: "negligible S \ (\x\S. \r>0. \e>0. \d. 0 < d \ d \ r \