# Theory Change_Of_Vars

```(*  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) ` (cbox a b) ∈ lmeasurable"
(is  "?f ` _ ∈ _")
and measure_shear_interval: "measure lebesgue ((λx. χ i. if i = m then x\$m + x\$n else x\$i) ` cbox a b)
= measure lebesgue (cbox a b)" (is "?Q")
proof -
have lin: "linear ?f"
by (rule linearI) (auto simp: plus_vec_def scaleR_vec_def algebra_simps)
show fab: "?f ` cbox a b ∈ lmeasurable"
let ?c = "χ i. if i = m then b\$m + b\$n else b\$i"
let ?mn = "axis m 1 - axis n (1::real)"
have eq1: "measure lebesgue (cbox a ?c)
= measure lebesgue (?f ` cbox a b)
+ measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≤ a\$m})
+ measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m})"
proof (rule measure_Un3_negligible)
show "cbox a ?c ∩ {x. ?mn ∙ x ≤ a\$m} ∈ lmeasurable" "cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m} ∈ lmeasurable"
by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
have "negligible {x. ?mn ∙ x = a\$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "?f ` cbox a b ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m}) ⊆ {x. ?mn ∙ x = a\$m}"
using ‹m ≠ n› antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
ultimately show "negligible ((?f ` cbox a b) ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m}))"
by (rule negligible_subset)
have "negligible {x. ?mn ∙ x = b\$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "(?f ` cbox a b) ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m}) ⊆ {x. ?mn ∙ x = b\$m}"
using ‹m ≠ n› antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
ultimately show "negligible (?f ` cbox a b ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m}))"
by (rule negligible_subset)
have "negligible {x. ?mn ∙ x = b\$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "(cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m} ∩ (cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m})) ⊆ {x. ?mn ∙ x = b\$m}"
using ‹m ≠ n› ab_ne
apply (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. ?mn ∙ x ≥ b\$m}))"
by (rule negligible_subset)
show "?f ` cbox a b ∪ cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m} ∪ cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m} = cbox a ?c" (is "?lhs = _")
proof
show "?lhs ⊆ cbox a ?c"
show "cbox a ?c ⊆ ?lhs"
apply (clarsimp simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF ‹m ≠ n›])
by (smt (verit, del_insts) mem_box_cart(2) vec_lambda_beta)
qed
qed (fact fab)
let ?d = "χ i. if i = m then a \$ m - b \$ m else 0"
have eq2: "measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m}) + measure lebesgue (cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m})
= measure lebesgue (cbox a (χ i. if i = m then a \$ m + b \$ n else b \$ i))"
proof (rule measure_translate_add[of "cbox a ?c ∩ {x. ?mn ∙ x ≤ a\$m}" "cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m}"
"(χ i. if i = m then a\$m - b\$m else 0)" "cbox a (χ i. if i = m then a\$m + b\$n else b\$i)"])
show "(cbox a ?c ∩ {x. ?mn ∙ x ≤ a\$m}) ∈ lmeasurable"
"cbox a ?c ∩ {x. ?mn ∙ x ≥ b\$m} ∈ lmeasurable"
by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
have "⋀x. ⟦x \$ n + a \$ m ≤ x \$ m⟧
⟹ x ∈ (+) (χ i. if i = m then a \$ m - b \$ m else 0) ` {x. x \$ n + b \$ m ≤ x \$ m}"
using ‹m ≠ n›
by (rule_tac x="x - (χ i. if i = m then a\$m - b\$m else 0)" in image_eqI)
then have imeq: "(+) ?d ` {x. b \$ m ≤ ?mn ∙ x} = {x. a \$ m ≤ ?mn ∙ x}"
using ‹m ≠ n› by (auto simp: mem_box_cart inner_axis' algebra_simps)
have "⋀x. ⟦0 ≤ a \$ n; x \$ n + a \$ m ≤ x \$ m;
∀i. i ≠ m ⟶ a \$ i ≤ x \$ i ∧ x \$ i ≤ b \$ i⟧
⟹ a \$ m ≤ x \$ m"
using ‹m ≠ n›  by force
then have "(+) ?d ` (cbox a ?c ∩ {x. b \$ m ≤ ?mn ∙ x})
= cbox a (χ i. if i = m then a \$ m + b \$ n else b \$ i) ∩ {x. a \$ m ≤ ?mn ∙ x}"
using an ab_ne
apply (simp add: cbox_translation [symmetric] translation_Int interval_ne_empty_cart imeq)
apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib)
then show "cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m} ∪
(+) ?d ` (cbox a ?c ∩ {x. b \$ m ≤ ?mn ∙ x}) =
cbox a (χ i. if i = m then a \$ m + b \$ n else b \$ i)"  (is "?lhs = ?rhs")
using an ‹m ≠ n›
apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib, force)
apply (drule_tac x=n in spec)+
by (meson ab_ne add_mono_thms_linordered_semiring(3) dual_order.trans interval_ne_empty_cart(1))
have "negligible{x. ?mn ∙ x = a\$m}"
by (metis ‹m ≠ n› axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
moreover have "(cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m} ∩
(+) ?d ` (cbox a ?c ∩ {x. b \$ m ≤ ?mn ∙ x})) ⊆ {x. ?mn ∙ x = a\$m}"
using ‹m ≠ n› antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
ultimately show "negligible (cbox a ?c ∩ {x. ?mn ∙ x ≤ a \$ m} ∩
(+) ?d ` (cbox a ?c ∩ {x. b \$ m ≤ ?mn ∙ x}))"
by (rule negligible_subset)
qed
have ac_ne: "cbox a ?c ≠ {}"
by (smt (verit, del_insts) ab_ne an interval_ne_empty_cart(1) vec_lambda_beta)
have ax_ne: "cbox a (χ i. if i = m then a \$ m + b \$ n else b \$ i) ≠ {}"
using ab_ne an
by (smt (verit, ccfv_threshold) interval_ne_empty_cart(1) vec_lambda_beta)
have eq3: "measure lebesgue (cbox a ?c) = measure lebesgue (cbox a (χ i. if i = m then a\$m + b\$n else b\$i)) + measure lebesgue (cbox a b)"
by (simp add: content_cbox_if_cart ab_ne ac_ne ax_ne algebra_simps prod.delta_remove
if_distrib [of "λu. u - z" for z] prod.remove)
show ?Q
using eq1 eq2 eq3 by (simp add: algebra_simps)
qed

proposition
fixes S :: "(real^'n) set"
assumes "S ∈ lmeasurable"
shows measurable_stretch: "((λx. χ k. m k * x\$k) ` S) ∈ lmeasurable" (is  "?f ` S ∈ _")
and measure_stretch: "measure lebesgue ((λx. χ k. m k * x\$k) ` S) = ¦prod m UNIV¦ * measure lebesgue S"
(is "?MEQ")
proof -
have "(?f ` S) ∈ lmeasurable ∧ ?MEQ"
proof (cases "∀k. m k ≠ 0")
case True
have m0: "0 < ¦prod m UNIV¦"
using True by simp
have "(indicat_real (?f ` S) has_integral ¦prod m UNIV¦ * measure lebesgue S) UNIV"
proof (clarsimp simp add: has_integral_alt [where i=UNIV])
fix e :: "real"
assume "e > 0"
have "(indicat_real S has_integral (measure lebesgue S)) UNIV"
using assms lmeasurable_iff_has_integral by blast
then obtain B where "B>0"
and B: "⋀a b. ball 0 B ⊆ cbox a b ⟹
∃z. (indicat_real S has_integral z) (cbox a b) ∧
¦z - measure lebesgue S¦ < e / ¦prod m UNIV¦"
by (simp add: has_integral_alt [where i=UNIV]) (metis (full_types) divide_pos_pos m0  m0 ‹e > 0›)
show "∃B>0. ∀a b. ball 0 B ⊆ cbox a b ⟶
(∃z. (indicat_real (?f ` S) has_integral z) (cbox a b) ∧
¦z - ¦prod m UNIV¦ * measure lebesgue S¦ < e)"
proof (intro exI conjI allI)
let ?C = "Max (range (λk. ¦m k¦)) * B"
show "?C > 0"
using True ‹B > 0› by (simp add: Max_gr_iff)
show "ball 0 ?C ⊆ cbox u v ⟶
(∃z. (indicat_real (?f ` S) has_integral z) (cbox u v) ∧
¦z - ¦prod m UNIV¦ * measure lebesgue S¦ < e)" for u v
proof
assume uv: "ball 0 ?C ⊆ cbox u v"
with ‹?C > 0› have cbox_ne: "cbox u v ≠ {}"
using centre_in_ball by blast
let ?α = "λk. u\$k / m k"
let ?β = "λk. v\$k / m k"
have invm0: "⋀k. inverse (m k) ≠ 0"
using True by auto
have "ball 0 B ⊆ (λx. χ k. x \$ k / m k) ` ball 0 ?C"
proof clarsimp
fix x :: "real^'n"
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 < B› 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)) (χ k. max (?α k) (?β k)))"
and zless: "¦z - measure lebesgue S¦ < e / ¦prod m UNIV¦"
using B [OF Bsub] by blast
have ind: "indicat_real (?f ` S) = (λx. indicator S (χ k. x\$k / m k))"
using True stretch_Galois [of m] by (force simp: indicator_def)
show "∃z. (indicat_real (?f ` S) has_integral z) (cbox u v) ∧
¦z - ¦prod m UNIV¦ * measure lebesgue S¦ < e"
proof (simp add: ind, intro conjI exI)
have "((λx. indicat_real S (χ k. x \$ k/ m k)) has_integral z *⇩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"]
moreover have "((λx. χ k. x \$ k * m k) ` cbox (χ k. min (?α k) (?β k)) (χ k. max (?α k) (?β k))) = cbox u v"
using True image_stretch_interval_cart [of "inverse ∘ m" u v, symmetric]
image_stretch_interval_cart [of "λk. 1" u v, symmetric] ‹cbox u v ≠ {}›
by (simp add: field_simps image_comp o_def)
ultimately show "((λx. indicat_real S (χ k. x \$ k/ m k)) has_integral z *⇩R ¦prod m UNIV¦) (cbox u v)"
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 right_diff_distrib')
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 measurable_integrable)
next
case False
then obtain k where "m k = 0" and prm: "prod m UNIV = 0"
by auto
have nfS: "negligible (?f ` S)"
by (rule negligible_subset [OF negligible_standard_hyperplane_cart]) (use ‹m k = 0› in auto)
then show ?thesis
qed
then show "(?f ` S) ∈ lmeasurable" ?MEQ
by metis+
qed

proposition
fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n::_"
assumes "linear f" "S ∈ lmeasurable"
shows measurable_linear_image: "(f ` S) ∈ lmeasurable"
and measure_linear_image: "measure lebesgue (f ` S) = ¦det (matrix f)¦ * measure lebesgue S" (is "?Q f S")
proof -
have "∀S ∈ lmeasurable. (f ` S) ∈ lmeasurable ∧ ?Q f S"
proof (rule induct_linear_elementary [OF ‹linear f›]; intro ballI)
fix f g and S :: "(real,'n) vec set"
assume "linear f" and "linear g"
and f [rule_format]: "∀S ∈ lmeasurable. f ` S ∈ lmeasurable ∧ ?Q f S"
and g [rule_format]: "∀S ∈ lmeasurable. g ` S ∈ lmeasurable ∧ ?Q g S"
and S: "S ∈ lmeasurable"
then have gS: "g ` S ∈ lmeasurable"
by blast
show "(f ∘ g) ` S ∈ lmeasurable ∧ ?Q (f ∘ g) S"
using f [OF gS] g [OF S] matrix_compose [OF ‹linear g› ‹linear f›]
by (simp add: o_def image_comp abs_mult det_mul)
next
fix f :: "real^'n::_ ⇒ 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_component)
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 negligible_linear_singular_image by blast
have "measure lebesgue (f ` S) = 0"
by (meson ‹¬ inj f› ‹linear f› negligible_imp_measure0 negligible_linear_singular_image)
also have "… = ¦det (matrix f)¦ * measure lebesgue S"
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_diagonal)
qed
next
fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
assume "m ≠ n" and "S ∈ lmeasurable"
let ?h = "λv::(real, 'n) vec. χ i. v \$ Transposition.transpose m n i"
have lin: "linear ?h"
by (rule linearI) (simp_all add: plus_vec_def scaleR_vec_def)
have meq: "measure lebesgue ((λv::(real, 'n) vec. χ i. v \$ Transposition.transpose m n i) ` cbox a b)
= measure lebesgue (cbox a b)" for a b
proof (cases "cbox a b = {}")
case True 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 = Transposition.transpose m n i then 1 else (0::real))"
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 \$ j = (0::real)"
using ‹j < i› axis_def ‹m < n› by auto
with ‹m < n› show ?thesis
by (auto simp: matrix_def axis_def cong: if_cong)
qed
show ?thesis
using ‹m ≠ n› by (subst det_upperdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong)
next
assume "n < m"
have *: "matrix ?h \$ i \$ j = (0::real)" if "j > i" for i j :: 'n
proof -
have "axis j 1 = (χ n. if n = j then 1 else (0::real))"
using axis_def by blast
then have "(χ p q. if p = m then axis q 1 \$ m + axis q 1 \$ n else axis q 1 \$ p) \$ i \$ j = (0::real)"
using ‹j > i› axis_def ‹m > n› by auto
with ‹m > n› show ?thesis
by (auto simp: matrix_def axis_def cong: if_cong)
qed
show ?thesis
using ‹m ≠ n›
by (subst det_lowerdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong)
qed
have meq: "measure lebesgue (?h ` (cbox a b)) = measure lebesgue (cbox a b)" for a b
proof (cases "cbox a b = {}")
case True then show ?thesis by simp
next
case False
then have ne: "(+) (χ i. if i = n then - a \$ n else 0) ` cbox a b ≠ {}"
by auto
let ?v = "χ i. if i = n then - a \$ n else 0"
have "?h ` cbox a b
= (+) (χ i. if i = m ∨ i = n then a \$ n else 0) ` ?h ` (+) ?v ` (cbox a b)"
using ‹m ≠ n› unfolding image_comp o_def by (force simp: vec_eq_iff)
then have "measure lebesgue (?h ` (cbox a b))
= measure lebesgue ((λv. χ i. if i = m then v \$ m + v \$ n else v \$ i) `
(+) ?v ` cbox a b)"
by (rule ssubst) (rule measure_translation)
also have "… = measure lebesgue ((λv. χ i. if i = m then v \$ m + v \$ n else v \$ i) ` cbox (?v +a) (?v + b))"
by (metis (no_types, lifting) cbox_translation)
also have "… = measure lebesgue ((+) ?v ` cbox a b)"
apply (subst measure_shear_interval)
using ‹m ≠ n› ne apply auto
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"
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 - frontier S) < e"
by (metis fmeasurableD)
with null have "U ∈ lmeasurable"
by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel)
have "measure lebesgue (U - frontier S) = measure lebesgue U"
using mS0 by (simp add: ‹U ∈ lmeasurable› fmeasurableD measure_Diff_null_set null)
with U have mU: "measure lebesgue U < e"
show ?thesis
proof
have "U ≠ UNIV"
using ‹U ∈ lmeasurable› by auto
then have "- U ≠ {}"
by blast
with ‹open U› ‹frontier S ⊆ U› show "setdist (frontier S) (- U) > 0"
by (auto simp: ‹bounded S› open_closed compact_frontier_bounded setdist_gt_0_compact_closed frS)
fix T
assume "T ∈ lmeasurable"
and T: "⋀t. t ∈ T ⟹ ∃y. y ∈ S ∧ dist y t < setdist (frontier S) (- U)"
then have "measure lebesgue T - measure lebesgue S ≤ measure lebesgue (T - S)"
by (simp add: ‹S ∈ lmeasurable› measure_diff_le_measure_setdiff)
also have "…  ≤ measure lebesgue U"
proof -
have "T - S ⊆ U"
proof clarify
fix x
assume "x ∈ T" and "x ∉ S"
then obtain y where "y ∈ S" and y: "dist y x < setdist (frontier S) (- U)"
using T by blast
have "closed_segment x y ∩ frontier S ≠ {}"
using connected_Int_frontier ‹x ∉ S› ‹y ∈ S› by blast
then obtain z where z: "z ∈ closed_segment x y" "z ∈ frontier S"
by auto
with y have "dist z x < setdist(frontier S) (- U)"
by (auto simp: dist_commute dest!: dist_in_closed_segment)
with z have False if "x ∈ -U"
using setdist_le_dist [OF ‹z ∈ frontier S› that] by auto
then show "x ∈ U"
by blast
qed
then show ?thesis
by (simp add: ‹S ∈ lmeasurable› ‹T ∈ lmeasurable› ‹U ∈ lmeasurable› fmeasurableD measure_mono_fmeasurable sets.Diff)
qed
finally have "measure lebesgue T - measure lebesgue S ≤ measure lebesgue U" .
with mU show "measure lebesgue T < measure lebesgue S + e"
by linarith
qed
qed

proposition
fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n::_"
assumes S: "S ∈ lmeasurable"
and deriv: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and int: "(λx. ¦det (matrix (f' x))¦) integrable_on S"
and bounded: "⋀x. x ∈ S ⟹ ¦det (matrix (f' x))¦ ≤ B"
shows measurable_bounded_differentiable_image:
"f ` S ∈ lmeasurable"
and measure_bounded_differentiable_image:
"measure lebesgue (f ` S) ≤ B * measure lebesgue S" (is "?M")
proof -
have "f ` S ∈ lmeasurable ∧ measure lebesgue (f ` S) ≤ B * measure lebesgue S"
proof (cases "B < 0")
case True
then have "S = {}"
by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI)
then show ?thesis
by auto
next
case False
then have "B ≥ 0"
by arith
let ?μ = "measure lebesgue"
have f_diff: "f differentiable_on S"
using deriv by (auto simp: differentiable_on_def differentiable_def)
have eps: "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ (B+e) * ?μ S" (is "?ME")
if "e > 0" for e
proof -
have eps_d: "f ` S ∈ lmeasurable"  "?μ (f ` S) ≤ (B+e) * (?μ S + d)" (is "?MD")
if "d > 0" for d
proof -
obtain T where T: "open T" "S ⊆ T" and TS: "(T-S) ∈ lmeasurable" and "emeasure lebesgue (T-S) < ennreal d"
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 within S)"
using deriv ‹x ∈ S› by (auto simp: has_derivative_within bounded_linear.linear field_simps)
have bo: "bounded (f' x ` ball 0 1)"
by (simp add: bounded_linear_image linear_linear lin)
have neg: "negligible (frontier (f' x ` ball 0 1))"
using deriv has_derivative_linear ‹x ∈ S›
by (auto intro!: negligible_convex_frontier [OF convex_linear_image])
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"
then have "dist (f' x ((y - x) /⇩R r)) ((f y - f x) /⇩R r) = norm (f' x (y - x) /⇩R r - (f y - f x) /⇩R r)"
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 mult_right_mono)
also have "… < k"
using that ‹0 < ζ› by (simp add: dist_commute r_def  ζ [OF ‹y ∈ S› False])
finally show "dist (f' x ((y - x) /⇩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_lebesgue)
let ?B = "(λ(x, y). x + y) ` (f' x ` ball 0 1 × ball 0 k)"
have "bounded ?B"
by (simp add: bounded_plus [OF bo])
moreover have "?rfs ⊆ ?B"
apply (auto simp: dist_norm image_iff dest!: ex_lessK)
ultimately show "bounded (?rfs)"
by (rule bounded_subset)
qed
then have "(λx. r *⇩R x) ` ?rfs ∈ lmeasurable"
with ‹r > 0› have "(+) (- f x) ` f ` (S ∩ ball x r) ∈ lmeasurable"
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"
have "?μ (f ` (S ∩ ball x r)) = ?μ (?rfs) * r ^ CARD('n)"
using ‹r > 0› fsb
by (simp add: measure_linear_image measure_translation_subtract measurable_translation_subtract field_simps cong: image_cong_simp)
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 order_refl sets.Int differentiable_image_in_sets_lebesgue)
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))"
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.case subset_iff)
also have "… ≤ (B + e) * (?μ S + d)"
using ‹B ≥ 0› ‹e > 0› Tless by simp
finally show ?thesis .
qed
have fSUB_mble: "(f ` (S ∩ ?UB)) ∈ lmeasurable"
unfolding eq using Csub r False ‹e > 0› that
by (auto simp: intro!: fmeasurable_UN_bound [OF ‹countable C› _ mle])
have fSUB_meas: "?μ (f ` (S ∩ ?UB)) ≤ (B + e) * (?μ S + d)"  (is "?MUB")
unfolding eq using Csub r False ‹e > 0› that
by (auto simp: intro!: measure_UN_bound [OF ‹countable C› _ mle])
have neg: "negligible ((f ` (S ∩ ?UB) - f ` S) ∪ (f ` S - f ` (S ∩ ?UB)))"
proof (rule negligible_subset [OF negligible_differentiable_image_negligible [OF order_refl negC, where f=f]])
show "f differentiable_on S - (⋃i∈C. ball (fst i) (snd i))"
by (meson DiffE differentiable_on_subset subsetI f_diff)
qed force
show "f ` S ∈ lmeasurable"
by (rule lmeasurable_negligible_symdiff [OF fSUB_mble neg])
show ?MD
using fSUB_meas measure_negligible_symdiff [OF fSUB_mble neg] by simp
qed
show "f ` S ∈ lmeasurable"
using eps_d [of 1] by simp
show ?ME
proof (rule field_le_epsilon)
fix δ :: real
assume "0 < δ"
then show "?μ (f ` S) ≤ (B + e) * ?μ S + δ"
using eps_d [of "δ / (B+e)"] ‹e > 0› ‹B ≥ 0› by (auto simp: divide_simps mult_ac)
qed
qed
show ?thesis
proof (cases "?μ S = 0")
case True
with eps have "?μ (f ` S) = 0"
by (metis mult_zero_right not_le zero_less_measure_iff)
then show ?thesis
using eps [of 1] by (simp add: True)
next
case False
have "?μ (f ` S) ≤ B * ?μ S"
proof (rule field_le_epsilon)
fix e :: real
assume "e > 0"
then show "?μ (f ` S) ≤ B * ?μ S + e"
using eps [of "e / ?μ S"] False by (auto simp: algebra_simps zero_less_measure_iff)
qed
with eps [of 1] show ?thesis by auto
qed
qed
then show "f ` S ∈ lmeasurable" ?M by blast+
qed

lemma m_diff_image_weak:
fixes f :: "real^'n::{finite,wellorder} ⇒ real^'n::_"
assumes S: "S ∈ lmeasurable"
and deriv: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
and int: "(λx. ¦det (matrix (f' x))¦) integrable_on S"
shows "f ` S ∈ lmeasurable ∧ measure lebesgue (f ` S) ≤ integral S (λx. ¦det (matrix (f' x))¦)"
proof -
let ?μ = "measure lebesgue"
have aint_S: "(λx. ¦det (matrix (f' x))¦) absolutely_integrable_on S"
using int unfolding absolutely_integrable_on_def by auto
define m where "m ≡ integral S (λx. ¦det (matrix (f' x))¦)"
have *: "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ m + e * ?μ S"
if "e > 0" for e
proof -
define T where "T ≡ λn. {x ∈ S. n * e ≤ ¦det (matrix (f' x))¦ ∧
¦det (matrix (f' x))¦ < (Suc n) * e}"
have meas_t: "T n ∈ lmeasurable" for n
proof -
have *: "(λx. ¦det (matrix (f' x))¦) ∈ borel_measurable (lebesgue_on S)"
using aint_S by (simp add: S borel_measurable_restrict_space_iff fmeasurableD set_integrable_def)
have [intro]: "x ∈ sets (lebesgue_on S) ⟹ x ∈ sets lebesgue" for x
using S sets_restrict_space_subset by blast
have "{x ∈ S. real n * e ≤ ¦det (matrix (f' x))¦} ∈ sets lebesgue"
using * by (auto simp: borel_measurable_iff_halfspace_ge space_restrict_space)
then have 1: "{x ∈ S. real n * e ≤ ¦det (matrix (f' x))¦} ∈ lmeasurable"
using S by (simp add: fmeasurableI2)
have "{x ∈ S. ¦det (matrix (f' x))¦ < (1 + real n) * e} ∈ sets lebesgue"
using * by (auto simp: borel_measurable_iff_halfspace_less space_restrict_space)
then have 2: "{x ∈ S. ¦det (matrix (f' x))¦ < (1 + real n) * e} ∈ lmeasurable"
using S by (simp add: fmeasurableI2)
show ?thesis
using fmeasurable.Int [OF 1 2] by (simp add: T_def Int_def cong: conj_cong)
qed
have aint_T: "⋀k. (λx. ¦det (matrix (f' x))¦) absolutely_integrable_on T k"
using set_integrable_subset [OF aint_S] meas_t T_def by blast
have Seq: "S = (⋃n. T n)"
apply (auto simp: T_def)
apply (rule_tac x = "nat ⌊¦det (matrix (f' x))¦ / e⌋" in exI)
by (smt (verit, del_insts) divide_nonneg_nonneg floor_eq_iff of_nat_nat pos_divide_less_eq that zero_le_floor)
have meas_ft: "f ` T n ∈ lmeasurable" for n
proof (rule measurable_bounded_differentiable_image)
show "T n ∈ lmeasurable"
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 subsetI T_def)
show "¦det (matrix (f' x))¦ ≤ (Suc n) * e"
using ‹x ∈ T n› T_def by auto
next
show "(λx. ¦det (matrix (f' x))¦) integrable_on T n"
using aint_T absolutely_integrable_on_def by blast
qed
have disT: "disjoint (range T)"
unfolding disjoint_def
proof clarsimp
show "T m ∩ T n = {}" if "T m ≠ T n" for m n
using that
proof (induction m n rule: linorder_less_wlog)
case (less m n)
with ‹e > 0› show ?case
unfolding T_def
proof (clarsimp simp add: Collect_conj_eq [symmetric])
fix x
assume "e > 0"  "m < n"  "n * e ≤ ¦det (matrix (f' x))¦"  "¦det (matrix (f' x))¦ < (1 + real m) * e"
then have "n < 1 + real m"
by (metis (no_types, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_iff2)
then show "False"
using less.hyps by linarith
qed
qed auto
qed
have injT: "inj_on T ({n. T n ≠ {}})"
unfolding inj_on_def
proof clarsimp
show "m = n" if "T m = T n" "T n ≠ {}" for m n
using that
proof (induction m n rule: linorder_less_wlog)
case (less m n)
have False if "T n ⊆ T m" "x ∈ T n" for x
using ‹e > 0› ‹m < n› that
apply (auto simp: T_def mult.commute intro: less_le_trans dest!: subsetD)
by (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 :: "_ ⇒ real" and n
proof (subst sum.reindex_nontrivial)
fix i j  assume "i ∈ {..n}" "j ∈ {..n}" "i ≠ j" "T i = T j"
with that  injT [unfolded inj_on_def] show "f (T i) = 0"
by simp metis
qed (use atMost_atLeast0 in auto)
let ?B = "m + e * ?μ S"
have "(∑k≤n. ?μ (f ` T k)) ≤ ?B" for n
proof -
have "(∑k≤n. ?μ (f ` T k)) ≤ (∑k≤n. ((k+1) * e) * ?μ(T k))"
proof (rule sum_mono [OF measure_bounded_differentiable_image])
show "(f has_derivative f' x) (at x within T k)" if "x ∈ T k" for k x
using that unfolding T_def by (blast intro: deriv has_derivative_subset)
show "(λx. ¦det (matrix (f' x))¦) integrable_on T k" for k
using absolutely_integrable_on_def aint_T by blast
show "¦det (matrix (f' x))¦ ≤ real (k + 1) * e" if "x ∈ T k" for k x
using T_def that by auto
qed (use meas_t in auto)
also have "… ≤ (∑k≤n. (k * e) * ?μ(T k)) + (∑k≤n. e * ?μ(T k))"
also have "… ≤ ?B"
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' x))¦)) S"
using absolutely_integrable_on_def aint_T by blast
next
show "pairwise (λS S'. negligible (S ∩ S')) (T ` {..n})"
using disT unfolding disjnt_iff by (auto simp: pairwise_def intro!: empty_imp_negligible)
qed auto
also have "… ≤ m"
unfolding m_def
proof (rule integral_subset_le)
have "(λx. ¦det (matrix (f' x))¦) absolutely_integrable_on (⋃k≤n. T k)"
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_distrib_left that)
qed
finally show "(∑k≤n. ?μ (f ` T k)) ≤ ?B" .
qed
moreover have "measure lebesgue (⋃k≤n. f ` T k) ≤ (∑k≤n. ?μ (f ` T k))" for n
by (simp add: fmeasurableD meas_ft measure_UNION_le)
ultimately have B_ge_m: "?μ (⋃k≤n. (f ` T k)) ≤ ?B" for n
by (meson order_trans)
have "(⋃n. f ` T n) ∈ lmeasurable"
by (rule fmeasurable_countable_Union [OF meas_ft B_ge_m])
moreover have "?μ (⋃n. f ` T n) ≤ m + e * ?μ S"
by (rule measure_countable_Union_le [OF meas_ft B_ge_m])
ultimately show "f ` S ∈ lmeasurable" "?μ (f ` S) ≤ m + e * ?μ S"
by (auto simp: Seq image_Union)
qed
show ?thesis
proof
show "f ` S ∈ lmeasurable"
using * linordered_field_no_ub by blast
let ?x = "m - ?μ (f ` S)"
have False if "?μ (f ` S) > integral S (λx. ¦det (matrix (f' x))¦)"
proof -
have ml: "m < ?μ (f ` S)"
using m_def that by blast
then have "?μ S ≠ 0"
using "*"(2) bgauge_existence_lemma by fastforce
with ml have 0: "0 < - (m - ?μ (f ` S))/2 / ?μ S"
using that zero_less_measure_iff by force
then show ?thesis
using * [OF 0] that by (auto simp: 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^'n::_"
by (smt (verit, best) Finite_Cartesian_Product.norm_nth_le nat_ceiling_le_eq
real_nat_ceiling_ge real_norm_def)
then have Seq: "S = (⋃n. ?I n)"
by auto
have fIn: "f ` ?I n ∈ lmeasurable"
and mfIn: "?μ (f ` ?I n) ≤ integral S (λx. ¦det (matrix (f' x))¦)" (is ?MN) for n
proof -
have In: "?I n ∈ lmeasurable"
by (simp add: S bounded_Int bounded_set_imp_lmeasurable sets.Int)
moreover have "⋀x. x ∈ ?I n ⟹ (f has_derivative f' x) (at x within ?I n)"
by (meson Int_iff deriv has_derivative_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 (matrix (f' x))¦)"
using m_diff_image_weak by metis+
moreover have "integral (?I n) (λx. ¦det (matrix (f' x))¦) ≤ integral S (λx. ¦det (matrix (f' x))¦)"
by (simp add: int_In int integral_subset_le)
ultimately show "f ` ?I n ∈ lmeasurable" ?MN
by auto
qed
have "?I k ⊆ ?I n" if "k ≤ n" for k n
by (rule Int_mono) (use that in ‹auto simp: subset_interval_imp_cart›)
then have "(⋃k≤n. f ` ?I k) = f ` ?I n" for n
with mfIn have "?μ (⋃k≤n. f ` ?I k) ≤ integral S (λx. ¦det (matrix (f' x))¦)" for n
by simp
then have "(⋃n. f ` ?I n) ∈ lmeasurable" "?μ (⋃n. f ` ?I n) ≤ integral S (λx. ¦det (matrix (f' x))¦)"
by (rule fmeasurable_countable_Union [OF fIn] measure_countable_Union_le [OF fIn])+
then show "f ` S ∈ lmeasurable" ?M
by (metis Seq image_UN)+
qed

lemma borel_measurable_simple_function_limit_increasing:
fixes f :: "'a::euclidean_space ⇒ real"
shows "(f ∈ borel_measurable lebesgue ∧ (∀x. 0 ≤ f x)) ⟷
(∃g. (∀n x. 0 ≤ g n x ∧ g n x ≤ f x) ∧ (∀n x. g n x ≤ (g(Suc n) x)) ∧
(∀n. g n ∈ borel_measurable lebesgue) ∧ (∀n. finite(range (g n))) ∧
(∀x. (λn. g n x) ⇢ f x))"
(is "?lhs = ?rhs")
proof
assume f: ?lhs
have leb_f: "{x. a ≤ f x ∧ f x < b} ∈ sets lebesgue" for a b
proof -
have "{x. a ≤ f x ∧ f x < b} = {x. f x < b} - {x. f x < a}"
by auto
also have "… ∈ sets lebesgue"
using borel_measurable_vimage_halfspace_component_lt [of f UNIV] f by auto
finally show ?thesis .
qed
have "g n x ≤ f x"
if inc_g: "⋀n x. 0 ≤ g n x ∧ g n x ≤ g (Suc n) x"
and meas_g: "⋀n. g n ∈ borel_measurable lebesgue"
and fin: "⋀n. finite(range (g n))" and lim: "⋀x. (λn. g n x) ⇢ f x" for g n x
proof -
have "∃r>0. ∀N. ∃n≥N. dist (g n x) (f x) ≥ r" if "g n x > f x"
proof -
have g: "g n x ≤ g (N + n) x" for N
by (rule transitive_stepwise_le) (use inc_g in auto)
have "∃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 x) ⇢ f x)"
proof (intro exI allI conjI)
show "0 ≤ ?g n x" for n x
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 ∧ f y < (k+1/2)/2^n} x) +
(∑k | k ∈ ℤ ∧ ¦k¦ ≤ 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n ≤ f y ∧ f y < (k+1)/2^n} x)"