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"
    by (simp add: lin measurable_linear_image_interval)
  let ?c = "χ i. if i = m then b$m + b$n else b$i"
  let ?mn = "axis m 1 - axis n (1::real)"
  have eq1: "measure lebesgue (cbox a ?c)
            = measure lebesgue (?f ` cbox a b)
            + measure lebesgue (cbox a ?c  {x. ?mn  x  a$m})
            + measure lebesgue (cbox a ?c  {x. ?mn  x  b$m})"
  proof (rule measure_Un3_negligible)
    show "cbox a ?c  {x. ?mn  x  a$m}  lmeasurable" "cbox a ?c  {x. ?mn  x  b$m}  lmeasurable"
      by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
    have "negligible {x. ?mn  x = a$m}"
      by (metis m  n axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
    moreover have "?f ` cbox a b  (cbox a ?c  {x. ?mn  x  a $ m})  {x. ?mn  x = a$m}"
      using m  n antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
    ultimately show "negligible ((?f ` cbox a b)  (cbox a ?c  {x. ?mn  x  a $ m}))"
      by (rule negligible_subset)
    have "negligible {x. ?mn  x = b$m}"
      by (metis m  n axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
    moreover have "(?f ` cbox a b)  (cbox a ?c  {x. ?mn  x  b$m})  {x. ?mn  x = b$m}"
      using m  n antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
    ultimately show "negligible (?f ` cbox a b  (cbox a ?c  {x. ?mn  x  b$m}))"
      by (rule negligible_subset)
    have "negligible {x. ?mn  x = b$m}"
      by (metis m  n axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
    moreover have "(cbox a ?c  {x. ?mn  x  a $ m}  (cbox a ?c  {x. ?mn  x  b$m}))  {x. ?mn  x = b$m}"
      using m  n ab_ne
      apply (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"
        by (auto simp: mem_box_cart add_mono) (meson add_increasing2 an order_trans)
      show "cbox a ?c  ?lhs"
        apply (clarsimp simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF m  n])
        by (smt (verit, del_insts) mem_box_cart(2) vec_lambda_beta)
    qed
  qed (fact fab)
  let ?d = "χ i. if i = m then a $ m - b $ m else 0"
  have eq2: "measure lebesgue (cbox a ?c  {x. ?mn  x  a $ m}) + measure lebesgue (cbox a ?c  {x. ?mn  x  b$m})
           = measure lebesgue (cbox a (χ i. if i = m then a $ m + b $ n else b $ i))"
  proof (rule measure_translate_add[of "cbox a ?c  {x. ?mn  x  a$m}" "cbox a ?c  {x. ?mn  x  b$m}"
     "(χ i. if i = m then a$m - b$m else 0)" "cbox a (χ i. if i = m then a$m + b$n else b$i)"])
    show "(cbox a ?c  {x. ?mn  x  a$m})  lmeasurable"
      "cbox a ?c  {x. ?mn  x  b$m}  lmeasurable"
      by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
    have "x. x $ n + a $ m  x $ m
          x  (+) (χ i. if i = m then a $ m - b $ m else 0) ` {x. x $ n + b $ m  x $ m}"
      using m  n
      by (rule_tac x="x - (χ i. if i = m then a$m - b$m else 0)" in image_eqI)
         (simp_all add: mem_box_cart)
    then have imeq: "(+) ?d ` {x. b $ m  ?mn  x} = {x. a $ m  ?mn  x}"
      using m  n by (auto simp: mem_box_cart inner_axis' algebra_simps)
    have "x. 0  a $ n; x $ n + a $ m  x $ m;
                i. i  m  a $ i  x $ i  x $ i  b $ i
          a $ m  x $ m"
      using m  n  by force
    then have "(+) ?d ` (cbox a ?c  {x. b $ m  ?mn  x})
            = cbox a (χ i. if i = m then a $ m + b $ n else b $ i)  {x. a $ m  ?mn  x}"
      using an ab_ne
      apply (simp add: cbox_translation [symmetric] translation_Int interval_ne_empty_cart imeq)
      apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib)
      by (metis (full_types) add_mono mult_2_right)
    then show "cbox a ?c  {x. ?mn  x  a $ m} 
          (+) ?d ` (cbox a ?c  {x. b $ m  ?mn  x}) =
          cbox a (χ i. if i = m then a $ m + b $ n else b $ i)"  (is "?lhs = ?rhs")
      using an m  n
      apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib, force)
        apply (drule_tac x=n in spec)+
      by (meson ab_ne add_mono_thms_linordered_semiring(3) dual_order.trans interval_ne_empty_cart(1))
    have "negligible{x. ?mn  x = a$m}"
      by (metis m  n axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
    moreover have "(cbox a ?c  {x. ?mn  x  a $ m} 
                                 (+) ?d ` (cbox a ?c  {x. b $ m  ?mn  x}))  {x. ?mn  x = a$m}"
      using m  n antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
    ultimately show "negligible (cbox a ?c  {x. ?mn  x  a $ m} 
                                 (+) ?d ` (cbox a ?c  {x. b $ m  ?mn  x}))"
      by (rule negligible_subset)
  qed
  have ac_ne: "cbox a ?c  {}"
    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"]
              by (simp add: field_simps prod_dividef)
            moreover have "((λx. χ k. x $ k * m k) ` cbox (χ k. min ( k) ( k)) (χ k. max ( k) ( k))) = cbox u v"
              using True image_stretch_interval_cart [of "inverse  m" u v, symmetric]
                image_stretch_interval_cart [of "λk. 1" u v, symmetric] cbox u v  {}
              by (simp add: field_simps image_comp o_def)
            ultimately show "((λx. indicat_real S (χ k. x $ k/ m k)) has_integral z *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
      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 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"
        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_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
        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 - frontier S) < e"
    by (metis fmeasurableD)
  with null have "U  lmeasurable"
    by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel)
  have "measure lebesgue (U - frontier S) = measure lebesgue U"
    using mS0 by (simp add: U  lmeasurable fmeasurableD measure_Diff_null_set null)
  with U have mU: "measure lebesgue U < e"
    by (simp 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_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"
                  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) /R r - (f y - f x) /R r)"
                  by (simp add: dist_norm)
                also have " = norm (f' x (y - x) - (f y - f x)) / r"
                  using r > 0 by (simp add: 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)
                by (metis (no_types, opaque_lifting) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball)
              ultimately show "bounded (?rfs)"
                by (rule bounded_subset)
            qed
            then have "(λx. r *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_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  (iK.  (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))"
            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.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 - (iC. 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"
        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 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_left_pos)
            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: "(kn. 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 "(kn.  (f ` T k))  ?B" for n
    proof -
      have "(kn.  (f ` T k))  (kn. ((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 "  (kn. (k * e) * (T k)) + (kn. e * (T k))"
        by (simp add: algebra_simps sum.distrib)
      also have "  ?B"
      proof (rule add_mono)
        have "(kn. real k * e *  (T k)) = (kn. integral (T k) (λx. k * e))"
          by (simp add: lmeasure_integral [OF meas_t]
                   flip: integral_mult_right integral_mult_left)
        also have "  (kn. 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 (kn. 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 (kn. 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 (kn. T k)"
            using absolutely_integrable_on_def by blast
        qed (use Seq int in auto)
        finally show "(kn. real k * e *  (T k))  m" .
      next
        have "(kn.  (T k)) = sum  (T ` {..n})"
          by (auto intro: sum_eq_Tim)
        also have " =  (kn. 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 "(kn.  (T k))   S" .
        then show "(kn. 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 "(kn.  (f ` T k))  ?B" .
    qed
    moreover have "measure lebesgue (kn. f ` T k)  (kn.  (f ` T k))" for n
      by (simp add: fmeasurableD meas_ft measure_UNION_le)
    ultimately have B_ge_m: " (kn. (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::_"
    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 (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 "(kn. f ` ?I k) = f ` ?I n" for n
    by (fastforce simp add:)
  with mfIn have " (kn. 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. nN. 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 "mN. 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
    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  f y < (k+1/2)/2^n} x) +
                       (k | k    ¦k¦  2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n  f y  f y < (k+1)/2^n} x)"
        by (simp add:  comm_monoid_add_class.sum.distrib algebra_simps)
      also have " = (k | k    ¦k¦  2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k)/2 ^ Suc n  f y  f y < (2 * k<