diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -6,9 +6,7 @@
 
 theory Henstock_Kurzweil_Integration
 imports
-  Derivative
-  Uniform_Limit
-  "~~/src/HOL/Library/Indicator_Function"
+  Lebesgue_Measure
 begin
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -22,122 +20,19 @@
 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
 
+lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
+  by auto
+
 declare norm_triangle_ineq4[intro]
 
-lemma simple_image: "{f x |x . x \<in> s} = f ` s"
-  by blast
-
-lemma linear_simps:
-  assumes "bounded_linear f"
-  shows
-    "f (a + b) = f a + f b"
-    "f (a - b) = f a - f b"
-    "f 0 = 0"
-    "f (- a) = - f a"
-    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
-proof -
-  interpret f: bounded_linear f by fact
-  show "f (a + b) = f a + f b" by (rule f.add)
-  show "f (a - b) = f a - f b" by (rule f.diff)
-  show "f 0 = 0" by (rule f.zero)
-  show "f (- a) = - f a" by (rule f.minus)
-  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
-qed
-
-lemma bounded_linearI:
-  assumes "\<And>x y. f (x + y) = f x + f y"
-    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
-    and "\<And>x. norm (f x) \<le> norm x * K"
-  shows "bounded_linear f"
-  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
-
-lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
-  by (rule bounded_linear_inner_left)
-
-lemma transitive_stepwise_lt_eq:
-  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
-  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
-  (is "?l = ?r")
-proof safe
-  assume ?r
-  fix n m :: nat
-  assume "m < n"
-  then show "R m n"
-  proof (induct n arbitrary: m)
-    case 0
-    then show ?case by auto
-  next
-    case (Suc n)
-    show ?case
-    proof (cases "m < n")
-      case True
-      show ?thesis
-        apply (rule assms[OF Suc(1)[OF True]])
-        using \<open>?r\<close>
-        apply auto
-        done
-    next
-      case False
-      then have "m = n"
-        using Suc(2) by auto
-      then show ?thesis
-        using \<open>?r\<close> by auto
-    qed
-  qed
-qed auto
-
-lemma transitive_stepwise_gt:
-  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
-  shows "\<forall>n>m. R m n"
-proof -
-  have "\<forall>m. \<forall>n>m. R m n"
-    apply (subst transitive_stepwise_lt_eq)
-    apply (blast intro: assms)+
-    done
-  then show ?thesis by auto
-qed
-
-lemma transitive_stepwise_le_eq:
-  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
-  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
-  (is "?l = ?r")
-proof safe
-  assume ?r
-  fix m n :: nat
-  assume "m \<le> n"
-  then show "R m n"
-  proof (induct n arbitrary: m)
-    case 0
-    with assms show ?case by auto
-  next
-    case (Suc n)
-    show ?case
-    proof (cases "m \<le> n")
-      case True
-      with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
-        by blast
-    next
-      case False
-      then have "m = Suc n"
-        using Suc(2) by auto
-      then show ?thesis
-        using assms(1) by auto
-    qed
-  qed
-qed auto
-
 lemma transitive_stepwise_le:
-  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
-    and "\<And>n. R n (Suc n)"
+  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
   shows "\<forall>n\<ge>m. R m n"
-proof -
-  have "\<forall>m. \<forall>n\<ge>m. R m n"
-    apply (subst transitive_stepwise_le_eq)
-    apply (blast intro: assms)+
-    done
-  then show ?thesis by auto
-qed
-
+proof (intro allI impI)
+  show "m \<le> n \<Longrightarrow> R m n" for n
+    by (induction rule: dec_induct)
+       (use assms in blast)+
+qed
 
 subsection \<open>Some useful lemmas about intervals.\<close>
 
@@ -208,13 +103,28 @@
     "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
   using interior_Union_subset_cbox[of f "UNIV - s"] by auto
 
+lemma interval_split:
+  fixes a :: "'a::euclidean_space"
+  assumes "k \<in> Basis"
+  shows
+    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
+    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
+  apply (rule_tac[!] set_eqI)
+  unfolding Int_iff mem_box mem_Collect_eq
+  using assms
+  apply auto
+  done
+
+lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
+  by (simp add: box_ne_empty)
+
 subsection \<open>Bounds on intervals where they exist.\<close>
 
 definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
 
 definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
-   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
+  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
 
 lemma interval_upperbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
@@ -242,7 +152,6 @@
     and "interval_lowerbound (cbox a b) = a"
   using assms unfolding box_ne_empty by auto
 
-
 lemma interval_upperbound_Times:
   assumes "A \<noteq> {}" and "B \<noteq> {}"
   shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
@@ -273,219 +182,83 @@
 
 subsection \<open>Content (length, area, volume...) of an interval.\<close>
 
-definition "content (s::('a::euclidean_space) set) =
-  (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
-
-lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
-  unfolding box_eq_empty unfolding not_ex not_less by auto
-
-lemma content_cbox:
-  fixes a :: "'a::euclidean_space"
-  assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-  using interval_not_empty[OF assms]
-  unfolding content_def
-  by auto
-
-lemma content_cbox':
-  fixes a :: "'a::euclidean_space"
-  assumes "cbox a b \<noteq> {}"
-  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-    using assms box_ne_empty(1) content_cbox by blast
+abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
+  where "content s \<equiv> measure lborel s"
+
+lemma content_cbox_cases:
+  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
+  by (simp add: measure_lborel_cbox_eq inner_diff)
+
+lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+  unfolding content_cbox_cases by simp
+
+lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+  by (simp add: box_ne_empty inner_diff)
 
 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
-  by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
+  by simp
 
 lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
   by (auto simp: content_real)
 
-lemma content_singleton[simp]: "content {a} = 0"
-proof -
-  have "content (cbox a a) = 0"
-    by (subst content_cbox) (auto simp: ex_in_conv)
-  then show ?thesis by (simp add: cbox_sing)
-qed
-
-lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
- proof -
-   have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
-    by auto
-  have "0 \<in> cbox 0 (One::'a)"
-    unfolding mem_box by auto
-  then show ?thesis
-     unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
- qed
-
-lemma content_pos_le[intro]:
-  fixes a::"'a::euclidean_space"
-  shows "0 \<le> content (cbox a b)"
-proof (cases "cbox a b = {}")
-  case False
-  then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-    unfolding box_ne_empty .
-  have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
-    apply (rule setprod_nonneg)
-    unfolding interval_bounds[OF *]
-    using *
-    apply auto
-    done
-  also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
-  finally show ?thesis .
-qed (simp add: content_def)
-
-corollary content_nonneg [simp]:
-  fixes a::"'a::euclidean_space"
-  shows "~ content (cbox a b) < 0"
-using not_le by blast
-
-lemma content_pos_lt:
-  fixes a :: "'a::euclidean_space"
-  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
-  shows "0 < content (cbox a b)"
-  using assms
-  by (auto simp: content_def box_eq_empty intro!: setprod_pos)
-
-lemma content_eq_0:
-  "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
-  by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
-
-lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
-  by auto
-
-lemma content_cbox_cases:
-  "content (cbox a (b::'a::euclidean_space)) =
-    (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
-  by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
+lemma content_singleton: "content {a} = 0"
+  by simp
+
+lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
+  by simp
+
+lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
+  by simp
+
+corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
+  using not_le by blast
+
+lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
+  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
+
+lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
+  by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
 
 lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
-  unfolding content_eq_0 interior_cbox box_eq_empty
-  by auto
-
-lemma content_pos_lt_eq:
-  "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
-proof (rule iffI)
-  assume "0 < content (cbox a b)"
-  then have "content (cbox a b) \<noteq> 0" by auto
-  then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
-    unfolding content_eq_0 not_ex not_le by fastforce
-next
-  assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
-  then show "0 < content (cbox a b)"
-    by (metis content_pos_lt)
-qed
+  unfolding content_eq_0 interior_cbox box_eq_empty by auto
+
+lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
+  by (auto simp add: content_cbox_cases less_le setprod_nonneg)
 
 lemma content_empty [simp]: "content {} = 0"
-  unfolding content_def by auto
+  by simp
 
 lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
   by (simp add: content_real)
 
-lemma content_subset:
-  assumes "cbox a b \<subseteq> cbox c d"
-  shows "content (cbox a b) \<le> content (cbox c d)"
-proof (cases "cbox a b = {}")
-  case True
-  then show ?thesis
-    using content_pos_le[of c d] by auto
-next
-  case False
-  then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-    unfolding box_ne_empty by auto
-  then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
-    unfolding mem_box by auto
-  have "cbox c d \<noteq> {}" using assms False by auto
-  then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
-    using assms unfolding box_ne_empty by auto
-  have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
-    using ab_ne by auto
-  moreover
-  have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
-    using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
-          assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
-      by (metis diff_mono)
-  ultimately show ?thesis
-    unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
-    by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
-qed
+lemma content_subset: "cbox a b \<subseteq> cbox c d \<Longrightarrow> content (cbox a b) \<le> content (cbox c d)"
+  unfolding measure_def
+  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
 
 lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
   unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
 
-lemma content_times[simp]: "content (A \<times> B) = content A * content B"
-proof (cases "A \<times> B = {}")
-  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
-  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
-  assume nonempty: "A \<times> B \<noteq> {}"
-  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
-      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
-  also have "... = content A * content B" unfolding content_def using nonempty
-    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
-    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
-    done
-  finally show ?thesis .
-qed (auto simp: content_def)
-
 lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
-  by (simp add: cbox_Pair_eq)
+  unfolding measure_lborel_cbox_eq Basis_prod_def
+  apply (subst setprod.union_disjoint)
+  apply (auto simp: bex_Un ball_Un)
+  apply (subst (1 2) setprod.reindex_nontrivial)
+  apply auto
+  done
 
 lemma content_cbox_pair_eq0_D:
    "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
   by (simp add: content_Pair)
 
-lemma content_eq_0_gen:
-  fixes s :: "'a::euclidean_space set"
-  assumes "bounded s"
-  shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)"  (is "_ = ?rhs")
-proof safe
-  assume "content s = 0" then show ?rhs
-    apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
-    apply (rule_tac x=a in bexI)
-    apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
-    apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
-    apply (drule cSUP_eq_cINF_D)
-    apply (auto simp: bounded_inner_imp_bdd_above [OF assms]  bounded_inner_imp_bdd_below [OF assms])
-    done
-next
-  fix i a
-  assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
-  then show "content s = 0"
-    apply (clarsimp simp: content_def)
-    apply (rule_tac x=i in bexI)
-    apply (auto simp: interval_upperbound_def interval_lowerbound_def)
-    done
-qed
-
-lemma content_0_subset_gen:
-  fixes a :: "'a::euclidean_space"
-  assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
-proof -
-  have "bounded s"
-    using assms by (metis bounded_subset)
-  then show ?thesis
-    using assms
-    by (auto simp: content_eq_0_gen)
-qed
-
-lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
-  by (simp add: content_0_subset_gen bounded_cbox)
-
-
-lemma interval_split:
-  fixes a :: "'a::euclidean_space"
-  assumes "k \<in> Basis"
-  shows
-    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
-    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
-  apply (rule_tac[!] set_eqI)
-  unfolding Int_iff mem_box mem_Collect_eq
-  using assms
-  apply auto
-  done
+lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
+  using emeasure_mono[of s "cbox a b" lborel]
+  by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
 
 lemma content_split:
   fixes a :: "'a::euclidean_space"
   assumes "k \<in> Basis"
   shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+  -- \<open>Prove using measure theory\<close>
 proof cases
   note simps = interval_split[OF assms] content_cbox_cases
   have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
@@ -2040,11 +1813,6 @@
   "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
   unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
 
-lemma
-  shows real_inner_1_left: "inner 1 x = x"
-  and real_inner_1_right: "inner x 1 = x"
-  by simp_all
-
 lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
   by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
 
@@ -3988,8 +3756,7 @@
   have "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
     using norm_setsum by blast
   also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
-    apply (simp add: setsum_right_distrib[symmetric] mult.commute)
-    using assms(2) mult_right_mono by blast
+    by (simp add: setsum_right_distrib[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg)
   also have "... \<le> e * content (cbox a b)"
     apply (rule mult_left_mono [OF _ e])
     apply (simp add: sumeq)
@@ -4458,65 +4225,70 @@
   assumes "0 < e"
     and k: "k \<in> Basis"
   obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
-proof (cases "content (cbox a b) = 0")
-  case True
-  then have ce: "content (cbox a b) < e"
-    by (metis \<open>0 < e\<close>)
+proof cases
+  assume *: "a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j)"
+  define a' where "a' d = (\<Sum>j\<in>Basis. (if j = k then max (a\<bullet>j) (c - d) else a\<bullet>j) *\<^sub>R j)" for d
+  define b' where "b' d = (\<Sum>j\<in>Basis. (if j = k then min (b\<bullet>j) (c + d) else b\<bullet>j) *\<^sub>R j)" for d
+
+  have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)"
+    by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
+  also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
+    using k *
+    by (intro setprod_zero bexI[OF _ k])
+       (auto simp: b'_def a'_def inner_diff inner_setsum_left inner_not_same_Basis intro!: setsum.cong)
+  also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
+    ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
+  proof (intro tendsto_cong eventually_at_rightI)
+    fix d :: real assume d: "d \<in> {0<..<1}"
+    have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d
+      using * d k by (auto simp add: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
+    moreover have "j \<in> Basis \<Longrightarrow> a' d \<bullet> j \<le> b' d \<bullet> j" for j
+      using * d k by (auto simp: a'_def b'_def)
+    ultimately show "(\<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) = content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})"
+      by simp
+  qed simp
+  finally have "((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" .
+  from order_tendstoD(2)[OF this \<open>0<e\<close>]
+  obtain d' where "0 < d'" and d': "\<And>y. y > 0 \<Longrightarrow> y < d' \<Longrightarrow> content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> y}) < e"
+    by (subst (asm) eventually_at_right[of _ 1]) auto
   show ?thesis
-    apply (rule that[of 1])
-    apply simp
-    unfolding interval_doublesplit[OF k]
-    apply (rule le_less_trans[OF content_subset ce])
-    apply (auto simp: interval_doublesplit[symmetric] k)
-    done
+    by (rule that[of "d'/2"], insert \<open>0<d'\<close> d'[of "d'/2"], auto)
 next
-  case False
-  define d where "d = e / 3 / setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
-  note False[unfolded content_eq_0 not_ex not_le, rule_format]
-  then have "\<And>x. x \<in> Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x"
-    by (auto simp add:not_le)
-  then have prod0: "0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
-    by (force simp add: setprod_pos field_simps)
-  then have "d > 0"
-    using assms
-    by (auto simp add: d_def field_simps)
-  then show ?thesis
-  proof (rule that[of d])
-    have *: "Basis = insert k (Basis - {k})"
-      using k by auto
-    have less_e: "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
-    proof -
-      have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d"
+  assume *: "\<not> (a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j))"
+  then have "(\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j) \<or> (c < a \<bullet> k \<or> b \<bullet> k < c)"
+    by (auto simp: not_le)
+  show thesis
+  proof cases
+    assume "\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j"
+    then have [simp]: "cbox a b = {}"
+      using box_ne_empty(1)[of a b] by auto
+    show ?thesis
+      by (rule that[of 1]) (simp_all add: \<open>0<e\<close>)
+  next
+    assume "\<not> (\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j)"
+    with * have "c < a \<bullet> k \<or> b \<bullet> k < c"
+      by auto
+    then show thesis
+    proof
+      assume c: "c < a \<bullet> k"
+      moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
+        using k c by (auto simp: cbox_def)
+      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
+        using k by (auto simp: cbox_def)
+      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
         by auto
-      also have "\<dots> < e / (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i)"
-        unfolding d_def
-        using assms prod0
-        by (auto simp add: field_simps)
-      finally show "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
-        unfolding pos_less_divide_eq[OF prod0] .
-    qed
-    show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
-    proof (cases "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {}")
-      case True
-      then show ?thesis
-        using assms by simp
     next
-      case False
-      then have
-          "(\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
-                interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i)
-           = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
-        by (simp add: box_eq_empty interval_doublesplit[OF k])
-      then show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
-        unfolding content_def
-        using assms False
-        apply (subst *)
-        apply (subst setprod.insert)
-        apply (simp_all add: interval_doublesplit[OF k] box_eq_empty not_less less_e)
-        done
-    qed
-  qed
-qed
+      assume c: "b \<bullet> k < c"
+      moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
+        using k c by (auto simp: cbox_def)
+      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
+        using k by (auto simp: cbox_def)
+      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
+        by auto
+    qed
+  qed
+qed
+
 
 lemma negligible_standard_hyperplane[intro]:
   fixes k :: "'a::euclidean_space"
@@ -5695,6 +5467,7 @@
     by auto
   from fundamental_theorem_of_calculus[rule_format, OF \<open>a \<le> b\<close> deriv]
   have "(i has_integral ?sum b - ?sum a) {a .. b}"
+    using atLeastatMost_empty'[simp del]
     by (simp add: i_def g_def Dg_def)
   also
   have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
@@ -6036,7 +5809,7 @@
         done
       show ?thesis
         using False
-        apply (simp add: abs_eq_content del: content_real_if)
+        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
         using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
         done
@@ -6054,7 +5827,7 @@
         done
       have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
         using True
-        apply (simp add: abs_eq_content del: content_real_if)
+        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
         using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
         done
@@ -6274,6 +6047,62 @@
 
 subsection \<open>Special case of a basic affine transformation.\<close>
 
+lemma AE_lborel_inner_neq:
+  assumes k: "k \<in> Basis"
+  shows "AE x in lborel. x \<bullet> k \<noteq> c"
+proof -
+  interpret finite_product_sigma_finite "\<lambda>_. lborel" Basis
+    proof qed simp
+
+  have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c} = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
+    using k
+    by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
+       (auto simp: space_PiM PiE_iff extensional_def split: if_split_asm)
+  also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
+    by (intro measure_times) auto
+  also have "\<dots> = 0"
+    by (intro setprod_zero bexI[OF _ k]) auto
+  finally show ?thesis
+    by (subst AE_iff_measurable[OF _ refl]) auto
+qed
+
+lemma content_image_stretch_interval:
+  fixes m :: "'a::euclidean_space \<Rightarrow> real"
+  defines "s f x \<equiv> (\<Sum>k::'a\<in>Basis. (f k * (x\<bullet>k)) *\<^sub>R k)"
+  shows "content (s m ` cbox a b) = \<bar>\<Prod>k\<in>Basis. m k\<bar> * content (cbox a b)"
+proof cases
+  have s[measurable]: "s f \<in> borel \<rightarrow>\<^sub>M borel" for f
+    by (auto simp: s_def[abs_def])
+  assume m: "\<forall>k\<in>Basis. m k \<noteq> 0"
+  then have s_comp_s: "s (\<lambda>k. 1 / m k) \<circ> s m = id" "s m \<circ> s (\<lambda>k. 1 / m k) = id"
+    by (auto simp: s_def[abs_def] fun_eq_iff euclidean_representation)
+  then have "inv (s (\<lambda>k. 1 / m k)) = s m" "bij (s (\<lambda>k. 1 / m k))"
+    by (auto intro: inv_unique_comp o_bij)
+  then have eq: "s m ` cbox a b = s (\<lambda>k. 1 / m k) -` cbox a b"
+    using bij_vimage_eq_inv_image[OF \<open>bij (s (\<lambda>k. 1 / m k))\<close>, of "cbox a b"] by auto
+  show ?thesis
+    using m unfolding eq measure_def
+    by (subst lborel_affine_euclidean[where c=m and t=0])
+       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
+                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
+next
+  assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
+  then obtain k where k: "k \<in> Basis" "m k = 0" by auto
+  then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
+    by (intro setprod_zero) auto
+  have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
+  proof (rule emeasure_eq_0_AE)
+    show "AE x in lborel. x \<notin> s m ` cbox a b"
+      using AE_lborel_inner_neq[OF \<open>k\<in>Basis\<close>]
+    proof eventually_elim
+      show "x \<bullet> k \<noteq> 0 \<Longrightarrow> x \<notin> s m ` cbox a b " for x
+        using k by (auto simp: s_def[abs_def] cbox_def)
+    qed
+  qed
+  then show ?thesis
+    by (simp add: measure_def)
+qed
+
 lemma interval_image_affinity_interval:
   "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::euclidean_space) + c) ` cbox a b = cbox u v"
   unfolding image_affinity_cbox
@@ -6344,43 +6173,6 @@
 
 subsection \<open>Special case of stretching coordinate axes separately.\<close>
 
-lemma content_image_stretch_interval:
-  "content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
-    \<bar>setprod m Basis\<bar> * content (cbox a b)"
-proof (cases "cbox a b = {}")
-  case True
-  then show ?thesis
-    unfolding content_def image_is_empty image_stretch_interval if_P[OF True] by auto
-next
-  case False
-  then have "(\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b \<noteq> {}"
-    by auto
-  then show ?thesis
-    using False
-    unfolding content_def image_stretch_interval
-    apply -
-    unfolding interval_bounds' if_not_P
-    unfolding abs_setprod setprod.distrib[symmetric]
-    apply (rule setprod.cong)
-    apply (rule refl)
-    unfolding lessThan_iff
-    apply (simp only: inner_setsum_left_Basis)
-  proof -
-    fix i :: 'a
-    assume i: "i \<in> Basis"
-    have "(m i < 0 \<or> m i > 0) \<or> m i = 0"
-      by auto
-    then show "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) - min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) =
-      \<bar>m i\<bar> * (b \<bullet> i - a \<bullet> i)"
-      apply -
-      apply (erule disjE)+
-      unfolding min_def max_def
-      using False[unfolded box_ne_empty,rule_format,of i] i
-      apply (auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos)
-      done
-  qed
-qed
-
 lemma has_integral_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_integral i) (cbox a b)"
@@ -9324,7 +9116,7 @@
     proof (rule, goal_cases)
       case prems: (1 x)
       have "e / (4 * content (cbox a b)) > 0"
-        using \<open>e>0\<close> False content_pos_le[of a b] by auto
+        using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
       from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
       guess n .. note n=this
       then show ?case
@@ -10314,7 +10106,7 @@
             done
           also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
             apply (rule setsum.mono_neutral_left)
-            apply (subst simple_image)
+            apply (subst Setcompr_eq_image)
             apply (rule finite_imageI)+
             apply fact
             unfolding d'_def uv
@@ -10330,7 +10122,7 @@
               using l by auto
           qed
           also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
-            unfolding simple_image
+            unfolding Setcompr_eq_image
             apply (rule setsum.reindex_nontrivial [unfolded o_def])
             apply (rule finite_imageI)
             apply (rule p')
@@ -10518,7 +10310,7 @@
             apply auto
             done
           also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
-            unfolding simple_image
+            unfolding Setcompr_eq_image
             apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
             apply (rule d')
           proof goal_cases
@@ -10539,7 +10331,7 @@
           qed
           also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
             apply (rule setsum.mono_neutral_right)
-            unfolding simple_image
+            unfolding Setcompr_eq_image
             apply (rule finite_imageI)
             apply (rule d')
             apply blast
@@ -11394,7 +11186,7 @@
       also have "\<dots> < e' * norm (x - x0)"
         using \<open>e' > 0\<close> content_pos_le[of a b]
         by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
-          (auto simp: divide_simps e_def)
+           (auto simp: divide_simps e_def simp del: measure_nonneg)
       finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
       then show ?case
         by (auto simp: divide_simps)
@@ -11509,7 +11301,7 @@
       with \<open>e > 0\<close> have "e' > 0" by simp
       then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
         using u content_nonzero content_pos_le[of a b]
-        by (auto simp: uniform_limit_iff dist_norm)
+        by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
       then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
       proof eventually_elim
         case (elim n)
@@ -11568,7 +11360,7 @@
       fix k :: nat
       show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
         apply (rule integral_norm_bound_integral)
-        unfolding simple_image
+        unfolding Setcompr_eq_image
         apply (rule absolutely_integrable_onD)
         apply (rule absolutely_integrable_inf_real)
         prefer 5
@@ -11585,7 +11377,7 @@
     qed
     fix k :: nat
     show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding simple_image
+      unfolding Setcompr_eq_image
       apply (rule absolutely_integrable_onD)
       apply (rule absolutely_integrable_inf_real)
       prefer 3
@@ -11638,7 +11430,7 @@
     proof safe
       fix k :: nat
       show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
-        apply (rule integral_norm_bound_integral) unfolding simple_image
+        apply (rule integral_norm_bound_integral) unfolding Setcompr_eq_image
         apply (rule absolutely_integrable_onD)
         apply(rule absolutely_integrable_sup_real)
         prefer 5 unfolding real_norm_def
@@ -11656,7 +11448,7 @@
     qed
     fix k :: nat
     show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding simple_image
+      unfolding Setcompr_eq_image
       apply (rule absolutely_integrable_onD)
       apply (rule absolutely_integrable_sup_real)
       prefer 3
@@ -12541,11 +12333,11 @@
   define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
   define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
 
-  have has_integral_f: "(f n has_integral (F n - F a)) {a..}" 
+  have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
     if n: "n \<ge> a" for n :: nat
   proof -
     from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
-      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros 
+      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
             simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
     hence "(f n has_integral (F n - F a)) {a..n}"
       by (rule has_integral_eq [rotated]) (simp add: f_def)
@@ -12559,12 +12351,12 @@
   next
     case False
     have "(f n has_integral 0) {a}" by (rule has_integral_refl)
-    hence "(f n has_integral 0) {a..}" 
+    hence "(f n has_integral 0) {a..}"
       by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
     with False show ?thesis by (simp add: integral_unique)
   qed
-  
-  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and> 
+
+  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
            (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
   proof (intro monotone_convergence_increasing allI ballI)
     fix n :: nat
@@ -12582,7 +12374,7 @@
     from filterlim_real_sequentially
       have "eventually (\<lambda>n. real n \<ge> x) at_top"
       by (simp add: filterlim_at_top)
-    with x have "eventually (\<lambda>n. f n x = x powr e) at_top" 
+    with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
       by (auto elim!: eventually_mono simp: f_def)
     thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
   next
@@ -12603,11 +12395,11 @@
   hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
     by eventually_elim (simp add: integral_f)
   moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
-    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr] 
+    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
           filterlim_ident filterlim_real_sequentially | simp)+)
   hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
   ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
-  from conjunct2[OF *] and this 
+  from conjunct2[OF *] and this
     have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
   with conjunct1[OF *] show ?thesis
     by (simp add: has_integral_integral F_def)
@@ -12620,7 +12412,7 @@
 proof -
   from assms have "real_of_int (-int n) < -1" by simp
   note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
-  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) = 
+  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
                  1 / (real (n - 1) * a powr (real (n - 1)))" using assms
     by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
   also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
@@ -12630,4 +12422,33 @@
        (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
 qed
 
+subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
+
+lemma integral_component_eq_cart[simp]:
+  fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
+  assumes "f integrable_on s"
+  shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
+  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
+
+lemma content_closed_interval:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "a \<le> b"
+  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+  using content_cbox[of a b] assms
+  by (simp add: cbox_interval eucl_le[where 'a='a])
+
+lemma integrable_const_ivl[intro]:
+  fixes a::"'a::ordered_euclidean_space"
+  shows "(\<lambda>x. c) integrable_on {a .. b}"
+  unfolding cbox_interval[symmetric]
+  by (rule integrable_const)
+
+lemma integrable_on_subinterval:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s"
+    and "{a .. b} \<subseteq> s"
+  shows "f integrable_on {a .. b}"
+  using integrable_on_subcbox[of f s a b] assms
+  by (simp add: cbox_interval)
+
 end