SSL Improper_Integral.thy Sprache: Isabelle

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

section \<open>Continuity of the indefinite integral; improper integral theorem\<close>

theory "Improper_Integral"(*  Title:      HOL/Analysis/Improper_Integral.thy
  imports Equivalence_Lebesgue_Henstock_Integration
begin

subsection \<open>Equiintegrability\<close>

text\<open>The definition here only really makes sense for an elementary set.
     We just use compact intervals in applications below.\<close>

definition\<^marker>\<open>tag important\<close> equiintegrable_on (infixr \<open>equiintegrable'_on\<close> 46)
  where "F equiintegrable_on I \<equiv>
         (\<forall>f \<in> F. f integrable_on I) \<and>
         (\<forall>e > 0. \<exists>\<gamma>. gauge \<gamma> \<and>
                    (\<forall>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma> fine \<D>
                          \<longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < e))"

lemma equiintegrable_on_integrable:
     "\<lbrakk>F equiintegrable_on I; f \<in> F\<rbrakk> \<Longrightarrow> f integrable_on I"
  using equiintegrable_on_def by metis

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

lemma equiintegrable_on_subset: "\<lbrakk>F equiintegrable_on I; G \<subseteq> F\<rbrakk> \<Longrightarrow> 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 \<union> G) equiintegrable_on I"
  unfolding equiintegrable_on_def
proof (intro conjI impI allI)
  show "\<forall>f\<in>F \<union> G. f integrable_on I"
    using assms unfolding equiintegrable_on_def by blast
  show "\<exists>\<gamma>. gauge \<gamma> \<and>
            (\<forall>f \<D>. f \<in> F \<union> G \<and>
                   \<D> tagged_division_of I \<and> \<gamma> fine \<D> \<longrightarrow>
                   norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
         if "\<epsilon> > 0" for \<epsilon>
  proof -
    obtain \<gamma>1 where "gauge \<gamma>1"
      and \<gamma>1: "\<And>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma>1 fine \<D>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by auto
    obtain \<gamma>2 where  "gauge \<gamma>2"
      and \<gamma>2: "\<And>f \<D>. f \<in> G \<and> \<D> tagged_division_of I \<and> \<gamma>2 fine \<D>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by auto
    have "gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
      using \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close> by blast
    moreover have "\<forall>f \<D>. f \<in> F \<union> G \<and> \<D> tagged_division_of I \<and> (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x) fine \<D> \<longrightarrow>
          norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
      using \<gamma>1 \<gamma>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 "(\<Union>c \<in> {-k..k}. \<Union>f \<in> F. {(\<lambda>x. c *\<^sub>R f x)}) equiintegrable_on I"
  unfolding equiintegrable_on_def
  proof (intro conjI impI allI ballI)
  show "f integrable_on I"
    if "f \<in> (\<Union>c\<in>{- k..k}. \<Union>f\<in>F. {\<lambda>x. c *\<^sub>R f x})"
    for f :: "'a \<Rightarrow> 'b"
    using that assms equiintegrable_on_integrable integrable_cmul by blast
  show "\<exists>\<gamma>. gauge \<gamma> \<and> (\<forall>f \<D>. f \<in> (\<Union>c\<in>{- k..k}. \<Union>f\<in>F. {\<lambda>x. c *\<^sub>R f x}) \<and> \<D> tagged_division_of I
          \<and> \<gamma> fine \<D> \<longrightarrow> norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
    if "\<epsilon> > 0" for \<epsilon>
  proof -
    obtain \<gamma> where "gauge \<gamma>"
      and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of I; \<gamma> fine \<D>\<rbrakk>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon> / (\<bar>k\<bar> + 1)"
      using assms \<open>\<epsilon> > 0\<close> 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 ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R c *\<^sub>R (f x)) - integral I (\<lambda>x. c *\<^sub>R f x)) < \<epsilon>"
      if c: "c \<in> {- k..k}"
        and "f \<in> F" "\<D> tagged_division_of I" "\<gamma> fine \<D>"
      for \<D> c f
    proof -
      have "norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R c *\<^sub>R f x) - integral I (\<lambda>x. c *\<^sub>R f x))
          = \<bar>c\<bar> * norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R f x) - integral I f)"
        by (simp add: algebra_simps scale_sum_right case_prod_unfold flip: norm_scaleR)
      also have "\<dots> \<le> (\<bar>k\<bar> + 1) * norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R f x) - integral I f)"
        using c by (auto simp: mult_right_mono)
      also have "\<dots> < (\<bar>k\<bar> + 1) * (\<epsilon> / (\<bar>k\<bar> + 1))"
        by (rule mult_strict_left_mono) (use \<gamma> less_eq_real_def that in auto)
      also have "\<dots> = \<epsilon>"
        by auto
      finally show ?thesis .
    qed
    ultimately show ?thesis
      by (rule_tac x="\<gamma>" in exI) auto
  qed
qed

lemma equiintegrable_add:
  assumes F: "F equiintegrable_on I" and G: "G equiintegrable_on I"
  shows "(\<Union>f \<in> F. \<Union>g \<in> G. {(\<lambda>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 \<in> (\<Union>f\<in>F. \<Union>g\<in>G. {\<lambda>x. f x + g x})" for f
    using that equiintegrable_on_integrable assms  by (auto intro: integrable_add)
  show "\<exists>\<gamma>. gauge \<gamma> \<and> (\<forall>f \<D>. f \<in> (\<Union>f\<in>F. \<Union>g\<in>G. {\<lambda>x. f x + g x}) \<and> \<D> tagged_division_of I
          \<and> \<gamma> fine \<D> \<longrightarrow> norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
    if "\<epsilon> > 0" for \<epsilon>
  proof -
    obtain \<gamma>1 where "gauge \<gamma>1"
      and \<gamma>1: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of I; \<gamma>1 fine \<D>\<rbrakk>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>/2"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    obtain \<gamma>2 where  "gauge \<gamma>2"
      and \<gamma>2: "\<And>g \<D>. \<lbrakk>g \<in> G; \<D> tagged_division_of I; \<gamma>2 fine \<D>\<rbrakk>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral I g) < \<epsilon>/2"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    have "gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
      using \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close> by blast
    moreover have "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R h x) - integral I h) < \<epsilon>"
      if h: "h \<in> (\<Union>f\<in>F. \<Union>g\<in>G. {\<lambda>x. f x + g x})"
        and \<D>: "\<D> tagged_division_of I" and fine: "(\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x) fine \<D>"
      for h \<D>
    proof -
      obtain f g where "f \<in> F" "g \<in> G" and heq: "h = (\<lambda>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 ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R h x) - integral I h)
          = norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x + content K *\<^sub>R g x) - (integral I f + integral I g))"
        by (simp add: heq algebra_simps integral_add int)
      also have "\<dots> = norm (((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f + (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral I g))"
        by (simp add: sum.distrib algebra_simps case_prod_unfold)
      also have "\<dots> \<le> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) + norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral I g)"
        by (metis (mono_tags) add_diff_eq norm_triangle_ineq)
      also have "\<dots> < \<epsilon>/2 + \<epsilon>/2"
        using \<gamma>1 [OF \<open>f \<in> F\<close> \<D>] \<gamma>2 [OF \<open>g \<in> G\<close> \<D>] fine  by (simp add: fine_Int)
      finally show ?thesis by simp
    qed
    ultimately show ?thesis
      by meson
  qed
qed

lemma equiintegrable_minus:
  assumes "F equiintegrable_on I"
  shows "(\<Union>f \<in> F. {(\<lambda>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 "(\<Union>f \<in> F. \<Union>g \<in> G. {(\<lambda>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 \<Rightarrow> 'b::euclidean_space) set"
  assumes "F equiintegrable_on cbox a b"
  shows "(\<Union>I \<in> Collect finite. \<Union>c \<in> {c. (\<forall>i \<in> I. c i \<ge> 0) \<and> sum c I = 1}.
          \<Union>f \<in> I \<rightarrow> F. {(\<lambda>x. sum (\<lambda>i::'j. c i *\<^sub>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 \<in> ?G" for f
    using that assms by (auto simp: equiintegrable_on_def intro!: integrable_sum integrable_cmul)
  show "\<exists>\<gamma>. gauge \<gamma>
           \<and> (\<forall>g \<D>. g \<in> ?G \<and> \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D>
              \<longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral (cbox a b) g) < \<epsilon>)"
    if "\<epsilon> > 0" for \<epsilon>
  proof -
    obtain \<gamma> where "gauge \<gamma>"
      and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f) < \<epsilon> / 2"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
    moreover have "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral (cbox a b) g) < \<epsilon>"
      if g: "g \<in> ?G"
        and \<D>: "\<D> tagged_division_of cbox a b"
        and fine: "\<gamma> fine \<D>"
      for \<D> g
    proof -
      obtain I c f where "finite I" and 0: "\<And>i::'j. i \<in> I \<Longrightarrow> 0 \<le> c i"
        and 1: "sum c I = 1" and f: "f \<in> I \<rightarrow> F" and geq: "g = (\<lambda>x. \<Sum>i\<in>I. c i *\<^sub>R f i x)"
        using g by auto
      have fi_int: "f i integrable_on cbox a b" if "i \<in> I" for i
        by (metis Pi_iff assms equiintegrable_on_def f that)
      have *: "integral (cbox a b) (\<lambda>x. c i *\<^sub>R f i x) = (\<Sum>(x, K)\<in>\<D>. integral K (\<lambda>x. c i *\<^sub>R f i x))"
        if "i \<in> I" for i
      proof -
        have "f i integrable_on cbox a b"
          by (metis Pi_iff assms equiintegrable_on_def f that)
        then show ?thesis
          by (intro \<D> integrable_cmul integral_combine_tagged_division_topdown)
      qed
      have "finite \<D>"
        using \<D> by blast
      have swap: "(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R (\<Sum>i\<in>I. c i *\<^sub>R f i x))
            = (\<Sum>i\<in>I. c i *\<^sub>R (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f i x))"
        by (simp add: scale_sum_right case_prod_unfold algebra_simps) (rule sum.swap)
      have "norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R g x) - integral (cbox a b) g)
          = norm ((\<Sum>i\<in>I. c i *\<^sub>R ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>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 \<open>finite I\<close> sum_subtractf flip: sum_diff)
      also have "\<dots> \<le> (\<Sum>i\<in>I. c i * \<epsilon> / 2)"
      proof (rule sum_norm_le)
        show "norm (c i *\<^sub>R ((\<Sum>(xa, K)\<in>\<D>. content K *\<^sub>R f i xa) - integral (cbox a b) (f i))) \<le> c i * \<epsilon> / 2"
          if "i \<in> I" for i
        proof -
          have "norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f i x) - integral (cbox a b) (f i)) \<le> \<epsilon>/2"
            using \<gamma> [OF _ \<D> fine, of "f i"] funcset_mem [OF f] that  by auto
          then show ?thesis
            using that by (auto simp: 0 mult.assoc intro: mult_left_mono)
        qed
      qed
      also have "\<dots> < \<epsilon>"
        using 1 \<open>\<epsilon> > 0\<close> by (simp add: flip: sum_divide_distrib sum_distrib_right)
      finally show ?thesis .
    qed
    ultimately show ?thesis
      by (rule_tac x="\<gamma>" in exI) auto
  qed
qed

corollary equiintegrable_sum_real:
  fixes F :: "(real \<Rightarrow> 'b::euclidean_space) set"
  assumes "F equiintegrable_on {a..b}"
  shows "(\<Union>I \<in> Collect finite. \<Union>c \<in> {c. (\<forall>i \<in> I. c i \<ge> 0) \<and> sum c I = 1}.
          \<Union>f \<in> I \<rightarrow> F. {(\<lambda>x. sum (\<lambda>i. c i *\<^sub>R f i x) I)})
         equiintegrable_on {a..b}"
  using equiintegrable_sum [of F a b] assms by auto

text\<open> Basic combining theorems for the interval of integration.\<close>

lemma equiintegrable_on_null [simp]:
   "content(cbox a b) = 0 \<Longrightarrow> 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\<open> Main limit theorem for an equiintegrable sequence.\<close>

theorem equiintegrable_limit:
  fixes g :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
  assumes feq: "range f equiintegrable_on cbox a b"
      and to_g: "\<And>x. x \<in> cbox a b \<Longrightarrow> (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
    shows "g integrable_on cbox a b \<and> (\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> integral (cbox a b) g"
proof -
  have "Cauchy (\<lambda>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 \<gamma> where "gauge \<gamma>"
         and \<gamma>: "\<And>n \<D>. \<lbrakk>\<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
                       \<Longrightarrow> norm((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) < e/3"
      using feq unfolding equiintegrable_on_def
      by (meson image_eqI iso_tuple_UNIV_I)
    obtain \<D> where \<D>: "\<D> tagged_division_of (cbox a b)" and "\<gamma> fine \<D>"  "finite \<D>"
      by (meson \<open>gauge \<gamma>\<close> fine_division_exists tagged_division_of_finite)
    with \<gamma> have \<delta>T: "\<And>n. dist ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x)) (integral (cbox a b) (f n)) < e/3"
      by (force simp: dist_norm)
    have "(\<lambda>n. \<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x) \<longlonglongrightarrow> (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x)"
      using \<D> to_g by (auto intro!: tendsto_sum tendsto_scaleR)
    then have "Cauchy (\<lambda>n. \<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x)"
      by (meson convergent_eq_Cauchy)
    with e3 obtain M where
      M: "\<And>m n. \<lbrakk>m\<ge>M; n\<ge>M\<rbrakk> \<Longrightarrow> dist (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f m x) (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x)
                      < e/3"
      unfolding Cauchy_def by blast
    have "\<And>m n. \<lbrakk>m\<ge>M; n\<ge>M;
                 dist (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f m x) (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x) < e/3\<rbrakk>
                \<Longrightarrow> dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
       by (metis \<delta>T dist_commute dist_triangle_third [OF _ _ \<delta>T])
    then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
      using M by auto
  qed
  then obtain L where L: "(\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> 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 \<gamma> where "gauge \<gamma>"
      and \<gamma>: "\<And>n \<D>. \<lbrakk>\<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
                    \<Longrightarrow> norm((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>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 ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L) < e"
              if "\<D> tagged_division_of cbox a b" "\<gamma> fine \<D>" for \<D>
    proof -
      have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L) \<le> e/2"
      proof (rule Lim_norm_ubound)
        show "(\<lambda>n. (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) \<longlonglongrightarrow> (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L"
          using to_g that L
          by (intro tendsto_diff tendsto_sum) (auto simp: tag_in_interval tendsto_scaleR)
        show "\<forall>\<^sub>F n in sequentially.
                norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) \<le> e/2"
          by (intro eventuallyI less_imp_le \<gamma> that)
      qed auto
      with \<open>0 < e\<close> show ?thesis
        by linarith
    qed
    ultimately
    show "\<exists>\<gamma>. gauge \<gamma> \<and>
             (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
                  norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L) < e)"
      by meson
  qed
  with L show ?thesis
    by (simp add: \<open>(\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> L\<close> has_integral_integrable_integral)
qed

lemma equiintegrable_reflect:
  assumes "F equiintegrable_on cbox a b"
  shows "(\<lambda>f. f \<circ> uminus) ` F equiintegrable_on cbox (-b) (-a)"
proof -
  have \<section>: "\<exists>\<gamma>. gauge \<gamma> \<and>
            (\<forall>f \<D>. f \<in> (\<lambda>f. f \<circ> uminus) ` F \<and> \<D> tagged_division_of cbox (- b) (- a) \<and> \<gamma> fine \<D> \<longrightarrow>
                   norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)"
       if "gauge \<gamma>" and
           \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk> \<Longrightarrow>
                     norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f) < e" for e \<gamma>
  proof (intro exI, safe)
    show "gauge (\<lambda>x. uminus ` \<gamma> (-x))"
      by (metis \<open>gauge \<gamma>\<close> gauge_reflect)
    show "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R (f \<circ> uminus) x) - integral (cbox (- b) (- a)) (f \<circ> uminus)) < e"
      if "f \<in> F" and tag: "\<D> tagged_division_of cbox (- b) (- a)"
         and fine: "(\<lambda>x. uminus ` \<gamma> (- x)) fine \<D>" for f \<D>
    proof -
      have 1: "(\<lambda>(x,K). (- x, uminus ` K)) ` \<D> tagged_partial_division_of cbox a b"
        if "\<D> tagged_partial_division_of cbox (- b) (- a)"
      proof -
        have "- y \<in> cbox a b"
          if "\<And>x K. (x,K) \<in> \<D> \<Longrightarrow> x \<in> K \<and> K \<subseteq> cbox (- b) (- a) \<and> (\<exists>a b. K = cbox a b)"
             "(x, Y) \<in> \<D>" "y \<in> Y" for x Y y
        proof -
          have "y \<in> uminus ` cbox a b"
            using that by auto
          then show "- y \<in> 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: "\<exists>K. (\<exists>x. (x,K) \<in> (\<lambda>(x,K). (- x, uminus ` K)) ` \<D>) \<and> x \<in> K"
              if "\<Union>{K. \<exists>x. (x,K) \<in> \<D>} = cbox (- b) (- a)" "x \<in> cbox a b" for x
      proof -
        have xm: "x \<in> uminus ` \<Union>{A. \<exists>a. (a, A) \<in> \<D>}"
          by (simp add: that)
        then obtain a X where "-x \<in> X" "(a, X) \<in> \<D>"
          by auto
        then show ?thesis
          by (metis (no_types, lifting) add.inverse_inverse image_iff pair_imageI)
      qed
      have 3: "\<And>x X y. \<lbrakk>\<D> tagged_partial_division_of cbox (- b) (- a); (x, X) \<in> \<D>; y \<in> X\<rbrakk> \<Longrightarrow> - y \<in> cbox a b"
        by (metis (no_types, lifting) equation_minus_iff imageE subsetD tagged_partial_division_ofD(3) uminus_interval_vector)
      have tag': "(\<lambda>(x,K). (- x, uminus ` K)) ` \<D> tagged_division_of cbox a b"
        using tag  by (auto simp: tagged_division_of_def dest: 1 2 3)
      have fine': "\<gamma> fine (\<lambda>(x,K). (- x, uminus ` K)) ` \<D>"
        using fine by (fastforce simp: fine_def)
      have inj: "inj_on (\<lambda>(x,K). (- x, uminus ` K)) \<D>"
        unfolding inj_on_def by force
      have eq: "content (uminus ` I) = content I"
               if I: "(x, I) \<in> \<D>" and fnz: "f (- x) \<noteq> 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 "(\<Sum>(x,K) \<in> (\<lambda>(x,K). (- x, uminus ` K)) ` \<D>.  content K *\<^sub>R f x) =
            (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f (- x))"
        by (auto simp add: eq sum.reindex [OF inj] intro!: sum.cong)
      then show ?thesis
        using \<gamma> [OF \<open>f \<in> F\<close> 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 \<section> by fastforce
qed

subsection\<open>Subinterval restrictions for equiintegrable families\<close>

text\<open>First, some technical lemmas about minimizing a "flat" part of a sum over a division.\<close>

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

lemma content_division_lemma1:
  assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
      and mt: "\<And>K. K \<in> \<D> \<Longrightarrow> content K \<noteq> 0"
      and disj: "(\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}) \<or> (\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {})"
   shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
          \<le> content(cbox a b)"   (is "?lhs \<le> ?rhs")
proof -
  have "finite \<D>"
    using div by blast
  define extend where
    "extend \<equiv> \<lambda>K. cbox (\<Sum>j \<in> Basis. if j = i then (a \<bullet> i) *\<^sub>R i else (interval_lowerbound K \<bullet> j) *\<^sub>R j)
                       (\<Sum>j \<in> Basis. if j = i then (b \<bullet> i) *\<^sub>R i else (interval_upperbound K \<bullet> j) *\<^sub>R j)"
  have div_subset_cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<subseteq> cbox a b"
    using S div by auto
  have "\<And>K. K \<in> \<D> \<Longrightarrow> K \<noteq> {}"
    using div by blast
  have extend_cbox: "\<And>K.  K \<in> \<D> \<Longrightarrow> \<exists>a b. extend K = cbox a b"
    using extend_def by blast
  have extend: "extend K \<noteq> {}" "extend K \<subseteq> cbox a b" if K: "K \<in> \<D>" for K
  proof -
    obtain u v where K: "K = cbox u v" "K \<noteq> {}" "K \<subseteq> cbox a b"
      using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
    with i show "extend K \<subseteq> cbox a b"
      by (auto simp: extend_def subset_box box_ne_empty)
    have "a \<bullet> i \<le> b \<bullet> i"
      using K by (metis bot.extremum_uniqueI box_ne_empty(1) i)
    with K show "extend K \<noteq> {}"
      by (simp add: extend_def i box_ne_empty)
  qed
  have int_extend_disjoint:
       "interior(extend K1) \<inter> interior(extend K2) = {}" if K: "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2" for K1 K2
  proof -
    obtain u v where K1: "K1 = cbox u v" "K1 \<noteq> {}" "K1 \<subseteq> 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 \<noteq> {}" "K2 \<subseteq> cbox a b"
      using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
    have cboxes: "cbox u v \<in> \<D>" "cbox w z \<in> \<D>" "cbox u v \<noteq> cbox w z"
      using K1 K2 that by auto
    with div have "interior (cbox u v) \<inter> interior (cbox w z) = {}"
      by blast
    moreover
    have "\<exists>x. x \<in> box u v \<and> x \<in> box w z"
         if "x \<in> interior (extend K1)" "x \<in> interior (extend K2)" for x
    proof -
      have "a \<bullet> i < x \<bullet> i" "x \<bullet> i < b \<bullet> i"
       and ux: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> u \<bullet> k < x \<bullet> k"
       and xv: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> x \<bullet> k < v \<bullet> k"
       and wx: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> w \<bullet> k < x \<bullet> k"
       and xz: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> x \<bullet> k < z \<bullet> k"
        using that K1 K2 i by (auto simp: extend_def box_ne_empty mem_box)
      have "box u v \<noteq> {}" "box w z \<noteq> {}"
        using cboxes interior_cbox by (auto simp: content_eq_0_interior dest: mt)
      then obtain q s
        where q: "\<And>k. k \<in> Basis \<Longrightarrow> w \<bullet> k < q \<bullet> k \<and> q \<bullet> k < z \<bullet> k"
          and s: "\<And>k. k \<in> Basis \<Longrightarrow> u \<bullet> k < s \<bullet> k \<and> s \<bullet> k < v \<bullet> k"
        by (meson all_not_in_conv mem_box(1))
      show ?thesis  using disj
      proof
        assume "\<forall>K\<in>\<D>. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}"
        then have uva: "(cbox u v) \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}"
             and  wza: "(cbox w z) \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}"
          using cboxes by (auto simp: content_eq_0_interior)
        then obtain r t where "r \<bullet> i = a \<bullet> i" and r: "\<And>k. k \<in> Basis \<Longrightarrow> w \<bullet> k \<le> r \<bullet> k \<and> r \<bullet> k \<le> z \<bullet> k"
                        and "t \<bullet> i = a \<bullet> i" and t: "\<And>k. k \<in> Basis \<Longrightarrow> u \<bullet> k \<le> t \<bullet> k \<and> t \<bullet> k \<le> v \<bullet> k"
          by (fastforce simp: mem_box)
        have u: "u \<bullet> i < q \<bullet> i"
          using i K2(1) K2(3) \<open>t \<bullet> i = a \<bullet> i\<close> q s t [OF i] by (force simp: subset_box)
        have w: "w \<bullet> i < s \<bullet> i"
          using i K1(1) K1(3) \<open>r \<bullet> i = a \<bullet> i\<close> s r [OF i] by (force simp: subset_box)
        define \<xi> where "\<xi> \<equiv> (\<Sum>j \<in> Basis. if j = i then min (q \<bullet> i) (s \<bullet> i) *\<^sub>R i else (x \<bullet> j) *\<^sub>R j)"
        have [simp]: "\<xi> \<bullet> j = (if j = i then min (q \<bullet> j) (s \<bullet> j) else x \<bullet> j)" if "j \<in> Basis" for j
          unfolding \<xi>_def
          by (intro sum_if_inner that \<open>i \<in> Basis\<close>)
        show ?thesis
        proof (intro exI conjI)
          have "min (q \<bullet> i) (s \<bullet> i) < v \<bullet> i"
            using i s by fastforce
          with \<open>i \<in> Basis\<close> s u ux xv
          show "\<xi> \<in> box u v"
            by (force simp: mem_box)
          have "min (q \<bullet> i) (s \<bullet> i) < z \<bullet> i"
            using i q by force
          with \<open>i \<in> Basis\<close> q w wx xz
          show "\<xi> \<in> box w z"
            by (force simp: mem_box)
        qed
      next
        assume "\<forall>K\<in>\<D>. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {}"
        then have uva: "(cbox u v) \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {}"
             and  wza: "(cbox w z) \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {}"
          using cboxes by (auto simp: content_eq_0_interior)
        then obtain r t where "r \<bullet> i = b \<bullet> i" and r: "\<And>k. k \<in> Basis \<Longrightarrow> w \<bullet> k \<le> r \<bullet> k \<and> r \<bullet> k \<le> z \<bullet> k"
                        and "t \<bullet> i = b \<bullet> i" and t: "\<And>k. k \<in> Basis \<Longrightarrow> u \<bullet> k \<le> t \<bullet> k \<and> t \<bullet> k \<le> v \<bullet> k"
          by (fastforce simp: mem_box)
        have z: "s \<bullet> i < z \<bullet> i"
          using K1(1) K1(3) \<open>r \<bullet> i = b \<bullet> i\<close> r [OF i] i s  by (force simp: subset_box)
        have v: "q \<bullet> i < v \<bullet> i"
          using K2(1) K2(3) \<open>t \<bullet> i = b \<bullet> i\<close> t [OF i] i q  by (force simp: subset_box)
        define \<xi> where "\<xi> \<equiv> (\<Sum>j \<in> Basis. if j = i then max (q \<bullet> i) (s \<bullet> i) *\<^sub>R i else (x \<bullet> j) *\<^sub>R j)"
        have [simp]: "\<xi> \<bullet> j = (if j = i then max (q \<bullet> j) (s \<bullet> j) else x \<bullet> j)" if "j \<in> Basis" for j
          unfolding \<xi>_def
          by (intro sum_if_inner that \<open>i \<in> Basis\<close>)
        show ?thesis
        proof (intro exI conjI)
          show "\<xi> \<in> box u v"
            using \<open>i \<in> Basis\<close> s by (force simp: mem_box ux v xv)
          show "\<xi> \<in> box w z"
            using \<open>i \<in> Basis\<close> q by (force simp: mem_box wx xz z)
        qed
      qed
    qed
    ultimately show ?thesis by auto
  qed
  define interv_diff where "interv_diff \<equiv> \<lambda>K. \<lambda>i::'a. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i"
  have "?lhs = (\<Sum>K\<in>\<D>. (b \<bullet> i - a \<bullet> i) * content K / (interv_diff K i))"
    by (simp add: sum_distrib_left interv_diff_def)
  also have "\<dots> = sum (content \<circ> extend) \<D>"
  proof (rule sum.cong [OF refl])
    fix K assume "K \<in> \<D>"
    then obtain u v where K: "K = cbox u v" "cbox u v \<noteq> {}" "K \<subseteq> cbox a b"
      using cbox_division_memE [OF _ div] div_subset_cbox by metis
    then have uv: "u \<bullet> i < v \<bullet> i"
      using mt [OF \<open>K \<in> \<D>\<close>] \<open>i \<in> Basis\<close> content_eq_0 by fastforce
    have "insert i (Basis \<inter> -{i}) = Basis"
      using \<open>i \<in> Basis\<close> by auto
    then have "(b \<bullet> i - a \<bullet> i) * content K / (interv_diff K i)
             = (b \<bullet> i - a \<bullet> i) * (\<Prod>i \<in> insert i (Basis \<inter> -{i}). v \<bullet> i - u \<bullet> i) / (interv_diff (cbox u v) i)"
      using K box_ne_empty(1) content_cbox by fastforce
    also have "... = (\<Prod>x\<in>Basis. if x = i then b \<bullet> x - a \<bullet> x
                      else (interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) \<bullet> x)"
      using \<open>i \<in> Basis\<close> K uv by (simp add: prod.If_cases interv_diff_def) (simp add: algebra_simps)
    also have "... = (\<Prod>k\<in>Basis.
                        (\<Sum>j\<in>Basis. if j = i then (b \<bullet> i - a \<bullet> i) *\<^sub>R i
                                    else ((interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) \<bullet> j) *\<^sub>R j) \<bullet> k)"
      using \<open>i \<in> Basis\<close> by (subst prod.cong [OF refl sum_if_inner]; simp)
    also have "... = (\<Prod>k\<in>Basis.
                        (\<Sum>j\<in>Basis. if j = i then (b \<bullet> i) *\<^sub>R i else (interval_upperbound (cbox u v) \<bullet> j) *\<^sub>R j) \<bullet> k -
                        (\<Sum>j\<in>Basis. if j = i then (a \<bullet> i) *\<^sub>R i else (interval_lowerbound (cbox u v) \<bullet> j) *\<^sub>R j) \<bullet> k)"
      using \<open>i \<in> Basis\<close>
      by (intro prod.cong [OF refl]) (subst sum_if_inner; simp add: algebra_simps)+
    also have "... = (content \<circ> extend) K"
      using \<open>i \<in> Basis\<close> K box_ne_empty \<open>K \<in> \<D>\<close> extend(1)
      by (auto simp add: extend_def content_cbox_if)
    finally show "(b \<bullet> i - a \<bullet> i) * content K / (interv_diff K i) = (content \<circ> extend) K" .
  qed
  also have "... = sum content (extend ` \<D>)"
  proof -
    have "\<lbrakk>K1 \<in> \<D>; K2 \<in> \<D>; K1 \<noteq> K2; extend K1 = extend K2\<rbrakk> \<Longrightarrow> 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 \<open>finite \<D>\<close>])
  qed
  also have "... \<le> ?rhs"
  proof (rule subadditive_content_division)
    show "extend ` \<D> division_of \<Union> (extend ` \<D>)"
      using int_extend_disjoint  by (auto simp: division_of_def \<open>finite \<D>\<close> extend extend_cbox)
    show "\<Union> (extend ` \<D>) \<subseteq> cbox a b"
      using extend by fastforce
  qed
  finally show ?thesis .
qed

proposition sum_content_area_over_thin_division:
  assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
    and "a \<bullet> i \<le> c" "c \<le> b \<bullet> i"
    and nonmt: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<inter> {x. x \<bullet> i = c} \<noteq> {}"
  shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
          \<le> 2 * content(cbox a b)"
proof (cases "content(cbox a b) = 0")
  case True
  have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> 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 \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
    using content_pos_lt_eq that by blast
  have "finite \<D>"
    using div by blast
  define Dlec where "Dlec \<equiv> {L \<in> (\<lambda>L. L \<inter> {x. x \<bullet> i \<le> c}) ` \<D>. content L \<noteq> 0}"
  define Dgec where "Dgec \<equiv> {L \<in> (\<lambda>L. L \<inter> {x. x \<bullet> i \<ge> c}) ` \<D>. content L \<noteq> 0}"
  define a' where "a' \<equiv> (\<Sum>j\<in>Basis. (if j = i then c else a \<bullet> j) *\<^sub>R j)"
  define b' where "b' \<equiv> (\<Sum>j\<in>Basis. (if j = i then c else b \<bullet> j) *\<^sub>R j)"
  define interv_diff where "interv_diff \<equiv> \<lambda>K. \<lambda>i::'a. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i"
  have Dlec_cbox: "\<And>K. K \<in> Dlec \<Longrightarrow> \<exists>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: "\<lbrakk>content (L \<inter> {x. x \<bullet> i \<le> c}) \<noteq> 0; L \<in> \<D>\<rbrakk> \<Longrightarrow> \<exists>a b. L \<inter> {x. x \<bullet> i \<le> c} = cbox a b" for L
    using Dlec_def by blast
  have Dgec_cbox: "\<And>K. K \<in> Dgec \<Longrightarrow> \<exists>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: "\<lbrakk>content (L \<inter> {x. x \<bullet> i \<ge> c}) \<noteq> 0; L \<in> \<D>\<rbrakk> \<Longrightarrow> \<exists>a b. L \<inter> {x. x \<bullet> i \<ge> c} = cbox a b" for L
    using Dgec_def by blast

  have zero_left: "\<And>x y. \<lbrakk>x \<in> \<D>; y \<in> \<D>; x \<noteq> y; x \<inter> {x. x \<bullet> i \<le> c} = y \<inter> {x. x \<bullet> i \<le> c}\<rbrakk>
           \<Longrightarrow> content (y \<inter> {x. x \<bullet> i \<le> c}) = 0"
    by (metis division_split_left_inj [OF div] lec_is_cbox content_eq_0_interior)
  have zero_right: "\<And>x y. \<lbrakk>x \<in> \<D>; y \<in> \<D>; x \<noteq> y; x \<inter> {x. c \<le> x \<bullet> i} = y \<inter> {x. c \<le> x \<bullet> i}\<rbrakk>
           \<Longrightarrow> content (y \<inter> {x. c \<le> x \<bullet> i}) = 0"
    by (metis division_split_right_inj [OF div] gec_is_cbox content_eq_0_interior)

  have "(b' \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>Dlec. content K / interv_diff K i) \<le> content(cbox a b')"
    unfolding interv_diff_def
  proof (rule content_division_lemma1)
    show "Dlec division_of \<Union>Dlec"
      unfolding division_of_def
    proof (intro conjI ballI Dlec_cbox)
      show "\<And>K1 K2. \<lbrakk>K1 \<in> Dlec; K2 \<in> Dlec\<rbrakk> \<Longrightarrow> K1 \<noteq> K2 \<longrightarrow> interior K1 \<inter> interior K2 = {}"
        by (clarsimp simp: Dlec_def) (use div in auto)
    qed (use \<open>finite \<D>\<close> Dlec_def in auto)
    show "\<Union>Dlec \<subseteq> cbox a b'"
      using Dlec_def div S by (auto simp: b'_def division_of_def mem_box)
    show "(\<forall>K\<in>Dlec. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}) \<or> (\<forall>K\<in>Dlec. K \<inter> {x. x \<bullet> i = b' \<bullet> i} \<noteq> {})"
      using nonmt by (fastforce simp: Dlec_def b'_def i)
  qed (use i Dlec_def in auto)
  moreover
  have "(\<Sum>K\<in>Dlec. content K / (interv_diff K i)) = (\<Sum>K\<in>(\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}) ` \<D>. content K / interv_diff K i)"
    unfolding Dlec_def using \<open>finite \<D>\<close> by (auto simp: sum.mono_neutral_left)
  moreover have "... =
        (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)"
    by (simp add: zero_left sum.reindex_nontrivial [OF \<open>finite \<D>\<close>])
  moreover have "(b' \<bullet> i - a \<bullet> i) = (c - a \<bullet> i)"
    by (simp add: b'_def i)
  ultimately
  have lec: "(c - a \<bullet> i) * (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
             \<le> content(cbox a b')"
    by simp

  have "(b \<bullet> i - a' \<bullet> i) * (\<Sum>K\<in>Dgec. content K / (interv_diff K i)) \<le> content(cbox a' b)"
    unfolding interv_diff_def
  proof (rule content_division_lemma1)
    show "Dgec division_of \<Union>Dgec"
      unfolding division_of_def
    proof (intro conjI ballI Dgec_cbox)
      show "\<And>K1 K2. \<lbrakk>K1 \<in> Dgec; K2 \<in> Dgec\<rbrakk> \<Longrightarrow> K1 \<noteq> K2 \<longrightarrow> interior K1 \<inter> interior K2 = {}"
        by (clarsimp simp: Dgec_def) (use div in auto)
    qed (use \<open>finite \<D>\<close> Dgec_def in auto)
    show "\<Union>Dgec \<subseteq> cbox a' b"
      using Dgec_def div S by (auto simp: a'_def division_of_def mem_box)
    show "(\<forall>K\<in>Dgec. K \<inter> {x. x \<bullet> i = a' \<bullet> i} \<noteq> {}) \<or> (\<forall>K\<in>Dgec. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {})"
      using nonmt by (fastforce simp: Dgec_def a'_def i)
  qed (use i Dgec_def in auto)
  moreover
  have "(\<Sum>K\<in>Dgec. content K / (interv_diff K i)) = (\<Sum>K\<in>(\<lambda>K. K \<inter> {x. c \<le> x \<bullet> i}) ` \<D>.
       content K / interv_diff K i)"
    unfolding Dgec_def using \<open>finite \<D>\<close> by (auto simp: sum.mono_neutral_left)
  moreover have "\<dots> =
        (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
    by (simp add: zero_right sum.reindex_nontrivial [OF \<open>finite \<D>\<close>])
  moreover have "(b \<bullet> i - a' \<bullet> i) = (b \<bullet> i - c)"
    by (simp add: a'_def i)
  ultimately
  have gec: "(b \<bullet> i - c) * (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
             \<le> content(cbox a' b)"
    by simp

  show ?thesis
  proof (cases "c = a \<bullet> i \<or> c = b \<bullet> i")
    case True
    then show ?thesis
    proof
      assume c: "c = a \<bullet> i"
      moreover
      have "(\<Sum>j\<in>Basis. (if j = i then a \<bullet> i else a \<bullet> j) *\<^sub>R j) = a"
        using euclidean_representation [of a] sum.cong [OF refl, of Basis "\<lambda>i. (a \<bullet> i) *\<^sub>R i"] by presburger
      ultimately have "a' = a"
        by (simp add: i a'_def cong: if_cong)
      then have "content (cbox a' b) \<le> 2 * content (cbox a b)"  by simp
      moreover
      have eq: "(\<Sum>K\<in>\<D>. content (K \<inter> {x. a \<bullet> i \<le> x \<bullet> i}) / interv_diff (K \<inter> {x. a \<bullet> i \<le> x \<bullet> i}) i)
              = (\<Sum>K\<in>\<D>. content K / interv_diff K i)"
        (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K \<in> \<D>"
        then have "a \<bullet> i \<le> x \<bullet> i" if "x \<in> K" for x
          by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
        then have "K \<inter> {x. a \<bullet> i \<le> x \<bullet> 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 \<bullet> i"
      moreover have "(\<Sum>j\<in>Basis. (if j = i then b \<bullet> i else b \<bullet> j) *\<^sub>R j) = b"
        using euclidean_representation [of b] sum.cong [OF refl, of Basis "\<lambda>i. (b \<bullet> i) *\<^sub>R i"] by presburger
      ultimately have "b' = b"
        by (simp add: i b'_def cong: if_cong)
      then have "content (cbox a b') \<le> 2 * content (cbox a b)"  by simp
      moreover
      have eq: "(\<Sum>K\<in>\<D>. content (K \<inter> {x. x \<bullet> i \<le> b \<bullet> i}) / interv_diff (K \<inter> {x. x \<bullet> i \<le> b \<bullet> i}) i)
              = (\<Sum>K\<in>\<D>. content K / interv_diff K i)"
               (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K \<in> \<D>"
        then have "x \<bullet> i \<le> b \<bullet> i" if "x \<in> K" for x
          by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
        then have "K \<inter> {x. x \<bullet> i \<le> b \<bullet> 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: "(\<Prod>k\<in>Basis \<inter> - {i}. f k) = (\<Prod>k\<in>Basis. f k) / f i" if "f i \<noteq> (0::real)" for f
    proof -
      have "f i * prod f (Basis \<inter> - {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 \<bullet> i < c" "c < b \<bullet> i"
      using False assms by auto
    then have "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
                  \<le> content(cbox a b') / (c - a \<bullet> i)"
              "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
                 \<le> content(cbox a' b) / (b \<bullet> i - c)"
      using lec gec by (simp_all add: field_split_simps)
    moreover
    have "(\<Sum>K\<in>\<D>. content K / (interv_diff K i))
          \<le> (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K) +
            (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
           (is "?lhs \<le> ?rhs")
    proof -
      have "?lhs \<le>
            (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K +
                    ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
            (is "sum ?f _ \<le> sum ?g _")
      proof (rule sum_mono)
        fix K assume "K \<in> \<D>"
        then obtain u v where uv: "K = cbox u v"
          using div by blast
        obtain u' v' where uv': "cbox u v \<inter> {x. x \<bullet> i \<le> c} = cbox u v'"
                                "cbox u v \<inter> {x. c \<le> x \<bullet> i} = cbox u' v"
                                "\<And>k. k \<in> Basis \<Longrightarrow> u' \<bullet> k = (if k = i then max (u \<bullet> i) c else u \<bullet> k)"
                                "\<And>k. k \<in> Basis \<Longrightarrow> v' \<bullet> k = (if k = i then min (v \<bullet> i) c else v \<bullet> k)"
          using i by (auto simp: interval_split)
        have *: "\<lbrakk>content (cbox u v') = 0; content (cbox u' v) = 0\<rbrakk> \<Longrightarrow> content (cbox u v) = 0"
                "content (cbox u' v) \<noteq> 0 \<Longrightarrow> content (cbox u v) \<noteq> 0"
                "content (cbox u v') \<noteq> 0 \<Longrightarrow> content (cbox u v) \<noteq> 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: "\<And>j. \<lbrakk>j \<in> Basis; \<not> u \<bullet> j \<le> v \<bullet> j\<rbrakk> \<Longrightarrow> j = i"
          by (metis \<open>K \<in> \<D>\<close> box_ne_empty(1) div division_of_def uv)
        show "?f K \<le> ?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 \<bullet> i) = content (cbox a b) / (b \<bullet> i - a \<bullet> 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 "\<lambda>f. f x" for x] prod.If_cases [of Basis "\<lambda>x. x = i", simplified] prod_if field_simps)
      done
    moreover have "content (cbox a' b) / (b \<bullet> i - c) = content (cbox a b) / (b \<bullet> i - a \<bullet> 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 "\<lambda>x. x = i", simplified] prod_if field_simps)
      done
    ultimately
    have "(\<Sum>K\<in>\<D>. content K / (interv_diff K i)) \<le> 2 * content (cbox a b) / (b \<bullet> i - a \<bullet> 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 \<Rightarrow> 'b::euclidean_space"
  assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F" and "0 < \<epsilon>"
      and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
  obtains \<gamma> where "gauge \<gamma>"
             "\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
                         \<gamma> fine S; h \<in> F; \<And>x K. (x,K) \<in> S \<Longrightarrow> (K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {})\<rbrakk>
                        \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
proof (cases "content(cbox a b) = 0")
  case True
  show ?thesis
  proof
    show "gauge (\<lambda>x. ball x 1)"
      by (simp add: gauge_trivial)
    show "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
         if "S tagged_partial_division_of cbox a b" "(\<lambda>x. ball x 1) fine S" for S and h:: "'a \<Rightarrow> 'b"
    proof -
      have "(\<Sum>(x,K) \<in> S. norm (integral K h)) = 0"
          using that True content_0_subset
          by (fastforce simp: tagged_partial_division_of_def intro: sum.neutral)
      with \<open>0 < \<epsilon>\<close> 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: "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
    by (auto simp: content_pos_lt_eq)
  obtain \<gamma>0 where "gauge \<gamma>0"
            and \<gamma>0: "\<And>S h. \<lbrakk>S tagged_partial_division_of cbox a b; \<gamma>0 fine S; h \<in> F\<rbrakk>
                           \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
  proof -
    obtain \<gamma> where "gauge \<gamma>"
               and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
                              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f)
                                  < \<epsilon>/(5 * (Suc DIM('b)))"
    proof -
      have e5: "\<epsilon>/(5 * (Suc DIM('b))) > 0"
        using \<open>\<epsilon> > 0\<close> by auto
      then show ?thesis
        using F that by (auto simp: equiintegrable_on_def)
    qed
    show ?thesis
    proof
      show "gauge \<gamma>"
        by (rule \<open>gauge \<gamma>\<close>)
      show "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
           if "S tagged_partial_division_of cbox a b" "\<gamma> fine S" "h \<in> F" for S h
      proof -
        have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) \<le> 2 * real DIM('b) * (\<epsilon>/(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 \<gamma>"
            by (rule \<open>gauge \<gamma>\<close>)
        qed (use that \<open>\<epsilon> > 0\<close> \<gamma> in auto)
        also have "... < \<epsilon>/2"
          using \<open>\<epsilon> > 0\<close> by (simp add: divide_simps)
        finally show ?thesis .
      qed
    qed
  qed
  define \<gamma> where "\<gamma> \<equiv> \<lambda>x. \<gamma>0 x \<inter>
                          ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
  define interv_diff where "interv_diff \<equiv> \<lambda>K. \<lambda>i::'a. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> 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 (\<lambda>x. ball x
                    (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
    using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b
    by (auto simp add: gauge_def field_split_simps add_nonneg_eq_0_iff finite_less_Inf_iff)
  then have "gauge \<gamma>"
    unfolding \<gamma>_def using \<open>gauge \<gamma>0\<close> gauge_Int by auto
  moreover
  have "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
       if "c \<in> cbox a b" "i \<in> Basis" and S: "S tagged_partial_division_of cbox a b"
          and "\<gamma> fine S" "h \<in> F" and ne: "\<And>x K. (x,K) \<in> S \<Longrightarrow> K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {}" for c i S h
  proof -
    have "cbox c b \<subseteq> 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 "\<gamma>0 fine S" and fineS:
         "(\<lambda>x. ball x (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
      using \<open>\<gamma> fine S\<close> by (auto simp: \<gamma>_def fine_Int)
    then have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
      by (intro \<gamma>0 that fineS)
    moreover have "(\<Sum>(x,K) \<in> S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h)) \<le> \<epsilon>/2"
    proof -
      have "(\<Sum>(x,K) \<in> S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h))
            \<le> (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x))"
      proof (clarify intro!: sum_mono)
        fix x K
        assume xK: "(x,K) \<in> S"
        have "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \<le> norm (integral K h - (integral K h - content K *\<^sub>R h x))"
          by (metis norm_minus_commute norm_triangle_ineq2)
        also have "... \<le> norm (content K *\<^sub>R h x)"
          by simp
        finally show "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \<le> norm (content K *\<^sub>R h x)" .
      qed
      also have "... \<le> (\<Sum>(x,K) \<in> S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K / interv_diff K i)"
      proof (clarify intro!: sum_mono)
        fix x K
        assume xK: "(x,K) \<in> S"
        then have x: "x \<in> cbox a b"
          using S unfolding tagged_partial_division_of_def by (meson subset_iff)
        show "norm (content K *\<^sub>R h x) \<le> \<epsilon>/4 * (b \<bullet> i - a \<bullet> 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 \<open>(x,K) \<in> S\<close> unfolding tagged_partial_division_of_def by blast
          then have u_less_v: "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i < v \<bullet> 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) \<le> (\<epsilon> * (b \<bullet> i - a \<bullet> i)) / (4 * content (cbox a b) * interv_diff K i)"
          proof -
            have "dist x u < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
                 "dist x v < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> 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 "\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
                  \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
            proof (intro mult_left_mono divide_right_mono)
              show "(INF m\<in>Basis. b \<bullet> m - a \<bullet> m) \<le> b \<bullet> i - a \<bullet> i"
                using \<open>i \<in> Basis\<close> by (auto intro!: cInf_le_finite)
            qed (use \<open>0 < \<epsilon>\<close> in auto)
            ultimately
            have "dist x u < \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
                 "dist x v < \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
              by linarith+
            then have duv: "dist u v < \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b))"
              using dist_triangle_half_r by blast
            have uvi: "\<bar>v \<bullet> i - u \<bullet> i\<bar> \<le> norm (v - u)"
              by (metis inner_commute inner_diff_right \<open>i \<in> Basis\<close> Basis_le_norm)
            have "norm (h x) \<le> norm (f x)"
              using x that by (auto simp: norm_f)
            also have "... < (norm (f x) + 1)"
              by simp
            also have "... < \<epsilon> * (b \<bullet> i - a \<bullet> 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 "... = \<epsilon> * (b \<bullet> i - a \<bullet> i) / norm (v - u) / (4 * content (cbox a b))"
              by (simp add: dist_norm norm_minus_commute)
            also have "... \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / \<bar>v \<bullet> i - u \<bullet> i\<bar> / (4 * content (cbox a b))"
            proof (intro mult_right_mono divide_left_mono divide_right_mono uvi)
              show "norm (v - u) * \<bar>v \<bullet> i - u \<bullet> i\<bar> > 0"
                using u_less_v [OF \<open>i \<in> Basis\<close>]
                by (auto simp: less_eq_real_def zero_less_mult_iff that)
              show "\<epsilon> * (b \<bullet> i - a \<bullet> i) \<ge> 0"
                using a_less_b \<open>0 < \<epsilon>\<close> \<open>i \<in> Basis\<close> by force
            qed auto
            also have "... = \<epsilon> * (b \<bullet> i - a \<bullet> 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 *\<^sub>R h x) \<le> content K * ((\<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b)) / interv_diff K i)"
            using mult_left_mono by fastforce
          also have "... = \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K / interv_diff K i"
            by (simp add: field_split_simps)
          finally show ?thesis .
        qed
      qed
      also have "... = (\<Sum>K\<in>snd ` S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> 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 "... = \<epsilon>/2 * ((b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / interv_diff K i))"
        by (simp add: interv_diff_def sum_distrib_left mult.assoc)
      also have "... \<le> (\<epsilon>/2) * 1"
      proof (rule mult_left_mono)
        have "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>snd ` S. content K / interv_diff K i) \<le> 2 * content (cbox a b)"
          unfolding interv_diff_def
        proof (rule sum_content_area_over_thin_division)
          show "snd ` S division_of \<Union>(snd ` S)"
            by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
          show "\<Union>(snd ` S) \<subseteq> cbox a b"
            using S unfolding tagged_partial_division_of_def by force
          show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
            using mem_box(2) that by blast+
        qed (use that in auto)
        then show "(b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / interv_diff K i) \<le> 1"
          by (simp add: contab_gt0)
      qed (use \<open>0 < \<epsilon>\<close> in auto)
      finally show ?thesis by simp
    qed
    then have "(\<Sum>(x,K) \<in> S. norm (integral K h)) - (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) \<le> \<epsilon>/2"
      by (simp add: Groups_Big.sum_subtractf [symmetric])
    ultimately show "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
      by linarith
  qed
  ultimately show ?thesis using that by auto
qed

proposition equiintegrable_halfspace_restrictions_le:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
    and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
  shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<le> 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 \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
    using content_pos_lt_eq that by blast
  have int_F: "f integrable_on cbox a b" if "f \<in> F" for f
    using F that by (simp add: equiintegrable_on_def)
  let ?CI = "\<lambda>K h x. content K *\<^sub>R h x - integral K h"
  show ?thesis
    unfolding equiintegrable_on_def
  proof (intro conjI; clarify)
    show int_lec: "\<lbrakk>i \<in> Basis; h \<in> F\<rbrakk> \<Longrightarrow> (\<lambda>x. if x \<bullet> i \<le> c then h x else 0) integrable_on cbox a b" for i c h
      using integrable_restrict_Int [of "{x. x \<bullet> i \<le> c}" h]
      by (simp add: inf_commute int_F integrable_split(1))
    show "\<exists>\<gamma>. gauge \<gamma> \<and>
              (\<forall>f T. f \<in> (\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>F. {\<lambda>x. if x \<bullet> i \<le> c then h x else 0}) \<and>
                     T tagged_division_of cbox a b \<and> \<gamma> fine T \<longrightarrow>
                     norm ((\<Sum>(x,K) \<in> T. content K *\<^sub>R f x) - integral (cbox a b) f) < \<epsilon>)"
      if "\<epsilon> > 0" for \<epsilon>
    proof -
      obtain \<gamma>0 where "gauge \<gamma>0" and \<gamma>0:
        "\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
                        \<gamma>0 fine S; h \<in> F; \<And>x K. (x,K) \<in> S \<Longrightarrow> (K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {})\<rbrakk>
                       \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>/12"
      proof (rule bounded_equiintegral_over_thin_tagged_partial_division [OF F f, of \<open>\<epsilon>/12\<close>])
        show "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm (h x) \<le> norm (f x)"
          by (auto simp: norm_f)
      qed (use \<open>\<epsilon> > 0\<close> in auto)
      obtain \<gamma>1 where "gauge \<gamma>1"
        and \<gamma>1: "\<And>h T. \<lbrakk>h \<in> F; T tagged_division_of cbox a b; \<gamma>1 fine T\<rbrakk>
                              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> T. content K *\<^sub>R h x) - integral (cbox a b) h)
                                  < \<epsilon>/(7 * (Suc DIM('b)))"
      proof -
        have e5: "\<epsilon>/(7 * (Suc DIM('b))) > 0"
          using \<open>\<epsilon> > 0\<close> by auto
        then show ?thesis
          using F that by (auto simp: equiintegrable_on_def)
      qed
      have h_less3: "(\<Sum>(x,K) \<in> T. norm (?CI K h x)) < \<epsilon>/3"
        if "T tagged_partial_division_of cbox a b" "\<gamma>1 fine T" "h \<in> F" for T h
      proof -
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.21 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.