| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 203 kB |
|
Quellcode-Bibliothek Change_Of_Vars.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/Analysis/Change_Of_Vars.thy Authors: LC Paulson, based on material from HOL Light *) section‹Change of Variables Theorems› theory Change_Of_Vars imports Vitali_Covering_Theorem Determinants begin subsection ‹Measurable Shear and Stretch› 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) ` (cbo (is "?f ` _ ∈ _") and measure_shear_interval: "measure lebesgue ((λx. χ i. if i = m then x$m + x$n els = measure lebesgue (cbox a b)" (is "?Q") proof - have lin: "linear ?f" by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps) show fab: "?f ` cbox a b ∈ lmeasurable" by (simp add: lin measurable_linear_image_interval) let ?c = "χ i. if i = m then b$m + b$n else b$i" let ?mn = "axis m 1 - axis n (1::real)" have eq1: "measure lebesgue (cbox a ?c) = measure lebesgue (?f ` cbox a b) + measure lebesgue (cbox a ?c ∩ {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 by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurabl 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 = 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 = 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} using ‹m ≠ n› ab_ne apply (clarsimp simp: algebra_simps mem_box_cart inner_axis') by (smt (verit, ccfv_SIG) interval_ne_empty_cart(1)) ultimately show "negligible (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∩ (cbox a ?c ∩ {x. ? by (rule negligible_subset) show "?f ` cbox a b ∪ cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m} ∪ cbox a ?c ∩ {x. ?mn ∙ x proof show "?lhs ⊆ cbox a ?c" by (auto simp: mem_box_cart add_mono) (meson add_increasing2 an order_trans) show "cbox a ?c ⊆ ?lhs" apply (clarsimp simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF ‹m ≠ n›] by (smt (verit, del_insts) mem_box_cart(2) vec_lambda_beta) qed qed (fact fab) let ?d = "χ i. if i = m then a $ m - b $ m else 0" have eq2: "measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≤ a $ m}) + measure lebesgue = 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 ∩ { "(χ i. if i = m then a$m - b$m else 0)" "cbox a (χ i. if i = m then a$m + b$n else 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 measurabl 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 im 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, forc apply (drule_tac x=n in spec)+ by (meson ab_ne add_mono_thms_linordered_semiring(3) dual_order.trans interval_ne_emp 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 ≠ {}" by (smt (verit, del_insts) ab_ne an interval_ne_empty_cart(1) vec_lambda_beta) have ax_ne: "cbox a (χ i. if i = m then a $ m + b $ n else b $ i) ≠ {}" using ab_ne an by (smt (verit, ccfv_threshold) interval_ne_empty_cart(1) vec_lambda_beta) have eq3: "measure lebesgue (cbox a ?c) = measure lebesgue (cbox a (χ i. if i = m t 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∣ * (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) UNI 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 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" 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∣)) *🪙R x)" by (rule norm_le_componentwise_cart) (auto simp: abs_mult intro: mult_right_mono) also have "… < ?C" using x ‹0 🚫MAX k. ∣m k∣) * B› ‹0 🚫› zero_less_mult_pos2 by fastforce 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)) (χ 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 *🪙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) ( 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 *🪙R ∣prod m by simp have "∣z *🪙R ∣prod m UNIV∣ - ∣prod m UNIV∣ * measure lebesgue S∣ = ∣prod m UNIV∣ * ∣z - measure lebesgue S∣" by (metis (no_types, opaque_lifting) abs_abs abs_scaleR mult.commute real_scaleR_def rig also have "… < e" using zless True by (simp add: field_simps) finally show "∣z *🪙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 measurab 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 then show ?thesis by (simp add: negligible_iff_measure prm) 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 l 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::_ ==> real^'n::_" and i and S :: "(real^'n::_) 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_componen have detf: "det (matrix f) = 0" using ‹¬ inj f› det_nz_iff_inj[OF ‹linear f›] by blast show "f ` S ∈ lmeasurable ∧ ?Q f S" proof show "f ` S ∈ lmeasurable" using lmeasurable_iff_indicator_has_integral ‹linear f› ‹¬ inj f› negligible_UNIV n have "measure lebesgue (f ` S) = 0" by (meson ‹¬ inj f› ‹linear f› negligible_imp_measure0 negligible_linear_singular_i 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::_) 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_diagona qed next fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set" assume "m ≠ n" and "S ∈ lmeasurable" let ?h = "λv::(real, 'n) vec. χ i. v $ Transposition.transpose m n i" have lin: "linear ?h" by (rule linearI) (simp_all add: plus_vec_def scaleR_vec_def) have meq: "measure lebesgue ((λv::(real, 'n) vec. χ i. v $ Transposition.transpose m = 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 transpose_involutory)+ show ?thesis using him prod.permute [OF permutes_swap_id, where S=UNIV and g="λi. (b - a)$i", symmetric by (simp add: eq content_cbox_cart False) qed have "(χ i j. if Transposition.transpose m n i = j then 1 else 0) = (χ i j. if j = by (auto intro!: Cart_lambda_cong) then have "matrix ?h = transpose(χ i j. mat 1 $ i $ Transposition.transpose m n j)" by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def) 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" using measure_linear_sufficient [OF lin ‹S ∈ lmeasurable›] meq 1 by force next fix m n :: "'n" and S :: "(real, 'n) vec set" assume "m ≠ n" and "S ∈ lmeasurable" let ?h = "λv::(real, 'n) vec. χ i. if i = m then v $ m + v $ n else v $ i" have lin: "linear ?h" by (rule linearI) (auto simp: algebra_simps plus_vec_def scaleR_vec_def vec_eq_iff) consider "m < n" | " n < m" using ‹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 using ‹j 🚫› axis_def ‹m 🚫› by auto with ‹m 🚫› 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_ 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 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) ` by (metis (no_types, lifting) cbox_translation) also have "… = measure lebesgue ((+) ?v ` 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 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› sets_lebesgue_outer_open obtain U where "open U" and U: "frontier S ⊆ U" "U - frontier S ∈ lmeasurable" "emeasure lebesgue (U - front 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 add: emeasure_eq_measure2 ennreal_less_iff) 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_ 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 mea 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 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 subset 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 T: "open T" "S ⊆ T" and TS: "(T-S) ∈ lmeasurable" and "emeasure lebesgue (T using S ‹d > 0› sets_lebesgue_outer_open by blast then have "?μ (T-S) < d" by (metis emeasure_eq_measure2 ennreal_leI not_less) with S T TS have "T ∈ lmeasurable" and Tless: "?μ T < ?μ S + d" by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D) have "∃r. 0 < r ∧ r < d ∧ ball x r ⊆ T ∧ f ` (S ∩ ball x r) ∈ lmeasurable ∧ ?μ (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))) /🪙R norm(y - x)) ---> 0) (at x withi using deriv ‹x ∈ S› by (auto simp: has_derivative_within bounded_linear.linear field_si 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]) let ?unit_vol = "content (ball (0 :: real ^ 'n :: {finite, wellorder}) 1)" have 0: "0 < e * ?unit_vol" using ‹e > 0› by (simp add: content_ball_pos) obtain k where "k > 0" and k: "∧U. [U ∈ lmeasurable; ∧y. y ∈ U ==> ∃z. z ∈ f' x ` ball 0 1 ∧ dist z y < k] ==> ?μ U < ?μ (f' x ` ball 0 1) + e * ?unit_vol" using measure_semicontinuous_with_hausdist_explicit [OF bo neg 0] by blast obtain l where "l > 0" and l: "ball x l ⊆ T" using ‹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 (simp add: Lim_within) (auto simp add: field_simps) define r where "r ≡ min (min l (ζ/2)) (min 1 (d/2))" show ?thesis proof (intro exI conjI) show "r > 0" "r < d" using ‹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) /🪙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) /🪙R r" in bexI) have "f' x ((y - x) /🪙R r) = f' x (y - x) /🪙R r" by (simp add: lin linear_scale) then have "dist (f' x ((y - x) /🪙R r)) ((f y - f x) /🪙R r) = norm (f' x (y - x) by (simp add: dist_norm) also have "… = norm (f' x (y - x) - (f y - f x)) / r" using ‹r > 0› by (simp add: divide_simps scale_right_diff_distrib [symmetric]) also have "… ≤ norm (f y - (f x + f' x (y - x))) / norm (y - x)" using that ‹r > 0› False by (simp add: field_split_simps dist_norm norm_minus_commute mul also have "… < k" using that ‹0 🚫ζ› by (simp add: dist_commute r_def ζ [OF ‹y ∈ S› False]) finally show "dist (f' x ((y - x) /🪙R r)) ((f y - f x) /🪙R r) < k" . show "(y - x) /🪙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 /🪙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 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, opaque_lifting) add.commute diff_add_cancel dist_0_norm dist_commu ultimately show "bounded (?rfs)" by (rule bounded_subset) qed then have "(λx. r *🪙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› fsb by (simp add: measure_linear_image measure_translation_subtract measurable_translatio also have "… ≤ (∣det (matrix (f' x))∣ * ?unit_vol + e * ?unit_vol) * r ^ CARD('n)" proof - have "?μ (?rfs) < ?μ (f' x ` ball 0 1) + e * ?unit_vol" using rfs_mble by (force intro: k dest!: ex_lessK) then have "?μ (?rfs) < ∣det (matrix (f' x))∣ * ?unit_vol + e * ?unit_vol" by (simp add: lin measure_linear_image [of "f' x"]) 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: algebra_simps content_ball_conv_unit_ball[of r] content_ball_pos) 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 pairwise_image pairwise_mono by fastforce have "?l ≤ (∑i∈K. ?μ (case i of (x, s) ==> f ` (S ∩ ball x s)))" proof (rule measure_UNION_le [OF ‹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 ord qed also have "… ≤ (∑(x,s) ∈ K. (B + e) * ?μ (ball x s))" using Csub r ‹K ⊆ C› by (intro sum_mono) 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 using measure_mono_fmeasurable [OF _ _ ‹T ∈ lmeasurable›] Csub rT by (smt (verit) SUP_least measure_nonneg measure_notin_sets mem_Collect_eq old.prod.cas 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 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 m_diff_image_weak: fixes f :: "real^'n::{finite,wellorder} ==> real^'n::_" assumes S: "S ∈ lmeasurable" and deriv: "∧x. x ∈ S ==> (f has_derivative f' x) (at x within S)" and int: "(λx. ∣det (matrix (f' x))∣) integrable_on S" shows "f ` S ∈ lmeasurable ∧ measure lebesgue (f ` S) ≤ integral S (λx. ∣det (matr 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_integr 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 ⌊∣det (matrix (f' x))∣ / e⌋" in exI) by (smt (verit, del_insts) divide_nonneg_nonneg floor_eq_iff of_nat_nat pos_divide_less 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_subset mem_Collect_eq subs 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, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_l 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 🚫› that apply (auto simp: T_def mult.commute intro: less_le_trans dest!: subsetD) by (smt (verit, best) mult_less_cancel_left_disj nat_less_real_le) 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 :: "_ ==> rea proof (subst sum.reindex_nontrivial) fix i j assume "i ∈ {..n}" "j ∈ {..n}" "i ≠ j" "T i = T j" with that injT [unfolded inj_on_def] show "f (T i) = 0" by simp metis qed (use atMost_atLeast0 in auto) let ?B = "m + e * ?μ S" have "(∑k≤n. ?μ (f ` T k)) ≤ ?B" for n proof - have "(∑k≤n. ?μ (f ` T k)) ≤ (∑k≤n. ((k+1) * e) * ?μ(T k))" proof (rule sum_mono [OF measure_bounded_differentiable_image]) show "(f has_derivative f' x) (at x within T k)" if "x ∈ T k" for k x using that unfolding T_def by (blast intro: deriv has_derivative_subset) show "(λx. ∣det (matrix (f' x))∣) integrable_on T k" for k using absolutely_integrable_on_def aint_T by blast show "∣det (matrix (f' x))∣ ≤ real (k + 1) * e" if "x ∈ T k" for k x using T_def that by auto qed (use meas_t in auto) 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] flip: 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 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)" proof (rule set_integrable_subset [OF aint_S]) show "∪ (T ` {..n}) ∈ sets lebesgue" by (intro measurable meas_t fmeasurableD) qed (force simp: Seq) 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_distr 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: field_split_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^ apply (simp add: mem_box_cart) by (smt (verit, best) component_le_norm_cart le_of_int_ceiling) then have Seq: "S = (∪n. ?I n)" by blast have fIn: "f ` ?I n ∈ lmeasurable" and mfIn: "?μ (f ` ?I n) ≤ integral S (λx. ∣det (matrix (f' x))∣)" (is ?MN) for n proof - 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_subset subsetI) moreover have int_In: "(λx. ∣det (matrix (f' x))∣) integrable_on ?I n" by (metis (mono_tags) Int_commute int integrable_altD(1) integrable_restrict_Int) ultimately have "f ` ?I n ∈ lmeasurable" "?μ (f ` ?I n) ≤ integral (?I n) (λx. ∣det ( using m_diff_image_weak by metis+ moreover have "integral (?I n) (λx. ∣det (matrix (f' x))∣) ≤ integral S (λx. ∣det (m 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 (m 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 "∃m≥N. g n x - f x ≤ dist (g m x) (f x)" for N proof show "N ≤ N + n ∧ g n x - f x ≤ dist (g (N + n) x) (f x)" using g [of N] by (auto simp: dist_norm) qed with that show ?thesis using diff_gt_0_iff_gt by blast qed with lim show ?thesis unfolding lim_sequentially by (meson less_le_not_le not_le_imp_less) qed moreover let ?Ω = "λ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 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 (clarsimp simp: indicator_def field_split_simps Ints_def) by (smt (verit) int_less_real_le mult_nonneg_nonneg of_int_0 zero_le_power) qed show "?g n x ≤ ?g (Suc n) x" for n x proof - have "?g n x = (∑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 field_split_simps) also have "… = (∑k | k ∈ ℤ ∧ ∣k∣ ≤ 2 ^ (2*n). k/2^n * indicator {y. k/2^n ≤ f y ∧ (∑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 | k ∈ ℤ ∧ ∣k∣ ≤ 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ S 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 (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 :: "re 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 field_split_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 \ 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 \ apply (clarsimp simp: image_subset_iff) using one_le_power [of "2::real" "2*n"] by linarith have *: "[x ∈ (S ∪ T) - U; ∧x. x ∈ S ==> x ∈ U; ∧x. x ∈ T ==> x ∈ U] ==> P x" for S T by blast have "0 ≤ b" if "b ∈ ℤ" "f x * (2 * 2^n) < b + 1" for b by (smt (verit, ccfv_SIG) Ints_cases f int_le_real_less mult_nonneg_nonneg of_int_add one 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 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" f 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_num also have "… ≤ 2 ^ (2*n)" by (metis that add_leD1 add_le_cancel_left mult.commute mult_2_right one_less_numeral_i 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 show ?thesis using eq by (simp add: dist_real_def) 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 lebesgue_on_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 /🪙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 - interpret linear f by fact have "dim {x. f x = 0} ≤ DIM('a)" by (rule dim_subset_UNIV) 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_base) 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 /🪙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 "∀🪙F i in sequentially. 0 ≤ ((λx. ∣d ∙ x∣ - k) ∘ ((λn. α n /🪙R norm (α n)) ∘ ρ) using α kd by (auto simp: field_split_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 /🪙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 /🪙R norm x) ∘ (α ∘ ρ)) <---- 0" by (force simp: tendsto_at_iff_sequentially) then show "(f ∘ (λn. α n /🪙R norm (α n)) ∘ ρ) <---- 0" by (simp add: o_def scale) 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) dim_eq_full UNIV_I eq_0_on_span mem_Collect_eq span_raw_d qed lemma lemma_partial_derivatives: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes "linear f" and lim: "((λx. f (x - a) /🪙R norm (x - a)) ---> 0) (at a within and lb: "∧v. v ≠ 0 ==> (∃k>0. ∀e>0. ∃x ∈ S - {a}. norm(a - x) < e ∧ k * norm(a - x) ≤ shows "f x = 0" proof - have "((λx. f x /🪙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 - 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 * nor 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 ⟶ nor 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 (top_of_set S) (S ∩ ∩ U)] ==> closedin (top_of_set 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} by auto have sets: "S ∩ (∩y∈S. {x ∈ S. norm (y - x) < d ⟶ norm (f y - f x - A *v (y - x)) ≤ e ∈ sets lebesgue" for e A d proof - have clo: "closedin (top_of_set 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 * by (force intro: contf continuous_intros)+ have clo1: "closedin (top_of_set 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 (top_of_set 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 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') proof (clarsimp simp: dist_norm norm_minus_commute) fix y w 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)" by (metis Diff_iff False ‹y ∈ S› d dless empty_iff insert_iff 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 *🪙R axis k (1::re 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 *🪙R axis k (1::real)" and "inj T" "bij T" and invT: "orthogona by (metis UNIV_I b_def T v bij_betw_inv_into_left orthogonal_transformation_inj orthogon 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 su 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 *🪙R axis k 1) ∙ (y - x)∣ = b * ∣inv T y $ k - ?x' $ k∣" for y proof - have "∣T (b *🪙R axis k 1) ∙ (y - x)∣ = ∣(b *🪙R axis k 1) ∙ inv T (y - x)∣" by (metis (no_types, opaque_lifting) 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_po 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 by (metis component_le_norm_cart less_eq_real_def le_less_trans vector_minus_componen 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 field_simps power_diff split: if_split_ 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 intro: content_cball_pos) also have "… = e * content (ball x (min d r))" using ‹r > 0› ‹d > 0› content_ball_conv_unit_ball[of "min d r" "inv T x"] content_ball_conv_unit_ball[of "min d r" x] by (simp add: content_cball_conv_ball) finally show "measure lebesgue ?W < e * content (ball x (min d r))" . qed qed have *: "(∧x. (x ∉ S) ==> (x ∈ T ⟷ x ∈ U)) ==> (T - U) ∪ (U - T) ⊆ S" for S T U :: "(rea 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, opaque_lifting) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_di 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_iff) also have "… = UNIV" proof - have "dim ?CA ≤ CARD('m)" using dim_subset_UNIV[of ?CA] by auto 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) /🪙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) /🪙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_Archimedean 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 qed with ‹strict_mono ρ› show "(γ ∘ ρ) <---- x" by (metis LIMSEQ_subseq_LIMSEQ) show "(λn. ((γ ∘ ρ) n - x) /🪙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) /🪙R norm (γ y - x))∣ - ξ) <---- ∣d ∙ z∣ - ξ" by auto moreover have "∀🪙F i in sequentially. 0 ≤ ∣d ∙ ((γ i - x) /🪙R norm (γ i - x))∣ - ξ" proof (rule eventuallyI) fix n show "0 ≤ ∣d ∙ ((γ n - x) /🪙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) /🪙R norm (γ k - x))" have "∀🪙F k in sequentially. dist (γ k) x < min (δ i) (δ j)" using γx [unfolded tendsto_iff] by (meson min_less_iff_conj δ) then have even: "∀🪙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)" using ij ‹N > 0› by (intro add_mono mult_right_mono) (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) /🪙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: field_split_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) /🪙R norm (γ w - x)) - A j *v ((γ w - x) /🪙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)) *🪙R (f y - (f x + f' x (y - x)))) ---> 0) (a using ‹x ∈ S› assms by (auto simp: has_derivative_within linear_linear) moreover interpret linear "f' x" by fact 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) /🪙R norm (y - x)) ---> 0) ( using tendsto_minus [OF lim_df] by (simp add: field_split_simps) then show "((λy. (matrix (f' x) - B) *v (y - x) /🪙R norm (y - x)) -- proof (rule Lim_transform) have "((λy. ((f y + B *v x - (f x + B *v y)) /🪙R norm (y - x))) -- 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 🚫/2" by (metis divide_pos_pos inverse_eq_divide real_arch_inverse z 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 "∀🪙F k in sequentially. norm (onorm (λy. (A k - B) *v y)) proof (rule eventually_sequentiallyI) fix k :: "nat" assume "0 ≤ k" have "0 ≤ onorm ((*v) (A k - B))" using matrix_vector_mul_bounded_linear by (rule onorm_pos_le) then show "norm (onorm ((*v) (A k - B))) ≤ (∑i∈UNIV. ∑j∈UNIV by (simp add: onorm_le_matrix_component_sum del: vector_mi qed next show "?g <---- 0" using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: qed with ‹e > 0› obtain p where "∧n. n ≥ p ==> ∣onorm ((*v) (A n - B unfolding lim_sequentially by (metis diff_zero dist_real_def d then have pqe2: "\<bar>onorm ((*v) (A (p + q) - B))\<bar> < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y 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) by (metis linear_linear matrix_vector_mul_linear matrix_vector_mult_diff_rdistrib ono 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: field_split_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: field_split_simps algebra_simps) qed qed then show "((λy. (matrix (f' x) - B) *v (y - x) /🪙R norm (y - x) - (f x + f' x (y - x) - f y) /🪙R norm (y - x)) ---> 0) (at x within S)" by (simp add: algebra_simps diff lin_df scalar_mult_eq_scaleR) qed qed (use x in ‹simp; auto simp: not_less›) ultimately have "f' x = (*v) B" by (force simp: algebra_simps scalar_mult_eq_scaleR) 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 "∀🪙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›] by (simp add: Deriv.has_derivative_at_within Lim_within) (auto simp add: 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 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" fo 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 - by (simp add: 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 (rule le_onorm) auto 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: field_split_simps False) have "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) = norm ((χ i j by (simp add: algebra_simps) also have "… = norm((e/4) *🪙R (y - x)$n *🪙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 * 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) *🪙R (y - by (auto simp: vec_eq_iff matrix_vector_mult_def) then show ?thesis by metis qed also have "… ≤ e * norm (y - x) / 4" proof - have "∣y $ n - x $ n∣ ≤ norm (y - x)" by (metis component_le_norm_cart vector_minus_component) with ‹e > 0› show ?thesis by (simp add: norm_mult abs_mult) qed finally show "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) ≤ e * 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 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 wi 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.*) theorem 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} ∈ se 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_if [OF assms, sym by blast qed lemma sets_lebesgue_almost_borel: assumes "S ∈ sets lebesgue" obtains B N where "B ∈ sets borel" "negligible N" "B ∪ N = S" by (metis assms negligible_iff_null_sets negligible_subset null_sets_completionI sets_ 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 subsection‹Simplest case of Sard's theorem (we don't need continuity of derivati lemma Sard_lemma00: fixes P :: "'b::euclidean_space set" assumes "a ≥ 0" and a: "a *🪙R i ≠ 0" and i: "i ∈ Basis" and P: "P ⊆ {x. a *🪙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) *🪙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\_MULTIP 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 *🪙R axis 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 *🪙R axis k 1 ∙ x = 0" if "T x ∈ P" for x by (smt (verit, del_insts) P T a mem_Collect_eq orthogonal_transformation_def subset_eq th then show "T -` P ⊆ {x. norm a *🪙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 -` 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" by (smt (verit, del_insts) T Tinv 🍋 linear_diff orthogonal_transformation_def orthogonal 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 text‹As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TA 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_base 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 D where D: "countable D" and sub_cc: "∪D ⊆ cbox (- vec c) (vec c)" and cbox: "∧K. K ∈ D ==> interior K ≠ {} ∧ (∃u v. K = cbox u v)" and djointish: "pairwise (λA B. interior A ∩ interior B = {}) D" and covered: "∧K. K ∈ D ==> ∃x ∈ S ∩ K. K ⊆ ball x (r x)" and close: "∧u v. cbox u v ∈ D ==> ∃n. ∀i::'m. v $ i - u $ i = 2*c / 2^n" and covers: "S ⊆ ∪D" 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 ∈ D" for K proof - obtain u v where uv: "K = cbox u v" using cbox ‹K ∈ D› 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 ∈ D› covered uv by blast then have "dim (range (f' x)) < ?n" using rank_dim_range [of "matrix (f' x)"] x rank[of x] by (auto simp: matrix_works scalar_mult_eq_scaleR lin_f') 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 and measT: "?μ T ≤ (2 * (d * norm(v - u))) * (2 * ((2 * B) * norm(v - u))) ^ (?n - (is "_ ≤ ?DVU") using Sard_lemma1 [of "range (f' x)" "(2 * B) * norm(v - u)" "d * norm(v - u)"] using ‹B > 0› ‹d > 0› by auto show ?thesis proof (intro exI conjI) have "f ` (K ∩ S) ⊆ {z. norm(z - f x) ≤ (2 * B) * norm(v - u) ∧ (∃t ∈ range (f' x 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 "norm ((y - x) $ i) ≤ norm ((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)" by (meson B IntE lin_f' linear_linear mult_mono' norm_ge_zero onorm_pos_le x(1) yx_le) 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)" by (smt (verit, best) ‹0 🚫› le_dyx mult_le_cancel_left_pos yx_le) 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) 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, opaque_lifting) dist_commute dist_norm less_eq_real_def less_le_tr 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 ∈ D› 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: field_split_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 ∈ D ==> g K ∈ lmeasurable" and sub_g: "∧K. K ∈ D ==> f ` (K ∩ S) ⊆ g K" and le_g: "∧K. K ∈ D ==> ?μ (g K) ≤ e / (2*c)^?m * ?μ K" by metis have le_e: "?μ (∪i∈F. g i) ≤ e" if "F ⊆ D" "finite F" for F proof - have "?μ (∪i∈F. g i) ≤ (∑i∈F. ?μ (g i))" using meas_g ‹F ⊆ D› by (auto intro: measure_UNION_le [OF ‹finite F›]) also have "… ≤ (∑K∈F. e / (2*c) ^ ?m * ?μ K)" using ‹F ⊆ D› sum_mono [OF le_g] by (meson le_g subsetCE sum_mono) also have "… = e / (2*c) ^ ?m * (∑K∈F. ?μ K)" by (simp add: sum_distrib_left) also have "… ≤ e" proof - have "F division_of ∪F" proof (rule division_ofI) show "K ⊆ ∪F" "K ≠ {}" "∃a b. K = cbox a b" if "K ∈ F" for K using ‹K ∈ F› covered cbox ‹F ⊆ D› by (auto simp: Union_upper) show "interior K ∩ interior L = {}" if "K ∈ F" and "L ∈ F" and "K ≠ L" for K L by (metis (mono_tags, lifting) ‹F ⊆ D› pairwiseD djointish pairwise_subset that) qed (use that in auto) then have "sum ?μ F ≤ ?μ (∪F)" by (simp add: content_division) also have "… ≤ ?μ (cbox (- vec c) (vec c) :: (real, 'm) vec set)" proof (rule measure_mono_fmeasurable) show "∪F ⊆ cbox (- vec c) (vec c)" by (meson Sup_subset_mono sub_cc order_trans ‹F ⊆ D›) qed (use ‹F division_of ∪F› 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 ?μ F ≤ (2 ^ ?m * c ^ ?m)" . then show ?thesis using ‹e > 0› ‹c > 0› by (auto simp: field_split_simps) qed finally show ?thesis . qed show "∃T. f ` S ⊆ T ∧ T ∈ lmeasurable ∧ ?μ T ≤ e" proof (intro exI conjI) show "f ` S ⊆ ∪ (g ` D)" using covers sub_g by force show "∪ (g ` D) ∈ lmeasurable" by (rule fmeasurable_UN_bound [OF ‹countable D› meas_g le_e]) show "?μ (∪ (g ` D)) ≤ e" by (rule measure_UN_bound [OF ‹countable D› 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 lebe 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 se 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 (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))" proof - have "(λv. det (matrix (g' v))) ∈ borel_measurable (lebesgue_on (S ∩ {v. h n (g v) by (metis Int_lower1 S assms(4) borel_measurable_det_Jacobian measurable_restrict_mono then show ?thesis by (simp add: Int_commute) qed then have "(λx. if x ∈ {t. h n (g t) = y} ∩ S then ?D x else 0) ∈ borel_measurable 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 (leb by (simp add: if_if_eq_conj Int_commute borel_measurable_if [OF S, symmetric]) show "(λx. ?D x *🪙R f (g x) /🪙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 *🪙R f (g x) /🪙R 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 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} ∩ using integrable_restrict_Int by force have "(g ` ({t. h n (g t) = y} ∩ S)) ∈ lmeasurable" by (blast intro: has_derivative_subset [OF der_g] measurable_differentiable_image [OF h_ 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))∣)" by (blast intro: has_derivative_subset [OF der_g] measure_differentiable_image [OF h_lme ultimately show ?thesis using ‹y > 0› integral_restrict_Int [of S "{t. h n (g t) = y}" "λt. ∣det (matrix (g' t apply (simp add: integrable_on_indicator integral_indicator) apply (simp add: indicator_def of_bool_def if_distrib cong: if_cong) done qed show ?thesis proof show "h n integrable_on g ` S" apply (subst hn_eq) using yind by (force intro: integrable_sum [OF fin_R]) have "?lhs = integral (g ` S) (λx. ∑y∈range (h n). y * indicat_real {x. h n x = y} by (metis hn_eq) also have "… = (∑y∈range (h n). integral (g ` S) (λx. y * indicat_real {x. h n 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 using yind by (force intro: sum_mono) also have "… = integral S (λu. ∑y∈range (h n). ∣det (matrix (g' u))∣ * y * indicat_ 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)) integrab 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_restri then show "(λu. ∣det (matrix (g' u))∣ * y * indicat_real {x. h n x = y} (g u)) ∈ bo by (intro borel_measurable_times borel_measurable_abs borel_measurable_const borel_me next fix x assume "x ∈ S" then have "y * indicat_real {x. h n x = y} (g x) ≤ f (g x)" by (metis (full_types) h_le_f indicator_simps mem_Collect_eq mult.right_neutral mult_ze with ‹y ≥ 0› show "norm (?D x * y * indicat_real {x. h n x = y} (g x)) ≤ ?D x * f( 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))∣ *🪙R h n (g T)) ∈ borel_measurable (lebesgue_on S proof (intro borel_measurable_scaleR borel_measurable_abs borel_measurable_det_Jacob have eq: "{x ∈ S. f x ≤ a} = (∪b ∈ (f ` S) ∩ atMost a. {x. f x = b} ∩ S)" for f and a: 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› 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 by simp show "norm (?D x * h n (g x)) ≤ ?D x *🪙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) 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 (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_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 using integrable_imp_measurable lebesgue_on_UNIV_eq by force 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 lebesgue_on_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_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) /🪙R ∣?D x∣" have "(λx. if x ∈ S' then ∣?D x∣ * f (g x) else 0) = (λx. if x ∈ S then ∣?D x∣ * f 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 "(λv. det (matrix (g' v))) ∈ borel_measurable (lebesgue_on S')" using S' borel_measurable_det_Jacobian der_gS' by blast then have "?h ∈ borel_measurable (lebesgue_on S')" using "*" borel_measurable_abs borel_measurable_inverse borel_measurable_scaleR by bla 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_restri 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_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" fo 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 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_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" using negg null by (auto intro: integrable_spike_set [OF _ empty_imp_negligible negligible_subset]) 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 using integrable_imp_measurable lebesgue_on_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_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_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]) show "?D integrable_on ?P" proof (rule integrable_spike_set) show "?D integrable_on {x ∈ S. 0 < ?D x}" using Dgt by (auto intro: set_lebesgue_integral_eq_integral [OF set_integrable_subset] intS) qed (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 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))∣ *🪙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_r 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 ge the first that the transforming function has a continuous inverse, the second th 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" by (metis der_g der_h gh has_derivative_linear local.id matrix_compose matrix_id_mat_1 th 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" by (smt (verit, del_insts) abs_absolutely_integrableI_1 ddf f0 fT integrable_eq) 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) finally show "integral S (λx. ?D x) ≤ b" using intf by linarith 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 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( have "+": "(?DP has_integral b) {x ∈ S. f (g x) > 0} ⟷ (f has_integral b) {y ∈ T. 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 using that der_g has_derivative_subset by fastforce show "(h has_derivative h' y) (at y within {y ∈ T. f y > 0})" if "y ∈ {y ∈ T. f y > using that der_h has_derivative_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 ∈ 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) using that der_g has_derivative_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_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 using integrable_imp_measurable lebesgue_on_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_neg 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_neglig 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}" proof (rule absolutely_integrable_integrable_bound) show "(λx. - f x) integrable_on {y ∈ T. f y < 0}" using fN by (auto simp: integrable_neg_iff) qed (use fN in auto) 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}" using fP(1) nonnegative_absolutely_integrable_1 by fastforce 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 of_bool_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 U using integrable_imp_measurable lebesgue_on_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) 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 of_bool_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))∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣det (matrix (g' x))∣ *🪙R f(g x)) = b ⟷ f absolutely_integrable_on T ∧ integral T f = b" proof - let ?D = "λx. ∣det (matrix (g' x))∣ *🪙R f(g x)" have "((λx. ∣det (matrix (g' x))∣ * f(g x) $ i) absolutely_integrable_on S ∧ integ ((λ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_component absolutely_integrable_componentwise_iff [where f="?D"] has_integral_componentwise_i 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 and hg: "∧x. x ∈ S ==> continuous_on (g ` S) h ∧ h(g x) = x" shows "(λx. ∣det (matrix (g' x))∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣det (matrix (g' x))∣ *🪙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' 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_wit qed (use h' hg in auto) qed theorem 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))∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integr 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))∣ *🪙R 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_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" by (metis (no_types, lifting) der_g has_derivative_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 theorem 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))∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣det (matrix (g' x))∣ *🪙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))∣ *🪙R f(g x)) absolutely_integrable_on (∪n. F n) integral (∪n. F n) (λx. ∣det (matrix (g' x))∣ *🪙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))∣ *🪙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))∣ *🪙R f (g x)) absolutely_integrable_on (?U n) integral (?U n) (λx. ∣det (matrix (g' x))∣ *🪙R f (g x)) = b ⟷ f absolutely_integrable_on (g ` (?U n)) ∧ integral (g ` (?U n)) f = b" for n b and 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_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" f 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))∣ *🪙R (?li 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 ∈ ∪ (F ` {..k}) 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: tendsto_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: tendsto_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 r qed auto qed qed (use DU in metis) 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_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)" using absolutely_integrable_norm 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 by (force intro: tendsto_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!: tendsto_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 (∪n. F n) ?D" unfolding D_int [symmetric] by (rule integral_countable_UN [OF Dai F_leb]) qed (use fgU in metis) qed qed theorem 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))∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣det (matrix (g' x))∣ *🪙R f(g x)) = b ⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b" proof - obtain C N where "fsigma C" and N: "N ∈ null_sets lebesgue" and CNS: "C ∪ N = S" and "disjnt 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 have "negligible N" using N by (simp add: negligible_iff_null_sets) let ?D = "λx. ∣det (matrix (g' x))∣ *🪙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 ∈ ∪(F ` UNIV)" then show "(g has_derivative g' x) (at x within ∪(F ` UNIV))" using Ceq ‹C ∪ N = S› der_g has_derivative_subset by blast next have "∪(F ` UNIV) ⊆ S" using Ceq ‹C ∪ N = S› by blast then show "inj_on g (∪(F ` UNIV))" 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 s 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))∣ *🪙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))∣ *🪙R f(g x)) absolutely_integrable_on S)" shows "integral (g ` S) f = integral S (λx. ∣det (matrix (g' x))∣ *🪙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∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣g' x∣ *🪙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 (*🪙R) (g' z)) (at (vec z) within ?lif 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 (*🪙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∣ *🪙R f(g x)" have "((λx. ?fg x $ i) absolutely_integrable_on S ∧ ((λx. ?fg x $ i) has_integral b ⟷ (λx. f x $ i) absolutely_integrable_on g ` S ∧ ((λx. f x $ i) has_integral b $ i using has_absolute_integral_change_of_variables [OF S' der' inj', of "λx. ?lift(f (?drop unfolding integrable_on_1_iff integral_on_1_eq absolutely_integrable_on_1_iff absolu 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∣ *🪙R f(g x)) absolutely_integrable_on S)" using has_absolute_integral_change_of_variables_1 [OF assms] by auto text ‹when @{term "n=1"}› lemma has_absolute_integral_change_of_variables_1': fixes f :: "real ==> real" and g :: "real ==> real" assumes S: "S ∈ sets lebesgue" and der_g: "∧x. x ∈ S ==> (g has_field_derivative g' x) (at x within S)" and inj: "inj_on g S" shows "(λx. ∣g' x∣ * f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣g' x∣ * f (g x)) = b ⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b" proof - have "(λx. ∣g' x∣ *🪙R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S ∧ integral S (λx. ∣g' x∣ *🪙R vec (f(g x))) = (vec b :: real ^ 1) ⟷ (λx. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) ∧ integral (g ` S) (λx. vec (f x)) = (vec b :: real ^ 1)" using assms unfolding has_real_derivative_iff_has_vector_derivative by (intro has_absolute_integral_change_of_variables_1 assms) auto thus ?thesis by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq) qed 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)∣ *🪙R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ∣det (matrix g)∣ *🪙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 metis 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_d 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)∣ *🪙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 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)∣ *🪙R integral S (f ∘ g)" proof - have "((λx. ∣det (matrix g)∣ *🪙R f (g x)) absolutely_integrable_on S) ∨ (f absolu using absolutely_integrable_on_linear_image assms by blast moreover have ?thesis if "((λx. ∣det (matrix g)∣ *🪙R f (g x)) absolutely_integrable_on 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 lemma absolutely_integrable_change_of_variables_1': fixes f :: "real ==> real" and g :: "real ==> real" assumes "S ∈ sets lebesgue" assumes "∧x. x ∈ S ==> (g has_field_derivative h x) (at x within S)" assumes "inj_on g S" shows "f absolutely_integrable_on g ` S ⟷ (λx. ∣h x∣ * f (g x)) absolutely_integra using has_absolute_integral_change_of_variables_1'[of S g h f] assms by auto lemma absolutely_integrable_change_of_variables_real: fixes f :: "real ==> 'a :: euclidean_space" and g :: "real ==> real" assumes "S ∈ sets lebesgue" assumes "∧x. x ∈ S ==> (g has_field_derivative h x) (at x within S)" assumes "inj_on g S" shows "f absolutely_integrable_on g ` S ⟷ (λx. ∣h x∣ *🪙R f (g x)) absolutely_inte proof - have "(λx. ∣h x∣ *🪙R f (g x)) absolutely_integrable_on S ⟷ (∀a∈Basis. (λx. ∣h x∣ * (f (g x) ∙ a)) absolutely_integrable_on S)" by (subst absolutely_integrable_componentwise_iff) simp_all also have "… = (∀a∈Basis. (λx. f x ∙ a) absolutely_integrable_on g ` S)" by (intro ball_cong absolutely_integrable_change_of_variables_1' [symmetric] assms ref also have "… ⟷ f absolutely_integrable_on g ` S" by (subst absolutely_integrable_componentwise_iff) (simp_all add: Basis_complex_def) finally show ?thesis .. qed lemma has_absolute_integral_change_of_variables_real: fixes f :: "real ==> 'a :: euclidean_space" and g :: "real ==> real" assumes "S ∈ sets lebesgue" assumes "∧x. x ∈ S ==> (g has_field_derivative h x) (at x within S)" assumes "inj_on g S" shows "(λx. ∣h x∣ *🪙R f (g x)) absolutely_integrable_on S ∧ integral S (λx. ∣h x∣ ⟷ f absolutely_integrable_on g ` S ∧ integral (g ` S) f = b" proof (intro conj_cong) show iff: "(λx. ∣h x∣ *🪙R f (g x)) absolutely_integrable_on S ⟷ f absolutely_integrable_on g ` S" by (rule sym, rule absolutely_integrable_change_of_variables_real) fact+ assume "f absolutely_integrable_on g ` S" hence integrable: "f integrable_on g ` S" "(λx. ∣h x∣ *🪙R f (g x)) integrable_on S" using set_lebesgue_integral_eq_integral(1) iff by metis+ have "(λx. ∣h x∣ *🪙R f (g x)) absolutely_integrable_on S ∧ (integral S (λx. ∣h x∣ *🪙R f (g x)) = b) ⟷ (∀a∈Basis. (λx. (∣h x∣ *🪙R f (g x)) ∙ a) absolutely_integrable_on S ∧ (integral S (λx. (∣h x∣ *🪙R f (g x)) ∙ a) = b ∙ a))" by (subst absolutely_integrable_componentwise_iff, subst integral_eq_iff_componentwi (use integrable in auto) also have "… ⟷ (∀a∈Basis. (λx. ∣h x∣ * (f (g x) ∙ a)) absolutely_integrable_on S ∧ (integral S (λx. ∣h x∣ * (f (g x) ∙ a)) = b ∙ a))" by simp also have "… ⟷ (∀a∈Basis. (λx. f x ∙ a) absolutely_integrable_on g ` S ∧ (integral (g ` S) (λx. f x ∙ a) = b ∙ a))" by (intro ball_cong has_absolute_integral_change_of_variables_1' assms refl) also have "… ⟷ f absolutely_integrable_on g ` S ∧ integral (g ` S) f = b" by (subst (2) absolutely_integrable_componentwise_iff, subst (2) integral_eq_iff_compo (use integrable in auto) finally show "(integral S (λx. ∣h x∣ *🪙R f (g x)) = b) = (integral (g ` S) f = b)" using ‹f absolutely_integrable_on g ` S› iff 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 absolu 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 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 lemma has_absolute_integral_reflect_real: fixes f :: "real ==> real" assumes "uminus ` A ⊆ B" "uminus ` B ⊆ A" "A ∈ sets lebesgue" shows "(λx. f (-x)) absolutely_integrable_on A ∧ integral A (λx. f (-x)) = b ⟷ f absolutely_integrable_on B ∧ integral B f = b" proof - have bij: "bij_betw uminus A B" by (rule bij_betwI[of _ _ _ uminus]) (use assms in auto) have "((λx. ∣-1∣ * f (-x)) absolutely_integrable_on A ∧ integral A (λx. ∣-1∣ * f (-x)) = b) ⟷ (f absolutely_integrable_on uminus ` A ∧ integral (uminus ` A) f = b)" using assms by (intro has_absolute_integral_change_of_variables_1') (auto intro!: derivative_eq_i also have "uminus ` A = B" using bij by (simp add: bij_betw_def) finally show ?thesis by simp qed end
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.250Bemerkung: (vorverarbeitet am 2026-05-03) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26