# Theory Improper_Integral

theory Improper_Integral
imports Equivalence_Lebesgue_Henstock_Integration
```section‹Continuity of the indefinite integral; improper integral theorem›

theory "Improper_Integral"
imports Equivalence_Lebesgue_Henstock_Integration
begin

subsection‹Equiintegrability›

text‹The definition here only really makes sense for an elementary set.
We just use compact intervals in applications below.›

definition equiintegrable_on (infixr "equiintegrable'_on" 46)
where "F equiintegrable_on I ≡
(∀f ∈ F. f integrable_on I) ∧
(∀e > 0. ∃γ. gauge γ ∧
(∀f 𝒟. f ∈ F ∧ 𝒟 tagged_division_of I ∧ γ fine 𝒟
⟶ norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral I f) < e))"

lemma equiintegrable_on_integrable:
"⟦F equiintegrable_on I; f ∈ F⟧ ⟹ f integrable_on I"
using equiintegrable_on_def by metis

lemma equiintegrable_on_sing [simp]:
"{f} equiintegrable_on cbox a b ⟷ f integrable_on cbox a b"
by (simp add: equiintegrable_on_def has_integral_integral has_integral integrable_on_def)

lemma equiintegrable_on_subset: "⟦F equiintegrable_on I; G ⊆ F⟧ ⟹ G equiintegrable_on I"
unfolding equiintegrable_on_def Ball_def
by (erule conj_forward imp_forward all_forward ex_forward | blast)+

lemma equiintegrable_on_Un:
assumes "F equiintegrable_on I" "G equiintegrable_on I"
shows "(F ∪ G) equiintegrable_on I"
unfolding equiintegrable_on_def
proof (intro conjI impI allI)
show "∀f∈F ∪ G. f integrable_on I"
using assms unfolding equiintegrable_on_def by blast
show "∃γ. gauge γ ∧
(∀f 𝒟. f ∈ F ∪ G ∧
𝒟 tagged_division_of I ∧ γ fine 𝒟 ⟶
norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral I f) < ε)"
if "ε > 0" for ε
proof -
obtain γ1 where "gauge γ1"
and γ1: "⋀f 𝒟. f ∈ F ∧ 𝒟 tagged_division_of I ∧ γ1 fine 𝒟
⟹ norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral I f) < ε"
using assms ‹ε > 0› unfolding equiintegrable_on_def by auto
obtain γ2 where  "gauge γ2"
and γ2: "⋀f 𝒟. f ∈ G ∧ 𝒟 tagged_division_of I ∧ γ2 fine 𝒟
⟹ norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral I f) < ε"
using assms ‹ε > 0› unfolding equiintegrable_on_def by auto
have "gauge (λx. γ1 x ∩ γ2 x)"
using ‹gauge γ1› ‹gauge γ2› by blast
moreover have "∀f 𝒟. f ∈ F ∪ G ∧ 𝒟 tagged_division_of I ∧ (λx. γ1 x ∩ γ2 x) fine 𝒟 ⟶
norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral I f) < ε"
using γ1 γ2 by (auto simp: fine_Int)
ultimately show ?thesis
by (intro exI conjI) assumption+
qed
qed

lemma equiintegrable_on_insert:
assumes "f integrable_on cbox a b" "F equiintegrable_on cbox a b"
shows "(insert f F) equiintegrable_on cbox a b"
by (metis assms equiintegrable_on_Un equiintegrable_on_sing insert_is_Un)

text‹ Basic combining theorems for the interval of integration.›

lemma equiintegrable_on_null [simp]:
"content(cbox a b) = 0 ⟹ F equiintegrable_on cbox a b"
apply (auto simp: equiintegrable_on_def)
by (metis gauge_trivial norm_eq_zero sum_content_null)

text‹ Main limit theorem for an equiintegrable sequence.›

theorem equiintegrable_limit:
fixes g :: "'a :: euclidean_space ⇒ 'b :: banach"
assumes feq: "range f equiintegrable_on cbox a b"
and to_g: "⋀x. x ∈ cbox a b ⟹ (λn. f n x) ⇢ g x"
shows "g integrable_on cbox a b ∧ (λn. integral (cbox a b) (f n)) ⇢ integral (cbox a b) g"
proof -
have "Cauchy (λn. integral(cbox a b) (f n))"
fix e::real
assume "0 < e"
then have e3: "0 < e/3"
by simp
then obtain γ where "gauge γ"
and γ: "⋀n 𝒟. ⟦𝒟 tagged_division_of cbox a b; γ fine 𝒟⟧
⟹ norm((∑(x,K) ∈ 𝒟. content K *⇩R f n x) - integral (cbox a b) (f n)) < e/3"
using feq unfolding equiintegrable_on_def
by (meson image_eqI iso_tuple_UNIV_I)
obtain 𝒟 where 𝒟: "𝒟 tagged_division_of (cbox a b)" and "γ fine 𝒟"  "finite 𝒟"
by (meson ‹gauge γ› fine_division_exists tagged_division_of_finite)
with γ have δT: "⋀n. dist ((∑(x,K)∈𝒟. content K *⇩R f n x)) (integral (cbox a b) (f n)) < e/3"
by (force simp: dist_norm)
have "(λn. ∑(x,K)∈𝒟. content K *⇩R f n x) ⇢ (∑(x,K)∈𝒟. content K *⇩R g x)"
using 𝒟 to_g by (auto intro!: tendsto_sum tendsto_scaleR)
then have "Cauchy (λn. ∑(x,K)∈𝒟. content K *⇩R f n x)"
by (meson convergent_eq_Cauchy)
with e3 obtain M where
M: "⋀m n. ⟦m≥M; n≥M⟧ ⟹ dist (∑(x,K)∈𝒟. content K *⇩R f m x) (∑(x,K)∈𝒟. content K *⇩R f n x)
< e/3"
unfolding Cauchy_def by blast
have "⋀m n. ⟦m≥M; n≥M;
dist (∑(x,K)∈𝒟. content K *⇩R f m x) (∑(x,K)∈𝒟. content K *⇩R f n x) < e/3⟧
⟹ dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
by (metis δT dist_commute dist_triangle_third [OF _ _ δT])
then show "∃M. ∀m≥M. ∀n≥M. dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
using M by auto
qed
then obtain L where L: "(λn. integral (cbox a b) (f n)) ⇢ L"
by (meson convergent_eq_Cauchy)
have "(g has_integral L) (cbox a b)"
proof (clarsimp simp: has_integral)
fix e::real assume "0 < e"
then have e2: "0 < e/2"
by simp
then obtain γ where "gauge γ"
and γ: "⋀n 𝒟. ⟦𝒟 tagged_division_of cbox a b; γ fine 𝒟⟧
⟹ norm((∑(x,K)∈𝒟. content K *⇩R f n x) - integral (cbox a b) (f n)) < e/2"
using feq unfolding equiintegrable_on_def
by (meson image_eqI iso_tuple_UNIV_I)
moreover
have "norm ((∑(x,K)∈𝒟. content K *⇩R g x) - L) < e"
if "𝒟 tagged_division_of cbox a b" "γ fine 𝒟" for 𝒟
proof -
have "norm ((∑(x,K)∈𝒟. content K *⇩R g x) - L) ≤ e/2"
proof (rule Lim_norm_ubound)
show "(λn. (∑(x,K)∈𝒟. content K *⇩R f n x) - integral (cbox a b) (f n)) ⇢ (∑(x,K)∈𝒟. content K *⇩R g x) - L"
using to_g that L
by (intro tendsto_diff tendsto_sum) (auto simp: tag_in_interval tendsto_scaleR)
show "∀⇩F n in sequentially.
norm ((∑(x,K) ∈ 𝒟. content K *⇩R f n x) - integral (cbox a b) (f n)) ≤ e/2"
by (intro eventuallyI less_imp_le γ that)
qed auto
with ‹0 < e› show ?thesis
by linarith
qed
ultimately
show "∃γ. gauge γ ∧
(∀𝒟. 𝒟 tagged_division_of cbox a b ∧ γ fine 𝒟 ⟶
norm ((∑(x,K)∈𝒟. content K *⇩R g x) - L) < e)"
by meson
qed
with L show ?thesis
by (simp add: ‹(λn. integral (cbox a b) (f n)) ⇢ L› has_integral_integrable_integral)
qed

lemma equiintegrable_reflect:
assumes "F equiintegrable_on cbox a b"
shows "(λf. f ∘ uminus) ` F equiintegrable_on cbox (-b) (-a)"
proof -
have "∃γ. gauge γ ∧
(∀f 𝒟. f ∈ (λf. f ∘ uminus) ` F ∧ 𝒟 tagged_division_of cbox (- b) (- a) ∧ γ fine 𝒟 ⟶
norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral (cbox (- b) (- a)) f) < e)"
if "gauge γ" and
γ: "⋀f 𝒟. ⟦f ∈ F; 𝒟 tagged_division_of cbox a b; γ fine 𝒟⟧ ⟹
norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral (cbox a b) f) < e" for e γ
proof (intro exI, safe)
show "gauge (λx. uminus ` γ (-x))"
by (metis ‹gauge γ› gauge_reflect)
show "norm ((∑(x,K) ∈ 𝒟. content K *⇩R (f ∘ uminus) x) - integral (cbox (- b) (- a)) (f ∘ uminus)) < e"
if "f ∈ F" and tag: "𝒟 tagged_division_of cbox (- b) (- a)"
and fine: "(λx. uminus ` γ (- x)) fine 𝒟" for f 𝒟
proof -
have 1: "(λ(x,K). (- x, uminus ` K)) ` 𝒟 tagged_partial_division_of cbox a b"
if "𝒟 tagged_partial_division_of cbox (- b) (- a)"
proof -
have "- y ∈ cbox a b"
if "⋀x K. (x,K) ∈ 𝒟 ⟹ x ∈ K ∧ K ⊆ cbox (- b) (- a) ∧ (∃a b. K = cbox a b)"
"(x, Y) ∈ 𝒟" "y ∈ Y" for x Y y
proof -
have "y ∈ uminus ` cbox a b"
using that by auto
then show "- y ∈ cbox a b"
by force
qed
with that show ?thesis
by (fastforce simp: tagged_partial_division_of_def interior_negations image_iff)
qed
have 2: "∃K. (∃x. (x,K) ∈ (λ(x,K). (- x, uminus ` K)) ` 𝒟) ∧ x ∈ K"
if "⋃{K. ∃x. (x,K) ∈ 𝒟} = cbox (- b) (- a)" "x ∈ cbox a b" for x
proof -
have xm: "x ∈ uminus ` ⋃{A. ∃a. (a, A) ∈ 𝒟}"
then obtain a X where "-x ∈ X" "(a, X) ∈ 𝒟"
by auto
then show ?thesis
by (metis (no_types, lifting) add.inverse_inverse image_iff pair_imageI)
qed
have 3: "⋀x X y. ⟦𝒟 tagged_partial_division_of cbox (- b) (- a); (x, X) ∈ 𝒟; y ∈ X⟧ ⟹ - y ∈ cbox a b"
by (metis (no_types, lifting) equation_minus_iff imageE subsetD tagged_partial_division_ofD(3) uminus_interval_vector)
have tag': "(λ(x,K). (- x, uminus ` K)) ` 𝒟 tagged_division_of cbox a b"
using tag  by (auto simp: tagged_division_of_def dest: 1 2 3)
have fine': "γ fine (λ(x,K). (- x, uminus ` K)) ` 𝒟"
using fine by (fastforce simp: fine_def)
have inj: "inj_on (λ(x,K). (- x, uminus ` K)) 𝒟"
unfolding inj_on_def by force
have eq: "content (uminus ` I) = content I"
if I: "(x, I) ∈ 𝒟" and fnz: "f (- x) ≠ 0" for x I
proof -
obtain a b where "I = cbox a b"
using tag I that by (force simp: tagged_division_of_def tagged_partial_division_of_def)
then show ?thesis
using content_image_affinity_cbox [of "-1" 0] by auto
qed
have "(∑(x,K) ∈ (λ(x,K). (- x, uminus ` K)) ` 𝒟.  content K *⇩R f x) =
(∑(x,K) ∈ 𝒟. content K *⇩R f (- x))"
apply (simp add: sum.reindex [OF inj])
apply (auto simp: eq intro!: sum.cong)
done
then show ?thesis
using γ [OF ‹f ∈ F› tag' fine'] integral_reflect
by (metis (mono_tags, lifting) Henstock_Kurzweil_Integration.integral_cong comp_apply split_def sum.cong)
qed
qed
then show ?thesis
using assms
apply (auto simp: equiintegrable_on_def)
apply (rule integrable_eq)
by auto
qed

subsection‹Subinterval restrictions for equiintegrable families›

text‹First, some technical lemmas about minimizing a "flat" part of a sum over a division.›

lemma lemma0:
assumes "i ∈ Basis"
shows "content (cbox u v) / (interval_upperbound (cbox u v) ∙ i - interval_lowerbound (cbox u v) ∙ i) =
(if content (cbox u v) = 0 then 0
else ∏j ∈ Basis - {i}. interval_upperbound (cbox u v) ∙ j - interval_lowerbound (cbox u v) ∙ j)"
proof (cases "content (cbox u v) = 0")
case True
then show ?thesis by simp
next
case False
then show ?thesis
using prod.subset_diff [of "{i}" Basis] assms
by (force simp: content_cbox_if divide_simps  split: if_split_asm)
qed

lemma content_division_lemma1:
assumes div: "𝒟 division_of S" and S: "S ⊆ cbox a b" and i: "i ∈ Basis"
and mt: "⋀K. K ∈ 𝒟 ⟹ content K ≠ 0"
and disj: "(∀K ∈ 𝒟. K ∩ {x. x ∙ i = a ∙ i} ≠ {}) ∨ (∀K ∈ 𝒟. K ∩ {x. x ∙ i = b ∙ i} ≠ {})"
shows "(b ∙ i - a ∙ i) * (∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))
≤ content(cbox a b)"   (is "?lhs ≤ ?rhs")
proof -
have "finite 𝒟"
using div by blast
define extend where
"extend ≡ λK. cbox (∑j ∈ Basis. if j = i then (a ∙ i) *⇩R i else (interval_lowerbound K ∙ j) *⇩R j)
(∑j ∈ Basis. if j = i then (b ∙ i) *⇩R i else (interval_upperbound K ∙ j) *⇩R j)"
have div_subset_cbox: "⋀K. K ∈ 𝒟 ⟹ K ⊆ cbox a b"
using S div by auto
have "⋀K. K ∈ 𝒟 ⟹ K ≠ {}"
using div by blast
have extend: "extend K ≠ {}" "extend K ⊆ cbox a b" if K: "K ∈ 𝒟" for K
proof -
obtain u v where K: "K = cbox u v" "K ≠ {}" "K ⊆ cbox a b"
using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
with i show "extend K ≠ {}" "extend K ⊆ cbox a b"
apply (auto simp: extend_def subset_box box_ne_empty sum_if_inner)
by fastforce
qed
have int_extend_disjoint:
"interior(extend K1) ∩ interior(extend K2) = {}" if K: "K1 ∈ 𝒟" "K2 ∈ 𝒟" "K1 ≠ K2" for K1 K2
proof -
obtain u v where K1: "K1 = cbox u v" "K1 ≠ {}" "K1 ⊆ cbox a b"
using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
obtain w z where K2: "K2 = cbox w z" "K2 ≠ {}" "K2 ⊆ cbox a b"
using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
have cboxes: "cbox u v ∈ 𝒟" "cbox w z ∈ 𝒟" "cbox u v ≠ cbox w z"
using K1 K2 that by auto
with div have "interior (cbox u v) ∩ interior (cbox w z) = {}"
by blast
moreover
have "∃x. x ∈ box u v ∧ x ∈ box w z"
if "x ∈ interior (extend K1)" "x ∈ interior (extend K2)" for x
proof -
have "a ∙ i < x ∙ i" "x ∙ i < b ∙ i"
and ux: "⋀k. k ∈ Basis - {i} ⟹ u ∙ k < x ∙ k"
and xv: "⋀k. k ∈ Basis - {i} ⟹ x ∙ k < v ∙ k"
and wx: "⋀k. k ∈ Basis - {i} ⟹ w ∙ k < x ∙ k"
and xz: "⋀k. k ∈ Basis - {i} ⟹ x ∙ k < z ∙ k"
using that K1 K2 i by (auto simp: extend_def box_ne_empty sum_if_inner mem_box)
have "box u v ≠ {}" "box w z ≠ {}"
using cboxes interior_cbox by (auto simp: content_eq_0_interior dest: mt)
then obtain q s
where q: "⋀k. k ∈ Basis ⟹ w ∙ k < q ∙ k ∧ q ∙ k < z ∙ k"
and s: "⋀k. k ∈ Basis ⟹ u ∙ k < s ∙ k ∧ s ∙ k < v ∙ k"
by (meson all_not_in_conv mem_box(1))
show ?thesis  using disj
proof
assume "∀K∈𝒟. K ∩ {x. x ∙ i = a ∙ i} ≠ {}"
then have uva: "(cbox u v) ∩ {x. x ∙ i = a ∙ i} ≠ {}"
and  wza: "(cbox w z) ∩ {x. x ∙ i = a ∙ i} ≠ {}"
using cboxes by (auto simp: content_eq_0_interior)
then obtain r t where "r ∙ i = a ∙ i" and r: "⋀k. k ∈ Basis ⟹ w ∙ k ≤ r ∙ k ∧ r ∙ k ≤ z ∙ k"
and "t ∙ i = a ∙ i" and t: "⋀k. k ∈ Basis ⟹ u ∙ k ≤ t ∙ k ∧ t ∙ k ≤ v ∙ k"
by (fastforce simp: mem_box)
have u: "u ∙ i < q ∙ i"
using i K2(1) K2(3) ‹t ∙ i = a ∙ i› q s t [OF i] by (force simp: subset_box)
have w: "w ∙ i < s ∙ i"
using i K1(1) K1(3) ‹r ∙ i = a ∙ i› s r [OF i] by (force simp: subset_box)
let ?x = "(∑j ∈ Basis. if j = i then min (q ∙ i) (s ∙ i) *⇩R i else (x ∙ j) *⇩R j)"
show ?thesis
proof (intro exI conjI)
show "?x ∈ box u v"
using ‹i ∈ Basis› s apply (clarsimp simp: mem_box)
apply (subst sum_if_inner; simp)+
apply (fastforce simp: u ux xv)
done
show "?x ∈ box w z"
using ‹i ∈ Basis› q apply (clarsimp simp: mem_box)
apply (subst sum_if_inner; simp)+
apply (fastforce simp: w wx xz)
done
qed
next
assume "∀K∈𝒟. K ∩ {x. x ∙ i = b ∙ i} ≠ {}"
then have uva: "(cbox u v) ∩ {x. x ∙ i = b ∙ i} ≠ {}"
and  wza: "(cbox w z) ∩ {x. x ∙ i = b ∙ i} ≠ {}"
using cboxes by (auto simp: content_eq_0_interior)
then obtain r t where "r ∙ i = b ∙ i" and r: "⋀k. k ∈ Basis ⟹ w ∙ k ≤ r ∙ k ∧ r ∙ k ≤ z ∙ k"
and "t ∙ i = b ∙ i" and t: "⋀k. k ∈ Basis ⟹ u ∙ k ≤ t ∙ k ∧ t ∙ k ≤ v ∙ k"
by (fastforce simp: mem_box)
have z: "s ∙ i < z ∙ i"
using K1(1) K1(3) ‹r ∙ i = b ∙ i› r [OF i] i s  by (force simp: subset_box)
have v: "q ∙ i < v ∙ i"
using K2(1) K2(3) ‹t ∙ i = b ∙ i› t [OF i] i q  by (force simp: subset_box)
let ?x = "(∑j ∈ Basis. if j = i then max (q ∙ i) (s ∙ i) *⇩R i else (x ∙ j) *⇩R j)"
show ?thesis
proof (intro exI conjI)
show "?x ∈ box u v"
using ‹i ∈ Basis› s apply (clarsimp simp: mem_box)
apply (subst sum_if_inner; simp)+
apply (fastforce simp: v ux xv)
done
show "?x ∈ box w z"
using ‹i ∈ Basis› q apply (clarsimp simp: mem_box)
apply (subst sum_if_inner; simp)+
apply (fastforce simp: z wx xz)
done
qed
qed
qed
ultimately show ?thesis by auto
qed
have "?lhs = (∑K∈𝒟. (b ∙ i - a ∙ i) * content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))"
also have "… = sum (content ∘ extend) 𝒟"
proof (rule sum.cong [OF refl])
fix K assume "K ∈ 𝒟"
then obtain u v where K: "K = cbox u v" "cbox u v ≠ {}" "K ⊆ cbox a b"
using cbox_division_memE [OF _ div] div_subset_cbox by metis
then have uv: "u ∙ i < v ∙ i"
using mt [OF ‹K ∈ 𝒟›] ‹i ∈ Basis› content_eq_0 by fastforce
have "insert i (Basis ∩ -{i}) = Basis"
using ‹i ∈ Basis› by auto
then have "(b ∙ i - a ∙ i) * content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)
= (b ∙ i - a ∙ i) * (∏i ∈ insert i (Basis ∩ -{i}). v ∙ i - u ∙ i) / (interval_upperbound (cbox u v) ∙ i - interval_lowerbound (cbox u v) ∙ i)"
using K box_ne_empty(1) content_cbox by fastforce
also have "... = (∏x∈Basis. if x = i then b ∙ x - a ∙ x
else (interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) ∙ x)"
using ‹i ∈ Basis› K uv by (simp add: prod.If_cases) (simp add: algebra_simps)
also have "... = (∏k∈Basis.
(∑j∈Basis. if j = i then (b ∙ i - a ∙ i) *⇩R i else ((interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) ∙ j) *⇩R j) ∙ k)"
using ‹i ∈ Basis› by (subst prod.cong [OF refl sum_if_inner]; simp)
also have "... = (∏k∈Basis.
(∑j∈Basis. if j = i then (b ∙ i) *⇩R i else (interval_upperbound (cbox u v) ∙ j) *⇩R j) ∙ k -
(∑j∈Basis. if j = i then (a ∙ i) *⇩R i else (interval_lowerbound (cbox u v) ∙ j) *⇩R j) ∙ k)"
apply (rule prod.cong [OF refl])
using ‹i ∈ Basis›
apply (subst sum_if_inner; simp add: algebra_simps)+
done
also have "... = (content ∘ extend) K"
using ‹i ∈ Basis› K box_ne_empty
apply (subst content_cbox, auto)
done
finally show "(b ∙ i - a ∙ i) * content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)
= (content ∘ extend) K" .
qed
also have "... = sum content (extend ` 𝒟)"
proof -
have "⟦K1 ∈ 𝒟; K2 ∈ 𝒟; K1 ≠ K2; extend K1 = extend K2⟧ ⟹ content (extend K1) = 0" for K1 K2
using int_extend_disjoint [of K1 K2] extend_def by (simp add: content_eq_0_interior)
then show ?thesis
qed
also have "... ≤ ?rhs"
show "extend ` 𝒟 division_of UNION 𝒟 extend"
using int_extend_disjoint apply (auto simp: division_of_def ‹finite 𝒟› extend)
using extend_def apply blast
done
show "UNION 𝒟 extend ⊆ cbox a b"
using extend by fastforce
qed
finally show ?thesis .
qed

proposition sum_content_area_over_thin_division:
assumes div: "𝒟 division_of S" and S: "S ⊆ cbox a b" and i: "i ∈ Basis"
and "a ∙ i ≤ c" "c ≤ b ∙ i"
and nonmt: "⋀K. K ∈ 𝒟 ⟹ K ∩ {x. x ∙ i = c} ≠ {}"
shows "(b ∙ i - a ∙ i) * (∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))
≤ 2 * content(cbox a b)"
proof (cases "content(cbox a b) = 0")
case True
have "(∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) = 0"
using S div by (force intro!: sum.neutral content_0_subset [OF True])
then show ?thesis
by (auto simp: True)
next
case False
then have "content(cbox a b) > 0"
using zero_less_measure_iff by blast
then have "a ∙ i < b ∙ i" if "i ∈ Basis" for i
using content_pos_lt_eq that by blast
have "finite 𝒟"
using div by blast
define Dlec where "Dlec ≡ {L ∈ (λL. L ∩ {x. x ∙ i ≤ c}) ` 𝒟. content L ≠ 0}"
define Dgec where "Dgec ≡ {L ∈ (λL. L ∩ {x. x ∙ i ≥ c}) ` 𝒟. content L ≠ 0}"
define a' where "a' ≡ (∑j∈Basis. (if j = i then c else a ∙ j) *⇩R j)"
define b' where "b' ≡ (∑j∈Basis. (if j = i then c else b ∙ j) *⇩R j)"
have Dlec_cbox: "⋀K. K ∈ Dlec ⟹ ∃a b. K = cbox a b"
using interval_split [OF i] div by (fastforce simp: Dlec_def division_of_def)
then have lec_is_cbox: "⟦content (L ∩ {x. x ∙ i ≤ c}) ≠ 0; L ∈ 𝒟⟧ ⟹ ∃a b. L ∩ {x. x ∙ i ≤ c} = cbox a b" for L
using Dlec_def by blast
have Dgec_cbox: "⋀K. K ∈ Dgec ⟹ ∃a b. K = cbox a b"
using interval_split [OF i] div by (fastforce simp: Dgec_def division_of_def)
then have gec_is_cbox: "⟦content (L ∩ {x. x ∙ i ≥ c}) ≠ 0; L ∈ 𝒟⟧ ⟹ ∃a b. L ∩ {x. x ∙ i ≥ c} = cbox a b" for L
using Dgec_def by blast
have "(b' ∙ i - a ∙ i) * (∑K∈Dlec. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ≤ content(cbox a b')"
proof (rule content_division_lemma1)
show "Dlec division_of ⋃Dlec"
unfolding division_of_def
proof (intro conjI ballI Dlec_cbox)
show "⋀K1 K2. ⟦K1 ∈ Dlec; K2 ∈ Dlec⟧ ⟹ K1 ≠ K2 ⟶ interior K1 ∩ interior K2 = {}"
by (clarsimp simp: Dlec_def) (use div in auto)
qed (use ‹finite 𝒟› Dlec_def in auto)
show "⋃Dlec ⊆ cbox a b'"
using Dlec_def div S by (auto simp: b'_def division_of_def mem_box)
show "(∀K∈Dlec. K ∩ {x. x ∙ i = a ∙ i} ≠ {}) ∨ (∀K∈Dlec. K ∩ {x. x ∙ i = b' ∙ i} ≠ {})"
using nonmt by (fastforce simp: Dlec_def b'_def sum_if_inner i)
qed (use i Dlec_def in auto)
moreover
have "(∑K∈Dlec. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) =
(∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K)"
apply (subst sum.reindex_nontrivial [OF ‹finite 𝒟›, symmetric], simp)
apply (metis division_split_left_inj [OF div] lec_is_cbox content_eq_0_interior)
unfolding Dlec_def using ‹finite 𝒟› apply (auto simp: sum.mono_neutral_left)
done
moreover have "(b' ∙ i - a ∙ i) = (c - a ∙ i)"
by (simp add: b'_def sum_if_inner i)
ultimately
have lec: "(c - a ∙ i) * (∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K)
≤ content(cbox a b')"
by simp

have "(b ∙ i - a' ∙ i) * (∑K∈Dgec. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ≤ content(cbox a' b)"
proof (rule content_division_lemma1)
show "Dgec division_of ⋃Dgec"
unfolding division_of_def
proof (intro conjI ballI Dgec_cbox)
show "⋀K1 K2. ⟦K1 ∈ Dgec; K2 ∈ Dgec⟧ ⟹ K1 ≠ K2 ⟶ interior K1 ∩ interior K2 = {}"
by (clarsimp simp: Dgec_def) (use div in auto)
qed (use ‹finite 𝒟› Dgec_def in auto)
show "⋃Dgec ⊆ cbox a' b"
using Dgec_def div S by (auto simp: a'_def division_of_def mem_box)
show "(∀K∈Dgec. K ∩ {x. x ∙ i = a' ∙ i} ≠ {}) ∨ (∀K∈Dgec. K ∩ {x. x ∙ i = b ∙ i} ≠ {})"
using nonmt by (fastforce simp: Dgec_def a'_def sum_if_inner i)
qed (use i Dgec_def in auto)
moreover
have "(∑K∈Dgec. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) =
(∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)"
apply (subst sum.reindex_nontrivial [OF ‹finite 𝒟›, symmetric], simp)
apply (metis division_split_right_inj [OF div] gec_is_cbox content_eq_0_interior)
unfolding Dgec_def using ‹finite 𝒟› apply (auto simp: sum.mono_neutral_left)
done
moreover have "(b ∙ i - a' ∙ i) = (b ∙ i - c)"
by (simp add: a'_def sum_if_inner i)
ultimately
have gec: "(b ∙ i - c) * (∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)
≤ content(cbox a' b)"
by simp
show ?thesis
proof (cases "c = a ∙ i ∨ c = b ∙ i")
case True
then show ?thesis
proof
assume c: "c = a ∙ i"
then have "a' = a"
apply (simp add: sum_if_inner i a'_def cong: if_cong)
using euclidean_representation [of a] sum.cong [OF refl, of Basis "λi. (a ∙ i) *⇩R i"] by presburger
then have "content (cbox a' b) ≤ 2 * content (cbox a b)"  by simp
moreover
have eq: "(∑K∈𝒟. content (K ∩ {x. a ∙ i ≤ x ∙ i}) /
(interval_upperbound (K ∩ {x. a ∙ i ≤ x ∙ i}) ∙ i - interval_lowerbound (K ∩ {x. a ∙ i ≤ x ∙ i}) ∙ i))
= (∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))"
(is "sum ?f _ = sum ?g _")
proof (rule sum.cong [OF refl])
fix K assume "K ∈ 𝒟"
then have "a ∙ i ≤ x ∙ i" if "x ∈ K" for x
by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
then have "K ∩ {x. a ∙ i ≤ x ∙ i} = K"
by blast
then show "?f K = ?g K"
by simp
qed
ultimately show ?thesis
using gec c eq by auto
next
assume c: "c = b ∙ i"
then have "b' = b"
apply (simp add: sum_if_inner i b'_def cong: if_cong)
using euclidean_representation [of b] sum.cong [OF refl, of Basis "λi. (b ∙ i) *⇩R i"] by presburger
then have "content (cbox a b') ≤ 2 * content (cbox a b)"  by simp
moreover
have eq: "(∑K∈𝒟. content (K ∩ {x. x ∙ i ≤ b ∙ i}) /
(interval_upperbound (K ∩ {x. x ∙ i ≤ b ∙ i}) ∙ i - interval_lowerbound (K ∩ {x. x ∙ i ≤ b ∙ i}) ∙ i))
= (∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))"
(is "sum ?f _ = sum ?g _")
proof (rule sum.cong [OF refl])
fix K assume "K ∈ 𝒟"
then have "x ∙ i ≤ b ∙ i" if "x ∈ K" for x
by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
then have "K ∩ {x. x ∙ i ≤ b ∙ i} = K"
by blast
then show "?f K = ?g K"
by simp
qed
ultimately show ?thesis
using lec c eq by auto
qed
next
case False
have prod_if: "(∏k∈Basis ∩ - {i}. f k) = (∏k∈Basis. f k) / f i" if "f i ≠ (0::real)" for f
using that mk_disjoint_insert [OF i]
by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf mult.commute order_refl prod.insert subset_Compl_singleton)
have abc: "a ∙ i < c" "c < b ∙ i"
using False assms by auto
then have "(∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K)
≤ content(cbox a b') / (c - a ∙ i)"
"(∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)
≤ content(cbox a' b) / (b ∙ i - c)"
using lec gec by (simp_all add: divide_simps mult.commute)
moreover
have "(∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))
≤ (∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K) +
(∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)"
(is "?lhs ≤ ?rhs")
proof -
have "?lhs ≤
(∑K∈𝒟. ((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K +
((λK. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)"
(is "sum ?f _ ≤ sum ?g _")
proof (rule sum_mono)
fix K assume "K ∈ 𝒟"
then obtain u v where uv: "K = cbox u v"
using div by blast
obtain u' v' where uv': "cbox u v ∩ {x. x ∙ i ≤ c} = cbox u v'"
"cbox u v ∩ {x. c ≤ x ∙ i} = cbox u' v"
"⋀k. k ∈ Basis ⟹ u' ∙ k = (if k = i then max (u ∙ i) c else u ∙ k)"
"⋀k. k ∈ Basis ⟹ v' ∙ k = (if k = i then min (v ∙ i) c else v ∙ k)"
using i by (auto simp: interval_split)
have *: "⟦content (cbox u v') = 0; content (cbox u' v) = 0⟧ ⟹ content (cbox u v) = 0"
"content (cbox u' v) ≠ 0 ⟹ content (cbox u v) ≠ 0"
"content (cbox u v') ≠ 0 ⟹ content (cbox u v) ≠ 0"
using i uv uv' by (auto simp: content_eq_0 le_max_iff_disj min_le_iff_disj split: if_split_asm intro: order_trans)
show "?f K ≤ ?g K"
using i uv uv' apply (clarsimp simp add: lemma0 * intro!: prod_nonneg)
by (metis content_eq_0 le_less_linear order.strict_implies_order)
qed
also have "... = ?rhs"
finally show ?thesis .
qed
moreover have "content (cbox a b') / (c - a ∙ i) = content (cbox a b) / (b ∙ i - a ∙ i)"
using i abc
apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff)
apply (auto simp: if_distrib if_distrib [of "λf. f x" for x] prod.If_cases [of Basis "λx. x = i", simplified] prod_if field_simps)
done
moreover have "content (cbox a' b) / (b ∙ i - c) = content (cbox a b) / (b ∙ i - a ∙ i)"
using i abc
apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff)
apply (auto simp: if_distrib prod.If_cases [of Basis "λx. x = i", simplified] prod_if field_simps)
done
ultimately
have "(∑K∈𝒟. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))
≤ 2 * content (cbox a b) / (b ∙ i - a ∙ i)"
by linarith
then show ?thesis
using abc by (simp add: divide_simps mult.commute)
qed
qed

proposition bounded_equiintegral_over_thin_tagged_partial_division:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f ∈ F" and "0 < ε"
and norm_f: "⋀h x. ⟦h ∈ F; x ∈ cbox a b⟧ ⟹ norm(h x) ≤ norm(f x)"
obtains γ where "gauge γ"
"⋀c i S h. ⟦c ∈ cbox a b; i ∈ Basis; S tagged_partial_division_of cbox a b;
γ fine S; h ∈ F; ⋀x K. (x,K) ∈ S ⟹ (K ∩ {x. x ∙ i = c ∙ i} ≠ {})⟧
⟹ (∑(x,K) ∈ S. norm (integral K h)) < ε"
proof (cases "content(cbox a b) = 0")
case True
show ?thesis
proof
show "gauge (λx. ball x 1)"
show "(∑(x,K) ∈ S. norm (integral K h)) < ε"
if "S tagged_partial_division_of cbox a b" "(λx. ball x 1) fine S" for S and h:: "'a ⇒ 'b"
proof -
have "(∑(x,K) ∈ S. norm (integral K h)) = 0"
using that True content_0_subset
by (fastforce simp: tagged_partial_division_of_def intro: sum.neutral)
with ‹0 < ε› show ?thesis
by simp
qed
qed
next
case False
then have contab_gt0:  "content(cbox a b) > 0"
then have a_less_b: "⋀i. i ∈ Basis ⟹ a∙i < b∙i"
by (auto simp: content_pos_lt_eq)
obtain γ0 where "gauge γ0"
and γ0: "⋀S h. ⟦S tagged_partial_division_of cbox a b; γ0 fine S; h ∈ F⟧
⟹ (∑(x,K) ∈ S. norm (content K *⇩R h x - integral K h)) < ε/2"
proof -
obtain γ where "gauge γ"
and γ: "⋀f 𝒟. ⟦f ∈ F; 𝒟 tagged_division_of cbox a b; γ fine 𝒟⟧
⟹ norm ((∑(x,K) ∈ 𝒟. content K *⇩R f x) - integral (cbox a b) f)
< ε/(5 * (Suc DIM('b)))"
proof -
have e5: "ε/(5 * (Suc DIM('b))) > 0"
using ‹ε > 0› by auto
then show ?thesis
using F that by (auto simp: equiintegrable_on_def)
qed
show ?thesis
proof
show "gauge γ"
by (rule ‹gauge γ›)
show "(∑(x,K) ∈ S. norm (content K *⇩R h x - integral K h)) < ε/2"
if "S tagged_partial_division_of cbox a b" "γ fine S" "h ∈ F" for S h
proof -
have "(∑(x,K) ∈ S. norm (content K *⇩R h x - integral K h)) ≤ 2 * real DIM('b) * (ε/(5 * Suc DIM('b)))"
proof (rule Henstock_lemma_part2 [of h a b])
show "h integrable_on cbox a b"
using that F equiintegrable_on_def by metis
show "gauge γ"
by (rule ‹gauge γ›)
qed (use that ‹ε > 0› γ in auto)
also have "... < ε/2"
using ‹ε > 0› by (simp add: divide_simps)
finally show ?thesis .
qed
qed
qed
define γ where "γ ≡ λx. γ0 x ∩
ball x ((ε/8 / (norm(f x) + 1)) * (INF m:Basis. b ∙ m - a ∙ m) / content(cbox a b))"
have "gauge (λx. ball x
(ε * (INF m:Basis. b ∙ m - a ∙ m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
using ‹0 < content (cbox a b)› ‹0 < ε› a_less_b
apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral)
done
then have "gauge γ"
unfolding γ_def using ‹gauge γ0› gauge_Int by auto
moreover
have "(∑(x,K) ∈ S. norm (integral K h)) < ε"
if "c ∈ cbox a b" "i ∈ Basis" and S: "S tagged_partial_division_of cbox a b"
and "γ fine S" "h ∈ F" and ne: "⋀x K. (x,K) ∈ S ⟹ K ∩ {x. x ∙ i = c ∙ i} ≠ {}" for c i S h
proof -
have "cbox c b ⊆ cbox a b"
by (meson mem_box(2) order_refl subset_box(1) that(1))
have "finite S"
using S by blast
have "γ0 fine S" and fineS:
"(λx. ball x (ε * (INF m:Basis. b ∙ m - a ∙ m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
using ‹γ fine S› by (auto simp: γ_def fine_Int)
then have "(∑(x,K) ∈ S. norm (content K *⇩R h x - integral K h)) < ε/2"
by (intro γ0 that fineS)
moreover have "(∑(x,K) ∈ S. norm (integral K h) - norm (content K *⇩R h x - integral K h)) ≤ ε/2"
proof -
have "(∑(x,K) ∈ S. norm (integral K h) - norm (content K *⇩R h x - integral K h))
≤ (∑(x,K) ∈ S. norm (content K *⇩R h x))"
proof (clarify intro!: sum_mono)
fix x K
assume xK: "(x,K) ∈ S"
have "norm (integral K h) - norm (content K *⇩R h x - integral K h) ≤ norm (integral K h - (integral K h - content K *⇩R h x))"
by (metis norm_minus_commute norm_triangle_ineq2)
also have "... ≤ norm (content K *⇩R h x)"
by simp
finally show "norm (integral K h) - norm (content K *⇩R h x - integral K h) ≤ norm (content K *⇩R h x)" .
qed
also have "... ≤ (∑(x,K) ∈ S. ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) *
content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))"
proof (clarify intro!: sum_mono)
fix x K
assume xK: "(x,K) ∈ S"
then have x: "x ∈ cbox a b"
using S unfolding tagged_partial_division_of_def by (meson subset_iff)
let ?Δ = "interval_upperbound K ∙ i - interval_lowerbound K ∙ i"
show "norm (content K *⇩R h x) ≤ ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) * content K / ?Δ"
proof (cases "content K = 0")
case True
then show ?thesis by simp
next
case False
then have Kgt0: "content K > 0"
using zero_less_measure_iff by blast
moreover
obtain u v where uv: "K = cbox u v"
using S ‹(x,K) ∈ S› by blast
then have u_less_v: "⋀i. i ∈ Basis ⟹ u ∙ i < v ∙ i"
using content_pos_lt_eq uv Kgt0 by blast
then have dist_uv: "dist u v > 0"
using that by auto
ultimately have "norm (h x) ≤ (ε * (b ∙ i - a ∙ i)) / (4 * content (cbox a b) * ?Δ)"
proof -
have "dist x u < ε * (INF m:Basis. b ∙ m - a ∙ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
"dist x v < ε * (INF m:Basis. b ∙ m - a ∙ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
using fineS u_less_v uv xK
by (force simp: fine_def mem_box field_simps dest!: bspec)+
moreover have "ε * (INF m:Basis. b ∙ m - a ∙ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
≤ ε * (b ∙ i - a ∙ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
apply (intro mult_left_mono divide_right_mono)
using ‹i ∈ Basis› ‹0 < ε› apply (auto simp: intro!: cInf_le_finite)
done
ultimately
have "dist x u < ε * (b ∙ i - a ∙ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
"dist x v < ε * (b ∙ i - a ∙ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
by linarith+
then have duv: "dist u v < ε * (b ∙ i - a ∙ i) / (4 * (norm (f x) + 1) * content (cbox a b))"
using dist_triangle_half_r by blast
have uvi: "¦v ∙ i - u ∙ i¦ ≤ norm (v - u)"
by (metis inner_commute inner_diff_right ‹i ∈ Basis› Basis_le_norm)
have "norm (h x) ≤ norm (f x)"
using x that by (auto simp: norm_f)
also have "... < (norm (f x) + 1)"
by simp
also have "... < ε * (b ∙ i - a ∙ i) / dist u v / (4 * content (cbox a b))"
using duv dist_uv contab_gt0
apply (simp add: divide_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm)
by (meson add_nonneg_nonneg linorder_not_le measure_nonneg mult_nonneg_nonneg norm_ge_zero zero_le_numeral)
also have "... = ε * (b ∙ i - a ∙ i) / norm (v - u) / (4 * content (cbox a b))"
also have "... ≤ ε * (b ∙ i - a ∙ i) / ¦v ∙ i - u ∙ i¦ / (4 * content (cbox a b))"
apply (intro mult_right_mono divide_left_mono divide_right_mono uvi)
using ‹0 < ε› a_less_b [OF ‹i ∈ Basis›] u_less_v [OF ‹i ∈ Basis›] contab_gt0
by (auto simp: less_eq_real_def zero_less_mult_iff that)
also have "... = ε * (b ∙ i - a ∙ i)
/ (4 * content (cbox a b) * ?Δ)"
using uv False that(2) u_less_v by fastforce
finally show ?thesis by simp
qed
with Kgt0 have "norm (content K *⇩R h x) ≤ content K * ((ε/4 * (b ∙ i - a ∙ i) / content (cbox a b)) / ?Δ)"
using mult_left_mono by fastforce
also have "... = ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) *
content K / ?Δ"
finally show ?thesis .
qed
qed
also have "... = (∑K∈snd ` S. ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) * content K
/ (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))"
apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]])
done
also have "... = ε/2 * ((b ∙ i - a ∙ i) / (2 * content (cbox a b)) * (∑K∈snd ` S. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)))"
also have "... ≤ (ε/2) * 1"
proof (rule mult_left_mono)
have "(b ∙ i - a ∙ i) * (∑K∈snd ` S. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))
≤ 2 * content (cbox a b)"
proof (rule sum_content_area_over_thin_division)
show "snd ` S division_of ⋃(snd ` S)"
by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
show "UNION S snd ⊆ cbox a b"
using S by force
show "a ∙ i ≤ c ∙ i" "c ∙ i ≤ b ∙ i"
using mem_box(2) that by blast+
qed (use that in auto)
then show "(b ∙ i - a ∙ i) / (2 * content (cbox a b)) * (∑K∈snd ` S. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i)) ≤ 1"
qed (use ‹0 < ε› in auto)
finally show ?thesis by simp
qed
then have "(∑(x,K) ∈ S. norm (integral K h)) - (∑(x,K) ∈ S. norm (content K *⇩R h x - integral K h)) ≤ ε/2"
ultimately show "(∑(x,K) ∈ S. norm (integral K h)) < ε"
by linarith
qed
ultimately show ?thesis using that by auto
qed

proposition equiintegrable_halfspace_restrictions_le:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f ∈ F"
and norm_f: "⋀h x. ⟦h ∈ F; x ∈ cbox a b⟧ ⟹ norm(h x) ≤ norm(f x)"
shows "(⋃i ∈ Basis. ⋃c. ⋃h ∈ F. {(λx. if x ∙ i ≤ c then h x else 0)})
equiintegrable_on cbox a b"
proof (cases "content(cbox a b) = 0")
case True
then show ?thesis by simp
next
case False
then have "content(cbox a b) > 0"
using zero_less_measure_iff by blast
then have "a ∙ i < b ∙ i" if "i ∈ Basis" for i
using content_pos_lt_eq that by blast
have int_F: "f integrable_on cbox a b" if "f ∈ F" for f
using F that by (simp add: equiintegrable_on_def)
let ?CI = "λK h x. content K *⇩R h x - integral K h"
show ?thesis
unfolding equiintegrable_on_def
proof (intro conjI; clarify)
show int_lec: "⟦i ∈ Basis; h ∈ F⟧ ⟹ (λx. if x ∙ i ≤ c then h x else 0) integrable_on cbox a b" for i c h
using integrable_restrict_Int [of "{x. x ∙ i ≤ c}" h]
apply (auto simp: interval_split Int_commute mem_box intro!: integrable_on_subcbox int_F)
by (metis (full_types, hide_lams) min.bounded_iff)
show "∃γ. gauge γ ∧
(∀f T. f ∈ (⋃i∈Basis. ⋃c. ⋃h∈F. {λx. if x ∙ i ≤ c then h x else 0}) ∧
T tagged_division_of cbox a b ∧ γ fine T ⟶
norm ((∑(x,K) ∈ T. content K *⇩R f x) - integral (cbox a b) f) < ε)"
if "ε > 0" for ε
proof -
obtain γ0 where "gauge γ0" and γ0:
"⋀c i S h. ⟦c ∈ cbox a b; i ∈ Basis; S tagged_partial_division_of cbox a b;
γ0 fine S; h ∈ F; ⋀x K. (x,K) ∈ S ⟹ (K ∩ {x. x ∙ i = c ∙ i} ≠ {})⟧
⟹ (∑(x,K) ∈ S. norm (integral K h)) < ε/12"
apply (rule bounded_equiintegral_over_thin_tagged_partial_division [OF F f, of ‹ε/12›])
using ‹ε > 0› by (auto simp: norm_f)
obtain γ1 where "gauge γ1"
and γ1: "⋀h T. ⟦h ∈ F; T tagged_division_of cbox a b; γ1 fine T⟧
⟹ norm ((∑(x,K) ∈ T. content K *⇩R h x) - integral (cbox a b) h)
< ε/(7 * (Suc DIM('b)))"
proof -
have e5: "ε/(7 * (Suc DIM('b))) > 0"
using ‹ε > 0› by auto
then show ?thesis
using F that by (auto simp: equiintegrable_on_def)
qed
have h_less3: "(∑(x,K) ∈ T. norm (?CI K h x)) < ε/3"
if "T tagged_partial_division_of cbox a b" "γ1 fine T" "h ∈ F" for T h
proof -
have "(∑(x,K) ∈ T. norm (?CI K h x)) ≤ 2 * real DIM('b) * (ε/(7 * Suc DIM('b)))"
proof (rule Henstock_lemma_part2 [of h a b])
show "h integrable_on cbox a b"
using that F equiintegrable_on_def by metis
show "gauge γ1"
by (rule ‹gauge γ1›)
qed (use that ‹ε > 0› γ1 in auto)
also have "... < ε/3"
using ‹ε > 0› by (simp add: divide_simps)
finally show ?thesis .
qed
have *: "norm ((∑(x,K) ∈ T. content K *⇩R f x) - integral (cbox a b) f) < ε"
if f: "f = (λx. if x ∙ i ≤ c then h x else 0)"
and T: "T tagged_division_of cbox a b"
and fine: "(λx. γ0 x ∩ γ1 x) fine T" and "i ∈ Basis" "h ∈ F" for f T i c h
proof (cases "a ∙ i ≤ c ∧ c ≤ b ∙ i")
case True
have "finite T"
using T by blast
define T' where "T' ≡ {(x,K) ∈ T. K ∩ {x. x ∙ i ≤ c} ≠ {}}"
then have "T' ⊆ T"
by auto
then have "finite T'"
using ‹finite T› infinite_super by blast
have T'_tagged: "T' tagged_partial_division_of cbox a b"
by (meson T ‹T' ⊆ T› tagged_division_of_def tagged_partial_division_subset)
have fine': "γ0 fine T'" "γ1 fine T'"
using ‹T' ⊆ T› fine_Int fine_subset fine by blast+
have int_KK': "(∑(x,K) ∈ T. integral K f) = (∑(x,K) ∈ T'. integral K f)"
apply (rule sum.mono_neutral_right [OF ‹finite T› ‹T' ⊆ T›])
using f ‹finite T› ‹T' ⊆ T›
using integral_restrict_Int [of _ "{x. x ∙ i ≤ c}" h]
apply (auto simp: T'_def Int_commute)
done
have "(∑(x,K) ∈ T. content K *⇩R f x) = (∑(x,K) ∈ T'. content K *⇩R f x)"
apply (rule sum.mono_neutral_right [OF ‹finite T› ‹T' ⊆ T›])
using T f ‹finite T› ‹T' ⊆ T› apply (force simp: T'_def)
done
moreover have "norm ((∑(x,K) ∈ T'. content K *⇩R f x) - integral (cbox a b) f) < ε"
proof -
have *: "norm y < ε" if "norm x < ε/3" "norm(x - y) ≤ 2 * ε/3" for x y::'b
proof -
have "norm y ≤ norm x + norm(x - y)"
by (metis norm_minus_commute norm_triangle_sub)
also have "… < ε/3 + 2*ε/3"
using that by linarith
also have "... = ε"
by simp
finally show ?thesis .
qed
have "norm (∑(x,K) ∈ T'. ?CI K h x)
≤ (∑(x,K) ∈ T'. norm (?CI K h x))"
also have "... < ε/3"
by (intro h_less3 T'_tagged fine' that)
finally have "norm (∑(x,K) ∈ T'. ?CI K h x) < ε/3" .
moreover have "integral (cbox a b) f = (∑(x,K) ∈ T. integral K f)"
using int_lec that by (auto simp: integral_combine_tagged_division_topdown)
moreover have "norm (∑(x,K) ∈ T'. ?CI K h x - ?CI K f x)
≤ 2*ε/3"
proof -
define T'' where "T'' ≡ {(x,K) ∈ T'. ~ (K ⊆ {x. x ∙ i ≤ c})}"
then have "T'' ⊆ T'"
by auto
then have "finite T''"
using ‹finite T'› infinite_super by blast
have T''_tagged: "T'' tagged_partial_division_of cbox a b"
using T'_tagged ‹T'' ⊆ T'› tagged_partial_division_subset by blast
have fine'': "γ0 fine T''" "γ1 fine T''"
using ‹T'' ⊆ T'› fine' by (blast intro: fine_subset)+
have "(∑(x,K) ∈ T'. ?CI K h x - ?CI K f x)
= (∑(x,K) ∈ T''. ?CI K h x - ?CI K f x)"
proof (clarify intro!: sum.mono_neutral_right [OF ‹finite T'› ‹T'' ⊆ T'›])
fix x K
assume "(x,K) ∈ T'" "(x,K) ∉ T''"
then have "x ∈ K" "x ∙ i ≤ c" "{x. x ∙ i ≤ c} ∩ K = K"
using T''_def T'_tagged by blast+
then show "?CI K h x - ?CI K f x = 0"
using integral_restrict_Int [of _ "{x. x ∙ i ≤ c}" h] by (auto simp: f)
qed
moreover have "norm (∑(x,K) ∈ T''. ?CI K h x - ?CI K f x) ≤ 2*ε/3"
proof -
define A where "A ≡ {(x,K) ∈ T''. x ∙ i ≤ c}"
define B where "B ≡ {(x,K) ∈ T''. x ∙ i > c}"
then have "A ⊆ T''" "B ⊆ T''" and disj: "A ∩ B = {}" and T''_eq: "T'' = A ∪ B"
by (auto simp: A_def B_def)
then have "finite A" "finite B"
using ‹finite T''›  by (auto intro: finite_subset)
have A_tagged: "A tagged_partial_division_of cbox a b"
using T''_tagged ‹A ⊆ T''› tagged_partial_division_subset by blast
have fineA: "γ0 fine A" "γ1 fine A"
using ‹A ⊆ T''› fine'' by (blast intro: fine_subset)+
have B_tagged: "B tagged_partial_division_of cbox a b"
using T''_tagged ‹B ⊆ T''› tagged_partial_division_subset by blast
have fineB: "γ0 fine B" "γ1 fine B"
using ‹B ⊆ T''› fine'' by (blast intro: fine_subset)+
have "norm (∑(x,K) ∈ T''. ?CI K h x - ?CI K f x)
≤ (∑(x,K) ∈ T''. norm (?CI K h x - ?CI K f x))"
also have "... = (∑(x,K) ∈ A. norm (?CI K h x - ?CI K f x)) +
(∑(x,K) ∈ B. norm (?CI K h x - ?CI K f x))"
by (simp add: sum.union_disjoint T''_eq disj ‹finite A› ‹finite B›)
also have "... = (∑(x,K) ∈ A. norm (integral K h - integral K f)) +
(∑(x,K) ∈ B. norm (?CI K h x + integral K f))"
by (auto simp: A_def B_def f norm_minus_commute intro!: sum.cong arg_cong2 [where f= "op+"])
also have "... ≤ (∑(x,K)∈A. norm (integral K h)) +
(∑(x,K)∈(λ(x,K). (x,K ∩ {x. x ∙ i ≤ c})) ` A. norm (integral K h))
+ ((∑(x,K)∈B. norm (?CI K h x)) +
(∑(x,K)∈B. norm (integral K h)) +
(∑(x,K)∈(λ(x,K). (x,K ∩ {x. c ≤ x ∙ i})) ` B. norm (integral K h)))"
show "(∑(x,K)∈A. norm (integral K h - integral K f))
≤ (∑(x,K)∈A. norm (integral K h)) +
(∑(x,K)∈(λ(x,K). (x,K ∩ {x. x ∙ i ≤ c})) ` A.
norm (integral K h))"
proof (subst sum.reindex_nontrivial [OF ‹finite A›], clarsimp)
fix x K L
assume "(x,K) ∈ A" "(x,L) ∈ A"
and int_ne0: "integral (L ∩ {x. x ∙ i ≤ c}) h ≠ 0"
and eq: "K ∩ {x. x ∙ i ≤ c} = L ∩ {x. x ∙ i ≤ c}"
have False if "K ≠ L"
proof -
obtain u v where uv: "L = cbox u v"
using T'_tagged ‹(x, L) ∈ A› ‹A ⊆ T''› ‹T'' ⊆ T'› by blast
have "A tagged_division_of UNION A snd"
using A_tagged tagged_partial_division_of_Union_self by auto
then have "interior (K ∩ {x. x ∙ i ≤ c}) = {}"
apply (rule tagged_division_split_left_inj [OF _ ‹(x,K) ∈ A› ‹(x,L) ∈ A›])
using that eq ‹i ∈ Basis› by auto
then show False
using interval_split [OF ‹i ∈ Basis›] int_ne0 content_eq_0_interior eq uv by fastforce
qed
then show "K = L" by blast
next
show "(∑(x,K) ∈ A. norm (integral K h - integral K f))
≤ (∑(x,K) ∈ A. norm (integral K h)) +
sum ((λ(x,K). norm (integral K h)) ∘ (λ(x,K). (x,K ∩ {x. x ∙ i ≤ c}))) A"
using integral_restrict_Int [of _ "{x. x ∙ i ≤ c}" h] f
by (auto simp: Int_commute A_def [symmetric] sum.distrib [symmetric] intro!: sum_mono norm_triangle_ineq4)
qed
next
show "(∑(x,K)∈B. norm (?CI K h x + integral K f))
≤ (∑(x,K)∈B. norm (?CI K h x)) + (∑(x,K)∈B. norm (integral K h)) +
(∑(x,K)∈(λ(x,K). (x,K ∩ {x. c ≤ x ∙ i})) ` B. norm (integral K h))"
proof (subst sum.reindex_nontrivial [OF ‹finite B›], clarsimp)
fix x K L
assume "(x,K) ∈ B" "(x,L) ∈ B"
and int_ne0: "integral (L ∩ {x. c ≤ x ∙ i}) h ≠ 0"
and eq: "K ∩ {x. c ≤ x ∙ i} = L ∩ {x. c ≤ x ∙ i}"
have False if "K ≠ L"
proof -
obtain u v where uv: "L = cbox u v"
using T'_tagged ‹(x, L) ∈ B› ‹B ⊆ T''› ‹T'' ⊆ T'› by blast
have "B tagged_division_of UNION B snd"
using B_tagged tagged_partial_division_of_Union_self by auto
then have "interior (K ∩ {x. c ≤ x ∙ i}) = {}"
apply (rule tagged_division_split_right_inj [OF _ ‹(x,K) ∈ B› ‹(x,L) ∈ B›])
using that eq ‹i ∈ Basis› by auto
then show False
using interval_split [OF ‹i ∈ Basis›] int_ne0
content_eq_0_interior eq uv by fastforce
qed
then show "K = L" by blast
next
show "(∑(x,K) ∈ B. norm (?CI K h x + integral K f))
≤ (∑(x,K) ∈ B. norm (?CI K h x)) +
(∑(x,K) ∈ B. norm (integral K h)) + sum ((λ(x,K). norm (integral K h)) ∘ (λ(x,K). (x,K ∩ {x. c ≤ x ∙ i}))) B"
proof (clarsimp simp: B_def [symmetric] sum.distrib [symmetric] intro!: sum_mono)
fix x K
assume "(x,K) ∈ B"
have *: "i = i1 + i2 ⟹ norm(c + i1) ≤ norm c + norm i + norm(i2)"
for i::'b and c i1 i2
obtain u v where uv: "K = cbox u v"
using T'_tagged ‹(x,K) ∈ B› ‹B ⊆ T''› ‹T'' ⊆ T'› by blast
have "h integrable_on cbox a b"
by (simp add: int_F ‹h ∈ F›)
then have huv: "h integrable_on cbox u v"
apply (rule integrable_on_subcbox)
using B_tagged ‹(x,K) ∈ B› uv by blast
have "integral K h = integral K f + integral (K ∩ {x. c ≤ x ∙ i}) h"
using integral_restrict_Int [of _ "{x. x ∙ i ≤ c}" h] f uv ‹i ∈ Basis›
by (simp add: Int_commute integral_split [OF huv ‹i ∈ Basis›])
then show "norm (?CI K h x + integral K f)
≤ norm (?CI K h x) + norm (integral K h) + norm (integral (K ∩ {x. c ≤ x ∙ i}) h)"
by (rule *)
qed
qed
qed
also have "... ≤ 2*ε/3"
proof -
have overlap: "K ∩ {x. x ∙ i = c} ≠ {}" if "(x,K) ∈ T''" for x K
proof -
obtain y y' where y: "y' ∈ K" "c < y' ∙ i" "y ∈ K" "y ∙ i ≤ c"
using that  T''_def T'_def ‹(x,K) ∈ T''› by fastforce
obtain u v where uv: "K = cbox u v"
using T''_tagged ‹(x,K) ∈ T''› by blast
then have "connected K"
then have "(∃z ∈ K. z ∙ i = c)"
using y connected_ivt_component by fastforce
then show ?thesis
by fastforce
qed
have **: "⟦x < ε/12; y < ε/12; z ≤ ε/2⟧ ⟹ x + y + z ≤ 2 * ε/3" for x y z
by auto
show ?thesis
proof (rule **)
have cb_ab: "(∑j ∈ Basis. if j = i then c *⇩R i else (a ∙ j) *⇩R j) ∈ cbox a b"
using ‹i ∈ Basis› True ‹⋀i. i ∈ Basis ⟹ a ∙ i < b ∙ i›
apply (subst sum_if_inner | force)+
done
show "(∑(x,K) ∈ A. norm (integral K h)) < ε/12"
apply (rule γ0 [OF cb_ab ‹i ∈ Basis› A_tagged fineA(1) ‹h ∈ F›])
using ‹i ∈ Basis› ‹A ⊆ T''› overlap
apply (subst sum_if_inner | force)+
done
have 1: "(λ(x,K). (x,K ∩ {x. x ∙ i ≤ c})) ` A tagged_partial_division_of cbox a b"
using ‹finite A› ‹i ∈ Basis›
apply (auto simp: tagged_partial_division_of_def)
using A_tagged apply (auto simp: A_def)
using interval_split(1) by blast
have 2: "γ0 fine (λ(x,K). (x,K ∩ {x. x ∙ i ≤ c})) ` A"
using fineA(1) fine_def by fastforce
show "(∑(x,K) ∈ (λ(x,K). (x,K ∩ {x. x ∙ i ≤ c})) ` A. norm (integral K h)) < ε/12"
apply (rule γ0 [OF cb_ab ‹i ∈ Basis› 1 2 ‹h ∈ F›])
using ‹i ∈ Basis› apply (subst sum_if_inner | force)+
using overlap apply (auto simp: A_def)
done
have *: "⟦x < ε/3; y < ε/12; z < ε/12⟧ ⟹ x + y + z ≤ ε/2" for x y z
by auto
show "(∑(x,K) ∈ B. norm (?CI K h x)) +
(∑(x,K) ∈ B. norm (integral K h)) +
(∑(x,K) ∈ (λ(x,K). (x,K ∩ {x. c ≤ x ∙ i})) ` B. norm (integral K h))
≤ ε/2"
proof (rule *)
show "(∑(x,K) ∈ B. norm (?CI K h x)) < ε/3"
by (intro h_less3 B_tagged fineB that)
show "(∑(x,K) ∈ B. norm (integral K h)) < ε/12"
apply (rule γ0 [OF cb_ab ‹i ∈ Basis› B_tagged fineB(1) ‹h ∈ F›])
using ‹i ∈ Basis› ‹B ⊆ T''› overlap by (subst sum_if_inner | force)+
have 1: "(λ(x,K). (x,K ∩ {x. c ≤ x ∙ i})) ` B tagged_partial_division_of cbox a b"
using ‹finite B› ‹i ∈ Basis›
apply (auto simp: tagged_partial_division_of_def)
using B_tagged apply (auto simp: B_def)
using interval_split(2) by blast
have 2: "γ0 fine (λ(x,K). (x,K ∩ {x. c ≤ x ∙ i})) ` B"
using fineB(1) fine_def by fastforce
show "(∑(x,K) ∈ (λ(x,K). (x,K ∩ {x. c ≤ x ∙ i})) ` B. norm (integral K h)) < ε/12"
apply (rule γ0 [OF cb_ab ‹i ∈ Basis› 1 2 ‹h ∈ F›])
using ‹i ∈ Basis› apply (subst sum_if_inner | force)+
using overlap apply (auto simp: B_def)
done
qed
qed
qed
finally show ?thesis .
qed
ultimately show ?thesis by metis
qed
ultimately show ?thesis
by (simp add: sum_subtractf [symmetric] int_KK' *)
qed
ultimately show ?thesis by metis
next
case False
then consider "c < a ∙ i" | "b ∙ i < c"
by auto
then show ?thesis
proof cases
case 1
then have f0: "f x = 0" if "x ∈ cbox a b" for x
using that f ‹i ∈ Basis› mem_box(2) by force
then have int_f0: "integral (cbox a b) f = 0"
have f0_tag: "f x = 0" if "(x,K) ∈ T" for x K
using T f0 that by (force simp: tagged_division_of_def)
then have "(∑(x,K) ∈ T. content K *⇩R f x) = 0"
by (metis (mono_tags, lifting) real_vector.scale_eq_0_iff split_conv sum.neutral surj_pair)
then show ?thesis
using ‹0 < ε› by (simp add: int_f0)
next
case 2
then have fh: "f x = h x" if "x ∈ cbox a b" for x
using that f ‹i ∈ Basis› mem_box(2) by force
then have int_f: "integral (cbox a b) f = integral (cbox a b) h"
using integral_cong by blast
have fh_tag: "f x = h x" if "(x,K) ∈ T" for x K
using T fh that by (force simp: tagged_division_of_def)
then have "(∑(x,K) ∈ T. content K *⇩R f x) = (∑(x,K) ∈ T. content K *⇩R h x)"
by (metis (mono_tags, lifting) split_cong sum.cong)
with ‹0 < ε› show ?thesis
apply (rule less_trans [OF γ1])
using that fine_Int apply (force simp: divide_simps)+
done
qed
qed
have  "gauge (λx. γ0 x ∩ γ1 x)"
by (simp add: ‹gauge γ0› ‹gauge γ1› gauge_Int)
then show ?thesis
by (auto intro: *)
qed
qed
qed

corollary equiintegrable_halfspace_restrictions_ge:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f ∈ F"
and norm_f: "⋀h x. ⟦h ∈ F; x ∈ cbox a b⟧ ⟹ norm(h x) ≤ norm(f x)"
shows "(⋃i ∈ Basis. ⋃c. ⋃h ∈ F. {(λx. if x ∙ i ≥ c then h x else 0)})
equiintegrable_on cbox a b"
proof -
have *: "(⋃i∈Basis. ⋃c. ⋃h∈(λf. f ∘ uminus) ` F. {λx. if x ∙ i ≤ c then h x else 0})
equiintegrable_on  cbox (- b) (- a)"
proof (rule equiintegrable_halfspace_restrictions_le)
show "(λf. f ∘ uminus) ` F equiintegrable_on cbox (- b) (- a)"
using F equiintegrable_reflect by blast
show "f ∘ uminus ∈ (λf. f ∘ uminus) ` F"
using f by auto
show "⋀h x. ⟦h ∈ (λf. f ∘ uminus) ` F; x ∈ cbox (- b) (- a)⟧ ⟹ norm (h x) ≤ norm ((f ∘ uminus) x)"
using f apply (clarsimp simp:)
by (metis add.inverse_inverse image_eqI norm_f uminus_interval_vector)
qed
have eq: "(λf. f ∘ uminus) `
(⋃i∈Basis. ⋃c. ⋃h∈F. {λx. if x ∙ i ≤ c then (h ∘ uminus) x else 0}) =
(⋃i∈Basis. ⋃c. ⋃h∈F. {λx. if c ≤ x ∙ i then h x else 0})"
apply (auto simp: o_def cong: if_cong)
using minus_le_iff apply fastforce
apply (rule_tac x="λx. if c ≤ (-x) ∙ i then h(-x) else 0" in image_eqI)
using le_minus_iff apply fastforce+
done
show ?thesis
using equiintegrable_reflect [OF *] by (auto simp: eq)
qed

proposition equiintegrable_closed_interval_restrictions:
fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes f: "f integrable_on cbox a b"
shows "(⋃c d. {(λx. if x ∈ cbox c d then f x else 0)}) equiintegrable_on cbox a b"
proof -
let ?g = "λB c d x. if ∀i∈B. c ∙ i ≤ x ∙ i ∧ x ∙ i ≤ d ∙ i then f x else 0"
have *: "insert f (⋃c d. {?g B c d}) equiintegrable_on cbox a b" if "B ⊆ Basis" for B
proof -
have "finite B"
using finite_Basis finite_subset ‹B ⊆ Basis› by blast
then show ?thesis using ‹B ⊆ Basis›
proof (induction B)
case empty
with f show ?case by auto
next
case (insert i B)
then have "i ∈ Basis"
by auto
have *: "norm (h x) ≤ norm (f x)"
if "h ∈ insert f (⋃c d. {?g B c d})" "x ∈ cbox a b" for h x
using that by auto
have "(⋃i∈Basis.
⋃ξ. ⋃h∈insert f (⋃i∈Basis. ⋃ψ. ⋃h∈insert f (⋃c d. {?g B c d}). {λx. if x ∙ i ≤ ψ then h x else 0}).
{λx. if ξ ≤ x ∙ i then h x else 0})
equiintegrable_on cbox a b"
proof (rule equiintegrable_halfspace_restrictions_ge [where f=f])
show "insert f (⋃i∈Basis. ⋃ξ. ⋃h∈insert f (⋃c d. {?g B c d}).
{λx. if x ∙ i ≤ ξ then h x else 0}) equiintegrable_on cbox a b"
apply (intro * f equiintegrable_on_insert equiintegrable_halfspace_restrictions_le [OF insert.IH insertI1])
using insert.prems apply auto
done
show"norm(h x) ≤ norm(f x)"
if "h ∈ insert f (⋃i∈Basis. ⋃ξ. ⋃h∈insert f (⋃c d. {?g B c d}). {λx. if x ∙ i ≤ ξ then h x else 0})"
"x ∈ cbox a b" for h x
using that by auto
qed auto
then have "insert f (⋃i∈Basis.
⋃ξ. ⋃h∈insert f (⋃i∈Basis. ⋃ψ. ⋃h∈insert f (⋃c d. {?g B c d}). {λx. if x ∙ i ≤ ψ then h x else 0}).
{λx. if ξ ≤ x ∙ i then h x else 0})
equiintegrable_on cbox a b"
by (blast intro: f equiintegrable_on_insert)
then show ?case
apply (rule equiintegrable_on_subset, clarify)
using ‹i ∈ Basis› apply simp
apply (drule_tac x=i in bspec, assumption)
apply (drule_tac x="c ∙ i" in spec, clarify)
apply (drule_tac x=i in bspec, assumption)
apply (drule_tac x="d ∙ i" in spec)
apply (drule_tac x=c in spec)
apply (drule_tac x=d in spec)
done
qed
qed
show ?thesis
by (rule equiintegrable_on_subset [OF * [OF subset_refl]]) (auto simp: mem_box)
qed

subsection‹Continuity of the indefinite integral›

proposition indefinite_integral_continuous:
fixes f :: "'a :: euclidean_space ⇒ 'b :: euclidean_space"
assumes int_f: "f integrable_on cbox a b"
and c: "c ∈ cbox a b" and d: "d ∈ cbox a b" "0 < ε"
obtains δ where "0 < δ"
"⋀c' d'. ⟦c' ∈ cbox a b; d' ∈ cbox a b; norm(c' - c) ≤ δ; norm(d' - d) ≤ δ⟧
⟹ norm(integral(cbox c' d') f - integral(cbox c d) f) < ε"
proof -
{ assume "∃c' d'. c' ∈ cbox a b ∧ d' ∈ cbox a b ∧ norm(c' - c) ≤ δ ∧ norm(d' - d) ≤ δ ∧
norm(integral(cbox c' d') f - integral(cbox c d) f) ≥ ε"
(is "∃c' d'. ?Φ c' d' δ") if "0 < δ" for δ
then have "∃c' d'. ?Φ c' d' (1 / Suc n)" for n
by simp
then obtain u v where "⋀n. ?Φ (u n) (v n) (1 / Suc n)"
by metis
then have u: "u n ∈ cbox a b" and norm_u: "norm(u n - c) ≤ 1 / Suc n"
and  v: "v n ∈ cbox a b" and norm_v: "norm(v n - d) ≤ 1 / Suc n"
and ε: "ε ≤ norm (integral (cbox (u n) (v n)) f - integral (cbox c d) f)" for n
by blast+
then have False
proof -
have uvn: "cbox (u n) (v n) ⊆ cbox a b" for n
by (meson u v mem_box(2) subset_box(1))
define S where "S ≡ ⋃i ∈ Basis. {x. x ∙ i = c ∙ i} ∪ {x. x ∙ i = d ∙ i}"
have "negligible S"
unfolding S_def by force
then have int_f': "(λx. if x ∈ S then 0 else f x) integrable_on cbox a b"
by (rule integrable_spike) (auto intro: assms)
have get_n: "∃n. ∀m≥n. x ∈ cbox (u m) (v m) ⟷ x ∈ cbox c d" if x: "x ∉ S" for x
proof -
define ε where "ε ≡ Min ((λi. min ¦x ∙ i - c ∙ i¦ ¦x ∙ i - d ∙ i¦) ` Basis)"
have "ε > 0"
using ‹x ∉ S› by (auto simp: S_def ε_def)
then obtain n where "n ≠ 0" and n: "1 / (real n) < ε"
by (metis inverse_eq_divide real_arch_inverse)
have emin: "ε ≤ min ¦x ∙ i - c ∙ i¦ ¦x ∙ i - d ∙ i¦" if "i ∈ Basis" for i
unfolding ε_def
apply (rule Min.coboundedI)
using that by force+
have "1 / real (Suc n) < ε"
using n ‹n ≠ 0› ‹ε > 0› by (simp add: field_simps)
have "x ∈ cbox (u m) (v m) ⟷ x ∈ cbox c d" if "m ≥ n" for m
proof -
have *: "⟦¦u - c¦ ≤ n; ¦v - d¦ ≤ n; N < ¦x - c¦; N < ¦x - d¦; n ≤ N⟧
⟹ u ≤ x ∧ x ≤ v ⟷ c ≤ x ∧ x ≤ d" for N n u v c d and x::real
by linarith
have "(u m ∙ i ≤ x ∙ i ∧ x ∙ i ≤ v m ∙ i) = (c ∙ i ≤ x ∙ i ∧ x ∙ i ≤ d ∙ i)"
if "i ∈ Basis" for i
proof (rule *)
show "¦u m ∙ i - c ∙ i¦ ≤ 1 / Suc m"
using norm_u [of m]
by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that)
show "¦v m ∙ i - d ∙ i¦ ≤ 1 / real (Suc m)"
using norm_v [of m]
by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that)
show "1/n < ¦x ∙ i - c ∙ i¦" "1/n < ¦x ∙ i - d ∙ i¦"
using n ‹n ≠ 0› emin [OF ‹i ∈ Basis›]
show "1 / real (Suc m) ≤ 1 / real n"
using ‹n ≠ 0› ‹m ≥ n› by (simp add: divide_simps)
qed
then show ?thesis by (simp add: mem_box)
qed
then show ?thesis by blast
qed
have 1: "range (λn x. if x ∈ cbox (u n) (v n) then if x ∈ S then 0 else f x else 0) equiintegrable_on cbox a b"
by (blast intro: equiintegrable_on_subset [OF equiintegrable_closed_interval_restrictions [OF int_f']])
have 2: "(λn. if x ∈ cbox (u n) (v n) then if x ∈ S then 0 else f x else 0)
⇢ (if x ∈ cbox c d then if x ∈ S then 0 else f x else 0)" for x
by (fastforce simp: dest: get_n intro: Lim_eventually eventually_sequentiallyI)
have [simp]: "cbox c d ∩ cbox a b = cbox c d"
using c d by (force simp: mem_box)
have [simp]: "cbox (u n) (v n) ∩ cbox a b = cbox (u n) (v n)" for n
using u v by (fastforce simp: mem_box intro: order.trans)
have "⋀y A. y ∈ A - S ⟹ f y = (λx. if x ∈ S then 0 else f x) y"
by simp
then have "⋀A. integral A (λx. if x ∈ S then 0 else f (x)) = integral A (λx. f (x))"
by (blast intro: integral_spike [OF ‹negligible S›])
moreover
obtain N where "dist (integral (cbox (u N) (v N)) (λx. if x ∈ S then 0 else f x))
(integral (cbox c d) (λx. if x ∈ S then 0 else f x)) < ε"
using equiintegrable_limit [OF 1 2] ‹0 < ε› by (force simp: integral_restrict_Int lim_sequentially)
ultimately have "dist (integral (cbox (u N) (v N)) f) (integral (cbox c d) f) < ε"
by simp
then show False
by (metis dist_norm not_le ε)
qed
}
then show ?thesis
by (meson not_le that)
qed

corollary indefinite_integral_uniformly_continuous:
fixes f :: "'a :: euclidean_space ⇒ 'b :: euclidean_space"
assumes "f integrable_on cbox a b"
shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (λy. integral (cbox (fst y) (snd y)) f)"
proof -
show ?thesis
proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff)
fix c d and ε::real
assume c: "c ∈ cbox a b" and d: "d ∈ cbox a b" and "0 < ε"
obtain δ where "0 < δ" and δ:
"⋀c' d'. ⟦c' ∈ cbox a b; d' ∈ cbox a b; norm(c' - c) ≤ δ; norm(d' - d) ≤ δ⟧
⟹ norm(integral(cbox c' d') f -
integral(cbox c d) f) < ε"
using indefinite_integral_continuous ‹0 < ε› assms c d by blast
show "∃δ > 0. ∀x' ∈ cbox (a, a) (b, b).
dist x' (c, d) < δ ⟶
dist (integral (cbox (fst x') (snd x')) f)
(integral (cbox c d) f)
< ε"
using ‹0 < δ›
by (force simp: dist_norm intro: δ order_trans [OF norm_fst_le] order_trans [OF norm_snd_le] less_imp_le)
qed auto
qed

corollary bounded_integrals_over_subintervals:
fixes f :: "'a :: euclidean_space ⇒ 'b :: euclidean_space"
assumes "f integrable_on cbox a b"
shows "bounded {integral (cbox c d) f |c d. cbox c d ⊆ cbox a b}"
proof -
have "bounded ((λy. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))"
(is "bounded ?I")
by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms])
then obtain B where "B > 0" and B: "⋀x. x ∈ ?I ⟹ norm x ≤ B"
by (auto simp: bounded_pos)
have "norm x ≤ B" if "x = integral (cbox c d) f" "cbox c d ⊆ cbox a b" for x c d
proof (cases "cbox c d = {}")
case True
with ‹0 < B› that show ?thesis by auto
next
case False
show ?thesis
apply (rule B)
using that ‹B > 0› False apply (clarsimp simp: image_def)
by (metis cbox_Pair_iff interval_subset_is_interval is_interval_cbox prod.sel)
qed
then show ?thesis
by (blast intro: boundedI)
qed

text‹An existence theorem for "improper" integrals.
Hake's theorem implies that if the integrals over subintervals have a limit, the integral exists.
We only need to assume that the integrals are bounded, and we get absolute integrability,
but we also need a (rather weak) bound assumption on the function.›

theorem absolutely_integrable_improper:
fixes f :: "'M::euclidean_space ⇒ 'N::euclidean_space"
assumes int_f: "⋀c d. cbox c d ⊆ box a b ⟹ f integrable_on cbox c d"
and bo: "bounded {integral (cbox c d) f |c d. cbox c d ⊆ box a b}"
and absi: "⋀i. i ∈ Basis
⟹ ∃g. g absolutely_integrable_on cbox a b ∧
((∀x ∈ cbox a b. f x ∙ i ≤ g x) ∨ (∀x ∈ cbox a b. f x ∙ i ≥ g x))"
shows "f absolutely_integrable_on cbox a b"
proof (cases "content(cbox a b) = 0")
case True
then show ?thesis
by auto
next
case False
then have pos: "content(cbox a b) > 0"
using zero_less_measure_iff by blast
show ?thesis
unfolding absolutely_integrable_componentwise_iff [where f = f]
proof
fix j::'N
assume "j ∈ Basis"
then obtain g where absint_g: "g absolutely_integrable_on cbox a b"
and g: "(∀x ∈ cbox a b. f x ∙ j ≤ g x) ∨ (∀x ∈ cbox a b. f x ∙ j ≥ g x)"
using absi by blast
have int_gab: "g integrable_on cbox a b"
using absint_g set_lebesgue_integral_eq_integral(1) by blast
have 1: "cbox (a + (b - a) /⇩R real (Suc n)) (b - (b - a) /⇩R real (Suc n)) ⊆ box a b" for n
apply (rule subset_box_imp)
using pos apply (auto simp: content_pos_lt_eq algebra_simps)
done
have 2: "cbox (a + (b - a) /⇩R real (Suc n)) (b - (b - a) /⇩R real (Suc n)) ⊆
cbox (a + (b - a) /⇩R real (Suc n + 1)) (b - (b - a) /⇩R real (Suc n + 1))" for n
apply (rule subset_box_imp)
using pos apply (simp add: content_pos_lt_eq algebra_simps)
apply (auto simp: field_simps)
done
have getN: "∃N::nat. ∀k. k ≥ N ⟶ x ∈ cbox (a + (b - a) /⇩R real k) (b - (b - a) /⇩R real k)"
if x: "x ∈ box a b" for x
proof -
let ?Δ = "(⋃i ∈ Basis. {((x - a) ∙ i) / ((b - a) ∙ i), (b - x) ∙ i / ((b - a) ∙ i)})"
obtain N where N: "real N > 1 / Inf ?Δ"
using reals_Archimedean2 by blast
moreover have Δ: "Inf ?Δ > 0"
using that by (auto simp: finite_less_Inf_iff mem_box algebra_simps divide_simps)
ultimately have "N > 0"
using of_nat_0_less_iff by fastforce
show ?thesis
proof (intro exI impI allI)
fix k assume "N ≤ k"
with ‹0 < N› have "k > 0"
by linarith
have xa_gt: "(x - a) ∙ i > ((b - a) ∙ i) / (real k)" if "i ∈ Basis" for i
proof -
have *: "Inf ?Δ ≤ ((x - a) ∙ i) / ((b - a) ∙ i)"
using that by (force intro: cInf_le_finite)
have "1 / Inf ?Δ ≥ ((b - a) ∙ i) / ((x - a) ∙ i)"
using le_imp_inverse_le [OF * Δ]
with N have "k > ((b - a) ∙ i) / ((x - a) ∙ i)"
using ‹N ≤ k› by linarith
with x that show ?thesis
by (auto simp: mem_box algebra_simps divide_simps)
qed
have bx_gt: "(b - x) ∙ i > ((b - a) ∙ i) / k" if "i ∈ Basis" for i
proof -
have *: "Inf ?Δ ≤ ((b - x) ∙ i) / ((b - a) ∙ i)"
using that by (force intro: cInf_le_finite)
have "1 / Inf ?Δ ≥ ((b - a) ∙ i) / ((b - x) ∙ i)"
using le_imp_inverse_le [OF * Δ]
with N have "k > ((b - a) ∙ i) / ((b - x) ∙ i)"
using ‹N ≤ k› by linarith
with x that show ?thesis
by (auto simp: mem_box algebra_simps divide_simps)
qed
show "x ∈ cbox (a + (b - a) /⇩R k) (b - (b - a) /⇩R k)"
using that Δ ‹k > 0›
by (auto simp: mem_box algebra_simps divide_inverse dest: xa_gt bx_gt)
qed
qed
obtain Bf where "Bf > 0" and Bf: "⋀c d. cbox c d ⊆ box a b ⟹ norm (integral (cbox c d) f) ≤ Bf"
using bo unfolding bounded_pos by blast
obtain Bg where "Bg > 0" and Bg:"⋀c d. cbox c d ⊆ cbox a b ⟹ ¦integral (cbox c d) g¦ ≤ Bg"
using bounded_integrals_over_subintervals [OF int_gab] unfolding bounded_pos real_norm_def by blast
show "(λx. f x ∙ j) absolutely_integrable_on cbox a b"
using g
proof     ―‹A lot of duplication in the two proofs›
assume fg [rule_format]: "∀x∈cbox a b. f x ∙ j ≤ g x"
have "(λx. (f x ∙ j)) = (λx. g x - (g x - (f x ∙ j)))"
by simp
moreover have "(λx. g x - (g x - (f x ∙ j))) integrable_on cbox a b"
proof (rule Henstock_Kurzweil_Integration.integrable_diff [OF int_gab])
let ?φ = "λk x. if x ∈ cbox (a + (b - a) /⇩R (Suc k)) (b - (b - a) /⇩R (Suc k))
then g x - f x ∙ j else 0"
have "(λx. g x - f x ∙ j) integrable_on box a b"
proof (rule monotone_convergence_increasing [of ?φ, THEN conjunct1])
have *: "cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k)) ∩ box a b
= cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))" for k
using box_subset_cbox "1" by fastforce
show "?φ k integrable_on box a b" for k
apply (simp add: integrable_restrict_Int integral_restrict_Int *)
apply (rule integrable_diff [OF integrable_on_subcbox [OF int_gab]])
using "*" box_subset_cbox apply blast
by (metis "1" int_f integrable_component of_nat_Suc)
have cb12: "cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))
⊆ cbox (a + (b - a) /⇩R (2 + real k)) (b - (b - a) /⇩R (2 + real k))" for k
using False content_eq_0
apply (fastforce simp: field_simps)
done
show "?φ k x ≤ ?φ (Suc k) x" if "x ∈ box a b" for k x
using cb12 box_subset_cbox that by (force simp: intro!: fg)
show "(λk. ?φ k x) ⇢ g x - f x ∙ j" if x: "x ∈ box a b" for x
proof (rule Lim_eventually)
obtain N::nat where N: "⋀k. k ≥ N ⟹ x ∈ cbox (a + (b - a) /⇩R real k) (b - (b - a) /⇩R real k)"
using getN [OF x] by blast
show "∀⇩F k in sequentially. ?φ k x = g x - f x ∙ j"
proof
fix k::nat assume "N ≤ k"
have "x ∈ cbox (a + (b - a) /⇩R (Suc k)) (b - (b - a) /⇩R (Suc k))"
by (metis ‹N ≤ k› le_Suc_eq N)
then show "?φ k x = g x - f x ∙ j"
by simp
qed
qed
have "¦integral (box a b)
(λx. if x ∈ cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))
then g x - f x ∙ j else 0)¦ ≤ Bg + Bf" for k
proof -
let ?I = "cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))"
have I_int [simp]: "?I ∩ box a b = ?I"
using 1 by (simp add: Int_absorb2)
have int_fI: "f integrable_on ?I"
apply (rule integrable_subinterval [OF int_f order_refl])
using "*" box_subset_cbox by blast
then have "(λx. f x ∙ j) integrable_on ?I"
moreover have "g integrable_on ?I"
apply (rule integrable_subinterval [OF int_gab])
using "*" box_subset_cbox by blast
moreover
have "¦integral ?I (λx. f x ∙ j)¦ ≤ norm (integral ?I f)"
by (simp add: Basis_le_norm int_fI ‹j ∈ Basis›)
with 1 I_int have "¦integral ?I (λx. f x ∙ j)¦ ≤ Bf"
by (blast intro: order_trans [OF _ Bf])
ultimately show ?thesis
using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
qed
then show "bounded (range (λk. integral (box a b) (?φ k)))"
apply (rule_tac x="Bg+Bf" in exI)
using ‹0 < Bf› ‹0 < Bg›  apply auto
done
qed
then show "(λx. g x - f x ∙ j) integrable_on cbox a b"
qed
ultimately have "(λx. f x ∙ j) integrable_on cbox a b"
by auto
then show ?thesis
apply (rule absolutely_integrable_component_ubound [OF _ absint_g])
next
assume gf [rule_format]: "∀x∈cbox a b. g x ≤ f x ∙ j"
have "(λx. (f x ∙ j)) = (λx. ((f x ∙ j) - g x) + g x)"
by simp
moreover have "(λx. (f x ∙ j - g x) + g x) integrable_on cbox a b"
proof (rule Henstock_Kurzweil_Integration.integrable_add [OF _ int_gab])
let ?φ = "λk x. if x ∈ cbox (a + (b - a) /⇩R (Suc k)) (b - (b - a) /⇩R (Suc k))
then f x ∙ j - g x else 0"
have "(λx. f x ∙ j - g x) integrable_on box a b"
proof (rule monotone_convergence_increasing [of ?φ, THEN conjunct1])
have *: "cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k)) ∩ box a b
= cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))" for k
using box_subset_cbox "1" by fastforce
show "?φ k integrable_on box a b" for k
apply (simp add: integrable_restrict_Int integral_restrict_Int *)
apply (rule integrable_diff)
apply (metis "1" int_f integrable_component of_nat_Suc)
apply (rule integrable_on_subcbox [OF int_gab])
using "*" box_subset_cbox apply blast
done
have cb12: "cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))
⊆ cbox (a + (b - a) /⇩R (2 + real k)) (b - (b - a) /⇩R (2 + real k))" for k
using False content_eq_0
apply (fastforce simp: field_simps)
done
show "?φ k x ≤ ?φ (Suc k) x" if "x ∈ box a b" for k x
using cb12 box_subset_cbox that by (force simp: intro!: gf)
show "(λk. ?φ k x) ⇢ f x ∙ j - g x" if x: "x ∈ box a b" for x
proof (rule Lim_eventually)
obtain N::nat where N: "⋀k. k ≥ N ⟹ x ∈ cbox (a + (b - a) /⇩R real k) (b - (b - a) /⇩R real k)"
using getN [OF x] by blast
show "∀⇩F k in sequentially. ?φ k x = f x ∙ j - g x"
proof
fix k::nat assume "N ≤ k"
have "x ∈ cbox (a + (b - a) /⇩R (Suc k)) (b - (b - a) /⇩R (Suc k))"
by (metis ‹N ≤ k› le_Suc_eq N)
then show "?φ k x = f x ∙ j - g x"
by simp
qed
qed
have "¦integral (box a b)
(λx. if x ∈ cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))
then f x ∙ j - g x else 0)¦ ≤ Bf + Bg" for k
proof -
let ?I = "cbox (a + (b - a) /⇩R (1 + real k)) (b - (b - a) /⇩R (1 + real k))"
have I_int [simp]: "?I ∩ box a b = ?I"
using 1 by (simp add: Int_absorb2)
have int_fI: "f integrable_on ?I"
apply (rule integrable_subinterval [OF int_f order_refl])
using "*" box_subset_cbox by blast
then have "(λx. f x ∙ j) integrable_on ?I"
moreover have "g integrable_on ?I"
apply (rule integrable_subinterval [OF int_gab])
using "*" box_subset_cbox by blast
moreover
have "¦integral ?I (λx. f x ∙ j)¦ ≤ norm (integral ?I f)"
by (simp add: Basis_le_norm int_fI ‹j ∈ Basis›)
with 1 I_int have "¦integral ?I (λx. f x ∙ j)¦ ≤ Bf"
by (blast intro: order_trans [OF _ Bf])
ultimately show ?thesis
using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
qed
then show "bounded (range (λk. integral (box a b) (?φ k)))"
apply (rule_tac x="Bf+Bg" in exI)
using ‹0 < Bf› ‹0 < Bg›  by auto
qed
then show "(λx. f x ∙ j - g x) integrable_on cbox a b"