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"
  by (smt (verit, ccfv_SIG) norm_diff_triangle_ineq)

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 ∀i∈Basis. a∙i ≤ b∙i then prod (λi. b∙i - a∙i) Basis else 0)"
  by (simp add: measure_lborel_cbox_eq inner_diff)

lemma content_cbox: "∀i∈Basis. a∙i ≤ b∙i ⟹ content (cbox a b) = (∏i∈Basis. b∙i - a∙i)"
  unfolding content_cbox_cases by simp

lemma content_cbox': "cbox a b ≠ {} ⟹ content (cbox a b) = (∏i∈Basis. b∙i - a∙i)"
  by (simp add: box_ne_empty inner_diff)

lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else ∏i∈Basis. b∙i - a∙i)"
  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 x≤y 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

corollary✐‹tag unimportant› content_nonneg [simp]: "¬ content (cbox a b) < 0"
  using not_le by blast

lemma content_pos_lt: "∀i∈Basis. a∙i < b∙i ⟹ 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 ⟷ (∃i∈Basis. b∙i ≤ a∙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 ⟷ 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)) ⟷ (∀i∈Basis. a∙i < b∙i)"
  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"
  by (fact zero_less_measure_iff)

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. x∙k ≤ c}) + content(cbox a b ∩ {x. x∙k ≥ c})"
  ― ‹Prove using measure theory›
proof (cases "∀i∈Basis. a ∙ i ≤ b ∙ i")
  case True
  have 1: "⋀X Y Z. (∏i∈Basis. Z i (if i = k then X else Y i)) = Z k X * (∏i∈Basis-{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: "(∏i∈Basis. b∙i - a∙i) = (∏i∈Basis-{k}. b∙i - a∙i) * (b∙k - a∙k)"
    by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove)
  have "⋀x. min (b ∙ k) c = max (a ∙ k) c ⟹
    x * (b∙k - a∙k) = x * (max (a ∙ k) c - a ∙ k) + x * (b ∙ k - max (a ∙ k) c)"
    by  (auto simp add: field_simps)
  moreover
  have **: "(∏i∈Basis. ((∑i∈Basis. (if i = k then min (b ∙ k) c else b ∙ i) *⇩R i) ∙ i - a ∙ i)) =
      (∏i∈Basis. (if i = k then min (b ∙ k) c else b ∙ i) - a ∙ i)"
    "(∏i∈Basis. b ∙ i - ((∑i∈Basis. (if i = k then max (a ∙ k) c else a ∙ i) *⇩R i) ∙ i)) =
      (∏i∈Basis. 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. b∙i - x"] 1[of "λi x. x - a∙i"] 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 integrable_on_mult_left:
  fixes c :: "'a :: real_normed_algebra"
  assumes "f integrable_on A"
  shows   "(λx. f x * c) integrable_on A"
  using assms has_integral_mult_left by blast

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)

lemma integrable_on_divide:
  fixes c :: "'a :: real_normed_div_algebra"
  assumes "f integrable_on A"
  shows   "(λx. f x / c) integrable_on A"
  using assms has_integral_divide by blast

text‹The case analysis eliminates the condition \<^term>‹f 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) A ⟹ ((λx. c * f x) has_integral (c * y)) A"
  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)

lemma integrable_on_mult_right:
  fixes c :: "'a :: real_normed_algebra"
  assumes "f integrable_on A"
  shows   "(λx. c * f x) integrable_on A"
  using assms has_integral_mult_right by blast

lemma integrable_on_mult_right_iff [simp]:
  fixes c :: "'a :: real_normed_field"
  assumes "c ≠ 0"
  shows   "(λx. c * f x) integrable_on A ⟷ f integrable_on A"
    using integrable_on_mult_right[of f A c]
          integrable_on_mult_right[of "λx. c * f x" A "inverse c"] assms
    by (auto simp: field_simps)

lemma integrable_on_mult_left_iff [simp]:
  fixes c :: "'a :: real_normed_field"
  assumes "c ≠ 0"
  shows   "(λx. f x * c) integrable_on A ⟷ f integrable_on A"
  using integrable_on_mult_right_iff[OF assms, of f A] by (simp add: mult.commute)

lemma integrable_on_div_iff [simp]:
  fixes c :: "'a :: real_normed_field"
  assumes "c ≠ 0"
  shows   "(λx. f x / c) integrable_on A ⟷ f integrable_on A"
  using integrable_on_mult_right_iff[of "inverse c" f A] assms by (simp add: field_simps)

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"
  by (metis assms has_integral_is_0 has_integral_mult_right lambda_zero)

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. ∑a∈I. f a x) = (∑a∈I. 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. ∑a∈I. 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 integrable_cong:
  assumes "⋀x. x ∈ A ⟹ f x = g x"
  shows   "f integrable_on A ⟷ g integrable_on A"
  using has_integral_cong [OF assms] by fast

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 ⟷ (∀b∈Basis. ((λ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 "(∀b∈Basis. ((λx. f x ∙ b) has_integral (y ∙ b)) A)"
  hence "∀b∈Basis. (((λ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. ∑b∈Basis. (f x ∙ b) *⇩R b) has_integral (∑b∈Basis. (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 ⟷ (∀b∈Basis. (λ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 "(∀b∈Basis. ((λx. f x ∙ b) has_integral (y ∙ b)) A)"
    by (subst (asm) has_integral_componentwise_iff)
  thus "(∀b∈Basis. (λx. f x ∙ b) integrable_on A)" by (auto simp: integrable_on_def)
next
  assume "(∀b∈Basis. (λx. f x ∙ b) integrable_on A)"
  then obtain y where "∀b∈Basis. ((λx. f x ∙ b) has_integral y b) A"
    unfolding integrable_on_def by (subst (asm) bchoice_iff) blast
  hence "∀b∈Basis. (((λ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. ∑b∈Basis. (f x ∙ b) *⇩R b) has_integral (∑b∈Basis. 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 = (∑b∈Basis. integral A (λx. (f x ∙ b) *⇩R b))"
proof -
  from assms have integrable: "∀b∈Basis. (λ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. ∑b∈Basis. (f x ∙ b) *⇩R b)"
    by (simp add: euclidean_representation)
  also from integrable have "… = (∑a∈Basis. 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. i≤n ⟹ γ 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. ∀m≥M. ∀n≥M. 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. ∀n≥no. 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. x∙k ≤ c} = K2 ∩ {x. x∙k ≤ c}" "k ∈ Basis"
  shows "content (K1 ∩ {x. x∙k ≤ 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. x∙k ≥ c} = K2 ∩ {x. x∙k ≥ c}" "k ∈ Basis"
  shows "content (K1 ∩ {x. x∙k ≥ 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. x∙k ≤ c})"
      and fj: "(f has_integral j) (cbox a b ∩ {x. x∙k ≥ 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 x∙k = c then (γ1 x ∩ γ2 x) else ball x ¦x∙k - 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: "x∙k ≤ c" if as: "(x,K) ∈ p" and K: "K ∩ {x. x∙k ≤ 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¦" "y∙k ≤ 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: "x∙k ≥ c" if as: "(x,K) ∈ p" and K: "K ∩ {x. x∙k ≥ 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¦" "y∙k ≥ 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. x∙k ≤ c}) |x K. (x,K) ∈ p ∧ K ∩ {x. x∙k ≤ 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. x∙k ≤ 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,