Quellcode-Bibliothek Improper_Integral.thy

(*  Title:      HOL/Analysis/Improper_Integral.thy
  Author: LC Paulson (ported from HOL Light)
*)

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🍋‹tag important› equiintegrable_on (infixr ‹equiintegrable'_on› 46)
  where "F equiintegrable_on I ≡
         (∀f ∈ F. f integrable_on I) ∧
         (∀e > 0. ∃γ. gauge γ ∧
                    (∀f D. f ∈ F ∧ D tagged_division_of I ∧ γ fine D
                          ⟶ norm ((∑(x,K) ∈ D. 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 D. f ∈ F ∪ G ∧
                   D tagged_division_of I ∧ γ fine D ⟶
                   norm ((∑(x,K) ∈ D. content K *🪙R f x) - integral I f) < ε)"
         if "ε > 0" for ε
  proof -
    obtain γ1 where "gauge γ1"
      and γ1: "∧f D. f ∈ F ∧ D tagged_division_of I ∧ γ1 fine D
                    ==> norm ((∑(x,K) ∈ D. 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 D. f ∈ G ∧ D tagged_division_of I ∧ γ2 fine D
                    ==> norm ((∑(x,K) ∈ D. 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 D. f ∈ F ∪ G ∧ D tagged_division_of I ∧ (λx. γ1 x ∩ γ2 x) fine D ⟶
          norm ((∑(x,K) ∈ D. 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)


lemma equiintegrable_cmul:
  assumes F: "F equiintegrable_on I"
  shows "(∪c ∈ {-k..k}. ∪f ∈ F. {(λx. c *🪙R f x)}) equiintegrable_on I"
  unfolding equiintegrable_on_def
  proof (intro conjI impI allI ballI)
  show "f integrable_on I"
    if "f ∈ (∪c∈{- k..k}. ∪f∈F. {λx. c *🪙R f x})"
    for f :: "'a ==> 'b"
    using that assms equiintegrable_on_integrable integrable_cmul by blast
  show "∃γ. gauge γ ∧ (∀f D. f ∈ (∪c∈{- k..k}. ∪f∈F. {λx. c *🪙R f x}) ∧ D tagged_division_of I
          ∧ γ fine D ⟶ norm ((∑(x, K)∈D. content K *🪙R f x) - integral I f) < ε)"
    if "ε > 0" for ε
  proof -
    obtain γ where "gauge γ"
      and γ: "∧f D. [f ∈ F; D tagged_division_of I; γ fine D]
                    ==> norm ((∑(x,K) ∈ D. content K *🪙R f x) - integral I f) < ε / (∣k∣ + 1)"
      using assms ‹ε > 0› unfolding equiintegrable_on_def
      by (metis add.commute add.right_neutral add_strict_mono divide_pos_pos norm_eq_zero real_norm_def zero_less_norm_iff zero_less_one)
    moreover have "norm ((∑(x, K)∈D. content K *🪙R c *🪙R (f x)) - integral I (λx. c *🪙R f x)) < ε"
      if c: "c ∈ {- k..k}"
        and "f ∈ F" "D tagged_division_of I" "γ fine D"
      for D c f
    proof -
      have "norm ((∑x∈D. case x of (x, K) ==> content K *🪙R c *🪙R f x) - integral I (λx. c *🪙R f x))
          = ∣c∣ * norm ((∑x∈D. case x of (x, K) ==> content K *🪙R f x) - integral I f)"
        by (simp add: algebra_simps scale_sum_right case_prod_unfold flip: norm_scaleR)
      also have "… ≤ (∣k∣ + 1) * norm ((∑x∈D. case x of (x, K) ==> content K *🪙R f x) - integral I f)"
        using c by (auto simp: mult_right_mono)
      also have "… < (∣k∣ + 1) * (ε / (∣k∣ + 1))"
        by (rule mult_strict_left_mono) (use γ less_eq_real_def that in auto)
      also have "… = ε"
        by auto
      finally show ?thesis .
    qed
    ultimately show ?thesis
      by (rule_tac x="γ" in exI) auto
  qed
qed


lemma equiintegrable_add:
  assumes F: "F equiintegrable_on I" and G: "G equiintegrable_on I"
  shows "(∪f ∈ F. ∪g ∈ G. {(λx. f x + g x)}) equiintegrable_on I"
  unfolding equiintegrable_on_def
proof (intro conjI impI allI ballI)
  show "f integrable_on I"
    if "f ∈ (∪f∈F. ∪g∈G. {λx. f x + g x})" for f
    using that equiintegrable_on_integrable assms  by (auto intro: integrable_add)
  show "∃γ. gauge γ ∧ (∀f D. f ∈ (∪f∈F. ∪g∈G. {λx. f x + g x}) ∧ D tagged_division_of I
          ∧ γ fine D ⟶ norm ((∑(x, K)∈D. content K *🪙R f x) - integral I f) < ε)"
    if "ε > 0" for ε
  proof -
    obtain γ1 where "gauge γ1"
      and γ1: "∧f D. [f ∈ F; D tagged_division_of I; γ1 fine D]
                    ==> norm ((∑(x,K) ∈ D. content K *🪙R f x) - integral I f) < ε/2"
      using assms ‹ε > 0› unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    obtain γ2 where  "gauge γ2"
      and γ2: "∧g D. [g ∈ G; D tagged_division_of I; γ2 fine D]
                    ==> norm ((∑(x,K) ∈ D. content K *🪙R g x) - integral I g) < ε/2"
      using assms ‹ε > 0› unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    have "gauge (λx. γ1 x ∩ γ2 x)"
      using ‹gauge γ1› ‹gauge γ2› by blast
    moreover have "norm ((∑(x,K) ∈ D. content K *🪙R h x) - integral I h) < ε"
      if h: "h ∈ (∪f∈F. ∪g∈G. {λx. f x + g x})"
        and D: "D tagged_division_of I" and fine: "(λx. γ1 x ∩ γ2 x) fine D"
      for h D
    proof -
      obtain f g where "f ∈ F" "g ∈ G" and heq: "h = (λx. f x + g x)"
        using h by blast
      then have int: "f integrable_on I" "g integrable_on I"
        using F G equiintegrable_on_def by blast+
      have "norm ((∑(x,K) ∈ D. content K *🪙R h x) - integral I h)
          = norm ((∑(x,K) ∈ D. content K *🪙R f x + content K *🪙R g x) - (integral I f + integral I g))"
        by (simp add: heq algebra_simps integral_add int)
      also have "… = norm (((∑(x,K) ∈ D. content K *🪙R f x) - integral I f + (∑(x,K) ∈ D. content K *🪙R g x) - integral I g))"
        by (simp add: sum.distrib algebra_simps case_prod_unfold)
      also have "… ≤ norm ((∑(x,K) ∈ D. content K *🪙R f x) - integral I f) + norm ((∑(x,K) ∈ D. content K *🪙R g x) - integral I g)"
        by (metis (mono_tags) add_diff_eq norm_triangle_ineq)
      also have "… < ε/2 + ε/2"
        using γ1 [OF ‹f ∈ F› D] γ2 [OF ‹g ∈ G› D] fine  by (simp add: fine_Int)
      finally show ?thesis by simp
    qed
    ultimately show ?thesis
      by meson
  qed
qed

lemma equiintegrable_minus:
  assumes "F equiintegrable_on I"
  shows "(∪f ∈ F. {(λx. - f x)}) equiintegrable_on I"
  by (force intro: equiintegrable_on_subset [OF equiintegrable_cmul [OF assms, of 1]])

lemma equiintegrable_diff:
  assumes F: "F equiintegrable_on I" and G: "G equiintegrable_on I"
  shows "(∪f ∈ F. ∪g ∈ G. {(λx. f x - g x)}) equiintegrable_on I"
  by (rule equiintegrable_on_subset [OF equiintegrable_add [OF F equiintegrable_minus [OF G]]]) auto


lemma equiintegrable_sum:
  fixes F :: "('a::euclidean_space ==> 'b::euclidean_space) set"
  assumes "F equiintegrable_on cbox a b"
  shows "(∪I ∈ Collect finite. ∪c ∈ {c. (∀i ∈ I. c i ≥ 0) ∧ sum c I = 1}.
          ∪f ∈ I → F. {(λx. sum (λi::'j. c i *🪙R f i x) I)}) equiintegrable_on cbox a b"
    (is "?G equiintegrable_on _")
  unfolding equiintegrable_on_def
proof (intro conjI impI allI ballI)
  show "f integrable_on cbox a b" if "f ∈ ?G" for f
    using that assms by (auto simp: equiintegrable_on_def intro!: integrable_sum integrable_cmul)
  show "∃γ. gauge γ
           ∧ (∀g D. g ∈ ?G ∧ D tagged_division_of cbox a b ∧ γ fine D
              ⟶ norm ((∑(x,K) ∈ D. content K *🪙R g x) - integral (cbox a b) g) < ε)"
    if "ε > 0" for ε
  proof -
    obtain γ where "gauge γ"
      and γ: "∧f D. [f ∈ F; D tagged_division_of cbox a b; γ fine D]
                    ==> norm ((∑(x,K) ∈ D. content K *🪙R f x) - integral (cbox a b) f) < ε / 2"
      using assms ‹ε > 0› unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    moreover have "norm ((∑(x,K) ∈ D. content K *🪙R g x) - integral (cbox a b) g) < ε"
      if g: "g ∈ ?G"
        and D: "D tagged_division_of cbox a b"
        and fine: "γ fine D"
      for D g
    proof -
      obtain I c f where "finite I" and 0: "∧i::'j. i ∈ I ==> 0 ≤ c i"
        and 1: "sum c I = 1" and f: "f ∈ I → F" and geq: "g = (λx. ∑i∈I. c i *🪙R f i x)"
        using g by auto
      have fi_int: "f i integrable_on cbox a b" if "i ∈ I" for i
        by (metis Pi_iff assms equiintegrable_on_def f that)
      have *: "integral (cbox a b) (λx. c i *🪙R f i x) = (∑(x, K)∈D. integral K (λx. c i *🪙R f i x))"
        if "i ∈ I" for i
      proof -
        have "f i integrable_on cbox a b"
          by (metis Pi_iff assms equiintegrable_on_def f that)
        then show ?thesis
          by (intro D integrable_cmul integral_combine_tagged_division_topdown)
      qed
      have "finite D"
        using D by blast
      have swap: "(∑(x,K)∈D. content K *🪙R (∑i∈I. c i *🪙R f i x))
            = (∑i∈I. c i *🪙R (∑(x,K)∈D. content K *🪙R f i x))"
        by (simp add: scale_sum_right case_prod_unfold algebra_simps) (rule sum.swap)
      have "norm ((∑(x, K)∈D. content K *🪙R g x) - integral (cbox a b) g)
          = norm ((∑i∈I. c i *🪙R ((∑(x,K)∈D. content K *🪙R f i x) - integral (cbox a b) (f i))))"
        unfolding geq swap
        by (simp add: scaleR_right.sum algebra_simps integral_sum fi_int integrable_cmul ‹finite I› sum_subtractf flip: sum_diff)
      also have "… ≤ (∑i∈I. c i * ε / 2)"
      proof (rule sum_norm_le)
        show "norm (c i *🪙R ((∑(xa, K)∈D. content K *🪙R f i xa) - integral (cbox a b) (f i))) ≤ c i * ε / 2"
          if "i ∈ I" for i
        proof -
          have "norm ((∑(x, K)∈D. content K *🪙R f i x) - integral (cbox a b) (f i)) ≤ ε/2"
            using γ [OF _ D fine, of "f i"] funcset_mem [OF f] that  by auto
          then show ?thesis
            using that by (auto simp: 0 mult.assoc intro: mult_left_mono)
        qed
      qed
      also have "… < ε"
        using 1 ‹ε > 0› by (simp add: flip: sum_divide_distrib sum_distrib_right)
      finally show ?thesis .
    qed
    ultimately show ?thesis
      by (rule_tac x="γ" in exI) auto
  qed
qed

corollary equiintegrable_sum_real:
  fixes F :: "(real ==> 'b::euclidean_space) set"
  assumes "F equiintegrable_on {a..b}"
  shows "(∪I ∈ Collect finite. ∪c ∈ {c. (∀i ∈ I. c i ≥ 0) ∧ sum c I = 1}.
          ∪f ∈ I → F. {(λx. sum (λi. c i *🪙R f i x) I)})
         equiintegrable_on {a..b}"
  using equiintegrable_sum [of F a b] assms by auto


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"
  unfolding equiintegrable_on_def 
  by (metis diff_zero gauge_trivial integrable_on_null integral_null norm_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))"
  proof (clarsimp simp add: Cauchy_def)
    fix e::real
    assume "0 < e"
    then have e3: "0 < e/3"
      by simp
    then obtain γ where "gauge γ"
         and γ: "∧n D. [D tagged_division_of cbox a b; γ fine D]
                       ==> norm((∑(x,K) ∈ D. 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 D where D: "D tagged_division_of (cbox a b)" and "γ fine D"  "finite D"
      by (meson ‹gauge γ› fine_division_exists tagged_division_of_finite)
    with γ have δT: "∧n. dist ((∑(x,K)∈D. content K *🪙R f n x)) (integral (cbox a b) (f n)) < e/3"
      by (force simp: dist_norm)
    have "(λn. ∑(x,K)∈D. content K *🪙R f n x) <---- (∑(x,K)∈D. content K *🪙R g x)"
      using D to_g by (auto intro!: tendsto_sum tendsto_scaleR)
    then have "Cauchy (λn. ∑(x,K)∈D. 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)∈D. content K *🪙R f m x) (∑(x,K)∈D. content K *🪙R f n x)
                      < e/3"
      unfolding Cauchy_def by blast
    have "∧m n. [m≥M; n≥M;
                 dist (∑(x,K)∈D. content K *🪙R f m x) (∑(x,K)∈D. 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 D. [D tagged_division_of cbox a b; γ fine D]
                    ==> norm((∑(x,K)∈D. 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)∈D. content K *🪙R g x) - L) < e"
              if "D tagged_division_of cbox a b" "γ fine D" for D
    proof -
      have "norm ((∑(x,K)∈D. content K *🪙R g x) - L) ≤ e/2"
      proof (rule Lim_norm_ubound)
        show "(λn. (∑(x,K)∈D. content K *🪙R f n x) - integral (cbox a b) (f n)) <---- (∑(x,K)∈D. 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) ∈ D. 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 🚫› show ?thesis
        by linarith
    qed
    ultimately
    show "∃γ. gauge γ ∧
             (∀D. D tagged_division_of cbox a b ∧ γ fine D ⟶
                  norm ((∑(x,K)∈D. 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 D. f ∈ (λf. f ∘ uminus) ` F ∧ D tagged_division_of cbox (- b) (- a) ∧ γ fine D ⟶
                   norm ((∑(x,K) ∈ D. content K *🪙R f x) - integral (cbox (- b) (- a)) f) < e)"
       if "gauge γ" and
           γ: "∧f D. [f ∈ F; D tagged_division_of cbox a b; γ fine D] ==>
                     norm ((∑(x,K) ∈ D. 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) ∈ D. content K *🪙R (f ∘ uminus) x) - integral (cbox (- b) (- a)) (f ∘ uminus)) < e"
      if "f ∈ F" and tag: "D tagged_division_of cbox (- b) (- a)"
         and fine: "(λx. uminus ` γ (- x)) fine D" for f D
    proof -
      have 1: "(λ(x,K). (- x, uminus ` K)) ` D tagged_partial_division_of cbox a b"
        if "D tagged_partial_division_of cbox (- b) (- a)"
      proof -
        have "- y ∈ cbox a b"
          if "∧x K. (x,K) ∈ D ==> x ∈ K ∧ K ⊆ cbox (- b) (- a) ∧ (∃a b. K = cbox a b)"
             "(x, Y) ∈ D" "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)) ` D) ∧ x ∈ K"
              if "∪{K. ∃x. (x,K) ∈ D} = cbox (- b) (- a)" "x ∈ cbox a b" for x
      proof -
        have xm: "x ∈ uminus ` ∪{A. ∃a. (a, A) ∈ D}"
          by (simp add: that)
        then obtain a X where "-x ∈ X" "(a, X) ∈ D"
          by auto
        then show ?thesis
          by (metis (no_types, lifting) add.inverse_inverse image_iff pair_imageI)
      qed
      have 3: "∧x X y. [D tagged_partial_division_of cbox (- b) (- a); (x, X) ∈ D; 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)) ` D 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)) ` D"
        using fine by (fastforce simp: fine_def)
      have inj: "inj_on (λ(x,K). (- x, uminus ` K)) D"
        unfolding inj_on_def by force
      have eq: "content (uminus ` I) = content I"
               if I: "(x, I) ∈ D" 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)) ` D. content K *🪙R f x) =
            (∑(x,K) ∈ D. content K *🪙R f (- x))"
        by (auto simp add: eq sum.reindex [OF inj] intro!: sum.cong)
      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
   show ?thesis
    using assms
    apply (auto simp: equiintegrable_on_def)
    subgoal for f
      by (metis (mono_tags, lifting) comp_apply integrable_eq integrable_reflect)
    using 🍋 by fastforce
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: "D division_of S" and S: "S ⊆ cbox a b" and i: "i ∈ Basis"
      and mt: "∧K. K ∈ D ==> content K ≠ 0"
      and disj: "(∀K ∈ D. K ∩ {x. x ∙ i = a ∙ i} ≠ {}) ∨ (∀K ∈ D. K ∩ {x. x ∙ i = b ∙ i} ≠ {})"
   shows "(b ∙ i - a ∙ i) * (∑K∈D. content K / (interval_upperbound K ∙ i - interval_lowerbound K ∙ i))
          ≤ content(cbox a b)"   (is "?lhs ≤ ?rhs")
proof -
  have "finite D"
    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 ∈ D ==> K ⊆ cbox a b"
    using S div by auto
  have "∧K. K ∈ D ==> K ≠ {}"
    using div by blast
  have extend_cbox: "∧K. K ∈ D ==> ∃a b. extend K = cbox a b"
    using extend_def by blast
  have extend: "extend K ≠ {}" "extend K ⊆ cbox a b" if K: "K ∈ D" 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 ⊆ cbox a b"
      by (auto simp: extend_def subset_box box_ne_empty)
    have "a ∙ i ≤ b ∙ i"
      using K by (metis bot.extremum_uniqueI box_ne_empty(1) i)
    with K show "extend K ≠ {}"
      by (simp add: extend_def i box_ne_empty)
  qed
  have int_extend_disjoint:
       "interior(extend K1) ∩ interior(extend K2) = {}" if K: "K1 ∈ D" "K2 ∈ D" "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 ∈ D" "cbox w z ∈ D" "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 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∈D. 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)
        define ξ where "ξ ≡ (∑j ∈ Basis. if j = i then min (q ∙ i) (s ∙ i) *🪙R i else (x ∙ j) *🪙R j)"
        have [simp]: "ξ ∙ j = (if j = i then min (q ∙ j) (s ∙ j) else x ∙ j)" if "j ∈ Basis" for j
          unfolding ξ_def
          by (intro sum_if_inner that ‹i ∈ Basis›)
        show ?thesis
        proof (intro exI conjI)
          have "min (q ∙ i) (s ∙ i) < v ∙ i"
            using i s by fastforce
          with ‹i ∈ Basis› s u ux xv
          show "ξ ∈ box u v" 
            by (force simp: mem_box)
          have "min (q ∙ i) (s ∙ i) < z ∙ i"
            using i q by force
          with ‹i ∈ Basis› q w wx xz
          show "ξ ∈ box w z"
            by (force simp: mem_box)
        qed
      next
        assume "∀K∈D. 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)
        define ξ where "ξ ≡ (∑j ∈ Basis. if j = i then max (q ∙ i) (s ∙ i) *🪙R i else (x ∙ j) *🪙R j)"
        have [simp]: "ξ ∙ j = (if j = i then max (q ∙ j) (s ∙ j) else x ∙ j)" if "j ∈ Basis" for j
          unfolding ξ_def
          by (intro sum_if_inner that ‹i ∈ Basis›)
        show ?thesis
        proof (intro exI conjI)
          show "ξ ∈ box u v"
            using ‹i ∈ Basis› s by (force simp: mem_box ux v xv)
          show "ξ ∈ box w z"
            using ‹i ∈ Basis› q by (force simp: mem_box wx xz z)
        qed
      qed
    qed
    ultimately show ?thesis by auto
  qed
  define interv_diff where "interv_diff ≡ λK. λi::'a. interval_upperbound K ∙ i - interval_lowerbound K ∙ i"
  have "?lhs = (∑K∈D. (b ∙ i - a ∙ i) * content K / (interv_diff K i))"
    by (simp add: sum_distrib_left interv_diff_def)
  also have "… = sum (content ∘ extend) D"
  proof (rule sum.cong [OF refl])
    fix K assume "K ∈ D"
    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 ∈ D›] ‹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 / (interv_diff K i)
             = (b ∙ i - a ∙ i) * (∏i ∈ insert i (Basis ∩ -{i}). v ∙ i - u ∙ i) / (interv_diff (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 interv_diff_def) (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)"
      using ‹i ∈ Basis›
      by (intro prod.cong [OF refl]) (subst sum_if_inner; simp add: algebra_simps)+
    also have "... = (content ∘ extend) K"
      using ‹i ∈ Basis› K box_ne_empty ‹K ∈ D› extend(1) 
      by (auto simp add: extend_def content_cbox_if)
    finally show "(b ∙ i - a ∙ i) * content K / (interv_diff K i) = (content ∘ extend) K" .
  qed
  also have "... = sum content (extend ` D)"
  proof -
    have "[K1 ∈ D; K2 ∈ D; 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
      by (simp add: comm_monoid_add_class.sum.reindex_nontrivial [OF ‹finite D›])
  qed
  also have "... ≤ ?rhs"
  proof (rule subadditive_content_division)
    show "extend ` D division_of ∪ (extend ` D)"
      using int_extend_disjoint  by (auto simp: division_of_def ‹finite D› extend extend_cbox)
    show "∪ (extend ` D) ⊆ cbox a b"
      using extend by fastforce
  qed
  finally show ?thesis .
qed


proposition sum_content_area_over_thin_division:
  assumes div: "D division_of S" and S: "S ⊆ cbox a b" and i: "i ∈ Basis"
    and "a ∙ i ≤ c" "c ≤ b ∙ i"
    and nonmt: "∧K. K ∈ D ==> K ∩ {x. x ∙ i = c} ≠ {}"
  shows "(b ∙ i - a ∙ i) * (∑K∈D. 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∈D. 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 D"
    using div by blast
  define Dlec where "Dlec ≡ {L ∈ (λL. L ∩ {x. x ∙ i ≤ c}) ` D. content L ≠ 0}"
  define Dgec where "Dgec ≡ {L ∈ (λL. L ∩ {x. x ∙ i ≥ c}) ` D. 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)"
  define interv_diff where "interv_diff ≡ λK. λi::'a. interval_upperbound K ∙ i - interval_lowerbound K ∙ i"
  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 ∈ D] ==> ∃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 ∈ D] ==> ∃a b. L ∩ {x. x ∙ i ≥ c} = cbox a b" for L
    using Dgec_def by blast

  have zero_left: "∧x y. [x ∈ D; y ∈ D; x ≠ y; x ∩ {x. x ∙ i ≤ c} = y ∩ {x. x ∙ i ≤ c}]
           ==> content (y ∩ {x. x ∙ i ≤ c}) = 0"
    by (metis division_split_left_inj [OF div] lec_is_cbox content_eq_0_interior)
  have zero_right: "∧x y. [x ∈ D; y ∈ D; x ≠ y; x ∩ {x. c ≤ x ∙ i} = y ∩ {x. c ≤ x ∙ i}]
           ==> content (y ∩ {x. c ≤ x ∙ i}) = 0"
    by (metis division_split_right_inj [OF div] gec_is_cbox content_eq_0_interior)

  have "(b' ∙ i - a ∙ i) * (∑K∈Dlec. content K / interv_diff K i) ≤ content(cbox a b')"
    unfolding interv_diff_def
  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 D› 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 i)
  qed (use i Dlec_def in auto)
  moreover
  have "(∑K∈Dlec. content K / (interv_diff K i)) = (∑K∈(λK. K ∩ {x. x ∙ i ≤ c}) ` D. content K / interv_diff K i)"
    unfolding Dlec_def using ‹finite D› by (auto simp: sum.mono_neutral_left)
  moreover have "... =
        (∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K)"
    by (simp add: zero_left sum.reindex_nontrivial [OF ‹finite D›])
  moreover have "(b' ∙ i - a ∙ i) = (c - a ∙ i)"
    by (simp add: b'_def i)
  ultimately
  have lec: "(c - a ∙ i) * (∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K)
             ≤ content(cbox a b')"
    by simp

  have "(b ∙ i - a' ∙ i) * (∑K∈Dgec. content K / (interv_diff K i)) ≤ content(cbox a' b)"
    unfolding interv_diff_def
  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 D› 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 i)
  qed (use i Dgec_def in auto)
  moreover
  have "(∑K∈Dgec. content K / (interv_diff K i)) = (∑K∈(λK. K ∩ {x. c ≤ x ∙ i}) ` D.
       content K / interv_diff K i)"
    unfolding Dgec_def using ‹finite D› by (auto simp: sum.mono_neutral_left)
  moreover have "… =
        (∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)"
    by (simp add: zero_right sum.reindex_nontrivial [OF ‹finite D›])
  moreover have "(b ∙ i - a' ∙ i) = (b ∙ i - c)"
    by (simp add: a'_def i)
  ultimately
  have gec: "(b ∙ i - c) * (∑K∈D. ((λK. content K / (interv_diff 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"
      moreover
      have "(∑j∈Basis. (if j = i then a ∙ i else a ∙ j) *🪙R j) = a"
        using euclidean_representation [of a] sum.cong [OF refl, of Basis "λi. (a ∙ i) *🪙R i"] by presburger
      ultimately have "a' = a"
        by (simp add: i a'_def cong: if_cong)
      then have "content (cbox a' b) ≤ 2 * content (cbox a b)"  by simp
      moreover
      have eq: "(∑K∈D. content (K ∩ {x. a ∙ i ≤ x ∙ i}) / interv_diff (K ∩ {x. a ∙ i ≤ x ∙ i}) i)
              = (∑K∈D. content K / interv_diff K i)"
        (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K ∈ D"
        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 interv_diff_def by auto
    next
      assume c: "c = b ∙ i"
      moreover have "(∑j∈Basis. (if j = i then b ∙ i else b ∙ j) *🪙R j) = b"
        using euclidean_representation [of b] sum.cong [OF refl, of Basis "λi. (b ∙ i) *🪙R i"] by presburger
      ultimately have "b' = b"
        by (simp add: i b'_def cong: if_cong)
      then have "content (cbox a b') ≤ 2 * content (cbox a b)"  by simp
      moreover
      have eq: "(∑K∈D. content (K ∩ {x. x ∙ i ≤ b ∙ i}) / interv_diff (K ∩ {x. x ∙ i ≤ b ∙ i}) i)
              = (∑K∈D. content K / interv_diff K i)"
               (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K ∈ D"
        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 interv_diff_def 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
    proof -
      have "f i * prod f (Basis ∩ - {i}) = prod f Basis"
        using that mk_disjoint_insert [OF i]
        by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf order_refl prod.insert subset_Compl_singleton)
      then show ?thesis
        by (metis nonzero_mult_div_cancel_left that)
    qed
    have abc: "a ∙ i < c" "c < b ∙ i"
      using False assms by auto
    then have "(∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K)
                  ≤ content(cbox a b') / (c - a ∙ i)"
              "(∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)
                 ≤ content(cbox a' b) / (b ∙ i - c)"
      using lec gec by (simp_all add: field_split_simps)
    moreover
    have "(∑K∈D. content K / (interv_diff K i))
          ≤ (∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K) +
            (∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)"
           (is "?lhs ≤ ?rhs")
    proof -
      have "?lhs ≤
            (∑K∈D. ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≤ c}))) K +
                    ((λK. content K / (interv_diff K i)) ∘ ((λK. K ∩ {x. x ∙ i ≥ c}))) K)"
            (is "sum ?f _ ≤ sum ?g _")
      proof (rule sum_mono)
        fix K assume "K ∈ D"
        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)
        have uniq: "∧j. [j ∈ Basis; ¬ u ∙ j ≤ v ∙ j] ==> j = i"
          by (metis ‹K ∈ D› box_ne_empty(1) div division_of_def uv)
        show "?f K ≤ ?g K"
          using i uv uv'  by (auto simp add: interv_diff_def lemma0 dest: uniq * intro!: prod_nonneg)
      qed
      also have "... = ?rhs"
        by (simp add: sum.distrib)
      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∈D. content K / (interv_diff K i)) ≤ 2 * content (cbox a b) / (b ∙ i - a ∙ i)"
      by linarith
    then show ?thesis
      using abc interv_diff_def by (simp add: field_split_simps)
  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)"
      by (simp add: gauge_trivial)
    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"
    by (simp add: zero_less_measure_iff)
  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 D. [f ∈ F; D tagged_division_of cbox a b; γ fine D]
                              ==> norm ((∑(x,K) ∈ D. 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))"
  define interv_diff where "interv_diff ≡ λK. λi::'a. interval_upperbound K ∙ i - interval_lowerbound K ∙ i"
  have "8 * content (cbox a b) + norm (f x) * (8 * content (cbox a b)) > 0" for x
    by (metis add.right_neutral add_pos_pos contab_gt0 mult_pos_pos mult_zero_left norm_eq_zero zero_less_norm_iff zero_less_numeral)
  then have "gauge (λx. ball x
                    (ε * (INF m∈Basis. b ∙ m - a ∙ m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
    using ‹0 🚫 (cbox a b)› ‹0 🚫ε› a_less_b 
    by (auto simp add: gauge_def field_split_simps add_nonneg_eq_0_iff finite_less_Inf_iff)
  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 unfolding tagged_partial_division_of_def 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 / interv_diff 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)
        show "norm (content K *🪙R h x) ≤ ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) * content K / interv_diff K i"
        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› unfolding tagged_partial_division_of_def 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) * interv_diff K i)"
          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"
            proof (intro mult_left_mono divide_right_mono)
              show "(INF m∈Basis. b ∙ m - a ∙ m) ≤ b ∙ i - a ∙ i"
                using ‹i ∈ Basis› by (auto intro!: cInf_le_finite)
            qed (use ‹0 🚫ε› in auto)
            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))"
            proof -
              have "0 < norm (f x) + 1"
                by (simp add: add.commute add_pos_nonneg)
              then show ?thesis
                using duv dist_uv contab_gt0
                by (simp only: mult_ac divide_simps) auto
            qed
            also have "... = ε * (b ∙ i - a ∙ i) / norm (v - u) / (4 * content (cbox a b))"
              by (simp add: dist_norm norm_minus_commute)
            also have "... ≤ ε * (b ∙ i - a ∙ i) / ∣v ∙ i - u ∙ i∣ / (4 * content (cbox a b))"
            proof (intro mult_right_mono divide_left_mono divide_right_mono uvi)
              show "norm (v - u) * ∣v ∙ i - u ∙ i∣ > 0"
                using u_less_v [OF ‹i ∈ Basis›] 
                by (auto simp: less_eq_real_def zero_less_mult_iff that)
              show "ε * (b ∙ i - a ∙ i) ≥ 0"
                using a_less_b ‹0 🚫ε› ‹i ∈ Basis› by force
            qed auto
            also have "... = ε * (b ∙ i - a ∙ i) / (4 * content (cbox a b) * interv_diff K i)"
              using uv False that(2) u_less_v interv_diff_def 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)) / interv_diff K i)"
            using mult_left_mono by fastforce
          also have "... = ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) * content K / interv_diff K i"
            by (simp add: field_split_simps)
          finally show ?thesis .
        qed
      qed
      also have "... = (∑K∈snd ` S. ε/4 * (b ∙ i - a ∙ i) / content (cbox a b) * content K / interv_diff K i)"
        unfolding interv_diff_def
        apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]])
        apply (simp add: box_eq_empty(1) content_eq_0)
        done
      also have "... = ε/2 * ((b ∙ i - a ∙ i) / (2 * content (cbox a b)) * (∑K∈snd ` S. content K / interv_diff K i))"
        by (simp add: interv_diff_def sum_distrib_left mult.assoc)
      also have "... ≤ (ε/2) * 1"
      proof (rule mult_left_mono)
        have "(b ∙ i - a ∙ i) * (∑K∈snd ` S. content K / interv_diff K i) ≤ 2 * content (cbox a b)"
          unfolding interv_diff_def
        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 "∪(snd ` S) ⊆ cbox a b"
            using S unfolding tagged_partial_division_of_def 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 / interv_diff K i) ≤ 1"
          by (simp add: contab_gt0)
      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"
      by (simp add: Groups_Big.sum_subtractf [symmetric])
    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]
      by (simp add: inf_commute int_F integrable_split(1))
    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"
      proof (rule bounded_equiintegral_over_thin_tagged_partial_division [OF F f, of ‹ε/12›])
        show "∧h x. [h ∈ F; x ∈ cbox a b] ==> norm (h x) ≤ norm (f x)"
          by (auto simp: norm_f)
      qed (use ‹ε > 0› in auto)
      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
        qed (use that ‹ε > 0› ‹gauge γ1› γ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)"
        proof (rule sum.mono_neutral_right [OF ‹finite T› ‹T' ⊆ T›])
          show "∀i ∈ T - T'. (case i of (x, K) ==> integral K f) = 0"
            using f ‹finite T› ‹T' ⊆ T› integral_restrict_Int [of _ "{x. x ∙ i ≤ c}" h]
            by (auto simp: T'_def Int_commute)
        qed
        have "(∑(x,K) ∈ T. content K *🪙R f x) = (∑(x,K) ∈ T'. content K *🪙R f x)"
        proof (rule sum.mono_neutral_right [OF ‹finite T› ‹T' ⊆ T›])
          show "∀i ∈ T - T'. (case i of (x, K) ==> content K *🪙R f x) = 0"
            using T f ‹finite T› ‹T' ⊆ T› by (force simp: T'_def)
        qed
        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))"
            by (simp add: norm_sum split_def)
          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 tagged_partial_division_of_def 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))"
                by (simp add: norm_sum split_def)
              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= "(+)"])
              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)))"
              proof (rule add_mono)
                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 dest: tagged_partial_division_ofD)
                    have "interior (K ∩ {x. x ∙ i ≤ c}) = {}"
                    proof (rule tagged_division_split_left_inj [OF _ ‹(x,K) ∈ A› ‹(x,L) ∈ A›])
                      show "A tagged_division_of ∪(snd ` A)"
                        using A_tagged tagged_partial_division_of_Union_self by auto
                      show "K ∩ {x. x ∙ i ≤ c} = L ∩ {x. x ∙ i ≤ c}"
                        using eq ‹i ∈ Basis› by auto
                    qed (use that in 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 dest: tagged_partial_division_ofD)
                    have "interior (K ∩ {x. c ≤ x ∙ i}) = {}"
                    proof (rule tagged_division_split_right_inj [OF _ ‹(x,K) ∈ B› ‹(x,L) ∈ B›])
                      show "B tagged_division_of ∪(snd ` B)"
                        using B_tagged tagged_partial_division_of_Union_self by auto
                      show "K ∩ {x. c ≤ x ∙ i} = L ∩ {x. c ≤ x ∙ i}"
                        using eq ‹i ∈ Basis› by auto
                    qed (use that in 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
                      by (metis add.commute add.left_commute add_diff_cancel_right' dual_order.refl norm_add_rule_thm norm_triangle_ineq4)
                    obtain u v where uv: "K = cbox u v"
                      using T'_tagged ‹(x,K) ∈ B› ‹B ⊆ T''› ‹T'' ⊆ T'› by (blast dest: tagged_partial_division_ofD)
                    have huv: "h integrable_on cbox u v"
                    proof (rule integrable_on_subcbox)
                      show "cbox u v ⊆ cbox a b"
                        using B_tagged ‹(x,K) ∈ B› uv by (blast dest: tagged_partial_division_ofD)
                      show "h integrable_on cbox a b"
                        by (simp add: int_F ‹h ∈ F›)
                    qed
                    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 dest: tagged_partial_division_ofD)
                then have "connected K"
                  by (simp add: is_interval_connected)
                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 🚫 ∙ i›
                  by (force simp add: mem_box sum_if_inner [where f = "λj. c"])
                show "(∑(x,K) ∈ A. norm (integral K h)) < ε/12"
                  using ‹i ∈ Basis› ‹A ⊆ T''› overlap
                  by (force simp add: sum_if_inner [where f = "λj. c"] 
                       intro!: γ0 [OF cb_ab ‹i ∈ Basis› A_tagged fineA(1) ‹h ∈ F›])
                let ?F = "λ(x,K). (x, K ∩ {x. x ∙ i ≤ c})"
                have 1: "?F ` A tagged_partial_division_of cbox a b"
                  unfolding tagged_partial_division_of_def
                proof (intro conjI strip)
                  show "∧x K. (x, K) ∈ ?F ` A ==> ∃a b. K = cbox a b"
                    using A_tagged interval_split(1) [OF ‹i ∈ Basis›, of _ _ c]
                    by (force dest: tagged_partial_division_ofD(4))
                  show "∧x K. (x, K) ∈ ?F ` A ==> x ∈ K"
                    using A_def A_tagged by (fastforce dest: tagged_partial_division_ofD)
                qed (use A_tagged in ‹fastforce dest: tagged_partial_division_ofD›)+
                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"
                  using ‹i ∈ Basis› ‹A ⊆ T''› overlap
                  by (force simp add: sum_if_inner [where f = "λj. c"] 
                       intro!: γ0 [OF cb_ab ‹i ∈ Basis› 1 2 ‹h ∈ F›])
                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"
                  using ‹i ∈ Basis› ‹B ⊆ T''› overlap
                  by (force simp add: sum_if_inner [where f = "λj. c"] 
                       intro!: γ0 [OF cb_ab ‹i ∈ Basis› B_tagged fineB(1) ‹h ∈ F›])
                  let ?F = "λ(x,K). (x, K ∩ {x. c ≤ x ∙ i})"
                  have 1: "?F ` B tagged_partial_division_of cbox a b"
                    unfolding tagged_partial_division_of_def
                  proof (intro conjI strip)
                    show "∧x K. (x, K) ∈ ?F ` B ==> ∃a b. K = cbox a b"
                      using B_tagged interval_split(2) [OF ‹i ∈ Basis›, of _ _ c]
                      by (force dest: tagged_partial_division_ofD(4))
                    show "∧x K. (x, K) ∈ ?F ` B ==> x ∈ K"
                      using B_def B_tagged by (fastforce dest: tagged_partial_division_ofD)
                  qed (use B_tagged in ‹fastforce dest: tagged_partial_division_ofD›)+
                  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"
                  using ‹i ∈ Basis› ‹A ⊆ T''› overlap
                  by (force simp add: B_def sum_if_inner [where f = "λj. c"] 
                       intro!: γ0 [OF cb_ab ‹i ∈ Basis› 1 2 ‹h ∈ F›])
                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"
            by (simp add: integral_cong)
          have f0_tag: "f x = 0" if "(x,K) ∈ T" for x K
            using T f0 that by (meson tag_in_interval)
          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 (meson tag_in_interval)
          then have fh: "(∑(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)
          show ?thesis
            unfolding fh int_f
          proof (rule less_trans [OF γ1])
            show "γ1 fine T"
              by (meson fine fine_Int)
            show "ε / (7 * Suc DIM('b)) < ε"
              using ‹0 🚫ε› by (force simp: divide_simps)+
          qed (use that in auto)
        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 unfolding comp_def image_iff
      by (metis (no_types, lifting) equation_minus_iff imageE 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})"   (is "?lhs = ?rhs")
  proof
    show "?lhs ⊆ ?rhs"
      using minus_le_iff by fastforce
    show "?rhs ⊆ ?lhs"
    apply clarsimp
    apply (rule_tac x="λx. if c ≤ (-x) ∙ i then h(-x) else 0" in image_eqI)
      using le_minus_iff by fastforce+
  qed
  show ?thesis
    using equiintegrable_reflect [OF *] by (auto simp: eq)
qed

corollary equiintegrable_halfspace_restrictions_lt:
  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"
         (is "?G equiintegrable_on cbox a b")
proof -
  have *: "(∪i∈Basis. ∪c. ∪h∈F. {λx. if c ≤ x ∙ i then h x else 0}) equiintegrable_on cbox a b"
    using equiintegrable_halfspace_restrictions_ge [OF F f] norm_f by auto
  have "(λx. if x ∙ i < c then h x else 0) = (λx. h x - (if c ≤ x ∙ i then h x else 0))"
    if "i ∈ Basis" "h ∈ F" for i c h
    using that by force
  then show ?thesis
    by (blast intro: equiintegrable_on_subset [OF equiintegrable_diff [OF F *]])
qed

corollary equiintegrable_halfspace_restrictions_gt:
  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"
         (is "?G equiintegrable_on cbox a b")
proof -
  have *: "(∪i∈Basis. ∪c. ∪h∈F. {λx. if c ≥ x ∙ i then h x else 0}) equiintegrable_on cbox a b"
    using equiintegrable_halfspace_restrictions_le [OF F f] norm_f by auto
  have "(λx. if x ∙ i > c then h x else 0) = (λx. h x - (if c ≥ x ∙ i then h x else 0))"
    if "i ∈ Basis" "h ∈ F" for i c h
    using that by force
  then show ?thesis
    by (blast intro: equiintegrable_on_subset [OF equiintegrable_diff [OF F *]])
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" "B ⊆ 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
      define F where "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})"
      show ?case
      proof (rule equiintegrable_on_subset)
        have "F equiintegrable_on cbox a b"
          unfolding F_def
        proof (rule equiintegrable_halfspace_restrictions_ge)
          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"
            by (intro * f equiintegrable_on_insert equiintegrable_halfspace_restrictions_le [OF insert.IH insertI1] ‹B ⊆ Basis›)
          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 show "insert f F
             equiintegrable_on cbox a b"
          by (blast intro: f equiintegrable_on_insert)
        show "insert f (∪c d. {λx. if ∀j∈insert i B. c ∙ j ≤ x ∙ j ∧ x ∙ j ≤ d ∙ j then f x else 0})
            ⊆ insert f F"
          using ‹i ∈ Basis›
          apply clarify
          apply (simp add: F_def)
          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 (clarsimp simp: fun_eq_iff)
          apply (drule_tac x=c in spec)
          apply (drule_tac x=d in spec)
          apply (simp split: if_split_asm)
          done
      qed
    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 (force intro: integrable_spike 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 
          by (meson Min.coboundedI euclidean_space_class.finite_Basis finite_imageI image_iff that)
        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›]
              by (simp_all add: inverse_eq_divide)
            show "1 / real (Suc m) ≤ 1 / real n"
              using ‹n ≠ 0› ‹m ≥ n› by (simp add: field_split_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: tendsto_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 🚫› that show ?thesis by auto
  next
    case False
    then have "∃x ∈ cbox (a,a) (b,b). integral (cbox c d) f = integral (cbox (fst x) (snd x)) f"
      using that by (metis cbox_Pair_iff interval_subset_is_interval is_interval_cbox prod.sel)
    then show ?thesis
      using B that(1) by blast
  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
    define α where "α ≡ λk. a + (b - a) /🪙R real k"
    define β where "β ≡ λk. b - (b - a) /🪙R real k"
    define I where "I ≡ λk. cbox (α k) (β k)"
    have ISuc_box: "I (Suc n) ⊆ box a b" for n
      using pos unfolding I_def
      by (intro subset_box_imp) (auto simp: α_def β_def content_pos_lt_eq algebra_simps)
    have ISucSuc: "I (Suc n) ⊆ I (Suc (Suc n))" for n
    proof -
      have "∧i. i ∈ Basis
                 ==> a ∙ i / Suc n + b ∙ i / (real n + 2) ≤ b ∙ i / Suc n + a ∙ i / (real n + 2)"
        using pos 
        by (simp add: content_pos_lt_eq divide_simps) (auto simp: algebra_simps)
      then show ?thesis
        unfolding I_def
        by (intro subset_box_imp) (auto simp: algebra_simps inverse_eq_divide α_def β_def)
    qed
    have getN: "∃N::nat. ∀k. k ≥ N ⟶ x ∈ I k"
      if x: "x ∈ box a b" for x
    proof -
      define Δ where "Δ ≡ (∪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: Δ_def 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 🚫› 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)"
            unfolding Δ_def using that by (force intro: cInf_le_finite)
          have "1 / Inf Δ ≥ ((b - a) ∙ i) / ((x - a) ∙ i)"
            using le_imp_inverse_le [OF * Δ]
            by (simp add: field_simps)
          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 field_split_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 unfolding Δ_def by (force intro: cInf_le_finite)
          have "1 / Inf Δ ≥ ((b - a) ∙ i) / ((b - x) ∙ i)"
            using le_imp_inverse_le [OF * Δ]
            by (simp add: field_simps)
          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 field_split_simps)
        qed
        show "x ∈ I k"
          using that Δ ‹k > 0› unfolding I_def
          by (auto simp: α_def β_def mem_box algebra_simps divide_inverse dest: xa_gt bx_gt)
      qed
    qed
    obtain Bf where  Bf: "∧c d. cbox c d ⊆ box a b ==> norm (integral (cbox c d) f) ≤ Bf"
      using bo unfolding bounded_iff by blast
    obtain Bg where 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_iff 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])
        define φ where "φ ≡ λk x. if x ∈ I (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 *: "I (Suc k) ∩ box a b = I (Suc k)" for k
            using box_subset_cbox ISuc_box by fastforce
          show "φ k integrable_on box a b" for k
          proof -
            have "I (Suc k) ⊆ cbox a b"
              using "*" box_subset_cbox by blast
            moreover have "(λm. f m ∙ j) integrable_on I (Suc k)"
              by (metis ISuc_box I_def int_f integrable_component)
            ultimately have "(λm. g m - f m ∙ j) integrable_on I (Suc k)"
              by (metis Henstock_Kurzweil_Integration.integrable_diff I_def int_gab integrable_on_subcbox)
            then show ?thesis
              by (simp add: "*" φ_def integrable_restrict_Int)
          qed
          show "φ k x ≤ φ (Suc k) x" if "x ∈ box a b" for k x
            using ISucSuc box_subset_cbox that by (force simp: φ_def intro!: fg)
          show "(λk. φ k x) <---- g x - f x ∙ j" if x: "x ∈ box a b" for x
          proof (rule tendsto_eventually)
            obtain N::nat where N: "∧k. k ≥ N ==> x ∈ I 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 ∈ I (Suc k)"
                by (metis ‹N ≤ k› le_Suc_eq N)
              then show "φ k x = g x - f x ∙ j"
                by (simp add: φ_def)
            qed
          qed
          have "∣integral (box a b) (λx. if x ∈ I (Suc k) then g x - f x ∙ j else 0)∣ ≤ Bg + Bf" for k
          proof -
            have ABK_def [simp]: "I (Suc k) ∩ box a b = I (Suc k)"
              using ISuc_box by (simp add: Int_absorb2)
            have int_fI: "f integrable_on I (Suc k)"
              using ISuc_box I_def int_f by auto
            moreover
            have "∣integral (I (Suc k)) (λx. f x ∙ j)∣ ≤ norm (integral (I (Suc k)) f)"
              by (simp add: Basis_le_norm int_fI ‹j ∈ Basis›)
            with ISuc_box ABK_def have "∣integral (I (Suc k)) (λx. f x ∙ j)∣ ≤ Bf"
              by (metis Bf I_def ‹j ∈ Basis› int_fI integral_component_eq norm_bound_Basis_le) 
            ultimately 
            have "∣integral (I (Suc k)) g - integral (I (Suc k)) (λx. f x ∙ j)∣ ≤ Bg + Bf"
              using "*" box_subset_cbox unfolding I_def
              by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
            moreover have "g integrable_on I (Suc k)"
              by (metis ISuc_box I_def int_gab integrable_on_open_interval integrable_on_subcbox)
            moreover have "(λx. f x ∙ j) integrable_on I (Suc k)"
              using int_fI by (simp add: integrable_component)
           ultimately show ?thesis
              by (simp add: integral_restrict_Int integral_diff)
          qed
          then show "bounded (range (λk. integral (box a b) (φ k)))"
            by (auto simp add: bounded_iff φ_def)
        qed
        then show "(λx. g x - f x ∙ j) integrable_on cbox a b"
          by (simp add: integrable_on_open_interval)
      qed
      ultimately have "(λx. f x ∙ j) integrable_on cbox a b"
        by auto
      then show ?thesis
        using absolutely_integrable_component_ubound [OF _ absint_g] fg by force
    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 ∈ I(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 *: "I (Suc k) ∩ box a b = I (Suc k)" for k
            using box_subset_cbox ISuc_box by fastforce
          show "?φ k integrable_on box a b" for k
          proof (simp add: integrable_restrict_Int integral_restrict_Int *)
            show "(λx. f x ∙ j - g x) integrable_on I (Suc k)"
              by (metis ISuc_box Henstock_Kurzweil_Integration.integrable_diff I_def int_f int_gab integrable_component integrable_on_open_interval integrable_on_subcbox)
          qed
          show "?φ k x ≤ ?φ (Suc k) x" if "x ∈ box a b" for k x
            using ISucSuc box_subset_cbox that by (force simp: I_def intro!: gf)
          show "(λk. ?φ k x) <---- f x ∙ j - g x" if x: "x ∈ box a b" for x
          proof (rule tendsto_eventually)
            obtain N::nat where N: "∧k. k ≥ N ==> x ∈ I k"
              using getN [OF x] by blast
            then show "∀🪙F k in sequentially. ?φ k x = f x ∙ j - g x"
              by (metis (no_types, lifting) eventually_at_top_linorderI le_Suc_eq)
          qed
          have "∣integral (box a b)
                      (λx. if x ∈ I (Suc k) then f x ∙ j - g x else 0)∣ ≤ Bf + Bg" for k
          proof -
            define ABK where "ABK ≡ cbox (a + (b - a) /🪙R (1 + real k)) (b - (b - a) /🪙R (1 + real k))"
            have ABK_eq [simp]: "ABK ∩ box a b = ABK"
              using "*" I_def α_def β_def ABK_def by auto
            have int_fI: "f integrable_on ABK"
              unfolding ABK_def
              using ISuc_box I_def α_def β_def int_f by force
            then have "(λx. f x ∙ j) integrable_on ABK"
              by (simp add: integrable_component)
            moreover have "g integrable_on ABK"
              by (metis ABK_def ABK_eq IntE box_subset_cbox int_gab integrable_on_subcbox subset_eq)
            moreover
            have "∣integral ABK (λx. f x ∙ j)∣ ≤ norm (integral ABK f)"
              by (simp add: Basis_le_norm int_fI ‹j ∈ Basis›)
            then have "∣integral ABK (λx. f x ∙ j)∣ ≤ Bf"
              by (metis ABK_eq  ABK_def Bf IntE dual_order.trans subset_eq)
            ultimately show ?thesis
              using "*" box_subset_cbox
              apply (simp add: integral_restrict_Int integral_diff ABK_def I_def α_def β_def)
               by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
          qed
          then show "bounded (range (λk. integral (box a b) (?φ k)))"
            by (auto simp add: bounded_iff)
        qed
        then show "(λx. f x ∙ j - g x) integrable_on cbox a b"
          by (simp add: integrable_on_open_interval)
      qed
      ultimately have "(λx. f x ∙ j) integrable_on cbox a b"
        by auto
      then show ?thesis
        using absint_g absolutely_integrable_absolutely_integrable_lbound gf by blast
    qed
  qed
qed

subsection‹Second mean value theorem and corollaries›

lemma level_approx:
  fixes f :: "real ==> real" and n::nat
  assumes f: "∧x. x ∈ S ==> 0 ≤ f x ∧ f x ≤ 1" and "x ∈ S" "n ≠ 0"
  shows "∣f x - (∑k = Suc 0..n. if k / n ≤ f x then inverse n else 0)∣ < inverse n"
        (is "?lhs < _")
proof -
  have "n * f x ≥ 0"
    using assms by auto
  then obtain m::nat where m: "floor(n * f x) = int m"
    using nonneg_int_cases zero_le_floor by blast
  then have kn: "real k / real n ≤ f x ⟷ k ≤ m" for k
    using ‹n ≠ 0› by (simp add: field_split_simps) linarith
  then have "Suc n / real n ≤ f x ⟷ Suc n ≤ m"
    by blast
  have "real n * f x ≤ real n"
    by (simp add: ‹x ∈ S› f mult_left_le)
  then have "m ≤ n"
    using m by linarith
  have "?lhs = ∣f x - (∑k ∈ {Suc 0..n} ∩ {..m}. inverse n)∣"
    by (subst sum.inter_restrict) (auto simp: kn)
  also have "… < inverse n"
    using ‹m ≤ n› ‹n ≠ 0› m
    by (simp add: min_absorb2 field_split_simps) linarith
  finally show ?thesis .
qed


lemma SMVT_lemma2:
  fixes f :: "real ==> real"
  assumes f: "f integrable_on {a..b}"
    and g: "∧x y. x ≤ y ==> g x ≤ g y"
  shows "(∪y::real. {λx. if g x ≥ y then f x else 0}) equiintegrable_on {a..b}"
proof -
  have ffab: "{f} equiintegrable_on {a..b}"
    by (metis equiintegrable_on_sing f interval_cbox)
  then have ff: "{f} equiintegrable_on (cbox a b)"
    by simp
  have ge: "(∪c. {λx. if x ≥ c then f x else 0}) equiintegrable_on {a..b}"
    using equiintegrable_halfspace_restrictions_ge [OF ff] by auto
  have gt: "(∪c. {λx. if x > c then f x else 0}) equiintegrable_on {a..b}"
    using equiintegrable_halfspace_restrictions_gt [OF ff] by auto
  have 0: "{(λx. 0)} equiintegrable_on {a..b}"
    by (metis box_real(2) equiintegrable_on_sing integrable_0)
  have †: "(λx. if g x ≥ y then f x else 0) ∈ {(λx. 0), f} ∪ (∪z. {λx. if z < x then f x else 0}) ∪ (∪z. {λx. if z ≤ x then f x else 0})"
    for y
  proof (cases "(∀x. g x ≥ y) ∨ (∀x. ¬ (g x ≥ y))")
    let ?μ = "Inf {x. g x ≥ y}"
    case False
    have lower: "?μ ≤ x" if "g x ≥ y" for x
    proof (rule cInf_lower)
      show "x ∈ {x. y ≤ g x}"
        using False by (auto simp: that)
      show "bdd_below {x. y ≤ g x}"
        by (metis False bdd_belowI dual_order.trans g linear mem_Collect_eq)
    qed
    have greatest: "?μ ≥ z" if  "(∧x. g x ≥ y ==> z ≤ x)" for z
      by (metis False cInf_greatest empty_iff mem_Collect_eq that)
    show ?thesis
    proof (cases "g ?μ ≥ y")
      case True
      then obtain ζ where ζ: "∧x. g x ≥ y ⟷ x ≥ ζ"
        by (metis g lower order.trans)  🍋 ‹in fact y is @{term ?μ}›
      then show ?thesis
        by (force simp: ζ)
    next
      case False
      have "(y ≤ g x) ⟷ (?μ < x)" for x
      proof
        show "?μ < x" if "y ≤ g x"
          using that False less_eq_real_def lower by blast
        show "y ≤ g x" if "?μ < x"
          by (metis g greatest le_less_trans that less_le_trans linear not_less)
      qed
      then obtain ζ where ζ: "∧x. g x ≥ y ⟷ x > ζ" ..
      then show ?thesis
        by (force simp: ζ)
    qed
  qed auto
  show ?thesis
    using † by (simp add: UN_subset_iff equiintegrable_on_subset [OF equiintegrable_on_Un [OF gt equiintegrable_on_Un [OF ge equiintegrable_on_Un [OF ffab 0]]]])
qed


lemma SMVT_lemma4:
  fixes f :: "real ==> real"
  assumes f: "f integrable_on {a..b}"
    and "a ≤ b"
    and g: "∧x y. x ≤ y ==> g x ≤ g y"
    and 01: "∧x. [a ≤ x; x ≤ b] ==> 0 ≤ g x ∧ g x ≤ 1"
  obtains c where "a ≤ c" "c ≤ b" "((λx. g x *🪙R f x) has_integral integral {c..b} f) {a..b}"
proof -
  have "connected ((λx. integral {x..b} f) ` {a..b})"
    by (simp add: f indefinite_integral_continuous_1' connected_continuous_image)
  moreover have "compact ((λx. integral {x..b} f) ` {a..b})"
    by (simp add: compact_continuous_image f indefinite_integral_continuous_1')
  ultimately obtain m M where int_fab: "(λx. integral {x..b} f) ` {a..b} = {m..M}"
    using connected_compact_interval_1 by meson
  have "∃c. c ∈ {a..b} ∧
              integral {c..b} f =
              integral {a..b} (λx. (∑k = 1..n. if g x ≥ real k / real n then inverse n *🪙R f x else 0))" for n
  proof (cases "n=0")
    case True
    then show ?thesis
      using ‹a ≤ b› by auto
  next
    case False
    have "(∪c::real. {λx. if g x ≥ c then f x else 0}) equiintegrable_on {a..b}"
      using SMVT_lemma2 [OF f g] .
    then have int: "(λx. if g x ≥ c then f x else 0) integrable_on {a..b}" for c
      by (simp add: equiintegrable_on_def)
    have int': "(λx. if g x ≥ c then u * f x else 0) integrable_on {a..b}" for c u
    proof -
      have "(λx. if g x ≥ c then u * f x else 0) = (λx. u * (if g x ≥ c then f x else 0))"
        by (force simp: if_distrib)
      then show ?thesis
        using integrable_on_cmult_left [OF int] by simp
    qed
    have "∃d. d ∈ {a..b} ∧ integral {a..b} (λx. if g x ≥ y then f x else 0) = integral {d..b} f" for y
    proof -
      let ?X = "{x. g x ≥ y}"
      have *: "∃a. ?X = {a..} ∨ ?X = {a<..}"
        if 1: "?X ≠ {}" and 2: "?X ≠ UNIV"
      proof -
        let ?μ = "Inf{x. g x ≥ y}"
        have lower: "?μ ≤ x" if "g x ≥ y" for x
        proof (rule cInf_lower)
          show "x ∈ {x. y ≤ g x}"
            using 1 2 by (auto simp: that)
          show "bdd_below {x. y ≤ g x}"
            unfolding bdd_below_def
            by (metis "2" UNIV_eq_I dual_order.trans g less_eq_real_def mem_Collect_eq not_le)
        qed
        have greatest: "?μ ≥ z" if "∧x. g x ≥ y ==> z ≤ x" for z
          by (metis cInf_greatest mem_Collect_eq that 1)
        show ?thesis
        proof (cases "g ?μ ≥ y")
          case True
          then obtain ζ where ζ: "∧x. g x ≥ y ⟷ x ≥ ζ"
            by (metis g lower order.trans)  🍋 ‹in fact y is @{term ?μ}›
          then show ?thesis
            by (force simp: ζ)
        next
          case False
          have "(y ≤ g x) = (?μ < x)" for x
          proof
            show "?μ < x" if "y ≤ g x"
              using that False less_eq_real_def lower by blast
            show "y ≤ g x" if "?μ < x"
              by (metis g greatest le_less_trans that less_le_trans linear not_less)
          qed
          then obtain ζ where ζ: "∧x. g x ≥ y ⟷ x > ζ" ..
          then show ?thesis
            by (force simp: ζ)
        qed
      qed
      then consider "?X = {}" | "?X = UNIV" | (intv) d where "?X = {d..} ∨ ?X = {d<..}"
        by metis
      then have "∃d. d ∈ {a..b} ∧ integral {a..b} (λx. if x ∈ ?X then f x else 0) = integral {d..b} f"
      proof cases
        case (intv d)
        show ?thesis
        proof (cases "d < a")
          case True
          with intv have "integral {a..b} (λx. if y ≤ g x then f x else 0) = integral {a..b} f"
            by (intro Henstock_Kurzweil_Integration.integral_cong) force
          then show ?thesis
            by (rule_tac x=a in exI) (simp add: ‹a ≤ b›)
        next
          case False
          show ?thesis
          proof (cases "b < d")
            case True
            have "integral {a..b} (λx. if x ∈ {x. y ≤ g x} then f x else 0) = integral {a..b} (λx. 0)"
              by (rule Henstock_Kurzweil_Integration.integral_cong) (use intv True in fastforce)
            then show ?thesis
              using ‹a ≤ b› by auto
          next
            case False
            with ‹¬ d 🚫› have eq: "{d..} ∩ {a..b} = {d..b}" "{d<..} ∩ {a..b} = {d<..b}"
              by force+
            moreover have "integral {d<..b} f = integral {d..b} f"
              by (rule integral_spike_set [OF empty_imp_negligible negligible_subset [OF negligible_sing [of d]]]) auto
            ultimately 
            have "integral {a..b} (λx. if x ∈ {x. y ≤ g x} then f x else 0) = integral {d..b} f"
              unfolding integral_restrict_Int using intv by presburger
            moreover have "d ∈ {a..b}"
              using ‹¬ d 🚫› ‹a ≤ b› False by auto
            ultimately show ?thesis
              by auto
          qed
        qed
      qed (use ‹a ≤ b› in auto)
      then show ?thesis
        by auto
    qed
    then have "∀k. ∃d. d ∈ {a..b} ∧ integral {a..b} (λx. if real k / real n ≤ g x then f x else 0) = integral {d..b} f"
      by meson
    then obtain d where dab: "∧k. d k ∈ {a..b}"
      and deq: "∧k::nat. integral {a..b} (λx. if k/n ≤ g x then f x else 0) = integral {d k..b} f"
      by metis
    have "(∑k = 1..n. integral {a..b} (λx. if real k / real n ≤ g x then f x else 0)) /🪙R n ∈ {m..M}"
      unfolding scaleR_right.sum
    proof (intro conjI allI impI convex [THEN iffD1, rule_format])
      show "integral {a..b} (λxa. if real k / real n ≤ g xa then f xa else 0) ∈ {m..M}" for k
        by (metis (no_types, lifting) deq image_eqI int_fab dab)
    qed (use ‹n ≠ 0› in auto)
    then have "∃c. c ∈ {a..b} ∧
              integral {c..b} f = inverse n *🪙R (∑k = 1..n. integral {a..b} (λx. if g x ≥ real k / real n then f x else 0))"
      by (metis (no_types, lifting) int_fab imageE)
    then show ?thesis
      by (simp add: sum_distrib_left if_distrib integral_sum int' flip: integral_mult_right cong: if_cong)
  qed
  then obtain c where cab: "∧n. c n ∈ {a..b}"
    and c: "∧n. integral {c n..b} f = integral {a..b} (λx. (∑k = 1..n. if g x ≥ real k / real n then f x /🪙R n else 0))"
    by metis
  obtain d and σ :: "nat==>nat"
    where "d ∈ {a..b}" and σ: "strict_mono σ" and d: "(c ∘ σ) <---- d" and non0: "∧n. σ n ≥ Suc 0"
  proof -
    have "compact{a..b}"
      by auto
    with cab obtain d and s0
      where "d ∈ {a..b}" and s0: "strict_mono s0" and tends: "(c ∘ s0) <---- d"
      unfolding compact_def
      using that by blast
    show thesis
    proof
      show "d ∈ {a..b}"
        by fact
      show "strict_mono (s0 ∘ Suc)"
        using s0 by (auto simp: strict_mono_def)
      show "(c ∘ (s0 ∘ Suc)) <---- d"
        by (metis tends LIMSEQ_subseq_LIMSEQ Suc_less_eq comp_assoc strict_mono_def)
      show "∧n. (s0 ∘ Suc) n ≥ Suc 0"
        by (metis comp_apply le0 not_less_eq_eq old.nat.exhaust s0 seq_suble)
    qed
  qed
  define φ where "φ ≡ λn x. ∑k = Suc 0..σ n. if k/(σ n) ≤ g x then f x /🪙R (σ n) else 0"
  define ψ where "ψ ≡ λn x. ∑k = Suc 0..σ n. if k/(σ n) ≤ g x then inverse (σ n) else 0"
  have **: "(λx. g x *🪙R f x) integrable_on cbox a b ∧
            (λn. integral (cbox a b) (φ n)) <---- integral (cbox a b) (λx. g x *🪙R f x)"
  proof (rule equiintegrable_limit)
    have †: "((λn. λx. (∑k = Suc 0..n. if k / n ≤ g x then inverse n *🪙R f x else 0)) ` {Suc 0..}) equiintegrable_on {a..b}"
    proof -
      have *: "(∪c::real. {λx. if g x ≥ c then f x else 0}) equiintegrable_on {a..b}"
        using SMVT_lemma2 [OF f g] .
      show ?thesis
        apply (rule equiintegrable_on_subset [OF equiintegrable_sum_real [OF *]], clarify)
        apply (rule_tac a="{Suc 0..n}" in UN_I, force)
        apply (rule_tac a="λk. inverse n" in UN_I, auto)
        apply (rule_tac x="λk x. if real k / real n ≤ g x then f x else 0" in bexI)
         apply (force intro: sum.cong)+
        done
    qed
    show "range φ equiintegrable_on cbox a b"
      unfolding φ_def
      by (auto simp: non0 intro: equiintegrable_on_subset [OF †])
    show "(λn. φ n x) <---- g x *🪙R f x"
      if x: "x ∈ cbox a b" for x
    proof -
      have eq: "φ n x = ψ n x *🪙R f x"  for n
        by (auto simp: φ_def ψ_def sum_distrib_right if_distrib intro: sum.cong)
      show ?thesis
        unfolding eq
      proof (rule tendsto_scaleR [OF _ tendsto_const])
        show "(λn. ψ n x) <---- g x"
          unfolding lim_sequentially dist_real_def
        proof (intro allI impI)
          fix e :: real
          assume "e > 0"
          then obtain N where "N ≠ 0" "0 < inverse (real N)" and N: "inverse (real N) < e"
            using real_arch_inverse by metis
          moreover have "∣ψ n x - g x∣ < inverse (real N)" if "n≥N" for n
          proof -
            have "∣g x - ψ n x∣ < inverse (real (σ n))"
              unfolding ψ_def
            proof (rule level_approx [of "{a..b}" g])
              show "σ n ≠ 0"
                by (metis Suc_n_not_le_n non0)
            qed (use x 01 non0 in auto)
            also have "… ≤ inverse N"
              using seq_suble [OF σ] ‹N ≠ 0› non0 that by (auto intro: order_trans simp: field_split_simps)
            finally show ?thesis
              by linarith
          qed
          ultimately show "∃N. ∀n≥N. ∣ψ n x - g x∣ < e"
            using less_trans by blast
        qed
      qed
    qed
  qed
  show thesis
  proof
    show "a ≤ d" "d ≤ b"
      using ‹d ∈ {a..b}› atLeastAtMost_iff by blast+
    show "((λx. g x *🪙R f x) has_integral integral {d..b} f) {a..b}"
      unfolding has_integral_iff
    proof
      show "(λx. g x *🪙R f x) integrable_on {a..b}"
        using ** by simp
      show "integral {a..b} (λx. g x *🪙R f x) = integral {d..b} f"
      proof (rule tendsto_unique)
        show "(λn. integral {c(σ n)..b} f) <---- integral {a..b} (λx. g x *🪙R f x)"
          using ** by (simp add: c φ_def)
        have "continuous (at d within {a..b}) (λx. integral {x..b} f)"
          using indefinite_integral_continuous_1' [OF f] ‹d ∈ {a..b}›
          by (simp add: continuous_on_eq_continuous_within)
        then show "(λn. integral {c(σ n)..b} f) <---- integral {d..b} f"
          using d cab unfolding o_def
          by (simp add: continuous_within_sequentially o_def)
      qed auto
    qed
  qed
qed


theorem second_mean_value_theorem_full:
  fixes f :: "real ==> real"
  assumes f: "f integrable_on {a..b}" and "a ≤ b"
    and g: "∧x y. [a ≤ x; x ≤ y; y ≤ b] ==> g x ≤ g y"
  obtains c where "c ∈ {a..b}"
    and "((λx. g x * f x) has_integral (g a * integral {a..c} f + g b * integral {c..b} f)) {a..b}"
proof -
  have gab: "g a ≤ g b"
    using ‹a ≤ b› g by blast
  then consider "g a < g b" | "g a = g b"
    by linarith
  then show thesis
  proof cases
    case 1
    define h where "h ≡ λx. if x < a then 0 else if b < x then 1
                             else (g x - g a) / (g b - g a)"
    obtain c where "a ≤ c" "c ≤ b" and c: "((λx. h x *🪙R f x) has_integral integral {c..b} f) {a..b}"
    proof (rule SMVT_lemma4 [OF f ‹a ≤ b›, of h])
      show "h x ≤ h y" "0 ≤ h x ∧ h x ≤ 1"  if "x ≤ y" for x y
        using that gab by (auto simp: divide_simps g h_def)
    qed
    show ?thesis
    proof
      show "c ∈ {a..b}"
        using ‹a ≤ c› ‹c ≤ b› by auto
      have I: "((λx. g x * f x - g a * f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
      proof (subst has_integral_cong)
        show "g x * f x - g a * f x = (g b - g a) * h x *🪙R f x"
          if "x ∈ {a..b}" for x
          using 1 that by (simp add: h_def field_split_simps)
        show "((λx. (g b - g a) * h x *🪙R f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
          using has_integral_mult_right [OF c, of "g b - g a"] .
      qed
      have II: "((λx. g a * f x) has_integral g a * integral {a..b} f) {a..b}"
        using has_integral_mult_right [where c = "g a", OF integrable_integral [OF f]] .
      have "((λx. g x * f x) has_integral (g b - g a) * integral {c..b} f + g a * integral {a..b} f) {a..b}"
        using has_integral_add [OF I II] by simp
      then show "((λx. g x * f x) has_integral g a * integral {a..c} f + g b * integral {c..b} f) {a..b}"
        by (simp add: algebra_simps flip: integral_combine [OF ‹a ≤ c› ‹c ≤ b› f])
    qed
  next
    case 2
    show ?thesis
    proof
      show "a ∈ {a..b}"
        by (simp add: ‹a ≤ b›)
      have "((λx. g x * f x) has_integral g a * integral {a..b} f) {a..b}"
      proof (rule has_integral_eq)
        show "((λx. g a * f x) has_integral g a * integral {a..b} f) {a..b}"
          using f has_integral_mult_right by blast
        show "g a * f x = g x * f x"
          if "x ∈ {a..b}" for x
          by (metis atLeastAtMost_iff g less_eq_real_def not_le that 2)
      qed
      then show "((λx. g x * f x) has_integral g a * integral {a..a} f + g b * integral {a..b} f) {a..b}"
        by (simp add: 2)
    qed
  qed
qed


corollary second_mean_value_theorem:
  fixes f :: "real ==> real"
  assumes f: "f integrable_on {a..b}" and "a ≤ b"
   and g: "∧x y. [a ≤ x; x ≤ y; y ≤ b] ==> g x ≤ g y"
 obtains c where "c ∈ {a..b}"
                 "integral {a..b} (λx. g x * f x) = g a * integral {a..c} f + g b * integral {c..b} f"
    using second_mean_value_theorem_full [where g=g, OF assms]
    by (metis (full_types) integral_unique)

end