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+1)/2 ^ Suc n} x) +
                       (k | k    ¦k¦  2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n  f y  f y < ((2 * k+1) + 1)/2 ^ Suc n} x)"
        by (force simp: field_simps indicator_def intro: sum.cong)
      also have "  (k | k    ¦k¦  2 ^ (2 * Suc n). k/2 ^ Suc n * (indicator {y. k/2 ^ Suc n  f y  f y < (k+1)/2 ^ Suc n} x))"
                (is "?a + _  ?b")
      proof -
        have *: "sum f I  sum h I; a + sum h I  b  a + sum f I  b" for I a b f and h :: "realreal"
          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  . P k}  (λx. 2 * x + 1) ` {k  . P k} = {}" for P :: "real  bool"
          proof -
            have "2 * i  2 * j + 1" for i j :: int by arith
            thus ?thesis
              unfolding Ints_def by auto (use of_int_eq_iff in fastforce)
          qed
          have "?a + sum ?h {k  . ¦k¦  2 ^ (2*n)}
                = (k  (*)2 ` {k  . ¦k¦  2 ^ (2*n)}  (λx. 2*x + 1) ` {k  . ¦k¦  2 ^ (2*n)}.
                  k/2 ^ Suc n * indicator {y. k/2 ^ Suc n  f y  f y < (k+1)/2 ^ Suc n} x)"
            unfolding α β
            using finite_abs_int_segment [of "2 ^ (2*n)"]
            by (subst sum_Un) (auto simp: 0)
          also have "  ?b"
          proof (rule sum_mono2)
            show "finite {k::real. k    ¦k¦  2 ^ (2 * Suc n)}"
              by (rule finite_abs_int_segment)
            show "(*) 2 ` {k::real. k    ¦k¦  2^(2*n)}  (λx. 2*x + 1) ` {k  . ¦k¦  2^(2*n)}  {k  . ¦k¦  2 ^ (2 * Suc n)}"
              apply (clarsimp simp: image_subset_iff)
              using one_le_power [of "2::real" "2*n"]  by linarith
            have *: "x  (S  T) - U; x. x  S  x  U; x. x  T  x  U  P x" for S T U P
              by blast
            have "0  b" if "b  " "f x * (2 * 2^n) < b + 1" for b
              by (smt (verit, ccfv_SIG) Ints_cases f int_le_real_less mult_nonneg_nonneg of_int_add one_le_power that)
            then show "0  b/2 ^ Suc n * indicator {y. b/2 ^ Suc n  f y  f y < (b + 1)/2 ^ Suc n} x"
                  if "b  {k  . ¦k¦  2 ^ (2 * Suc n)} -
                          ((*) 2 ` {k  . ¦k¦  2 ^ (2*n)}  (λx. 2*x + 1) ` {k  . ¦k¦  2 ^ (2*n)})" for b
              using that by (simp add: indicator_def divide_simps)
          qed
          finally show "?a + sum ?h {k  . ¦k¦  2 ^ (2*n)}  ?b" .
        qed
      qed
      finally show ?thesis .
    qed
    show "?g n  borel_measurable lebesgue" for n
      apply (intro borel_measurable_indicator borel_measurable_times borel_measurable_sum)
      using leb_f sets_restrict_UNIV by auto
    show "finite (range (?g n))" for n
    proof -
      have "(k | k    ¦k¦  2 ^ (2*n). k/2^n *  n k x)
               (λk. k/2^n) ` {k  . ¦k¦  2 ^ (2*n)}" for x
      proof (cases "k. k    ¦k¦  2 ^ (2*n)  k/2^n  f x  f x < (k+1)/2^n")
        case True
        then show ?thesis
          by (blast intro: indicator_sum_eq)
      next
        case False
        then have "(k | k    ¦k¦  2 ^ (2*n). k/2^n *  n k x) = 0"
          by auto
        then show ?thesis by force
      qed
      then have "range (?g n)  ((λk. (k/2^n)) ` {k. k    ¦k¦  2 ^ (2*n)})"
        by auto
      moreover have "finite ((λk::real. (k/2^n)) ` {k  . ¦k¦  2 ^ (2*n)})"
        by (intro finite_imageI finite_abs_int_segment)
      ultimately show ?thesis
        by (rule finite_subset)
    qed
    show "(λn. ?g n x)  f x" for x
    proof (clarsimp simp add: lim_sequentially)
      fix e::real
      assume "e > 0"
      obtain N1 where N1: "2 ^ N1 > abs(f x)"
        using real_arch_pow by fastforce
      obtain N2 where N2: "(1/2) ^ N2 < e"
        using real_arch_pow_inv e > 0 by fastforce
      have "dist (k | k    ¦k¦  2 ^ (2*n). k/2^n *  n k x) (f x) < e" if "N1 + N2  n" for n
      proof -
        let ?m = "real_of_int 2^n * f x"
        have "¦?m¦  2^n * 2^N1"
          using N1 apply (simp add: f)
          by (meson floor_mono le_floor_iff less_le_not_le mult_le_cancel_left_pos zero_less_numeral zero_less_power)
        also have "  2 ^ (2*n)"
          by (metis that add_leD1 add_le_cancel_left mult.commute mult_2_right one_less_numeral_iff
                    power_add power_increasing_iff semiring_norm(76))
        finally have m_le: "¦?m¦  2 ^ (2*n)" .
        have "?m/2^n  f x" "f x < (?m + 1)/2^n"
          by (auto simp: mult.commute pos_divide_le_eq mult_imp_less_div_pos)
        then have eq: "dist (k | k    ¦k¦  2 ^ (2*n). k/2^n *  n k x) (f x)
                     = dist (?m/2^n) (f x)"
          by (subst indicator_sum_eq [of ?m]) (auto simp: m_le)
        have "¦2^n¦ * ¦?m/2^n - f x¦ = ¦2^n * (?m/2^n - f x)¦"
          by (simp add: abs_mult)
        also have " < 2 ^ N2 * e"
          using N2 by (simp add: divide_simps mult.commute) linarith
        also have "  ¦2^n¦ * e"
          using that e > 0 by auto
        finally show ?thesis
          using eq by (simp add: dist_real_def)
      qed
      then show "no. nno. 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. ρ::natnat. 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 ρ::"natnat"
       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))  ρ)) i"
      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_def)
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 S)"
    and lb: "v. v  0  (k>0.  e>0. x  S - {a}. norm(a - x) < e  k * norm(a - x)  ¦v  (x - a)¦)"
  shows "f x = 0"
proof -
  have "((λx. f x /R norm x)  0) (at 0 within (λx. x-a) ` S)"
    using lim by (simp add: Lim_within dist_norm)
  then show ?thesis
  proof (rule lemma_partial_derivatives0 [OF linear f])
    fix v :: "'a"
    assume v: "v  0"
    show "k>0. e>0. x. x  (λx. x - a) ` S - {0}  norm x < e  k * norm x  ¦v  x¦"
      using lb [OF v] by (force simp:  norm_minus_commute)
  qed
qed


proposition borel_measurable_partial_derivatives:
  fixes f :: "real^'m::{finite,wellorder}  real^'n"
  assumes S: "S  sets lebesgue"
    and f: "x. x  S  (f has_derivative f' x) (at x within S)"
  shows "(λx. (matrix(f' x)$m$n))  borel_measurable (lebesgue_on S)"
proof -
  have contf: "continuous_on S f"
    using continuous_on_eq_continuous_within f has_derivative_continuous by blast
  have "{x  S.  (matrix (f' x)$m$n)  b}  sets lebesgue" for b
  proof (rule sets_negligible_symdiff)
    let ?T = "{x  S. e>0. d>0. A. A$m$n < b  (i j. A$i$j  ) 
                       (y  S. norm(y - x) < d  norm(f y - f x - A *v (y - x))  e * norm(y - x))}"
    let ?U = "S 
              (e  {e  . e > 0}.
                A  {A. A$m$n < b  (i j. A$i$j  )}.
                  d  {d  . 0 < d}.
                     S  (y  S. {x  S. norm(y - x) < d  norm(f y - f x - A *v (y - x))  e * norm(y - x)}))"
    have "?T = ?U"
    proof (intro set_eqI iffI)
      fix x
      assume xT: "x  ?T"
      then show "x  ?U"
      proof (clarsimp simp add:)
        fix q :: real
        assume "q  " "q > 0"
        then obtain d A where "d > 0" and A: "A $ m $ n < b" "i j. A $ i $ j  "
          "y. yS;  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  (yS. norm (y - x) < s  norm (f y - f x - A *v (y - x))  q * norm (y - x)))"
          by force
      qed
    next
      fix x
      assume xU: "x  ?U"
      then show "x  ?T"
      proof clarsimp
        fix e :: "real"
        assume "e > 0"
        then obtain ε where ε: "e > ε" "ε > 0" "ε  "
          using Rats_dense_in_real by blast
        with xU obtain A r where "x  S" and Ar: "A $ m $ n < b" "i j. A $ i $ j  " "r  " "r > 0"
          and "yS. 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 "yS. 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  )  (yS. norm (y - x) < d  norm (f y - f x - A *v (y - x))  e * norm (y - x))"
          using x  S Ar by blast
      qed
    qed
    moreover have "?U  sets lebesgue"
    proof -
      have coQ: "countable {e  . 0 < e}"
        using countable_Collect countable_rat by blast
      have ne: "{e  . (0::real) < e}  {}"
        using zero_less_one Rats_1 by blast
      have coA: "countable {A. A $ m $ n < b  (i j. A $ i $ j  )}"
      proof (rule countable_subset)
        show "countable {A. i j. A $ i $ j  }"
          using countable_vector [OF countable_vector, of "λi j. "] by (simp add: countable_rat)
      qed blast
      have *: "U  {}  closedin (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}" for P Q R
        by auto
      have sets: "S  (yS. {x  S. norm (y - x) < d  norm (f y - f x - A *v (y - x))  e * norm (y - x)})
                   sets lebesgue" for e A d
      proof -
        have clo: "closedin (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 *v x)))"
            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  b} - ?T))"
    let  = "λx v. ξ>0. e>0. y  S-{x}. norm (x - y) < e  ¦v  (y - x)¦ < ξ * norm (x - y)"
    have nN: "negligible {x  S. v0.  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. v0.  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. zS - {x'}. norm (x' - z) < e  ¦v  (z - x')¦ < ξ * norm (x' - z))}  ball x (min d r)  ?W"
          proof (clarsimp simp: dist_norm norm_minus_commute)
            fix y w
            assume "y  S" "w  0"
              and less [rule_format]:
                    "ξ>0. e>0. zS - {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::real))"
            using rotation_rightward_line by metis
          define b where "b  norm v"
          have "b > 0"
            using v  0 by (auto simp: b_def)
          obtain eqb: "inv T v = b *R axis k (1::real)" and "inj T" "bij T" and invT: "orthogonal_transformation (inv T)"
            by (metis UNIV_I b_def  T v bij_betw_inv_into_left orthogonal_transformation_inj orthogonal_transformation_bij orthogonal_transformation_inv)
          let ?v = "χ i. min d r / CARD('m)"
          let ?v' = "χ i. if i = k then (e/2 * min d r) / CARD('m) ^ CARD('m) else min d r"
          let ?x' = "inv T x"
          let ?W' = "(ball ?x' (min d r)  {y. ¦(y - ?x')$k¦ < e * min d r / (2 * CARD('m) ^ CARD('m))})"
          have abs: "x - e  y  y  x + e  abs(y - x)  e" for x y e::real
            by auto
          have "?W = T ` ?W'"
          proof -
            have 1: "T ` (ball (inv T x) (min d r)) = ball x (min d r)"
              by (simp add: T image_orthogonal_transformation_ball orthogonal_transformation_surj surj_f_inv_f)
            have 2: "{y. ¦v  (y - x)¦ < b * e * min d r / (2 * real CARD('m) ^ CARD('m))} =
                      T ` {y. ¦y $ k - ?x' $ k¦ < e * min d r / (2 * real CARD('m) ^ CARD('m))}"
            proof -
              have *: "¦T (b *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_pos times_divide_eq_right [symmetric] del: times_divide_eq_right)
            qed
            show ?thesis
              using b > 0 by (simp add: image_Int inj T 1 2 b_def [symmetric])
          qed
          moreover have "?W'  lmeasurable"
            by (auto intro: fmeasurable_Int_fmeasurable)
          ultimately have "measure lebesgue ?W = measure lebesgue ?W'"
            by (metis measure_orthogonal_image T)
          also have "  measure lebesgue (cbox (?x' - ?v') (?x' + ?v'))"
          proof (rule measure_mono_fmeasurable)
            show "?W'  cbox (?x' - ?v') (?x' + ?v')"
              apply (clarsimp simp add: mem_box_cart abs dist_norm norm_minus_commute simp del: min_less_iff_conj min.bounded_iff)
              by (metis component_le_norm_cart less_eq_real_def le_less_trans vector_minus_component)
          qed auto
          also have "  e/2 * measure lebesgue (cbox (?x' - ?v) (?x' + ?v))"
          proof -
            have "cbox (?x' - ?v) (?x' + ?v)  {}"
              using r > 0 d > 0 by (auto simp: interval_eq_empty_cart divide_less_0_iff)
            with r > 0 d > 0 e > 0 show ?thesis
              apply (simp add: content_cbox_if_cart mem_box_cart)
              apply (auto simp: prod_nonneg)
              apply (simp add: abs if_distrib prod.delta_remove field_simps power_diff split: if_split_asm)
              done
          qed
          also have "  e/2 * measure lebesgue (cball ?x' (min d r))"
          proof (rule mult_left_mono [OF measure_mono_fmeasurable])
            have *: "norm (?x' - y)  min d r"
              if y: "i. ¦?x' $ i - y $ i¦  min d r / real CARD('m)" for y
            proof -
              have "norm (?x' - y)  (iUNIV. ¦(?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 :: "(real,'m) vec set"
      by blast
    have MN: "?M  {x  S. v0.  x v}"
    proof (rule *)
      fix x
      assume x: "x  {x  S. v0.  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  ) 
                                    (yS. 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_divide_1_iff)
          then obtain δ A where δ: "k. δ k > 0"
                           and Ab: "k. A k $ m $ n < b"
                           and A: "k y. y  S; norm (y - x) < δ k 
                                          norm (f y - f x - A k *v (y - x))  1/(Suc k) * norm (y - x)"
            by metis
          have "i j. a. (λn. A n $ i $ j)  a"
          proof (intro allI)
            fix i j
            have vax: "(A n *v axis j 1) $ i = A n $ i $ j" for n
              by (metis cart_eq_inner_axis matrix_vector_mul_component)
            let ?CA = "{x. Cauchy (λn. (A n) *v x)}"
            have "subspace ?CA"
              unfolding subspace_def convergent_eq_Cauchy [symmetric]
                by (force simp: algebra_simps intro: tendsto_intros)
            then have CA_eq: "?CA = span ?CA"
              by (metis span_eq_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_Archimedean2)
                      with γconv show "no. nno. norm (γ n - x) < r"
                        by (metis r > 0 add.commute divide_inverse inverse_inverse_eq inverse_less_imp_less less_trans mult.left_neutral nat_le_real_less of_nat_Suc)
                    qed
                    with strict_mono ρ show "(γ  ρ)  x"
                      by (metis LIMSEQ_subseq_LIMSEQ)
                    show "(λn. ((γ  ρ) n - x) /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. mM. nM. 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) (at x within S)"
            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) (at x within S)"
              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))  0) (at x within S)"
            proof (rule Lim_transform)
              have "((λy. ((f y + B *v x - (f x + B *v y)) /R norm (y - x)))  0) (at x within S)"
              proof (clarsimp simp add: Lim_within dist_norm)
                fix e :: "real"
                assume "e > 0"
                then obtain q::nat where "q  0" and qe2: "1/q < e/2"
                  by (metis divide_pos_pos inverse_eq_divide real_arch_inverse zero_less_numeral)
                let ?g = "λp. sum  (λi. sum (λj. abs((A p - B)$i$j)) UNIV) UNIV"
                have "(λk. onorm (λy. (A k - B) *v y))  0"
                proof (rule Lim_null_comparison)
                  show "F k in sequentially. norm (onorm (λy. (A k - B) *v y))  ?g k"
                  proof (rule eventually_sequentiallyI)
                    fix k :: "nat"
                    assume "0  k"
                    have "0  onorm ((*v) (A k - B))"
                      using matrix_vector_mul_bounded_linear
                      by (rule onorm_pos_le)
                    then show "norm (onorm ((*v) (A k - B)))  (iUNIV. jUNIV. ¦(A k - B) $ i $ j¦)"
                      by (simp add: onorm_le_matrix_component_sum del: vector_minus_component)
                  qed
                next
                  show "?g  0"
                    using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum)
                qed
                with e > 0 obtain p where "n. n  p  ¦onorm ((*v) (A n - B))¦ < e/2"
                  unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral)
                then have pqe2: "¦onorm ((*v) (A (p + q) - B))¦ < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*)
                  using le_add1 by blast
                show "d>0. yS. y  x  norm (y - x) < d 
                           inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e"
                proof (intro exI, safe)
                  show "0 < δ(p + q)"
                    by (simp add: δ)
                next
                  fix y
                  assume y: "y  S" "norm (y - x) < δ(p + q)" and "y  x"
                  have *: "norm(b - c) < e - d; norm(y - x - b)  d  norm(y - x - c) < e"
                    for b c d e x and y:: "real^'n"
                    using norm_triangle_ineq2 [of "y - x - c" "y - x - b"] by simp
                  have "norm (f y - f x - B *v (y - x)) < e * norm (y - x)"
                  proof (rule *)
                    show "norm (f y - f x - A (p + q) *v (y - x))  norm (y - x) / (Suc (p + q))"
                      using A [OF y] by simp
                    have "norm (A (p + q) *v (y - x) - B *v (y - x))  onorm(λx. (A(p + q) - B) *v x) * norm(y - x)"
                      by (metis linear_linear matrix_vector_mul_linear matrix_vector_mult_diff_rdistrib onorm)
                    also have " < (e/2) * norm (y - x)"
                      using y  x pqe2 by auto
                    also have "  (e - 1 / (Suc (p + q))) * norm (y - x)"
                    proof (rule mult_right_mono)
                      have "1 / Suc (p + q)  1 / q"
                        using q  0 by (auto simp: 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. yS  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  ) 
                (yS. norm (y - x) < d  norm (f y - f x - A *v (y - x))  e * norm (y - x))"
          proof (intro exI conjI ballI allI impI)
            show "d>0"
              by (rule d>0)
            show "B $ m $ n < b"
            proof -
              have "¦matrix ((*v) (?A - B)) $ m $ n¦  onorm ((*v) (?A - B))"
                using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis
              then show ?thesis
                using b Bo_e6 by simp
            qed
            show "B $ i $ j  " for i j
              using BRats by auto
            show "norm (f y - f x - B *v (y - x))  e * norm (y - x)"
              if "y  S" and y: "norm (y - x) < d" for y
            proof (cases "y = x")
              case True then show ?thesis
                by simp
            next
              case False
              have *: "norm(d' - d)  e/2  norm(y - (x + d')) < e/2  norm(y - x - d)  e" for d d' e and x y::"real^'n"
                using norm_triangle_le [of "d' - d" "y - (x + d')"] by simp
              show ?thesis
              proof (rule *)
                have split246: "norm y  e / 6; norm(x - y)  e / 4  norm x  e/2" if "e > 0" for e and x y :: "real^'n"
                  using norm_triangle_le [of y "x-y" "e/2"] e > 0 by simp
                have "linear (f' x)"
                  using True f has_derivative_linear by blast
                then have "norm (f' x (y - x) - B *v (y - x)) = norm ((matrix (f' x) - B) *v (y - x))"
                  by (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. if i = m  j = n then e / 4 else 0) *v (y - x))"
                    by (simp add: algebra_simps)
                  also have " = norm((e/4) *R (y - x)$n *R axis m (1::real))"
                  proof -
                    have "(jUNIV. (if i = m  j = n then e / 4 else 0) * (y $ j - x $ j)) * 4 = e * (y $ n - x $ n) * axis m 1 $ i" for i
                    proof (cases "i=m")
                      case True then show ?thesis
                        by (auto simp: if_distrib [of "λz. z * _"] cong: if_cong)
                    next
                      case False then show ?thesis
                        by (simp add: axis_def)
                    qed
                    then have "(χ i j. if i = m  j = n then e / 4 else 0) *v (y - x) = (e/4) *R (y - x)$n *R axis m (1::real)"
                      by (auto simp: vec_eq_iff matrix_vector_mult_def)
                    then show ?thesis
                      by metis
                  qed
                  also have "  e * norm (y - x) / 4"
                  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 * norm (y - x) / 4" .
                  show "0 < e * norm (y - x)"
                    by (simp add: False e > 0)
                qed
                finally show "norm (f' x (y - x) - B *v (y - x))  (e * norm (y - x)) / 2" .
                show "norm (f y - (f x + f' x (y - x))) < (e * norm (y - x)) / 2"
                  using False d [OF y  S] y by (simp add: dist_norm field_simps)
              qed
            qed
          qed
        qed
      qed auto
    qed
    show "negligible ?M"
      using negligible_subset [OF nN MN] .
  qed
  then show ?thesis
    by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff assms)
qed


theorem borel_measurable_det_Jacobian:
 fixes f :: "real^'n::{finite,wellorder}  real^'n::_"
  assumes S: "S  sets lebesgue" and f: "x. x  S  (f has_derivative f' x) (at x within S)"
  shows "(λx. det(matrix(f' x)))  borel_measurable (lebesgue_on S)"
  unfolding det_def
  by (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S])

text‹The localisation wrt S uses the same argument for many similar results.›
(*See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.*)
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}  sets lebesgue"
         if "T  sets borel" for T
    proof (cases "0  T")
      case True
      then have "{x  S. f x  T} = {x. (if x  S then f x else 0)  T}  S"
                "{x. (if x  S then f x else 0)  T} = {x  S. f x  T}  -S"
        by auto
      then show ?thesis
        by (metis (no_types, lifting) Compl_in_sets_lebesgue assms sets.Int sets.Un)
    next
      case False
      then have "{x. (if x  S then f x else 0)  T} = {x  S. f x  T}"
        by auto
      then show ?thesis
        by auto
    qed
    then show ?thesis
      unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_if [OF assms, symmetric]
      by blast
qed

lemma sets_lebesgue_almost_borel:
  assumes "S  sets lebesgue"
  obtains B N where "B  sets borel" "negligible N" "B  N = S"
  by (metis assms negligible_iff_null_sets negligible_subset null_sets_completionI sets_completionE sets_lborel)

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 derivative)›

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 = "(jBasis. (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  (tP. norm (z - t)  e)}  cbox (-?v) ?v"
      by (auto simp: mem_box)
    have *: "kBasis. - ?v  k  ?v  k"
      using 0  m 0  e by (auto simp: inner_Basis)
    have 2: "2 ^ DIM('b) = 2 * 2 ^ (DIM('b) - Suc 0)"
      by (metis DIM_positive Suc_pred power_Suc)
    show "measure lebesgue (cbox (-?v) ?v)  2 * e * (2 * m) ^ (DIM('b) - 1)"
      using i  Basis
      by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2)
  qed blast
qed

text‹As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})›
lemma Sard_lemma0:
  fixes P :: "(real^'n::{finite,wellorder}) set"
  assumes "a  0"
    and P: "P  {x. a  x = 0}" and "0  m" "0  e"
  obtains S where "S  lmeasurable"
    and "{z. norm z  m  (t  P. norm(z - t)  e)}  S"
    and "measure lebesgue S  (2 * e) * (2 * m) ^ (CARD('n) - 1)"
proof -
  obtain T and k::'n where T: "orthogonal_transformation T" and a: "a = T (norm a *R axis k (1::real))"
    using rotation_rightward_line by metis
  have Tinv [simp]: "T (inv T x) = x" for x
    by (simp add: T orthogonal_transformation_surj surj_f_inv_f)
  obtain S where S: "S  lmeasurable"
    and subS: "{z. norm z  m  (t  T-`P. norm(z - t)  e)}  S"
    and mS: "measure lebesgue S  (2 * e) * (2 * m) ^ (CARD('n) - 1)"
  proof (rule Sard_lemma00 [of "norm a" "axis k (1::real)" "T-`P" m e])
    have "norm a *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 that)
    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  (tP. norm (z - t)  e)}  T ` {z. norm z  m  (tT -` P. norm (z - t)  e)}"
    proof clarsimp
      fix x t
      assume §: "norm x  m" "t  P" "norm (x - t)  e"
      then have "norm (inv T x)  m"
        using orthogonal_transformation_inv [OF T] by (simp add: orthogonal_transformation_norm)
      moreover have "tT -` P. norm (inv T x - t)  e"
        by (smt (verit, del_insts) T Tinv § linear_diff orthogonal_transformation_def orthogonal_transformation_norm vimage_eq)
      ultimately show "x  T ` {z. norm z  m  (tT -` P. norm (z - t)  e)}"
        by force
    qed
    then show "{z. norm z  m  (tP. 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\_TAC})›
lemma Sard_lemma1:
  fixes P :: "(real^'n::{finite,wellorder}) set"
   assumes P: "dim P < CARD('n)" and "0  m" "0  e"
 obtains S where "S  lmeasurable"
            and "{z. norm(z - w)  m  (t  P. norm(z - w - t)  e)}  S"
            and "measure lebesgue S  (2 * e) * (2 * m) ^ (CARD('n) - 1)"
proof -
  obtain a where "a  0" "P  {x. a  x = 0}"
    using lowdim_subset_hyperplane [of P] P span_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  (tP. norm (z - w - t)  e)}  (+)w ` S"
      using subS by force
    show "measure lebesgue ((+)w ` S)  2 * e * (2 * m) ^ (CARD('n) - 1)"
      by (metis measure_translation mS)
  qed
qed

lemma Sard_lemma2:
  fixes f :: "real^'m::{finite,wellorder}  real^'n::{finite,wellorder}"
  assumes mlen: "CARD('m)  CARD('n)" (is "?m  ?n")
    and "B > 0" "bounded S"
    and derS: "x. x  S  (f has_derivative f' x) (at x within S)"
    and rank: "x. x  S  rank(matrix(f' x)) < CARD('n)"
    and B: "x. x  S  onorm(f' x)  B"
  shows "negligible(f ` S)"
proof -
  have lin_f': "x. x  S  linear(f' x)"
    using derS has_derivative_linear by blast
  show ?thesis
  proof (clarsimp simp add: negligible_outer_le)
    fix e :: "real"
    assume "e > 0"
    obtain c where csub: "S  cbox (- (vec c)) (vec c)" and "c > 0"
    proof -
      obtain b where b: "x. x  S  norm x  b"
        using bounded S by (auto simp: bounded_iff)
      show thesis
      proof
        have "- ¦b¦ - 1  x $ i  x $ i  ¦b¦ + 1" if "x  S" for x i
          using component_le_norm_cart [of x i] b [OF that] by auto
        then show "S  cbox (- vec (¦b¦ + 1)) (vec (¦b¦ + 1))"
          by (auto simp: mem_box_cart)
      qed auto
    qed
    then have box_cc: "box (- (vec c)) (vec c)  {}" and cbox_cc: "cbox (- (vec c)) (vec c)  {}"
      by (auto simp: interval_eq_empty_cart)
    obtain d where "d > 0" "d  B"
             and d: "(d * 2) * (4 * B) ^ (?n - 1)  e / (2*c) ^ ?m / ?m ^ ?m"
      apply (rule that [of "min B (e / (2*c) ^ ?m / ?m ^ ?m / (4 * B) ^ (?n - 1) / 2)"])
      using B > 0 c > 0 e > 0
      by (simp_all add: divide_simps min_mult_distrib_right)
    have "r. 0 < r  r  1/2 
              (x  S
                (y. y  S  norm(y - x) < r
                        norm(f y - f x - f' x (y - x))  d * norm(y - x)))" for x
    proof (cases "x  S")
      case True
      then obtain r where "r > 0"
              and "y. y  S; norm (y - x) < r
                        norm (f y - f x - f' x (y - x))  d * norm (y - x)"
        using derS d > 0 by (force simp: has_derivative_within_alt)
      then show ?thesis
        by (rule_tac x="min r (1/2)" in exI) simp
    next
      case False
      then show ?thesis
        by (rule_tac x="1/2" in exI) simp
    qed
    then obtain r where r12: "x. 0 < r x  r x  1/2"
            and r: "x y. x  S; y  S; norm(y - x) < r x
                           norm(f y - f x - f' x (y - x))  d * norm(y - x)"
      by metis
    then have ga: "gauge (λx. ball x (r x))"
      by (auto simp: gauge_def)
    obtain 𝒟 where 𝒟: "countable 𝒟" and sub_cc: "𝒟  cbox (- vec c) (vec c)"
      and cbox: "K. K  𝒟  interior K  {}  (u v. K = cbox u v)"
      and djointish: "pairwise (λA B. interior A  interior B = {}) 𝒟"
      and covered: "K. K  𝒟  x  S  K. K  ball x (r x)"
      and close: "u v. cbox u v  𝒟  n. i::'m. v $ i - u $ i = 2*c / 2^n"
      and covers: "S  𝒟"
      apply (rule covering_lemma [OF csub box_cc ga])
      apply (auto simp: Basis_vec_def cart_eq_inner_axis [symmetric])
      done
    let  = "measure lebesgue"
    have "T. T  lmeasurable  f ` (K  S)  T   T  e / (2*c) ^ ?m *  K"
      if "K  𝒟" for K
    proof -
      obtain u v where uv: "K = cbox u v"
        using cbox K  𝒟 by blast
      then have uv_ne: "cbox u v  {}"
        using cbox that by fastforce
      obtain x where x: "x  S  cbox u v" "cbox u v  ball x (r x)"
        using K  𝒟 covered uv by blast
      then have "dim (range (f' x)) < ?n"
        using rank_dim_range [of "matrix (f' x)"] 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 - f x - t)  d * norm(v - u))}  T"
            and measT: " T  (2 * (d * norm(v - u))) * (2 * ((2 * B) * norm(v - u))) ^ (?n - 1)"
                        (is "_  ?DVU")
        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). norm(z - f x - t)  d * norm(v - u))}"
          unfolding uv
        proof (clarsimp simp: mult.assoc, intro conjI)
          fix y
          assume y: "y  cbox u v" and "y  S"
          then have "norm (y - x) < r x"
            by (metis dist_norm mem_ball norm_minus_commute subsetCE x(2))
          then have le_dyx: "norm (f y - f x - f' x (y - x))  d * norm (y - x)"
            using r [of x y] x y  S by blast
          have yx_le: "norm (y - x)  norm (v - u)"
          proof (rule norm_le_componentwise_cart)
            show "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 < d 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_trans mem_ball)
            then have "norm (v - u) ^ ?n  norm (v - u) ^ ?m"
              by (simp add: power_decreasing [OF mlen])
            also have "   K * real (?m ^ ?m)"
            proof -
              obtain n where n: "i. v$i - u$i = 2 * c / 2^n"
                using close [of u v] K  𝒟 uv by blast
              have "norm (v - u) ^ ?m  (iUNIV. ¦(v - u) $ i¦) ^ ?m"
                by (intro norm_le_l1_cart power_mono) auto
              also have "  (iUNIV. 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  𝒟  g K  lmeasurable"
                    and sub_g: "K. K  𝒟  f ` (K  S)  g K"
                    and le_g: "K. K  𝒟   (g K)  e / (2*c)^?m *  K"
      by metis
    have le_e: " (i. g i)  e"
      if "  𝒟" "finite " for 
    proof -
      have " (i. g i)  (i.  (g i))"
        using meas_g   𝒟 by (auto intro: measure_UNION_le [OF finite ])
      also have "  (K. e / (2*c) ^ ?m *  K)"
        using   𝒟 sum_mono [OF le_g] by (meson le_g subsetCE sum_mono)
      also have " = e / (2*c) ^ ?m * (K.  K)"
        by (simp add: sum_distrib_left)
      also have "  e"
      proof -
        have " division_of "
        proof (rule division_ofI)
          show "K  "  "K  {}" "a b. K = cbox a b" if "K  " for K
            using K   covered cbox   𝒟 by (auto simp: Union_upper)
          show "interior K  interior L = {}" if "K  " and "L  " and "K  L" for K L
            by (metis (mono_tags, lifting)   𝒟 pairwiseD djointish pairwise_subset that)
        qed (use that in auto)
        then have "sum     ()"
          by (simp add: content_division)
        also have "   (cbox (- vec c) (vec c) :: (real, 'm) vec set)"
        proof (rule measure_mono_fmeasurable)
          show "  cbox (- vec c) (vec c)"
            by (meson Sup_subset_mono sub_cc order_trans   𝒟)
        qed (use  division_of  lmeasurable_division in auto)
        also have " = content (cbox (- vec c) (vec c) :: (real, 'm) vec set)"
          by simp
        also have "  (2 ^ ?m * c ^ ?m)"
          using c > 0 by (simp add: content_cbox_if_cart)
        finally have "sum    (2 ^ ?m * c ^ ?m)" .
        then show ?thesis
          using e > 0 c > 0 by (auto simp: 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 ` 𝒟)"
        using covers sub_g by force
      show " (g ` 𝒟)  lmeasurable"
        by (rule fmeasurable_UN_bound [OF countable 𝒟 meas_g le_e])
      show " ( (g ` 𝒟))  e"
        by (rule measure_UN_bound [OF countable 𝒟 meas_g le_e])
    qed
  qed
qed


theorem baby_Sard:
  fixes f :: "real^'m::{finite,wellorder}  real^'n::{finite,wellorder}"
  assumes mlen: "CARD('m)  CARD('n)"
    and der: "x. x  S  (f has_derivative f' x) (at x within S)"
    and rank: "x. x  S  rank(matrix(f' x)) < CARD('n)"
  shows "negligible(f ` S)"
proof -
  let ?U = "λn. {x  S. norm(x)  n  onorm(f' x)  real n}"
  have "x. x  S  n. norm x  real n  onorm (f' x)  real n"
    by (meson linear order_trans real_arch_simple)
  then have eq: "S = (n. ?U n)"
    by auto
  have "negligible (f ` ?U n)" for n
  proof (rule Sard_lemma2 [OF mlen])
    show "0 < real n + 1"
      by auto
    show "bounded (?U n)"
      using bounded_iff by blast
    show "(f has_derivative f' x) (at x within ?U n)" if "x  ?U n" for x
      using der that by (force intro: has_derivative_subset)
  qed (use rank in auto)
  then show ?thesis
    by (subst eq) (simp add: image_Union negligible_Union_nat)
qed


subsection‹A one-way version of change-of-variables not assuming injectivity. ›

lemma integral_on_image_ubound_weak:
  fixes f :: "real^'n::{finite,wellorder}  real"
  assumes S: "S  sets lebesgue"
      and f: "f  borel_measurable (lebesgue_on (g ` S))"
      and nonneg_fg:  "x. x  S  0  f(g x)"
      and der_g:   "x. x  S  (g has_derivative g' x) (at x within S)"
      and det_int_fg: "(λx. ¦det (matrix (g' x))¦ * f(g x)) integrable_on S"
      and meas_gim: "T. T  g ` S; T  sets lebesgue  {x  S. g x  T}  sets lebesgue"
    shows "f integrable_on (g ` S) 
           integral (g ` S) f  integral S (λx. ¦det (matrix (g' x))¦ * f(g x))"
         (is "_  _  ?b")
proof -
  let ?D = "λx. ¦det (matrix (g' x))¦"
  have cont_g: "continuous_on S g"
    using der_g has_derivative_continuous_on by blast
  have [simp]: "space (lebesgue_on S) = S"
    by (simp add: S)
  have gS_in_sets_leb: "g ` S  sets lebesgue"
    apply (rule differentiable_image_in_sets_lebesgue)
    using der_g by (auto simp: S differentiable_def differentiable_on_def)
  obtain h where nonneg_h: "n x. 0  h n x"
    and h_le_f: "n x. x  S  h n (g x)  f (g x)"
    and h_inc: "n x. h n x  h (Suc n) x"
    and h_meas: "n. h n  borel_measurable lebesgue"
    and fin_R: "n. finite(range (h n))"
    and lim: "x. x  g ` S  (λn. h n x)  f x"
  proof -
    let ?f = "λx. if x  g ` S then f x else 0"
    have "?f  borel_measurable lebesgue  (x. 0  ?f x)"
      by (auto simp: gS_in_sets_leb f nonneg_fg measurable_restrict_space_iff [symmetric])
    then show ?thesis
      apply (clarsimp simp add: borel_measurable_simple_function_limit_increasing)
      apply (rename_tac h)
      by (rule_tac h=h in that) (auto split: if_split_asm)
  qed
  have h_lmeas: "{t. h n (g t) = y}  S  sets lebesgue" for y n
  proof -
    have "space (lebesgue_on (UNIV::(real,'n) vec set)) = UNIV"
      by simp
    then have "((h n) -`{y}  g ` S)  sets (lebesgue_on (g ` S))"
      by (metis Int_commute borel_measurable_vimage h_meas image_eqI inf_top.right_neutral sets_restrict_space space_borel space_completion space_lborel)
    then have "({u. h n u = y}  g ` S)  sets lebesgue"
      using gS_in_sets_leb
      by (simp add: integral_indicator fmeasurableI2 sets_restrict_space_iff vimage_def)
    then have "{x  S. g x  ({u. h n u = y}  g ` S)}  sets lebesgue"
      using meas_gim[of "({u. h n u = y}  g ` S)"] by force
    moreover have "{t. h n (g t) = y}  S = {x  S. g x  ({u. h n u = y}  g ` S)}"
      by blast
    ultimately show ?thesis
      by auto
  qed
  have hint: "h n integrable_on g ` S  integral (g ` S) (h n)  integral S (λx. ?D x * h n (g x))"
          (is "?INT  ?lhs  ?rhs")  for n
  proof -
    let ?R = "range (h n)"
    have hn_eq: "h n = (λx. y?R. y * indicat_real {x. h n x = y} x)"
      by (simp add: indicator_def if_distrib fin_R cong: if_cong)
    have yind: "(λt. y * indicator{x. h n x = y} t) integrable_on (g ` S) 
                (integral (g ` S) (λt. y * indicator {x. h n x = y} t))
                  integral S (λt. ¦det (matrix (g' t))¦ * y * indicator {x. h n x = y} (g t))"
       if y: "y  ?R" for y::real
    proof (cases "y=0")
      case True
      then show ?thesis using gS_in_sets_leb integrable_0 by force
    next
      case False
      with that have "y > 0"
        using less_eq_real_def nonneg_h by fastforce
      have "(λx. if x  {t. h n (g t) = y} then ?D x else 0) integrable_on S"
      proof (rule measurable_bounded_by_integrable_imp_integrable)
        have "(λx. ?D x)  borel_measurable (lebesgue_on ({t. h n (g t) = y}  S))"
        proof -
          have "(λv. det (matrix (g' v)))  borel_measurable (lebesgue_on (S  {v. h n (g v) = y}))"
            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 lebesgue"
          by (rule borel_measurable_if_I [OF _ h_lmeas])
        then show "(λx. if x  {t. h n (g t) = y} then ?D x else 0)  borel_measurable (lebesgue_on S)"
          by (simp add: if_if_eq_conj Int_commute borel_measurable_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 y"
          if "x  S" for x
          using nonneg_h [of n x] y > 0 nonneg_fg [of x] h_le_f [of x n] that
          by (auto simp: divide_simps mult_left_mono)
      qed (use S in auto)
      then have int_det: "(λt. ¦det (matrix (g' t))¦) integrable_on ({t. h n (g t) = y}  S)"
        using integrable_restrict_Int by force
      have "(g ` ({t. h n (g t) = y}  S))  lmeasurable"
        by (blast intro: has_derivative_subset [OF der_g]  measurable_differentiable_image [OF h_lmeas] int_det)
      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_lmeas _ int_det])
      ultimately show ?thesis
        using y > 0 integral_restrict_Int [of S "{t. h n (g t) = y}" "λt. ¦det (matrix (g' t))¦ * y"]
        apply (simp add: integrable_on_indicator 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. yrange (h n). y * indicat_real {x. h n x = y} x)"
        by (metis hn_eq)
      also have " = (yrange (h n). integral (g ` S) (λx. y * indicat_real {x. h n x = y} x))"
        by (rule integral_sum [OF fin_R]) (use yind in blast)
      also have "  (yrange (h n). integral S (λu. ¦det (matrix (g' u))¦ * y * indicat_real {x. h n x = y} (g u)))"
        using yind by (force intro: sum_mono)
      also have " = integral S (λu. yrange (h n). ¦det (matrix (g' u))¦ * y * indicat_real {x. h n x = y} (g u))"
      proof (rule integral_sum [OF fin_R, symmetric])
        fix y assume y: "y  ?R"
        with nonneg_h have "y  0"
          by auto
        show "(λu. ¦det (matrix (g' u))¦ * y * indicat_real {x. h n x = y} (g u)) integrable_on S"
        proof (rule measurable_bounded_by_integrable_imp_integrable)
          have "(λx. indicat_real {x. h n x = y} (g x))  borel_measurable (lebesgue_on S)"
            using h_lmeas S
            by (auto simp: indicator_vimage [symmetric] borel_measurable_indicator_iff sets_restrict_space_iff)
          then show "(λu. ¦det (matrix (g' u))¦ * y * indicat_real {x. h n x = y} (g u))  borel_measurable (lebesgue_on S)"
            by (intro borel_measurable_times borel_measurable_abs borel_measurable_const borel_measurable_det_Jacobian [OF S der_g])
        next
          fix x
          assume "x  S"
          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_zero_right nonneg_fg)
          with y  0 show "norm (?D x * y * indicat_real {x. h n x = y} (g x))  ?D x * f(g x)"
            by (simp add: abs_mult mult.assoc mult_left_mono)
        qed (use S det_int_fg in auto)
      qed
      also have " = integral S (λT. ¦det (matrix (g' T))¦ *
                                        (yrange (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_Jacobian S  sets lebesgue)
        have eq: "{x  S. f x  a} = (b  (f ` S)  atMost a. {x. f x = b}  S)" for f and a::real
          by auto
        have "finite ((λx. h n (g x)) ` S  {..a})" for a
          by (force intro: finite_subset [OF _ fin_R])
        with h_lmeas [of n] show "(λx. h n (g x))  borel_measurable (lebesgue_on S)"
          apply (simp add: borel_measurable_vimage_halfspace_component_le S  sets lebesgue sets_restrict_space_iff eq)
          by (metis (mono_tags) SUP_inf sets.finite_UN)
      qed (use der_g in blast)
      then show "(λT. ¦det (matrix (g' T))¦ * h n (g T))  borel_measurable (lebesgue_on S)"
        by simp
      show "norm (?D x * h n (g x))  ?D x *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 (g' x))¦ * f(g x))"
         (is "_  _  ?b")
proof -
  let ?D = "λx. det (matrix (g' x))"
  define S' where "S'  {x  S. ?D x * f(g x)  0}"
  then have der_gS': "x. x  S'  (g has_derivative g' x) (at x within S')"
    by (metis (mono_tags, lifting) der_g has_derivative_subset mem_Collect_eq subset_iff)
  have "(λx. if x  S then ¦?D x¦ * f (g x) else 0) integrable_on UNIV"
    by (simp add: integrable_restrict_UNIV intS)
  then have Df_borel: "(λx. if x  S then ¦?D x¦ * f (g x) else 0)  borel_measurable lebesgue"
    using integrable_imp_measurable 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 (g x) else 0)"
        by (auto simp: S'_def)
      also have "  borel_measurable lebesgue"
        by (rule Df_borel)
      finally have *: "(λx. ¦?D x¦ * f (g x))  borel_measurable (lebesgue_on S')"
        by (simp add: borel_measurable_if_D)
      have "(λ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 blast
      moreover have "?h x = f(g x)" if "x  S'" for x
        using that by (auto simp: S'_def)
      ultimately have "(λx. f(g x))  borel_measurable (lebesgue_on S')"
        by (metis (no_types, lifting) measurable_lebesgue_cong)
      then show "{x  S'. f (g x)  T}  sets lebesgue"
        by (simp add: S'  sets lebesgue open T borel_measurable_vimage_open sets_restrict_space_iff)
      show "g differentiable_on {x  S'. f (g x)  T}"
        using der_g unfolding S'_def differentiable_def differentiable_on_def
        by (blast intro: has_derivative_subset)
    qed auto
    ultimately have "{x  g ` S'. f x  T}  sets lebesgue"
      by metis
    then show "{x  g ` S'. f x  T}  sets (lebesgue_on (g ` S'))"
      by (simp add: g ` S'  sets lebesgue sets_restrict_space_iff)
  qed
  have intS': "(λx. ¦?D x¦ * f (g x)) integrable_on S'"
    using intS
    by (rule integrable_spike_set) (auto simp: S'_def intro: empty_imp_negligible)
  have lebS': "{x  S'. g x  T}  sets lebesgue" if "T  g ` S'" "T  sets lebesgue" for T
  proof -
    have "g  borel_measurable (lebesgue_on S')"
      using der_gS' has_derivative_continuous_on S'
      by (blast intro: continuous_imp_measurable_on_sets_lebesgue)
    moreover have "{x  S'. g x  U}  sets lebesgue" if "negligible U" "U  g ` S'" for U
    proof (intro negligible_imp_sets negligible_differentiable_vimage that)
      fix x
      assume x: "x  S'"
      then have "linear (g' x)"
        using der_gS' has_derivative_linear by blast
      with x show "inj (g' x)"
        by (auto simp: S'_def det_nz_iff_inj)
    qed (use der_gS' in auto)
    ultimately show ?thesis
      using double_lebesgue_sets [OF S' gS' order_refl] that by blast
  qed
  have int_gS': "f integrable_on g ` S'  integral (g ` S') f  integral S' (λx. ¦?D x¦ * f(g x))"
    using integral_on_image_ubound_weak [OF S' f nonneg_fg der_gS' intS' lebS'] S'_def by blast
  have "negligible (g ` {x  S. det(matrix(g' x)) = 0})"
  proof (rule baby_Sard, simp_all)
    fix x
    assume x: "x  S  det (matrix (g' x)) = 0"
    then show "(g has_derivative g' x) (at x within {x  S. det (matrix (g' x)) = 0})"
      by (metis (no_types, lifting) der_g has_derivative_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 UNIV)"
    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, where f=f]
    by simp
qed


proposition absolutely_integrable_on_image:
  fixes f :: "real^'m::{finite,wellorder}  real^'n" and g :: "real^'m::_  real^'m::_"
  assumes der_g: "x. x  S  (g has_derivative g' x) (at x within S)"
    and intS: "(λx. ¦det (matrix (g' x))¦ *R f(g x)) absolutely_integrable_on S"
  shows "f absolutely_integrable_on (g ` S)"
  apply (rule absolutely_integrable_componentwise [OF absolutely_integrable_on_image_real [OF der_g]])
  using absolutely_integrable_component [OF intS]  by auto

proposition integral_on_image_ubound:
  fixes f :: "real^'n::{finite,wellorder}  real" and g :: "real^'n::_  real^'n::_"
  assumes"x. x  S  0  f(g x)"
    and "x. x  S  (g has_derivative g' x) (at x within S)"
    and "(λx. ¦det (matrix (g' x))¦ * f(g x)) integrable_on S"
  shows "integral (g ` S) f  integral S (λx. ¦det (matrix (g' x))¦ * f(g x))"
  using integral_on_image_ubound_nonneg [OF assms] by simp


subsection‹Change-of-variables theorem›

text‹The classic change-of-variables theorem. We have two versions with quite general hypotheses,
the first that the transforming function has a continuous inverse, the second that the base set is
Lebesgue measurable.›
lemma cov_invertible_nonneg_le:
  fixes f :: "real^'n::{finite,wellorder}  real" and g :: "real^'n::_  real^'n::_"
  assumes der_g: "x. x  S  (g has_derivative g' x) (at x within S)"
    and der_h: "y. y  T  (h has_derivative h' y) (at y within T)"
    and f0: "y. y  T  0  f y"
    and hg: "x. x  S  g x  T  h(g x) = x"
    and gh: "y. y  T  h y  S  g(h y) = y"
    and id: "y. y  T  h' y  g'(h y) = id"
  shows "f integrable_on T  (integral T f)  b 
             (λx. ¦det (matrix (g' x))¦ * f(g x)) integrable_on S 
             integral S (λx. ¦det (matrix (g' x))¦ * f(g x))  b"
        (is "?lhs = ?rhs")
proof -
  have Teq: "T = g`S" and Seq: "S = h`T"
    using hg gh image_iff by fastforce+
  have gS: "g differentiable_on S"
    by (meson der_g differentiable_def differentiable_on_def)
  let ?D = "λx. ¦det (matrix (g' x))¦ * f (g x)"
  show ?thesis
  proof
    assume ?lhs
    then have fT: "f integrable_on T" and intf: "integral T f  b"
      by blast+
    show ?rhs
    proof
      let ?fgh = "λx. ¦det (matrix (h' x))¦ * (¦det (matrix (g' (h x)))¦ * f (g (h x)))"
      have ddf: "?fgh x = f x"
        if "x  T" for x
      proof -
        have "matrix (h' x) ** matrix (g' (h x)) = mat 1"
          by (metis der_g der_h gh has_derivative_linear local.id matrix_compose matrix_id_mat_1 that)
        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) T"
  using cov_invertible_nonneg_le [OF assms]
  by (simp add: has_integral_iff) (meson eq_iff)


lemma cov_invertible_real:
  fixes f :: "real^'n::{finite,wellorder}  real" and g :: "real^'n::_  real^'n::_"
  assumes der_g: "x. x  S  (g has_derivative g' x) (at x within S)"
      and der_h: "y. y  T  (h has_derivative h' y) (at y within T)"
      and hg: "x. x  S  g x  T  h(g x) = x"
      and gh: "y. y  T  h y  S  g(h y) = y"
      and id: "y. y  T  h' y  g'(h y) = id"
  shows "(λx. ¦det (matrix (g' x))¦ * f(g x)) absolutely_integrable_on S 
           integral S (λx. ¦det (matrix (g' x))¦ * f(g x)) = b 
         f absolutely_integrable_on T  integral T f = b"
         (is "?lhs = ?rhs")
proof -
  have Teq: "T = g`S" and Seq: "S = h`T"
    using hg gh image_iff by fastforce+
  let ?DP = "λx. ¦det (matrix (g' x))¦ * f(g x)" and ?DN = "λx. ¦det (matrix (g' x))¦ * -f(g x)"
  have "+": "(?DP has_integral b) {x  S. f (g x) > 0}  (f has_integral b) {y  T. f y > 0}" for b
  proof (rule cov_invertible_nonneg_eq)
    have *: "(λx. f (g x)) -` Y  {x  S. f (g x) > 0}
          = ((λx. f (g x)) -` Y  S)  {x  S. f (g x) > 0}" for Y
      by auto
    show "(g has_derivative g' x) (at x within {x  S. f (g x) > 0})" if "x  {x  S. f (g x) > 0}" for x
      using that der_g has_derivative_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)
  have "-": "(?DN has_integral b) {x  S. f (g x) < 0}  ((λx. - f x) has_integral b) {y  T. f y < 0}" for b
  proof (rule cov_invertible_nonneg_eq)
    have *: "(λx. - f (g x)) -` y  {x  S. f (g x) < 0}
          = ((λx. f (g x)) -` uminus ` y  S)  {x  S. f (g x) < 0}" for y
      using image_iff by fastforce
    show "(g has_derivative g' x) (at x within {x  S. f (g x) < 0})" if "x  {x  S. f (g x) < 0}" for x
      using that der_g has_derivative_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 UNIV)"
      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_negligible)
    have "?DP absolutely_integrable_on {x  S. ?DP x < 0}"
      using LHS by (fast intro!: set_integrable_subset [OF _, of _ S] SN)
    then have aN: "?DP absolutely_integrable_on {x  S. f (g x) < 0}"
      by (rule absolutely_integrable_spike_set) (auto simp: mult_less_0_iff empty_imp_negligible)
    have fN: "f integrable_on {y  T. f y < 0}"
             "integral {y  T. f y < 0} f = integral {x  S. f (g x) < 0} ?DP"
      using "-" [of "integral {x  S. f(g x) < 0} ?DN"] aN
      by (auto simp: set_lebesgue_integral_eq_integral has_integral_iff integrable_neg_iff)
    have faN: "f absolutely_integrable_on {y  T. f y < 0}"
    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 UNIV)"
      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) > 0 then 1 else 0) * ?DP x" for x
        by force
      have "?DP absolutely_integrable_on ({x  S. f (g x) < 0}  {x  S. f (g x) > 0})"
        by (rule absolutely_integrable_Un [OF aDN aDP])
      then show I: "?DP absolutely_integrable_on S"
        by (simp add: indicator_def 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  integral S (λx. ¦det (matrix (g' x))¦ * (f(g x) $ i)) = b $ i) 
        ((λx. f x $ i) absolutely_integrable_on T  integral T (λx. f x $ i) = b $ i)" for i
    by (rule cov_invertible_real [OF der_g der_h hg gh id])
  then have "?D absolutely_integrable_on S  (?D has_integral b) S 
        f absolutely_integrable_on T  (f has_integral b) T"
    unfolding absolutely_integrable_componentwise_iff [where f=f] has_integral_componentwise_iff [of f]
              absolutely_integrable_componentwise_iff [where f="?D"] has_integral_componentwise_iff [of ?D]
    by (auto simp: all_conj_distrib Basis_vec_def cart_eq_inner_axis [symmetric]
           has_integral_iff set_lebesgue_integral_eq_integral)
  then show ?thesis
    using absolutely_integrable_on_def by blast
qed


lemma cv_inv_version4:
  fixes f :: "real^'m::{finite,wellorder}  real^'n" and g :: "real^'m::_  real^'m::_"
  assumes der_g: "x. x  S  (g has_derivative g' x) (at x within S)  invertible(matrix(g' x))"
    and hg: "x. x  S  continuous_on (g ` S) h  h(g x) = x"
  shows "(λx. ¦det (matrix (g' x))¦ *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' x = id"
    using der_g matrix_invertible has_derivative_linear by blast
  then obtain h' where h':
    "x. x  S
            (g has_derivative g' x) (at x within S) 
               linear (h' x)  g' x  (h' x) = id  (h' x)  g' x = id"
    by metis
  show ?thesis
  proof (rule cv_inv_version3)
    show "y. y  g ` S  (h has_derivative h' (h y)) (at y within g ` S)"
      using h' hg
      by (force simp: continuous_on_eq_continuous_within intro!: has_derivative_inverse_within)
  qed (use h' hg in auto)
qed


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  integral S (λx. ¦det (matrix (g' x))¦ *R f(g x)) = b 
         f absolutely_integrable_on (g ` S)  integral (g ` S) f = b"
    (is "?lhs = ?rhs")
proof -
  let ?S = "{x  S. invertible (matrix (g' x))}" and ?D = "λx. ¦det (matrix (g' x))¦ *R f(g x)"
  have *: "?D absolutely_integrable_on ?S  integral ?S ?D = b
            f absolutely_integrable_on (g ` ?S)  integral (g ` ?S) f = b"
  proof (rule cv_inv_version4)
    show "(g has_derivative g' x) (at x within ?S)  invertible (matrix (g' x))"
      if "x  ?S" for x
      using der_g that has_derivative_subset that by fastforce
    show "continuous_on (g ` ?S) h  h (g x) = x"
      if "x  ?S" for x
      using that continuous_on_subset [OF conth]  by (simp add: hg image_mono)
  qed
  have "(g has_derivative g' x) (at x within {x  S. rank (matrix (g' x)) < CARD('m)})" if "x  S" for x
    by (metis (no_types, lifting) der_g has_derivative_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. mn. F m"
  let ?lift = "vec::realreal^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 f :: "real^'m::_  real^'k"
  proof (rule has_absolute_integral_change_of_variables_compact)
    show "compact (?U n)"
      by (simp add: compact compact_UN)
    show "(g has_derivative g' x) (at x within (?U n))"
      if "x  ?U n" for x
      using that by (blast intro!: has_derivative_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 (mn. 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  (mk. g ` F m) then f x else 0) absolutely_integrable_on UNIV" for k
        unfolding absolutely_integrable_restrict_UNIV
        using fag by (simp add: image_UN)
      let ?nf = "λn x. if x  (mn. 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 (?lift  norm  f) (g x))"]
            unfolding absolutely_integrable_on_1_iff integral_on_1_eq by (auto simp: o_def)
        }
        moreover have "bounded (range (λk. integral (?U k) (norm  ?D)))"
          unfolding bounded_iff
        proof (rule exI, clarify)
          fix k
          show "norm (integral (?U k) (norm  ?D))  integral (n. F n) (norm  ?D)"
            unfolding integral_restrict_UNIV [of _ "norm  ?D", symmetric]
          proof (rule integral_norm_bound_integral)
            show "(λx. if x   (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  (mk. 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  (mk. 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 rangeI subsetI)
        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 (mn. g ` F m)"
      "(λn. integral (mn. 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 (mn. 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 (mn. 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) else 0)" for 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 (mn. 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 C N"
    using lebesgue_set_almost_fsigma [OF S] .
  then obtain F :: "nat  (real^'m::_) set"
    where F: "range F  Collect compact" and Ceq: "C = Union(range F)"
    using fsigma_Union_compact by metis
  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 sup.cobounded2)
    with negligible N
    have neg_gN: "negligible (g ` N)"
      by (blast intro: negligible_differentiable_image_negligible)
    have neg: "negligible {x  g ` C - g ` S. f x  0}"
              "negligible {x  g ` S - g ` C. f x  0}"
      using CNS by (blast intro: negligible_subset [OF neg_gN])+
    then show "(f absolutely_integrable_on g ` C) = (f absolutely_integrable_on g ` S)"
      by (rule absolutely_integrable_spike_set_eq)
    show "(integral (g ` C) f = b)  (integral (g ` S) f = b)"
      using integral_spike_set [OF neg] by simp
  qed
  ultimately show ?thesis
    by simp
qed


corollary absolutely_integrable_change_of_variables:
  fixes f :: "real^'m::{finite,wellorder}  real^'n" and g :: "real^'m::_  real^'m::_"
  assumes "S  sets lebesgue"
    and "x. x  S  (g has_derivative g' x) (at x within S)"
    and "inj_on g S"
  shows "f absolutely_integrable_on (g ` S)
      (λx. ¦det (matrix (g' x))¦ *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 ?lift ` S)"
    if "z  S" for z
    using der_g [OF that]
    by (simp add: has_vector_derivative_def has_derivative_vector_1)
  then have der': "x. x  ?lift ` S 
        (?lift  g  ?drop has_derivative (*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 $ i) S
     (λx. f x $ i) absolutely_integrable_on g ` S  ((λx. f x $ i) has_integral b $ i) (g ` S))" for i
    using has_absolute_integral_change_of_variables [OF S' der' inj', of "λx. ?lift(f (?drop x) $ i)" "?lift (b$i)"]
    unfolding integrable_on_1_iff integral_on_1_eq absolutely_integrable_on_1_iff absolutely_integrable_drop absolutely_integrable_on_def
    by (auto simp: image_comp o_def integral_vec1_eq has_integral_iff)
  then have "?fg absolutely_integrable_on S  (?fg has_integral b) S
          f absolutely_integrable_on (g ` S)  (f has_integral b) (g ` S)"
    unfolding has_integral_componentwise_iff [where y=b]
           absolutely_integrable_componentwise_iff [where f=f]
           absolutely_integrable_componentwise_iff [where f = ?fg]
    by (force simp: Basis_vec_def cart_eq_inner_axis)
  then show ?thesis
    using absolutely_integrable_on_def by blast
qed


corollary absolutely_integrable_change_of_variables_1:
  fixes f :: "real  real^'n::{finite,wellorder}" and g :: "real  real"
  assumes S: "S  sets lebesgue"
    and der_g: "x. x  S  (g has_vector_derivative g' x) (at x within S)"
    and inj: "inj_on g S"
  shows "(f absolutely_integrable_on g ` S 
             (λx. ¦g' x¦ *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¦ *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 -
  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_derivative h by blast
  qed (use h in auto)
qed

lemma absolutely_integrable_change_of_variables_linear:
  fixes f :: "real^'m::{finite,wellorder}  real^'n" and g :: "real^'m::_  real^'m::_"
  assumes "linear g"
  shows "(λx. ¦det (matrix g)¦ *R f(g x)) absolutely_integrable_on S
      f absolutely_integrable_on (g ` S)"
  using assms has_absolute_integral_change_of_variables_linear by blast

lemma absolutely_integrable_on_linear_image:
  fixes f :: "real^'m::{finite,wellorder}  real^'n" and g :: "real^'m::_  real^'m::_"
  assumes "linear g"
  shows "f absolutely_integrable_on (g ` S)
      (f  g) absolutely_integrable_on S  det(matrix g) = 0"
  unfolding assms absolutely_integrable_change_of_variables_linear [OF assms, symmetric] absolutely_integrable_on_scaleR_iff
  by (auto simp: set_integrable_def)

lemma integral_change_of_variables_linear:
  fixes f :: "real^'m::{finite,wellorder}  real^'n" and g :: "real^'m::_  real^'m::_"
  assumes "linear g"
      and "f absolutely_integrable_on (g ` S)  (f  g) absolutely_integrable_on S"
    shows "integral (g ` S) f = ¦det (matrix g)¦ *R integral S (f  g)"
proof -
  have "((λx. ¦det (matrix g)¦ *R f (g x)) absolutely_integrable_on S)  (f absolutely_integrable_on g ` S)"
    using absolutely_integrable_on_linear_image assms by blast
  moreover
  have ?thesis if "((λx. ¦det (matrix g)¦ *R f (g x)) absolutely_integrable_on S)" "(f absolutely_integrable_on g ` S)"
    using has_absolute_integral_change_of_variables_linear [OF linear g] that
    by (auto simp: o_def)
  ultimately show ?thesis
    using absolutely_integrable_change_of_variables_linear [OF linear g]
    by blast
qed

subsection‹Change of variable for measure›

lemma has_measure_differentiable_image:
  fixes f :: "real^'n::{finite,wellorder}  real^'n::_"
  assumes "S  sets lebesgue"
      and "x. x  S  (f has_derivative f' x) (at x within S)"
      and "inj_on f S"
  shows "f ` S  lmeasurable  measure lebesgue (f ` S) = m
      ((λx. ¦det (matrix (f' x))¦) has_integral m) S"
  using has_absolute_integral_change_of_variables [OF assms, of "λx. (1::real^1)" "vec m"]
  unfolding absolutely_integrable_on_1_iff integral_on_1_eq integrable_on_1_iff absolutely_integrable_on_def
  by (auto simp: has_integral_iff lmeasurable_iff_integrable_on lmeasure_integral)

lemma measurable_differentiable_image_eq:
  fixes f :: "real^'n::{finite,wellorder}  real^'n::_"
  assumes "S  sets lebesgue"
      and "x. x  S  (f has_derivative f' x) (at x within S)"
      and "inj_on f S"
  shows "f ` S  lmeasurable  (λx. ¦det (matrix (f' x))¦) integrable_on S"
  using has_measure_differentiable_image [OF assms]
  by blast

lemma measurable_differentiable_image_alt:
  fixes f :: "real^'n::{finite,wellorder}  real^'n::_"
  assumes "S  sets lebesgue"
    and "x. x  S  (f has_derivative f' x) (at x within S)"
    and "inj_on f S"
  shows "f ` S  lmeasurable  (λx. ¦det (matrix (f' x))¦) absolutely_integrable_on S"
  using measurable_differentiable_image_eq [OF assms]
  by (simp only: absolutely_integrable_on_iff_nonneg)

lemma measure_differentiable_image_eq:
  fixes f :: "real^'n::{finite,wellorder}  real^'n::_"
  assumes S: "S  sets lebesgue"
    and der_f: "x. x  S  (f has_derivative f' x) (at x within S)"
    and inj: "inj_on f S"
    and intS: "(λx. ¦det (matrix (f' x))¦) integrable_on S"
  shows "measure lebesgue (f ` S) = integral S (λx. ¦det (matrix (f' x))¦)"
  using measurable_differentiable_image_eq [OF S der_f inj]
        assms has_measure_differentiable_image by blast

end