Theory Henstock_Kurzweil_Integration

(*  Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
                Huge cleanup by LCP
*)

section Henstock-Kurzweil Gauge Integration in Many Dimensions

theory Henstock_Kurzweil_Integration
imports
  Lebesgue_Measure Tagged_Division
begin

lemma norm_diff2: "y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1)  e1; norm(y2 - x2)  e2
   norm(y-x)  e"
  using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
  by (simp add: add_diff_add)

lemma setcomp_dot1: "{z. P (z  (i,0))} = {(x,y). P(x  i)}"
  by auto

lemma setcomp_dot2: "{z. P (z  (0,i))} = {(x,y). P(y  i)}"
  by auto

lemma Sigma_Int_Paircomp1: "(Sigma A B)  {(x, y). P x} = Sigma (A  {x. P x}) B"
  by blast

lemma Sigma_Int_Paircomp2: "(Sigma A B)  {(x, y). P y} = Sigma A (λz. B z  {y. P y})"
  by blast
(* END MOVE *)

subsection Content (length, area, volume...) of an interval

abbreviation content :: "'a::euclidean_space set  real"
  where "content s  measure lborel s"

lemma content_cbox_cases:
  "content (cbox a b) = (if iBasis. ai  bi then prod (λi. bi - ai) Basis else 0)"
  by (simp add: measure_lborel_cbox_eq inner_diff)

lemma content_cbox: "iBasis. ai  bi  content (cbox a b) = (iBasis. bi - ai)"
  unfolding content_cbox_cases by simp

lemma content_cbox': "cbox a b  {}  content (cbox a b) = (iBasis. bi - ai)"
  by (simp add: box_ne_empty inner_diff)

lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else iBasis. bi - ai)"
  by (simp add: content_cbox')

lemma content_cbox_cart:
   "cbox a b  {}  content(cbox a b) = prod (λi. b$i - a$i) UNIV"
  by (simp add: content_cbox_if Basis_vec_def cart_eq_inner_axis axis_eq_axis prod.UNION_disjoint)

lemma content_cbox_if_cart:
   "content(cbox a b) = (if cbox a b = {} then 0 else prod (λi. b$i - a$i) UNIV)"
  by (simp add: content_cbox_cart)

lemma content_division_of:
  assumes "K  𝒟" "𝒟 division_of S"
  shows "content K = (i  Basis. interval_upperbound K  i - interval_lowerbound K  i)"
proof -
  obtain a b where "K = cbox a b"
    using cbox_division_memE assms by metis
  then show ?thesis
    using assms by (force simp: division_of_def content_cbox')
qed

lemma content_real: "a  b  content {a..b} = b - a"
  by simp

lemma abs_eq_content: "¦y - x¦ = (if xy then content {x..y} else content {y..x})"
  by (auto simp: content_real)

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 [iff]: "0  content X"
  by simp

corollarytag unimportant content_nonneg [simp]: "¬ content (cbox a b) < 0"
  using not_le by blast

lemma content_pos_lt: "iBasis. ai < bi  0 < content (cbox a b)"
  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)

lemma content_eq_0: "content (cbox a b) = 0  (iBasis. bi  ai)"
  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  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))  (iBasis. ai < bi)"
  by (auto simp add: content_cbox_cases less_le prod_nonneg)

lemma content_empty [simp]: "content {} = 0"
  by simp

lemma content_real_if [simp]: "content {a..b} = (if a  b then b - a else 0)"
  by (simp add: content_real)

lemma content_subset: "cbox a b  cbox c d  content (cbox a b)  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)  content (cbox a b)  0"
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce

lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
  unfolding measure_lborel_cbox_eq Basis_prod_def
  apply (subst prod.union_disjoint)
  apply (auto simp: bex_Un ball_Un)
  apply (subst (1 2) prod.reindex_nontrivial)
  apply auto
  done

lemma content_cbox_pair_eq0_D:
   "content (cbox (a,c) (b,d)) = 0  content (cbox a b) = 0  content (cbox c d) = 0"
  by (simp add: content_Pair)

lemma content_cbox_plus:
  fixes x :: "'a::euclidean_space"
  shows "content(cbox x (x + h *R One)) = (if h  0 then h ^ DIM('a) else 0)"
  by (simp add: algebra_simps content_cbox_if box_eq_empty)

lemma content_0_subset: "content(cbox a b) = 0  s  cbox a b  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_ball_pos:
  assumes "r > 0"
  shows   "content (ball c r) > 0"
proof -
  from rational_boxes[OF assms, of c] obtain a b where ab: "c  box a b" "box a b  ball c r"
    by auto
  from ab have "0 < content (box a b)"
    by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def)
  have "emeasure lborel (box a b)  emeasure lborel (ball c r)"
    using ab by (intro emeasure_mono) auto
  also have "emeasure lborel (box a b) = ennreal (content (box a b))"
    using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto
  also have "emeasure lborel (ball c r) = ennreal (content (ball c r))"
    using emeasure_lborel_ball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto
  finally show ?thesis
    using content (box a b) > 0 by simp
qed

lemma content_cball_pos:
  assumes "r > 0"
  shows   "content (cball c r) > 0"
proof -
  from rational_boxes[OF assms, of c] obtain a b where ab: "c  box a b" "box a b  ball c r"
    by auto
  from ab have "0 < content (box a b)"
    by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def)
  have "emeasure lborel (box a b)  emeasure lborel (ball c r)"
    using ab by (intro emeasure_mono) auto
  also have "  emeasure lborel (cball c r)"
    by (intro emeasure_mono) auto
  also have "emeasure lborel (box a b) = ennreal (content (box a b))"
    using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto
  also have "emeasure lborel (cball c r) = ennreal (content (cball c r))"
    using emeasure_lborel_cball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto
  finally show ?thesis
    using content (box a b) > 0 by simp
qed

lemma content_split:
  fixes a :: "'a::euclidean_space"
  assumes "k  Basis"
  shows "content (cbox a b) = content(cbox a b  {x. xk  c}) + content(cbox a b  {x. xk  c})"
  ― ‹Prove using measure theory
proof (cases "iBasis. a  i  b  i")
  case True
  have 1: "X Y Z. (iBasis. Z i (if i = k then X else Y i)) = Z k X * (iBasis-{k}. Z i (Y i))"
    by (simp add: if_distrib prod.delta_remove assms)
  note simps = interval_split[OF assms] content_cbox_cases
  have 2: "(iBasis. bi - ai) = (iBasis-{k}. bi - ai) * (bk - ak)"
    by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove)
  have "x. min (b  k) c = max (a  k) c 
    x * (bk - ak) = x * (max (a  k) c - a  k) + x * (b  k - max (a  k) c)"
    by  (auto simp add: field_simps)
  moreover
  have **: "(iBasis. ((iBasis. (if i = k then min (b  k) c else b  i) *R i)  i - a  i)) =
      (iBasis. (if i = k then min (b  k) c else b  i) - a  i)"
    "(iBasis. b  i - ((iBasis. (if i = k then max (a  k) c else a  i) *R i)  i)) =
      (iBasis. b  i - (if i = k then max (a  k) c else a  i))"
    by (auto intro!: prod.cong)
  have "¬ a  k  c  ¬ c  b  k  False"
    unfolding not_le using True assms by auto
  ultimately show ?thesis
    using assms unfolding simps ** 1[of "λi x. bi - x"] 1[of "λi x. x - ai"] 2
    by auto
next
  case False
  then have "cbox a b = {}"
    unfolding box_eq_empty by (auto simp: not_le)
  then show ?thesis
    by (auto simp: not_le)
qed

lemma division_of_content_0:
  assumes "content (cbox a b) = 0" "d division_of (cbox a b)" "K  d"
  shows "content K = 0"
  unfolding forall_in_division[OF assms(2)]
  by (meson assms content_0_subset division_of_def)

lemma sum_content_null:
  assumes "content (cbox a b) = 0"
    and "p tagged_division_of (cbox a b)"
  shows "((x,K)p. content K *R f x) = (0::'a::real_normed_vector)"
proof (rule sum.neutral, rule)
  fix y
  assume y: "y  p"
  obtain x K where xk: "y = (x, K)"
    using surj_pair[of y] by blast
  then obtain c d where k: "K = cbox c d" "K  cbox a b"
    by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
  have "(λ(x',K'). content K' *R f x') y = content K *R f x"
    unfolding xk by auto
  also have " = 0"
    using assms(1) content_0_subset k(2) by auto
  finally show "(λ(x, k). content k *R f x) y = 0" .
qed

global_interpretation sum_content: operative plus 0 content
  rewrites "comm_monoid_set.F plus 0 = sum"
proof -
  interpret operative plus 0 content
    by standard (auto simp add: content_split [symmetric] content_eq_0_interior)
  show "operative plus 0 content"
    by standard
  show "comm_monoid_set.F plus 0 = sum"
    by (simp add: sum_def)
qed

lemma additive_content_division: "d division_of (cbox a b)  sum content d = content (cbox a b)"
  by (fact sum_content.division)

lemma additive_content_tagged_division:
  "d tagged_division_of (cbox a b)  sum (λ(x,l). content l) d = content (cbox a b)"
  by (fact sum_content.tagged_division)

lemma subadditive_content_division:
  assumes "𝒟 division_of S" "S  cbox a b"
  shows "sum content 𝒟  content(cbox a b)"
proof -
  have "𝒟 division_of 𝒟" "𝒟  cbox a b"
    using assms by auto
  then obtain 𝒟' where "𝒟  𝒟'" "𝒟' division_of cbox a b"
    using partial_division_extend_interval by metis
  then have "sum content 𝒟  sum content 𝒟'"
    using sum_mono2 by blast
  also have "...  content(cbox a b)"
    by (simp add: 𝒟' division_of cbox a b additive_content_division less_eq_real_def)
  finally show ?thesis .
qed

lemma content_real_eq_0: "content {a..b::real} = 0  a  b"
  by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)

lemma property_empty_interval: "a b. content (cbox a b) = 0  P (cbox a b)  P {}"
  using content_empty unfolding empty_as_interval by auto

lemma interval_bounds_nz_content [simp]:
  assumes "content (cbox a b)  0"
  shows "interval_upperbound (cbox a b) = b"
    and "interval_lowerbound (cbox a b) = a"
  by (metis assms content_empty interval_bounds')+

subsection Gauge integral

text Case distinction to define it first on compact intervals first, then use a limit. This is only
much later unified. In Fremlin: Measure Theory, Volume 4I this is generalized using residual sets.

definition has_integral :: "('n::euclidean_space  'b::real_normed_vector)  'b  'n set  bool"
  (infixr "has'_integral" 46)
  where "(f has_integral I) s 
    (if a b. s = cbox a b
      then ((λp. (x,k)p. content k *R f x)  I) (division_filter s)
      else (e>0. B>0. a b. ball 0 B  cbox a b 
        (z. ((λp. (x,k)p. content k *R (if x  s then f x else 0))  z) (division_filter (cbox a b)) 
          norm (z - I) < e)))"

lemma has_integral_cbox:
  "(f has_integral I) (cbox a b)  ((λp. (x,k)p. content k *R f x)  I) (division_filter (cbox a b))"
  by (auto simp add: has_integral_def)

lemma has_integral:
  "(f has_integral y) (cbox a b) 
    (e>0. γ. gauge γ 
      (𝒟. 𝒟 tagged_division_of (cbox a b)  γ fine 𝒟 
        norm (sum (λ(x,k). content(k) *R f x) 𝒟 - y) < e))"
  by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)

lemma has_integral_real:
  "(f has_integral y) {a..b::real} 
    (e>0. γ. gauge γ 
      (𝒟. 𝒟 tagged_division_of {a..b}  γ fine 𝒟 
        norm (sum (λ(x,k). content(k) *R f x) 𝒟 - y) < e))"
  unfolding box_real[symmetric] by (rule has_integral)

lemma has_integralD[dest]:
  assumes "(f has_integral y) (cbox a b)"
    and "e > 0"
  obtains γ
    where "gauge γ"
      and "𝒟. 𝒟 tagged_division_of (cbox a b)  γ fine 𝒟 
        norm (((x,k)𝒟. content k *R f x) - y) < e"
  using assms unfolding has_integral by auto

lemma has_integral_alt:
  "(f has_integral y) i 
    (if a b. i = cbox a b
     then (f has_integral y) i
     else (e>0. B>0. a b. ball 0 B  cbox a b 
      (z. ((λx. if x  i then f x else 0) has_integral z) (cbox a b)  norm (z - y) < e)))"
  by (subst has_integral_def) (auto simp add: has_integral_cbox)

lemma has_integral_altD:
  assumes "(f has_integral y) i"
    and "¬ (a b. i = cbox a b)"
    and "e>0"
  obtains B where "B > 0"
    and "a b. ball 0 B  cbox a b 
      (z. ((λx. if x  i then f(x) else 0) has_integral z) (cbox a b)  norm(z - y) < e)"
  using assms has_integral_alt[of f y i] by auto

definition integrable_on (infixr "integrable'_on" 46)
  where "f integrable_on i  (y. (f has_integral y) i)"

definition "integral i f = (SOME y. (f has_integral y) i  ¬ f integrable_on i  y=0)"

lemma integrable_integral[intro]: "f integrable_on i  (f has_integral (integral i f)) i"
  unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)

lemma not_integrable_integral: "¬ f integrable_on i  integral i f = 0"
  unfolding integrable_on_def integral_def by blast

lemma has_integral_integrable[dest]: "(f has_integral i) s  f integrable_on s"
  unfolding integrable_on_def by auto

lemma has_integral_integral: "f integrable_on s  (f has_integral (integral s f)) s"
  by auto

subsection Basic theorems about integrals

lemma has_integral_eq_rhs: "(f has_integral j) S  i = j  (f has_integral i) S"
  by (rule forw_subst)

lemma has_integral_unique_cbox:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  shows "(f has_integral k1) (cbox a b)  (f has_integral k2) (cbox a b)  k1 = k2"
    by (auto simp: has_integral_cbox intro: tendsto_unique[OF division_filter_not_empty])    

lemma has_integral_unique:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes "(f has_integral k1) i" "(f has_integral k2) i"
  shows "k1 = k2"
proof (rule ccontr)
  let ?e = "norm (k1 - k2)/2"
  let ?F = "(λx. if x  i then f x else 0)"
  assume "k1  k2"
  then have e: "?e > 0"
    by auto
  have nonbox: "¬ (a b. i = cbox a b)"
    using k1  k2 assms has_integral_unique_cbox by blast
  obtain B1 where B1:
      "0 < B1"
      "a b. ball 0 B1  cbox a b 
        z. (?F has_integral z) (cbox a b)  norm (z - k1) < norm (k1 - k2)/2"
    by (rule has_integral_altD[OF assms(1) nonbox,OF e]) blast
  obtain B2 where B2:
      "0 < B2"
      "a b. ball 0 B2  cbox a b 
        z. (?F has_integral z) (cbox a b)  norm (z - k2) < norm (k1 - k2)/2"
    by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
  obtain a b :: 'n where ab: "ball 0 B1  cbox a b" "ball 0 B2  cbox a b"
    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox_symmetric)
  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
    using B1(2)[OF ab(1)] by blast
  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
    using B2(2)[OF ab(2)] by blast
  have "z = w"
    using has_integral_unique_cbox[OF w(1) z(1)] by auto
  then have "norm (k1 - k2)  norm (z - k2) + norm (w - k1)"
    using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
    by (auto simp add: norm_minus_commute)
  also have " < norm (k1 - k2)/2 + norm (k1 - k2)/2"
    by (metis add_strict_mono z(2) w(2))
  finally show False by auto
qed

lemma integral_unique [intro]: "(f has_integral y) k  integral k f = y"
  unfolding integral_def
  by (rule some_equality) (auto intro: has_integral_unique)

lemma has_integral_iff: "(f has_integral i) S  (f integrable_on S  integral S f = i)"
  by blast

lemma eq_integralD: "integral k f = y  (f has_integral y) k  ¬ f integrable_on k  y=0"
  unfolding integral_def integrable_on_def
  apply (erule subst)
  apply (rule someI_ex)
  by blast

lemma has_integral_const [intro]:
  fixes a b :: "'a::euclidean_space"
  shows "((λx. c) has_integral (content (cbox a b) *R c)) (cbox a b)"
  using eventually_division_filter_tagged_division[of "cbox a b"]
     additive_content_tagged_division[of _ a b]
  by (auto simp: has_integral_cbox split_beta' scaleR_sum_left[symmetric]
           elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const])

lemma has_integral_const_real [intro]:
  fixes a b :: real
  shows "((λx. c) has_integral (content {a..b} *R c)) {a..b}"
  by (metis box_real(2) has_integral_const)

lemma has_integral_integrable_integral: "(f has_integral i) s  f integrable_on s  integral s f = i"
  by blast

lemma integral_const [simp]:
  fixes a b :: "'a::euclidean_space"
  shows "integral (cbox a b) (λx. c) = content (cbox a b) *R c"
  by (rule integral_unique) (rule has_integral_const)

lemma integral_const_real [simp]:
  fixes a b :: real
  shows "integral {a..b} (λx. c) = content {a..b} *R c"
  by (metis box_real(2) integral_const)

lemma has_integral_is_0_cbox:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes "x. x  cbox a b  f x = 0"
  shows "(f has_integral 0) (cbox a b)"
    unfolding has_integral_cbox
    using eventually_division_filter_tagged_division[of "cbox a b"] assms
    by (subst tendsto_cong[where g="λ_. 0"])
       (auto elim!: eventually_mono intro!: sum.neutral simp: tag_in_interval)

lemma has_integral_is_0:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes "x. x  S  f x = 0"
  shows "(f has_integral 0) S"
proof (cases "(a b. S = cbox a b)")
  case True with assms has_integral_is_0_cbox show ?thesis
    by blast
next
  case False
  have *: "(λx. if x  S then f x else 0) = (λx. 0)"
    by (auto simp add: assms)
  show ?thesis
    using has_integral_is_0_cbox False
    by (subst has_integral_alt) (force simp add: *)
qed

lemma has_integral_0[simp]: "((λx::'n::euclidean_space. 0) has_integral 0) S"
  by (rule has_integral_is_0) auto

lemma has_integral_0_eq[simp]: "((λx. 0) has_integral i) S  i = 0"
  using has_integral_unique[OF has_integral_0] by auto

lemma has_integral_linear_cbox:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes f: "(f has_integral y) (cbox a b)"
    and h: "bounded_linear h"
  shows "((h  f) has_integral (h y)) (cbox a b)"
proof -
  interpret bounded_linear h using h .
  show ?thesis
    unfolding has_integral_cbox using tendsto [OF f [unfolded has_integral_cbox]]
    by (simp add: sum scaleR split_beta')
qed

lemma has_integral_linear:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes f: "(f has_integral y) S"
    and h: "bounded_linear h"
  shows "((h  f) has_integral (h y)) S"
proof (cases "(a b. S = cbox a b)")
  case True with f h has_integral_linear_cbox show ?thesis 
    by blast
next
  case False
  interpret bounded_linear h using h .
  from pos_bounded obtain B where B: "0 < B" "x. norm (h x)  norm x * B"
    by blast
  let ?S = "λf x. if x  S then f x else 0"
  show ?thesis
  proof (subst has_integral_alt, clarsimp simp: False)
    fix e :: real
    assume e: "e > 0"
    have *: "0 < e/B" using e B(1) by simp
    obtain M where M:
      "M > 0"
      "a b. ball 0 M  cbox a b 
        z. (?S f has_integral z) (cbox a b)  norm (z - y) < e/B"
      using has_integral_altD[OF f False *] by blast
    show "B>0. a b. ball 0 B  cbox a b 
      (z. (?S(h  f) has_integral z) (cbox a b)  norm (z - h y) < e)"
    proof (rule exI, intro allI conjI impI)
      show "M > 0" using M by metis
    next
      fix a b::'n
      assume sb: "ball 0 M  cbox a b"
      obtain z where z: "(?S f has_integral z) (cbox a b)" "norm (z - y) < e/B"
        using M(2)[OF sb] by blast
      have *: "?S(h  f) = h  ?S f"
        using zero by auto
      show "z. (?S(h  f) has_integral z) (cbox a b)  norm (z - h y) < e"
      proof (intro exI conjI)
        show "(?S(h  f) has_integral h z) (cbox a b)"
          by (simp add: * has_integral_linear_cbox[OF z(1) h])
        show "norm (h z - h y) < e"
          by (metis B diff le_less_trans pos_less_divide_eq z(2))
      qed
    qed
  qed
qed

lemma has_integral_scaleR_left:
  "(f has_integral y) S  ((λx. f x *R c) has_integral (y *R c)) S"
  using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)

lemma integrable_on_scaleR_left:
  assumes "f integrable_on A"
  shows "(λx. f x *R y) integrable_on A"
  using assms has_integral_scaleR_left unfolding integrable_on_def by blast

lemma has_integral_mult_left:
  fixes c :: "_ :: real_normed_algebra"
  shows "(f has_integral y) S  ((λx. f x * c) has_integral (y * c)) S"
  using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)

lemma has_integral_divide:
  fixes c :: "_ :: real_normed_div_algebra"
  shows "(f has_integral y) S  ((λx. f x / c) has_integral (y / c)) S"
  unfolding divide_inverse by (simp add: has_integral_mult_left)

textThe case analysis eliminates the condition termf integrable_on S at the cost
     of the type class constraint division_ring›
corollary integral_mult_left [simp]:
  fixes c:: "'a::{real_normed_algebra,division_ring}"
  shows "integral S (λx. f x * c) = integral S f * c"
proof (cases "f integrable_on S  c = 0")
  case True then show ?thesis
    by (force intro: has_integral_mult_left)
next
  case False then have "¬ (λx. f x * c) integrable_on S"
    using has_integral_mult_left [of "(λx. f x * c)" _ S "inverse c"]
    by (auto simp add: mult.assoc)
  with False show ?thesis by (simp add: not_integrable_integral)
qed

corollary integral_mult_right [simp]:
  fixes c:: "'a::{real_normed_field}"
  shows "integral S (λx. c * f x) = c * integral S f"
by (simp add: mult.commute [of c])

corollary integral_divide [simp]:
  fixes z :: "'a::real_normed_field"
  shows "integral S (λx. f x / z) = integral S (λx. f x) / z"
using integral_mult_left [of S f "inverse z"]
  by (simp add: divide_inverse_commute)

lemma has_integral_mult_right:
  fixes c :: "'a :: real_normed_algebra"
  shows "(f has_integral y) i  ((λx. c * f x) has_integral (c * y)) i"
  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)

lemma has_integral_cmul: "(f has_integral k) S  ((λx. c *R f x) has_integral (c *R k)) S"
  unfolding o_def[symmetric]
  by (metis has_integral_linear bounded_linear_scaleR_right)

lemma has_integral_cmult_real:
  fixes c :: real
  assumes "c  0  (f has_integral x) A"
  shows "((λx. c * f x) has_integral c * x) A"
proof (cases "c = 0")
  case True
  then show ?thesis by simp
next
  case False
  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
    unfolding real_scaleR_def .
qed

lemma has_integral_neg: "(f has_integral k) S  ((λx. -(f x)) has_integral -k) S"
  by (drule_tac c="-1" in has_integral_cmul) auto

lemma has_integral_neg_iff: "((λx. - f x) has_integral k) S  (f has_integral - k) S"
  using has_integral_neg[of f "- k"] has_integral_neg[of "λx. - f x" k] by auto

lemma has_integral_add_cbox:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes "(f has_integral k) (cbox a b)" "(g has_integral l) (cbox a b)"
  shows "((λx. f x + g x) has_integral (k + l)) (cbox a b)"
  using assms
    unfolding has_integral_cbox
    by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add)

lemma has_integral_add:
  fixes f :: "'n::euclidean_space  'a::real_normed_vector"
  assumes f: "(f has_integral k) S" and g: "(g has_integral l) S"
  shows "((λx. f x + g x) has_integral (k + l)) S"
proof (cases "a b. S = cbox a b")
  case True with has_integral_add_cbox assms show ?thesis
    by blast 
next
  let ?S = "λf x. if x  S then f x else 0"
  case False
  then show ?thesis
  proof (subst has_integral_alt, clarsimp, goal_cases)
    case (1 e)
    then have e2: "e/2 > 0"
      by auto
    obtain Bf where "0 < Bf"
      and Bf: "a b. ball 0 Bf  cbox a b 
                     z. (?S f has_integral z) (cbox a b)  norm (z - k) < e/2"
      using has_integral_altD[OF f False e2] by blast
    obtain Bg where "0 < Bg"
      and Bg: "a b. ball 0 Bg  (cbox a b) 
                     z. (?S g has_integral z) (cbox a b)  norm (z - l) < e/2"
      using has_integral_altD[OF g False e2] by blast
    show ?case
    proof (rule_tac x="max Bf Bg" in exI, clarsimp simp add: max.strict_coboundedI1 0 < Bf)
      fix a b
      assume "ball 0 (max Bf Bg)  cbox a (b::'n)"
      then have fs: "ball 0 Bf  cbox a (b::'n)" and gs: "ball 0 Bg  cbox a (b::'n)"
        by auto
      obtain w where w: "(?S f has_integral w) (cbox a b)" "norm (w - k) < e/2"
        using Bf[OF fs] by blast
      obtain z where z: "(?S g has_integral z) (cbox a b)" "norm (z - l) < e/2"
        using Bg[OF gs] by blast
      have *: "x. (if x  S then f x + g x else 0) = (?S f x) + (?S g x)"
        by auto
      show "z. (?S(λx. f x + g x) has_integral z) (cbox a b)  norm (z - (k + l)) < e"
      proof (intro exI conjI)
        show "(?S(λx. f x + g x) has_integral (w + z)) (cbox a b)"
          by (simp add: has_integral_add_cbox[OF w(1) z(1), unfolded *[symmetric]])
        show "norm (w + z - (k + l)) < e"
          by (metis dist_norm dist_triangle_add_half w(2) z(2))
      qed
    qed
  qed
qed

lemma has_integral_diff:
  "(f has_integral k) S  (g has_integral l) S 
    ((λx. f x - g x) has_integral (k - l)) S"
  using has_integral_add[OF _ has_integral_neg, of f k S g l]
  by (auto simp: algebra_simps)

lemma integral_0 [simp]:
  "integral S (λx::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
  by (rule integral_unique has_integral_0)+

lemma integral_add: "f integrable_on S  g integrable_on S 
    integral S (λx. f x + g x) = integral S f + integral S g"
  by (rule integral_unique) (metis integrable_integral has_integral_add)

lemma integral_cmul [simp]: "integral S (λx. c *R f x) = c *R integral S f"
proof (cases "f integrable_on S  c = 0")
  case True with has_integral_cmul integrable_integral show ?thesis
    by fastforce
next
  case False then have "¬ (λx. c *R f x) integrable_on S"
    using has_integral_cmul [of "(λx. c *R f x)" _ S "inverse c"] by auto
  with False show ?thesis by (simp add: not_integrable_integral)
qed

lemma integral_mult:
  fixes K::real
  shows "f integrable_on X  K * integral X f = integral X (λx. K * f x)"
  unfolding real_scaleR_def[symmetric] integral_cmul ..

lemma integral_neg [simp]: "integral S (λx. - f x) = - integral S f"
proof (cases "f integrable_on S")
  case True then show ?thesis
    by (simp add: has_integral_neg integrable_integral integral_unique)
next
  case False then have "¬ (λx. - f x) integrable_on S"
    using has_integral_neg [of "(λx. - f x)" _ S ] by auto
  with False show ?thesis by (simp add: not_integrable_integral)
qed

lemma integral_diff: "f integrable_on S  g integrable_on S 
    integral S (λx. f x - g x) = integral S f - integral S g"
  by (rule integral_unique) (metis integrable_integral has_integral_diff)

lemma integrable_0: "(λx. 0) integrable_on S"
  unfolding integrable_on_def using has_integral_0 by auto

lemma integrable_add: "f integrable_on S  g integrable_on S  (λx. f x + g x) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_add)

lemma integrable_cmul: "f integrable_on S  (λx. c *R f(x)) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_cmul)

lemma integrable_on_scaleR_iff [simp]:
  fixes c :: real
  assumes "c  0"
  shows "(λx. c *R f x) integrable_on S  f integrable_on S"
  using integrable_cmul[of "λx. c *R f x" S "1 / c"] integrable_cmul[of f S c] c  0
  by auto

lemma integrable_on_cmult_iff [simp]:
  fixes c :: real
  assumes "c  0"
  shows "(λx. c * f x) integrable_on S  f integrable_on S"
  using integrable_on_scaleR_iff [of c f] assms by simp

lemma integrable_on_cmult_left:
  assumes "f integrable_on S"
  shows "(λx. of_real c * f x) integrable_on S"
    using integrable_cmul[of f S "of_real c"] assms
    by (simp add: scaleR_conv_of_real)

lemma integrable_neg: "f integrable_on S  (λx. -f(x)) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_neg)

lemma integrable_neg_iff: "(λx. -f(x)) integrable_on S  f integrable_on S"
  using integrable_neg by fastforce

lemma integrable_diff:
  "f integrable_on S  g integrable_on S  (λx. f x - g x) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_diff)

lemma integrable_linear:
  "f integrable_on S  bounded_linear h  (h  f) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_linear)

lemma integral_linear:
  "f integrable_on S  bounded_linear h  integral S (h  f) = h (integral S f)"
  by (meson has_integral_iff has_integral_linear)

lemma integrable_on_cnj_iff:
  "(λx. cnj (f x)) integrable_on A  f integrable_on A"
  using integrable_linear[OF _ bounded_linear_cnj, of f A]
        integrable_linear[OF _ bounded_linear_cnj, of "cnj  f" A]
  by (auto simp: o_def)

lemma integral_cnj: "cnj (integral A f) = integral A (λx. cnj (f x))"
  by (cases "f integrable_on A")
     (simp_all add: integral_linear[OF _ bounded_linear_cnj, symmetric]
                    o_def integrable_on_cnj_iff not_integrable_integral)

lemma integral_component_eq[simp]:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
  assumes "f integrable_on S"
  shows "integral S (λx. f x  k) = integral S f  k"
  unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..

lemma has_integral_sum:
  assumes "finite T"
    and "a. a  T  ((f a) has_integral (i a)) S"
  shows "((λx. sum (λa. f a x) T) has_integral (sum i T)) S"
  using assms(1) subset_refl[of T]
proof (induct rule: finite_subset_induct)
  case empty
  then show ?case by auto
next
  case (insert x F)
  with assms show ?case
    by (simp add: has_integral_add)
qed

lemma integral_sum:
  "finite I;  a. a  I  f a integrable_on S 
   integral S (λx. aI. f a x) = (aI. integral S (f a))"
  by (simp add: has_integral_sum integrable_integral integral_unique)

lemma integrable_sum:
  "finite I;  a. a  I  f a integrable_on S  (λx. aI. f a x) integrable_on S"
  unfolding integrable_on_def using has_integral_sum[of I] by metis

lemma has_integral_eq:
  assumes "x. x  s  f x = g x"
    and "(f has_integral k) s"
  shows "(g has_integral k) s"
  using has_integral_diff[OF assms(2), of "λx. f x - g x" 0]
  using has_integral_is_0[of s "λx. f x - g x"]
  using assms(1)
  by auto

lemma integrable_eq: "f integrable_on s; x. x  s  f x = g x  g integrable_on s"
  unfolding integrable_on_def
  using has_integral_eq[of s f g] has_integral_eq by blast

lemma has_integral_cong:
  assumes "x. x  s  f x = g x"
  shows "(f has_integral i) s = (g has_integral i) s"
  using has_integral_eq[of s f g] has_integral_eq[of s g f] assms
  by auto

lemma integral_cong:
  assumes "x. x  s  f x = g x"
  shows "integral s f = integral s g"
  unfolding integral_def
by (metis (full_types, opaque_lifting) assms has_integral_cong integrable_eq)

lemma integrable_on_cmult_left_iff [simp]:
  assumes "c  0"
  shows "(λx. of_real c * f x) integrable_on s  f integrable_on s"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "(λx. of_real (1 / c) * (of_real c * f x)) integrable_on s"
    using integrable_cmul[of "λx. of_real c * f x" s "1 / of_real c"]
    by (simp add: scaleR_conv_of_real)
  then have "(λx. (of_real (1 / c) * of_real c * f x)) integrable_on s"
    by (simp add: algebra_simps)
  with c  0 show ?rhs
    by (metis (no_types, lifting) integrable_eq mult.left_neutral nonzero_divide_eq_eq of_real_1 of_real_mult)
qed (blast intro: integrable_on_cmult_left)

lemma integrable_on_cmult_right:
  fixes f :: "_  'b :: {comm_ring,real_algebra_1,real_normed_vector}"
  assumes "f integrable_on s"
  shows "(λx. f x * of_real c) integrable_on s"
using integrable_on_cmult_left [OF assms] by (simp add: mult.commute)

lemma integrable_on_cmult_right_iff [simp]:
  fixes f :: "_  'b :: {comm_ring,real_algebra_1,real_normed_vector}"
  assumes "c  0"
  shows "(λx. f x * of_real c) integrable_on s  f integrable_on s"
using integrable_on_cmult_left_iff [OF assms] by (simp add: mult.commute)

lemma integrable_on_cdivide:
  fixes f :: "_  'b :: real_normed_field"
  assumes "f integrable_on s"
  shows "(λx. f x / of_real c) integrable_on s"
by (simp add: integrable_on_cmult_right divide_inverse assms flip: of_real_inverse)

lemma integrable_on_cdivide_iff [simp]:
  fixes f :: "_  'b :: real_normed_field"
  assumes "c  0"
  shows "(λx. f x / of_real c) integrable_on s  f integrable_on s"
by (simp add: divide_inverse assms flip: of_real_inverse)

lemma has_integral_null [intro]: "content(cbox a b) = 0  (f has_integral 0) (cbox a b)"
  unfolding has_integral_cbox
  using eventually_division_filter_tagged_division[of "cbox a b"]
  by (subst tendsto_cong[where g="λ_. 0"]) (auto elim: eventually_mono intro: sum_content_null)

lemma has_integral_null_real [intro]: "content {a..b::real} = 0  (f has_integral 0) {a..b}"
  by (metis box_real(2) has_integral_null)

lemma has_integral_null_eq[simp]: "content (cbox a b) = 0  (f has_integral i) (cbox a b)  i = 0"
  by (auto simp add: has_integral_null dest!: integral_unique)

lemma integral_null [simp]: "content (cbox a b) = 0  integral (cbox a b) f = 0"
  by (metis has_integral_null integral_unique)

lemma integrable_on_null [intro]: "content (cbox a b) = 0  f integrable_on (cbox a b)"
  by (simp add: has_integral_integrable)

lemma has_integral_empty[intro]: "(f has_integral 0) {}"
  by (meson ex_in_conv has_integral_is_0)

lemma has_integral_empty_eq[simp]: "(f has_integral i) {}  i = 0"
  by (auto simp add: has_integral_empty has_integral_unique)

lemma integrable_on_empty[intro]: "f integrable_on {}"
  unfolding integrable_on_def by auto

lemma integral_empty[simp]: "integral {} f = 0"
  by (rule integral_unique) (rule has_integral_empty)

lemma has_integral_refl[intro]:
  fixes a :: "'a::euclidean_space"
  shows "(f has_integral 0) (cbox a a)"
    and "(f has_integral 0) {a}"
proof -
  show "(f has_integral 0) (cbox a a)"
     by (rule has_integral_null) simp
  then show "(f has_integral 0) {a}"
    by simp
qed

lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
  unfolding integrable_on_def by auto

lemma integral_refl [simp]: "integral (cbox a a) f = 0"
  by (rule integral_unique) auto

lemma integral_singleton [simp]: "integral {a} f = 0"
  by auto

lemma integral_blinfun_apply:
  assumes "f integrable_on s"
  shows "integral s (λx. blinfun_apply h (f x)) = blinfun_apply h (integral s f)"
  by (subst integral_linear[symmetric, OF assms blinfun.bounded_linear_right]) (simp add: o_def)

lemma blinfun_apply_integral:
  assumes "f integrable_on s"
  shows "blinfun_apply (integral s f) x = integral s (λy. blinfun_apply (f y) x)"
  by (metis (no_types, lifting) assms blinfun.prod_left.rep_eq integral_blinfun_apply integral_cong)

lemma has_integral_componentwise_iff:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  shows "(f has_integral y) A  (bBasis. ((λx. f x  b) has_integral (y  b)) A)"
proof safe
  fix b :: 'b assume "(f has_integral y) A"
  from has_integral_linear[OF this(1) bounded_linear_inner_left, of b]
    show "((λx. f x  b) has_integral (y  b)) A" by (simp add: o_def)
next
  assume "(bBasis. ((λx. f x  b) has_integral (y  b)) A)"
  hence "bBasis. (((λx. x *R b)  (λx. f x  b)) has_integral ((y  b) *R b)) A"
    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
  hence "((λx. bBasis. (f x  b) *R b) has_integral (bBasis. (y  b) *R b)) A"
    by (intro has_integral_sum) (simp_all add: o_def)
  thus "(f has_integral y) A" by (simp add: euclidean_representation)
qed

lemma has_integral_componentwise:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  shows "(b. b  Basis  ((λx. f x  b) has_integral (y  b)) A)  (f has_integral y) A"
  by (subst has_integral_componentwise_iff) blast

lemma integrable_componentwise_iff:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  shows "f integrable_on A  (bBasis. (λx. f x  b) integrable_on A)"
proof
  assume "f integrable_on A"
  then obtain y where "(f has_integral y) A" by (auto simp: integrable_on_def)
  hence "(bBasis. ((λx. f x  b) has_integral (y  b)) A)"
    by (subst (asm) has_integral_componentwise_iff)
  thus "(bBasis. (λx. f x  b) integrable_on A)" by (auto simp: integrable_on_def)
next
  assume "(bBasis. (λx. f x  b) integrable_on A)"
  then obtain y where "bBasis. ((λx. f x  b) has_integral y b) A"
    unfolding integrable_on_def by (subst (asm) bchoice_iff) blast
  hence "bBasis. (((λx. x *R b)  (λx. f x  b)) has_integral (y b *R b)) A"
    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
  hence "((λx. bBasis. (f x  b) *R b) has_integral (bBasis. y b *R b)) A"
    by (intro has_integral_sum) (simp_all add: o_def)
  thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation)
qed

lemma integrable_componentwise:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  shows "(b. b  Basis  (λx. f x  b) integrable_on A)  f integrable_on A"
  by (subst integrable_componentwise_iff) blast

lemma integral_componentwise:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes "f integrable_on A"
  shows "integral A f = (bBasis. integral A (λx. (f x  b) *R b))"
proof -
  from assms have integrable: "bBasis. (λx. x *R b)  (λx. (f x  b)) integrable_on A"
    by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI)
       (simp_all add: bounded_linear_scaleR_left)
  have "integral A f = integral A (λx. bBasis. (f x  b) *R b)"
    by (simp add: euclidean_representation)
  also from integrable have " = (aBasis. integral A (λx. (f x  a) *R a))"
    by (subst integral_sum) (simp_all add: o_def)
  finally show ?thesis .
qed

lemma integrable_component:
  "f integrable_on A  (λx. f x  (y :: 'b :: euclidean_space)) integrable_on A"
  by (drule integrable_linear[OF _ bounded_linear_inner_left[of y]]) (simp add: o_def)



subsection Cauchy-type criterion for integrability

proposition integrable_Cauchy:
  fixes f :: "'n::euclidean_space  'a::{real_normed_vector,complete_space}"
  shows "f integrable_on cbox a b 
        (e>0. γ. gauge γ 
          (𝒟1 𝒟2. 𝒟1 tagged_division_of (cbox a b)  γ fine 𝒟1 
            𝒟2 tagged_division_of (cbox a b)  γ fine 𝒟2 
            norm (((x,K)𝒟1. content K *R f x) - ((x,K)𝒟2. content K *R f x)) < e))"
  (is "?l = (e>0. γ. ?P e γ)")
proof (intro iffI allI impI)
  assume ?l
  then obtain y
    where y: "e. e > 0 
        γ. gauge γ 
            (𝒟. 𝒟 tagged_division_of cbox a b  γ fine 𝒟 
                 norm (((x,K)  𝒟. content K *R f x) - y) < e)"
    by (auto simp: integrable_on_def has_integral)
  show "γ. ?P e γ" if "e > 0" for e
  proof -
    have "e/2 > 0" using that by auto
    with y obtain γ where "gauge γ"
      and γ: "𝒟. 𝒟 tagged_division_of cbox a b  γ fine 𝒟 
                  norm (((x,K)𝒟. content K *R f x) - y) < e/2"
      by meson
    show ?thesis
    apply (rule_tac x=γ in exI, clarsimp simp: gauge γ)
        by (blast intro!: γ dist_triangle_half_l[where y=y,unfolded dist_norm])
    qed
next
  assume "e>0. γ. ?P e γ"
  then have "n::nat. γ. ?P (1 / (n + 1)) γ"
    by auto
  then obtain γ :: "nat  'n  'n set" where γ:
    "m. gauge (γ m)"
    "m 𝒟1 𝒟2. 𝒟1 tagged_division_of cbox a b;
              γ m fine 𝒟1; 𝒟2 tagged_division_of cbox a b; γ m fine 𝒟2
               norm (((x,K)  𝒟1. content K *R f x) - ((x,K)  𝒟2. content K *R f x))
                  < 1 / (m + 1)"
    by metis
  have "gauge (λx. {γ i x |i. i  {0..n}})" for n
    using γ by (intro gauge_Inter) auto
  then have "n. p. p tagged_division_of (cbox a b)  (λx. {γ i x |i. i  {0..n}}) fine p"
    by (meson fine_division_exists)
  then obtain p where p: "z. p z tagged_division_of cbox a b"
                         "z. (λx. {γ i x |i. i  {0..z}}) fine p z"
    by meson
  have dp: "i n. in  γ i fine p n"
    using p unfolding fine_Inter
    using atLeastAtMost_iff by blast
  have "Cauchy (λn. sum (λ(x,K). content K *R (f x)) (p n))"
  proof (rule CauchyI)
    fix e::real
    assume "0 < e"
    then obtain N where "N  0" and N: "inverse (real N) < e"
      using real_arch_inverse[of e] by blast
    show "M. mM. nM. norm (((x,K)  p m. content K *R f x) - ((x,K)  p n. content K *R f x)) < e"
    proof (intro exI allI impI)
      fix m n
      assume mn: "N  m" "N  n"
      have "norm (((x,K)  p m. content K *R f x) - ((x,K)  p n. content K *R f x)) < 1 / (real N + 1)"
        by (simp add: p(1) dp mn γ)
      also have "... < e"
        using  N N  0 0 < e by (auto simp: field_simps)
      finally show "norm (((x,K)  p m. content K *R f x) - ((x,K)  p n. content K *R f x)) < e" .
    qed
  qed
  then obtain y where y: "no. nno. norm (((x,K)  p n. content K *R f x) - y) < r" if "r > 0" for r
    by (auto simp: convergent_eq_Cauchy[symmetric] dest: LIMSEQ_D)
  show ?l
    unfolding integrable_on_def has_integral
  proof (rule_tac x=y in exI, clarify)
    fix e :: real
    assume "e>0"
    then have e2: "e/2 > 0" by auto
    then obtain N1::nat where N1: "N1  0" "inverse (real N1) < e/2"
      using real_arch_inverse by blast
    obtain N2::nat where N2: "n. n  N2  norm (((x,K)  p n. content K *R f x) - y) < e/2"
      using y[OF e2] by metis
    show "γ. gauge γ 
              (𝒟. 𝒟 tagged_division_of (cbox a b)  γ fine 𝒟 
                norm (((x,K)  𝒟. content K *R f x) - y) < e)"
    proof (intro exI conjI allI impI)
      show "gauge (γ (N1+N2))"
        using γ by auto
      show "norm (((x,K)  q. content K *R f x) - y) < e"
           if "q tagged_division_of cbox a b  γ (N1+N2) fine q" for q
      proof (rule norm_triangle_half_r)
        have "norm (((x,K)  p (N1+N2). content K *R f x) - ((x,K)  q. content K *R f x))
               < 1 / (real (N1+N2) + 1)"
          by (rule γ; simp add: dp p that)
        also have "... < e/2"
          using N1 0 < e by (auto simp: field_simps intro: less_le_trans)
        finally show "norm (((x,K)  p (N1+N2). content K *R f x) - ((x,K)  q. content K *R f x)) < e/2" .
        show "norm (((x,K)  p (N1+N2). content K *R f x) - y) < e/2"
          using N2 le_add_same_cancel2 by blast
      qed
    qed
  qed
qed


subsection Additivity of integral on abutting intervals

lemma tagged_division_split_left_inj_content:
  assumes 𝒟: "𝒟 tagged_division_of S"
    and "(x1, K1)  𝒟" "(x2, K2)  𝒟" "K1  K2" "K1  {x. xk  c} = K2  {x. xk  c}" "k  Basis"
  shows "content (K1  {x. xk  c}) = 0"
proof -
  from tagged_division_ofD(4)[OF 𝒟 (x1, K1)  𝒟] obtain a b where K1: "K1 = cbox a b"
    by auto
  then have "interior (K1  {x. x  k  c}) = {}"
    by (metis tagged_division_split_left_inj assms)
  then show ?thesis
    unfolding K1 interval_split[OF k  Basis] by (auto simp: content_eq_0_interior)
qed

lemma tagged_division_split_right_inj_content:
  assumes 𝒟: "𝒟 tagged_division_of S"
    and "(x1, K1)  𝒟" "(x2, K2)  𝒟" "K1  K2" "K1  {x. xk  c} = K2  {x. xk  c}" "k  Basis"
  shows "content (K1  {x. xk  c}) = 0"
proof -
  from tagged_division_ofD(4)[OF 𝒟 (x1, K1)  𝒟] obtain a b where K1: "K1 = cbox a b"
    by auto
  then have "interior (K1  {x. c  x  k}) = {}"
    by (metis tagged_division_split_right_inj assms)
  then show ?thesis
    unfolding K1 interval_split[OF k  Basis]
    by (auto simp: content_eq_0_interior)
qed


proposition has_integral_split:
  fixes f :: "'a::euclidean_space  'b::real_normed_vector"
  assumes fi: "(f has_integral i) (cbox a b  {x. xk  c})"
      and fj: "(f has_integral j) (cbox a b  {x. xk  c})"
      and k: "k  Basis"
shows "(f has_integral (i + j)) (cbox a b)"
  unfolding has_integral
proof clarify
  fix e::real
  assume "0 < e"
  then have e: "e/2 > 0"
    by auto
    obtain γ1 where γ1: "gauge γ1"
      and γ1norm:
        "𝒟. 𝒟 tagged_division_of cbox a b  {x. x  k  c}; γ1 fine 𝒟
              norm (((x,K)  𝒟. content K *R f x) - i) < e/2"
       apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
       apply (simp add: interval_split[symmetric] k)
      done
    obtain γ2 where γ2: "gauge γ2"
      and γ2norm:
        "𝒟. 𝒟 tagged_division_of cbox a b  {x. c  x  k}; γ2 fine 𝒟
              norm (((x, k)  𝒟. content k *R f x) - j) < e/2"
       apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
       apply (simp add: interval_split[symmetric] k)
       done
  let  = "λx. if xk = c then (γ1 x  γ2 x) else ball x ¦xk - c¦  γ1 x  γ2 x"
  have "gauge "
    using γ1 γ2 unfolding gauge_def by auto
  then show "γ. gauge γ 
                 (𝒟. 𝒟 tagged_division_of cbox a b  γ fine 𝒟 
                      norm (((x, k)𝒟. content k *R f x) - (i + j)) < e)"
  proof (rule_tac x="" in exI, safe)
    fix p
    assume p: "p tagged_division_of (cbox a b)" and " fine p"
    have ab_eqp: "cbox a b = {K. x. (x, K)  p}"
      using p by blast
    have xk_le_c: "xk  c" if as: "(x,K)  p" and K: "K  {x. xk  c}  {}" for x K
    proof (rule ccontr)
      assume **: "¬ x  k  c"
      then have "K  ball x ¦x  k - c¦"
        using  fine p as by (fastforce simp: not_le algebra_simps)
      with K obtain y where y: "y  ball x ¦x  k - c¦" "yk  c"
        by blast
      then have "¦x  k - y  k¦ < ¦x  k - c¦"
        using Basis_le_norm[OF k, of "x - y"]
        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
      with y show False
        using ** by (auto simp add: field_simps)
    qed
    have xk_ge_c: "xk  c" if as: "(x,K)  p" and K: "K  {x. xk  c}  {}" for x K
    proof (rule ccontr)
      assume **: "¬ x  k  c"
      then have "K  ball x ¦x  k - c¦"
        using  fine p as by (fastforce simp: not_le algebra_simps)
      with K obtain y where y: "y  ball x ¦x  k - c¦" "yk  c"
        by blast
      then have "¦x  k - y  k¦ < ¦x  k - c¦"
        using Basis_le_norm[OF k, of "x - y"]
        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
      with y show False
        using ** by (auto simp add: field_simps)
    qed
    have fin_finite: "finite {(x,f K) | x K. (x,K)  s  P x K}"
      if "finite s" for s and f :: "'a set  'a set" and P :: "'a  'a set  bool"
    proof -
      from that have "finite ((λ(x,K). (x, f K)) ` s)"
        by auto
      then show ?thesis
        by (rule rev_finite_subset) auto
    qed
    { fix 𝒢 :: "'a set  'a set"
      fix i :: "'a × 'a set"
      assume "i  (λ(x, k). (x, 𝒢 k)) ` p - {(x, 𝒢 k) |x k. (x, k)  p  𝒢 k  {}}"
      then obtain x K where xk: "i = (x, 𝒢 K)"  "(x,K)  p"
                                 "(x, 𝒢 K)  {(x, 𝒢 K) |x K. (x,K)  p  𝒢 K  {}}"
        by auto
      have "content (𝒢 K) = 0"
        using xk using content_empty by auto
      then have "(λ(x,K). content K *R f x) i = 0"
        unfolding xk split_conv by auto
    } note [simp] = this
    have "finite p"
      using p by blast
    let ?M1 = "{(x, K  {x. xk  c}) |x K. (x,K)  p  K  {x. xk  c}  {}}"
    have γ1_fine: "γ1 fine ?M1"
      using  fine p by (fastforce simp: fine_def split: if_split_asm)
    have "norm (((x, k)?M1. content k *R f x) - i) < e/2"
    proof (rule γ1norm [OF tagged_division_ofI γ1_fine])
      show "finite ?M1"
        by (rule fin_finite) (use p in blast)
      show "{k. x. (x, k)  ?M1} = cbox a b  {x. xk  c}"
        by (auto simp: ab_eqp)

      fix x L
      assume xL: "(x, L)  ?M1"
      then obtain x' L' where xL': "x = x'" "L = L'  {x. x  k  c}"
                                   "(x', L')  p" "L'  {x. x  k  c}  {}"
        by blast
      then obtain a' b' where ab': "L' = cbox a' b'"
        using p by blast
      show "x  L" "L  cbox a b  {x. x  k  c}"
        using p xk_le_c xL' by auto
      show "a b. L = cbox a b"
        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])

      fix y R
      assume yR: "(y, R)  ?M1"
      then obtain y' R' where yR': "y = y'" "R = R'  {x. x  k  c}"
                                   "(y', R')  p" "R'  {x. x  k  c}  {}"
        by blast
      assume as: "(x, L)  (y, R)"
      show "interior L  interior R = {}"
      proof (cases "L' = R'  x' = y'")
        case False
        have "interior R' = {}"
          by (metis (no_types) False Pair_inject inf.idem tagged_division_ofD(5) [OF p] xL'(3) yR'(3))
        then show ?thesis
          using yR' by simp
      next
        case True
        then have "L'  R'"
          using as unfolding xL' yR' by auto
        have "interior L'  interior R' = {}"
          by (metis (no_types) Pair_inject L'  R' p tagged_division_ofD(5) xL'(3) yR'(3))
        then show ?thesis
          using xL'(2) yR'(2) by auto
      qed
    qed
    moreover
    let ?M2 = "{(x,K  {x. xk  c}) |x K. (x,K)  p  K  {x. xk  c}  {}}"
    have γ2_fine: "γ2 fine ?M2"
      using  fine p by (fastforce simp: fine_def split: if_split_asm)
    have "norm (((x, k)?M2. content k *R f x) - j) < e/2"
    proof (rule γ2norm [OF tagged_division_ofI γ2_fine])
      show "finite ?M2"
        by (rule fin_finite) (use p in blast)
      show "{k. x. (x, k)  ?M2} = cbox a b  {x. xk  c}"
        by (auto simp: ab_eqp)

      fix x L
      assume xL: "(x, L)  ?M2"
      then obtain x' L' where xL': "x = x'" "L = L'  {x. x  k  c}"
                                   "(x', L')  p" "L'  {x. x  k  c}  {}"
        by blast
      then obtain a' b' where ab': "L' = cbox a' b'"
        using p by blast
      show "x  L" "L  cbox a b  {x. x  k  c}"
        using p xk_ge_c xL' by auto
      show "a b. L = cbox a b"
        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])

      fix y R
      assume yR: "(y, R)  ?M2"
      then obtain y' R' where yR': "y = y'" "R = R'  {x. x  k  c}"
                                   "(y', R')  p" "R'  {x. x  k  c}  {}"
        by blast
      assume as: "(x, L)  (y, R)"
      show "interior L  interior R = {}"
      proof (cases "L' = R'  x' = y'")
        case False
        have "interior R' = {}"
          by (metis (no_types) False Pair_inject inf.idem tagged_division_ofD(5) [OF p] xL'(3) yR'(3))
        then show ?thesis
          using yR' by simp
      next
        case True
        then have "L'  R'"
          using as unfolding xL' yR' by auto
        have "interior L'  interior R' = {}"
          by (metis (no_types) Pair_inject L'  R' p tagged_division_ofD(5) xL'(3) yR'(3))
        then show ?thesis
          using xL'(2) yR'(2) by auto
      qed
    qed
    ultimately