Theory HOL-Analysis.Improper_Integral

(*  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.›

definitiontag important› equiintegrable_on (infixr "equiintegrable'_on" 46)
  where "F equiintegrable_on I 
         (f  F. f integrable_on I) 
         (e > 0. γ. gauge γ 
                    (f 𝒟. f  F  𝒟 tagged_division_of I  γ fine 𝒟
                           norm (((x,K)  𝒟. content K *R f x) - integral I f) < e))"

lemma equiintegrable_on_integrable:
     "F equiintegrable_on I; f  F  f integrable_on I"
  using equiintegrable_on_def by metis

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

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

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


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


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}. fF. {λx. c *R f x})"
    for f :: "'a  'b"
    using that assms equiintegrable_on_integrable integrable_cmul by blast
  show "γ. gauge γ  (f 𝒟. f  (c{- k..k}. fF. {λx. c *R f x})  𝒟 tagged_division_of I
           γ fine 𝒟  norm (((x, K)𝒟. content K *R f x) - integral I f) < ε)"
    if "ε > 0" for ε
  proof -
    obtain γ where "gauge γ"
      and γ: "f 𝒟. f  F; 𝒟 tagged_division_of I; γ fine 𝒟
                     norm (((x,K)  𝒟. 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)𝒟. content K *R c *R (f x)) - integral I (λx. c *R f x)) < ε"
      if c: "c  {- k..k}"
        and "f  F" "𝒟 tagged_division_of I" "γ fine 𝒟"
      for 𝒟 c f
    proof -
      have "norm ((x𝒟. case x of (x, K)  content K *R c *R f x) - integral I (λx. c *R f x))
          = ¦c¦ * norm ((x𝒟. 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𝒟. 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  (fF. gG. {λx. f x + g x})" for f
    using that equiintegrable_on_integrable assms  by (auto intro: integrable_add)
  show "γ. gauge γ  (f 𝒟. f  (fF. gG. {λx. f x + g x})  𝒟 tagged_division_of I
           γ fine 𝒟  norm (((x, K)𝒟. content K *R f x) - integral I f) < ε)"
    if "ε > 0" for ε
  proof -
    obtain γ1 where "gauge γ1"
      and γ1: "f 𝒟. f  F; 𝒟 tagged_division_of I; γ1 fine 𝒟
                     norm (((x,K)  𝒟. content K *R f x) - integral I f) < ε/2"
      using assms ε > 0 unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    obtain γ2 where  "gauge γ2"
      and γ2: "g 𝒟. g  G; 𝒟 tagged_division_of I; γ2 fine 𝒟
                     norm (((x,K)  𝒟. 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)  𝒟. content K *R h x) - integral I h) < ε"
      if h: "h  (fF. gG. {λx. f x + g x})"
        and 𝒟: "𝒟 tagged_division_of I" and fine: "(λx. γ1 x  γ2 x) fine 𝒟"
      for h 𝒟
    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)  𝒟. content K *R h x) - integral I h)
          = norm (((x,K)  𝒟. 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)  𝒟. content K *R f x) - integral I f + ((x,K)  𝒟. content K *R g x) - integral I g))"
        by (simp add: sum.distrib algebra_simps case_prod_unfold)
      also have "  norm (((x,K)  𝒟. content K *R f x) - integral I f) + norm (((x,K)  𝒟. 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 𝒟] γ2 [OF g  G 𝒟] 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 𝒟. g  ?G  𝒟 tagged_division_of cbox a b  γ fine 𝒟
               norm (((x,K)  𝒟. content K *R g x) - integral (cbox a b) g) < ε)"
    if "ε > 0" for ε
  proof -
    obtain γ where "gauge γ"
      and γ: "f 𝒟. f  F; 𝒟 tagged_division_of cbox a b; γ fine 𝒟
                     norm (((x,K)  𝒟. content K *R f x) - integral (cbox a b) f) < ε / 2"
      using assms ε > 0 unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    moreover have "norm (((x,K)  𝒟. content K *R g x) - integral (cbox a b) g) < ε"
      if g: "g  ?G"
        and 𝒟: "𝒟 tagged_division_of cbox a b"
        and fine: "γ fine 𝒟"
      for 𝒟 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. iI. 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)𝒟. 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 𝒟 integrable_cmul integral_combine_tagged_division_topdown)
      qed
      have "finite 𝒟"
        using 𝒟 by blast
      have swap: "((x,K)𝒟. content K *R (iI. c i *R f i x))
            = (iI. c i *R ((x,K)𝒟. content K *R f i x))"
        by (simp add: scale_sum_right case_prod_unfold algebra_simps) (rule sum.swap)
      have "norm (((x, K)𝒟. content K *R g x) - integral (cbox a b) g)
          = norm ((iI. c i *R (((x,K)𝒟. 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 "  (iI. c i * ε / 2)"
      proof (rule sum_norm_le)
        show "norm (c i *R (((xa, K)𝒟. 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)𝒟. content K *R f i x) - integral (cbox a b) (f i))  ε/2"
            using γ [OF _ 𝒟 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 𝒟. 𝒟 tagged_division_of cbox a b; γ fine 𝒟
                        norm(((x,K)  𝒟. content K *R f n x) - integral (cbox a b) (f n)) < e/3"
      using feq unfolding equiintegrable_on_def
      by (meson image_eqI iso_tuple_UNIV_I)
    obtain 𝒟 where 𝒟: "𝒟 tagged_division_of (cbox a b)" and "γ fine 𝒟"  "finite 𝒟"
      by (meson gauge γ fine_division_exists tagged_division_of_finite)
    with γ have δT: "n. dist (((x,K)𝒟. content K *R f n x)) (integral (cbox a b) (f n)) < e/3"
      by (force simp: dist_norm)
    have "(λn. (x,K)𝒟. content K *R f n x)  ((x,K)𝒟. content K *R g x)"
      using 𝒟 to_g by (auto intro!: tendsto_sum tendsto_scaleR)
    then have "Cauchy (λn. (x,K)𝒟. content K *R f n x)"
      by (meson convergent_eq_Cauchy)
    with e3 obtain M where
      M: "m n. mM; nM  dist ((x,K)𝒟. content K *R f m x) ((x,K)𝒟. content K *R f n x)
                      < e/3"
      unfolding Cauchy_def by blast
    have "m n. mM; nM;
                 dist ((x,K)𝒟. content K *R f m x) ((x,K)𝒟. content K *R f n x) < e/3
                 dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
       by (metis δT dist_commute dist_triangle_third [OF _ _ δT])
    then show "M. mM. nM. dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
      using M by auto
  qed
  then obtain L where L: "(λn. integral (cbox a b) (f n))  L"
    by (meson convergent_eq_Cauchy)
  have "(g has_integral L) (cbox a b)"
  proof (clarsimp simp: has_integral)
    fix e::real assume "0 < e"
    then have e2: "0 < e/2"
      by simp
    then obtain γ where "gauge γ"
      and γ: "n 𝒟. 𝒟 tagged_division_of cbox a b; γ fine 𝒟
                     norm(((x,K)𝒟. content K *R f n x) - integral (cbox a b) (f n)) < e/2"
      using feq unfolding equiintegrable_on_def
      by (meson image_eqI iso_tuple_UNIV_I)
    moreover
    have "norm (((x,K)𝒟. content K *R g x) - L) < e"
              if "𝒟 tagged_division_of cbox a b" "γ fine 𝒟" for 𝒟
    proof -
      have "norm (((x,K)𝒟. content K *R g x) - L)  e/2"
      proof (rule Lim_norm_ubound)
        show "(λn. ((x,K)𝒟. content K *R f n x) - integral (cbox a b) (f n))  ((x,K)𝒟. content K *R g x) - L"
          using to_g that L
          by (intro tendsto_diff tendsto_sum) (auto simp: tag_in_interval tendsto_scaleR)
        show "F n in sequentially.
                norm (((x,K)  𝒟. content K *R f n x) - integral (cbox a b) (f n))  e/2"
          by (intro eventuallyI less_imp_le γ that)
      qed auto
      with 0 < e show ?thesis
        by linarith
    qed
    ultimately
    show "γ. gauge γ 
             (𝒟. 𝒟 tagged_division_of cbox a b  γ fine 𝒟 
                  norm (((x,K)𝒟. content K *R g x) - L) < e)"
      by meson
  qed
  with L show ?thesis
    by (simp add: (λn. integral (cbox a b) (f n))  L has_integral_integrable_integral)
qed


lemma equiintegrable_reflect:
  assumes "F equiintegrable_on cbox a b"
  shows "(λf. f  uminus) ` F equiintegrable_on cbox (-b) (-a)"
proof -
  have §: "γ. gauge γ 
            (f 𝒟. f  (λf. f  uminus) ` F  𝒟 tagged_division_of cbox (- b) (- a)  γ fine 𝒟 
                   norm (((x,K)  𝒟. content K *R f x) - integral (cbox (- b) (- a)) f) < e)"
       if "gauge γ" and
           γ: "f 𝒟. f  F; 𝒟 tagged_division_of cbox a b; γ fine 𝒟 
                     norm (((x,K)  𝒟. content K *R f x) - integral (cbox a b) f) < e" for e γ
  proof (intro exI, safe)
    show "gauge (λx. uminus ` γ (-x))"
      by (metis gauge γ gauge_reflect)
    show "norm (((x,K)  𝒟. content K *R (f  uminus) x) - integral (cbox (- b) (- a)) (f  uminus)) < e"
      if "f  F" and tag: "𝒟 tagged_division_of cbox (- b) (- a)"
         and fine: "(λx. uminus ` γ (- x)) fine 𝒟" for f 𝒟
    proof -
      have 1: "(λ(x,K). (- x, uminus ` K)) ` 𝒟 tagged_partial_division_of cbox a b"
        if "𝒟 tagged_partial_division_of cbox (- b) (- a)"
      proof -
        have "- y  cbox a b"
          if "x K. (x,K)  𝒟  x  K  K  cbox (- b) (- a)  (a b. K = cbox a b)"
             "(x, Y)  𝒟" "y  Y" for x Y y
        proof -
          have "y  uminus ` cbox a b"
            using that by auto
          then show "- y  cbox a b"
            by force
        qed
        with that show ?thesis
          by (fastforce simp: tagged_partial_division_of_def interior_negations image_iff)
      qed
      have 2: "K. (x. (x,K)  (λ(x,K). (- x, uminus ` K)) ` 𝒟)  x  K"
              if "{K. x. (x,K)  𝒟} = cbox (- b) (- a)" "x  cbox a b" for x
      proof -
        have xm: "x  uminus ` {A. a. (a, A)  𝒟}"
          by (simp add: that)
        then obtain a X where "-x  X" "(a, X)  𝒟"
          by auto
        then show ?thesis
          by (metis (no_types, lifting) add.inverse_inverse image_iff pair_imageI)
      qed
      have 3: "x X y. 𝒟 tagged_partial_division_of cbox (- b) (- a); (x, X)  𝒟; y  X  - y  cbox a b"
        by (metis (no_types, lifting) equation_minus_iff imageE subsetD tagged_partial_division_ofD(3) uminus_interval_vector)
      have tag': "(λ(x,K). (- x, uminus ` K)) ` 𝒟 tagged_division_of cbox a b"
        using tag  by (auto simp: tagged_division_of_def dest: 1 2 3)
      have fine': "γ fine (λ(x,K). (- x, uminus ` K)) ` 𝒟"
        using fine by (fastforce simp: fine_def)
      have inj: "inj_on (λ(x,K). (- x, uminus ` K)) 𝒟"
        unfolding inj_on_def by force
      have eq: "content (uminus ` I) = content I"
               if I: "(x, I)  𝒟" and fnz: "f (- x)  0" for x I
      proof -
        obtain a b where "I = cbox a b"
          using tag I that by (force simp: tagged_division_of_def tagged_partial_division_of_def)
        then show ?thesis
          using content_image_affinity_cbox [of "-1" 0] by auto
      qed
      have "((x,K)  (λ(x,K). (- x, uminus ` K)) ` 𝒟.  content K *R f x) =
            ((x,K)  𝒟. content K *R f (- x))"
        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: "𝒟 division_of S" and S: "S  cbox a b" and i: "i  Basis"
      and mt: "K. K  𝒟  content K  0"
      and disj: "(K  𝒟. K  {x. x  i = a  i}  {})  (K  𝒟. K  {x. x  i = b  i}  {})"
   shows "(b  i - a  i) * (K𝒟. content K / (interval_upperbound K  i - interval_lowerbound K  i))
           content(cbox a b)"   (is "?lhs  ?rhs")
proof -
  have "finite 𝒟"
    using div by blast
  define extend where
    "extend  λK. cbox (j  Basis. if j = i then (a  i) *R i else (interval_lowerbound K  j) *R j)
                       (j  Basis. if j = i then (b  i) *R i else (interval_upperbound K  j) *R j)"
  have div_subset_cbox: "K. K  𝒟  K  cbox a b"
    using S div by auto
  have "K. K  𝒟  K  {}"
    using div by blast
  have extend_cbox: "K.  K  𝒟  a b. extend K = cbox a b"
    using extend_def by blast
  have extend: "extend K  {}" "extend K  cbox a b" if K: "K  𝒟" for K
  proof -
    obtain u v where K: "K = cbox u v" "K  {}" "K  cbox a b"
      using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
    with i show "extend K  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  𝒟" "K2  𝒟" "K1  K2" for K1 K2
  proof -
    obtain u v where K1: "K1 = cbox u v" "K1  {}" "K1  cbox a b"
      using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
    obtain w z where K2: "K2 = cbox w z" "K2  {}" "K2  cbox a b"
      using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
    have cboxes: "cbox u v  𝒟" "cbox w z  𝒟" "cbox u v  cbox w z"
      using K1 K2 that by auto
    with div have "interior (cbox u v)  interior (cbox w z) = {}"
      by blast
    moreover
    have "x. x  box u v  x  box w z"
         if "x  interior (extend K1)" "x  interior (extend K2)" for x
    proof -
      have "a  i < x  i" "x  i < b  i"
       and ux: "k. k  Basis - {i}  u  k < x  k"
       and xv: "k. k  Basis - {i}  x  k < v  k"
       and wx: "k. k  Basis - {i}  w  k < x  k"
       and xz: "k. k  Basis - {i}  x  k < z  k"
        using that K1 K2 i by (auto simp: extend_def box_ne_empty mem_box)
      have "box u v  {}" "box w z  {}"
        using cboxes interior_cbox by (auto simp: content_eq_0_interior dest: mt)
      then obtain q s
        where q: "k. k  Basis  w  k < q  k  q  k < z  k"
          and s: "k. k  Basis  u  k < s  k  s  k < v  k"
        by (meson all_not_in_conv mem_box(1))
      show ?thesis  using disj
      proof
        assume "K𝒟. K  {x. x  i = a  i}  {}"
        then have uva: "(cbox u v)  {x. x  i = a  i}  {}"
             and  wza: "(cbox w z)  {x. x  i = a  i}  {}"
          using cboxes by (auto simp: content_eq_0_interior)
        then obtain r t where "r  i = a  i" and r: "k. k  Basis  w  k  r  k  r  k  z  k"
                        and "t  i = a  i" and t: "k. k  Basis  u  k  t  k  t  k  v  k"
          by (fastforce simp: mem_box)
        have u: "u  i < q  i"
          using i K2(1) K2(3) t  i = a  i q s t [OF i] by (force simp: subset_box)
        have w: "w  i < s  i"
          using i K1(1) K1(3) r  i = a  i s r [OF i] by (force simp: subset_box)
        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𝒟. 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𝒟. (b  i - a  i) * content K / (interv_diff K i))"
    by (simp add: sum_distrib_left interv_diff_def)
  also have " = sum (content  extend) 𝒟"
  proof (rule sum.cong [OF refl])
    fix K assume "K  𝒟"
    then obtain u v where K: "K = cbox u v" "cbox u v  {}" "K  cbox a b"
      using cbox_division_memE [OF _ div] div_subset_cbox by metis
    then have uv: "u  i < v  i"
      using mt [OF K  𝒟] i  Basis content_eq_0 by fastforce
    have "insert i (Basis  -{i}) = Basis"
      using i  Basis by auto
    then have "(b  i - a  i) * content K / (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 "... = (xBasis. 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 "... = (kBasis.
                        (jBasis. 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 "... = (kBasis.
                        (jBasis. if j = i then (b  i) *R i else (interval_upperbound (cbox u v)  j) *R j)  k -
                        (jBasis. 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  𝒟 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 ` 𝒟)"
  proof -
    have "K1  𝒟; K2  𝒟; K1  K2; extend K1 = extend K2  content (extend K1) = 0" for K1 K2
      using int_extend_disjoint [of K1 K2] extend_def by (simp add: content_eq_0_interior)
    then show ?thesis
      by (simp add: comm_monoid_add_class.sum.reindex_nontrivial [OF finite 𝒟])
  qed
  also have "...  ?rhs"
  proof (rule subadditive_content_division)
    show "extend ` 𝒟 division_of  (extend ` 𝒟)"
      using int_extend_disjoint  by (auto simp: division_of_def finite 𝒟 extend extend_cbox)
    show " (extend ` 𝒟)  cbox a b"
      using extend by fastforce
  qed
  finally show ?thesis .
qed


proposition sum_content_area_over_thin_division:
  assumes div: "𝒟 division_of S" and S: "S  cbox a b" and i: "i  Basis"
    and "a  i  c" "c  b  i"
    and nonmt: "K. K  𝒟  K  {x. x  i = c}  {}"
  shows "(b  i - a  i) * (K𝒟. content K / (interval_upperbound K  i - interval_lowerbound K  i))
           2 * content(cbox a b)"
proof (cases "content(cbox a b) = 0")
  case True
  have "(K𝒟. content K / (interval_upperbound K  i - interval_lowerbound K  i)) = 0"
    using S div by (force intro!: sum.neutral content_0_subset [OF True])
  then show ?thesis
    by (auto simp: True)
next
  case False
  then have "content(cbox a b) > 0"
    using zero_less_measure_iff by blast
  then have "a  i < b  i" if "i  Basis" for i
    using content_pos_lt_eq that by blast
  have "finite 𝒟"
    using div by blast
  define Dlec where "Dlec  {L  (λL. L  {x. x  i  c}) ` 𝒟. content L  0}"
  define Dgec where "Dgec  {L  (λL. L  {x. x  i  c}) ` 𝒟. content L  0}"
  define a' where "a'  (jBasis. (if j = i then c else a  j) *R j)"
  define b' where "b'  (jBasis. (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  𝒟  a b. L  {x. x  i  c} = cbox a b" for L
    using Dlec_def by blast
  have Dgec_cbox: "K. K  Dgec  a b. K = cbox a b"
    using interval_split [OF i] div by (fastforce simp: Dgec_def division_of_def)
  then have gec_is_cbox: "content (L  {x. x  i  c})  0; L  𝒟  a b. L  {x. x  i  c} = cbox a b" for L
    using Dgec_def by blast

  have zero_left: "x y. x  𝒟; y  𝒟; 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  𝒟; y  𝒟; 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) * (KDlec. 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 𝒟 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 "(KDlec. K  {x. x  i = a  i}  {})  (KDlec. 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 "(KDlec. content K / (interv_diff K i)) = (K(λK. K  {x. x  i  c}) ` 𝒟. content K / interv_diff K i)"
    unfolding Dlec_def using finite 𝒟 by (auto simp: sum.mono_neutral_left)
  moreover have "... =
        (K𝒟. ((λK. content K / (interv_diff K i))  ((λK. K  {x. x  i  c}))) K)"
    by (simp add: zero_left sum.reindex_nontrivial [OF finite 𝒟])
  moreover have "(b'  i - a  i) = (c - a  i)"
    by (simp add: b'_def i)
  ultimately
  have lec: "(c - a  i) * (K𝒟. ((λ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) * (KDgec. 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 𝒟 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 "(KDgec. K  {x. x  i = a'  i}  {})  (KDgec. 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 "(KDgec. content K / (interv_diff K i)) = (K(λK. K  {x. c  x  i}) ` 𝒟.
       content K / interv_diff K i)"
    unfolding Dgec_def using finite 𝒟 by (auto simp: sum.mono_neutral_left)
  moreover have " =
        (K𝒟. ((λK. content K / (interv_diff K i))  ((λK. K  {x. x  i  c}))) K)"
    by (simp add: zero_right sum.reindex_nontrivial [OF finite 𝒟])
  moreover have "(b  i - a'  i) = (b  i - c)"
    by (simp add: a'_def i)
  ultimately
  have gec: "(b  i - c) * (K𝒟. ((λ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 "(jBasis. (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𝒟. content (K  {x. a  i  x  i}) / interv_diff (K  {x. a  i  x  i}) i)
              = (K𝒟. content K / interv_diff K i)"
        (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K  𝒟"
        then have "a  i  x  i" if "x  K" for x
          by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
        then have "K  {x. a  i  x  i} = K"
          by blast
        then show "?f K = ?g K"
          by simp
      qed
      ultimately show ?thesis
        using gec c eq interv_diff_def by auto
    next
      assume c: "c = b  i"
      moreover have "(jBasis. (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𝒟. content (K  {x. x  i  b  i}) / interv_diff (K  {x. x  i  b  i}) i)
              = (K𝒟. content K / interv_diff K i)"
               (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K  𝒟"
        then have "x  i  b  i" if "x  K" for x
          by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
        then have "K  {x. x  i  b  i} = K"
          by blast
        then show "?f K = ?g K"
          by simp
      qed
      ultimately show ?thesis
        using lec c eq interv_diff_def by auto
    qed
  next
    case False
    have prod_if: "(kBasis  - {i}. f k) = (kBasis. 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𝒟. ((λK. content K / (interv_diff K i))  ((λK. K  {x. x  i  c}))) K)
                   content(cbox a b') / (c - a  i)"
              "(K𝒟. ((λ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𝒟. content K / (interv_diff K i))
           (K𝒟. ((λK. content K / (interv_diff K i))  ((λK. K  {x. x  i  c}))) K) +
            (K𝒟. ((λK. content K / (interv_diff K i))  ((λK. K  {x. x  i  c}))) K)"
           (is "?lhs  ?rhs")
    proof -
      have "?lhs 
            (K𝒟. ((λ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  𝒟"
        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  𝒟 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𝒟. 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  ai < bi"
    by (auto simp: content_pos_lt_eq)
  obtain γ0 where "gauge γ0"
            and γ0: "S h. S tagged_partial_division_of cbox a b; γ0 fine S; h  F
                            ((x,K)  S. norm (content K *R h x - integral K h)) < ε/2"
  proof -
    obtain γ where "gauge γ"
               and γ: "f 𝒟. f  F; 𝒟 tagged_division_of cbox a b; γ fine 𝒟
                               norm (((x,K)  𝒟. content K *R f x) - integral (cbox a b) f)
                                  < ε/(5 * (Suc DIM('b)))"
    proof -
      have e5: "ε/(5 * (Suc DIM('b))) > 0"
        using ε > 0 by auto
      then show ?thesis
        using F that by (auto simp: equiintegrable_on_def)
    qed
    show ?thesis
    proof
      show "gauge γ"
        by (rule gauge γ)
      show "((x,K)  S. norm (content K *R h x - integral K h)) < ε/2"
           if "S tagged_partial_division_of cbox a b" "γ fine S" "h  F" for S h
      proof -
        have "((x,K)  S. norm (content K *R h x - integral K h))  2 * real DIM('b) * (ε/(5 * Suc DIM('b)))"
        proof (rule Henstock_lemma_part2 [of h a b])
          show "h integrable_on cbox a b"
            using that F equiintegrable_on_def by metis
          show "gauge γ"
            by (rule gauge γ)
        qed (use that ε > 0 γ in auto)
        also have "... < ε/2"
          using ε > 0 by (simp add: divide_simps)
        finally show ?thesis .
      qed
    qed
  qed
  define γ where "γ  λx. γ0 x 
                          ball x ((ε/8 / (norm(f x) + 1)) * (INF mBasis. 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 mBasis. b  m - a  m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
    using 0 < content (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 mBasis. 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 mBasis. b  m - a  m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
                 "dist x v < ε * (INF mBasis. 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 mBasis. 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 mBasis. 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 "... = (Ksnd ` 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)) * (Ksnd ` 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) * (Ksnd ` 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)) * (Ksnd ` 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  (iBasis. c. hF. {λ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 < b  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 *: "(iBasis. 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) `
            (iBasis. c. hF. {λx. if x  i  c then (h  uminus) x else 0}) =
            (iBasis. c. hF. {λ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 *: "(iBasis. c. hF. {λ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 *: "(iBasis. c. hF. {λ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 iB. 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  (iBasis.
                ξ. hinsert f (iBasis. ψ. hinsert 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 (iBasis. ξ. hinsert 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 (iBasis. ξ. hinsert 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 jinsert 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. mn. 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 < B 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 < N have "k > 0"
          by linarith
        have xa_gt: "(x - a)  i > ((b - a)  i) / (real k)" if "i  Basis" for i
        proof -
          have *: "Inf Δ  ((x - a)  i) / ((b - a)  i)"
            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]: "xcbox 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]: "xcbox 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 < a 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 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 σ :: "natnat"
    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 "nN" 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. nN. ¦ψ 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