# 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)"

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)"

lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else ∏i∈Basis. b∙i - a∙i)"

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)"

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)"

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"

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
then 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
then show ?thesis
using ‹content (box a b) > 0›
by (smt (verit, best) Sigma_Algebra.measure_def emeasure_lborel_ball_finite enn2real_mono infinity_ennreal_def)
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
then 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 (cball 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 (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)"
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 (intro sum.neutral strip)
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"
qed

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

"d tagged_division_of (cbox a b) ⟹ sum (λ(x,l). content l) d = content (cbox a b)"
by (fact sum_content.tagged_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)"
finally show ?thesis .
qed

lemma content_real_eq_0: "content {a..b::real} = 0 ⟷ a ≥ b"
by simp

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))"

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

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

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 (meson division_filter_not_empty has_integral_cbox tendsto_unique)

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"]
also have "… < norm (k1 - k2)/2 + norm (k1 - k2)/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
by (metis (mono_tags, lifting))

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"]
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 blast

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

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)"
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"]
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"]

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

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

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)"
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 auto

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)"
by simp

lemma integral_neg [simp]: "integral S (λx. - f x) = - integral S f"
by (metis eq_integralD equation_minus_iff has_integral_iff has_integral_neg_iff neg_equal_0_iff_equal)

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"

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

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 has_integral_cnj: "(cnj ∘ f has_integral (cnj I)) A  = (f has_integral I) A"
unfolding has_integral_iff comp_def
by (metis integral_cnj complex_cnj_cancel_iff integrable_on_cnj_iff)

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 ‹finite T› subset_refl[of T]
by (induct rule: finite_subset_induct) (use assms in ‹auto simp: has_integral_add›)

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: "(f has_integral k) s"
shows "(g has_integral k) s"
using has_integral_diff[OF f, of "λx. f x - g x" 0]
using has_integral_is_0[of s "λx. f x - g x"]
using assms
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"
by (metis assms has_integral_eq)

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"]
then have "(λx. (of_real (1 / c) * of_real c * f x)) integrable_on s"
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_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)"

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 blast

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 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)
have "integral A f = integral A (λx. ∑b∈Basis. (f x ∙ b) *⇩R b)"
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"
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])
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])
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, 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. x∙k ≥ c}) |x K. (x,K) ∈ p ∧ K ∩ {x. x∙k ≥ 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])```