src/HOL/Analysis/Improper_Integral.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago) changeset 69981 3dced198b9ec parent 69722 b5163b2132c5 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 section \<open>Continuity of the indefinite integral; improper integral theorem\<close>
```
```     2
```
```     3 theory "Improper_Integral"
```
```     4   imports Equivalence_Lebesgue_Henstock_Integration
```
```     5 begin
```
```     6
```
```     7 subsection \<open>Equiintegrability\<close>
```
```     8
```
```     9 text\<open>The definition here only really makes sense for an elementary set.
```
```    10      We just use compact intervals in applications below.\<close>
```
```    11
```
```    12 definition%important equiintegrable_on (infixr "equiintegrable'_on" 46)
```
```    13   where "F equiintegrable_on I \<equiv>
```
```    14          (\<forall>f \<in> F. f integrable_on I) \<and>
```
```    15          (\<forall>e > 0. \<exists>\<gamma>. gauge \<gamma> \<and>
```
```    16                     (\<forall>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma> fine \<D>
```
```    17                           \<longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < e))"
```
```    18
```
```    19 lemma equiintegrable_on_integrable:
```
```    20      "\<lbrakk>F equiintegrable_on I; f \<in> F\<rbrakk> \<Longrightarrow> f integrable_on I"
```
```    21   using equiintegrable_on_def by metis
```
```    22
```
```    23 lemma equiintegrable_on_sing [simp]:
```
```    24      "{f} equiintegrable_on cbox a b \<longleftrightarrow> f integrable_on cbox a b"
```
```    25   by (simp add: equiintegrable_on_def has_integral_integral has_integral integrable_on_def)
```
```    26
```
```    27 lemma equiintegrable_on_subset: "\<lbrakk>F equiintegrable_on I; G \<subseteq> F\<rbrakk> \<Longrightarrow> G equiintegrable_on I"
```
```    28   unfolding equiintegrable_on_def Ball_def
```
```    29   by (erule conj_forward imp_forward all_forward ex_forward | blast)+
```
```    30
```
```    31 lemma equiintegrable_on_Un:
```
```    32   assumes "F equiintegrable_on I" "G equiintegrable_on I"
```
```    33   shows "(F \<union> G) equiintegrable_on I"
```
```    34   unfolding equiintegrable_on_def
```
```    35 proof (intro conjI impI allI)
```
```    36   show "\<forall>f\<in>F \<union> G. f integrable_on I"
```
```    37     using assms unfolding equiintegrable_on_def by blast
```
```    38   show "\<exists>\<gamma>. gauge \<gamma> \<and>
```
```    39             (\<forall>f \<D>. f \<in> F \<union> G \<and>
```
```    40                    \<D> tagged_division_of I \<and> \<gamma> fine \<D> \<longrightarrow>
```
```    41                    norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
```
```    42          if "\<epsilon> > 0" for \<epsilon>
```
```    43   proof -
```
```    44     obtain \<gamma>1 where "gauge \<gamma>1"
```
```    45       and \<gamma>1: "\<And>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma>1 fine \<D>
```
```    46                     \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
```
```    47       using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by auto
```
```    48     obtain \<gamma>2 where  "gauge \<gamma>2"
```
```    49       and \<gamma>2: "\<And>f \<D>. f \<in> G \<and> \<D> tagged_division_of I \<and> \<gamma>2 fine \<D>
```
```    50                     \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
```
```    51       using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by auto
```
```    52     have "gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
```
```    53       using \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close> by blast
```
```    54     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>
```
```    55           norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
```
```    56       using \<gamma>1 \<gamma>2 by (auto simp: fine_Int)
```
```    57     ultimately show ?thesis
```
```    58       by (intro exI conjI) assumption+
```
```    59   qed
```
```    60 qed
```
```    61
```
```    62
```
```    63 lemma equiintegrable_on_insert:
```
```    64   assumes "f integrable_on cbox a b" "F equiintegrable_on cbox a b"
```
```    65   shows "(insert f F) equiintegrable_on cbox a b"
```
```    66   by (metis assms equiintegrable_on_Un equiintegrable_on_sing insert_is_Un)
```
```    67
```
```    68
```
```    69 text\<open> Basic combining theorems for the interval of integration.\<close>
```
```    70
```
```    71 lemma equiintegrable_on_null [simp]:
```
```    72    "content(cbox a b) = 0 \<Longrightarrow> F equiintegrable_on cbox a b"
```
```    73   apply (auto simp: equiintegrable_on_def)
```
```    74   by (metis gauge_trivial norm_eq_zero sum_content_null)
```
```    75
```
```    76
```
```    77 text\<open> Main limit theorem for an equiintegrable sequence.\<close>
```
```    78
```
```    79 theorem equiintegrable_limit:
```
```    80   fixes g :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
```
```    81   assumes feq: "range f equiintegrable_on cbox a b"
```
```    82       and to_g: "\<And>x. x \<in> cbox a b \<Longrightarrow> (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
```
```    83     shows "g integrable_on cbox a b \<and> (\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> integral (cbox a b) g"
```
```    84 proof -
```
```    85   have "Cauchy (\<lambda>n. integral(cbox a b) (f n))"
```
```    86   proof (clarsimp simp add: Cauchy_def)
```
```    87     fix e::real
```
```    88     assume "0 < e"
```
```    89     then have e3: "0 < e/3"
```
```    90       by simp
```
```    91     then obtain \<gamma> where "gauge \<gamma>"
```
```    92          and \<gamma>: "\<And>n \<D>. \<lbrakk>\<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
```
```    93                        \<Longrightarrow> norm((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) < e/3"
```
```    94       using feq unfolding equiintegrable_on_def
```
```    95       by (meson image_eqI iso_tuple_UNIV_I)
```
```    96     obtain \<D> where \<D>: "\<D> tagged_division_of (cbox a b)" and "\<gamma> fine \<D>"  "finite \<D>"
```
```    97       by (meson \<open>gauge \<gamma>\<close> fine_division_exists tagged_division_of_finite)
```
```    98     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"
```
```    99       by (force simp: dist_norm)
```
```   100     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)"
```
```   101       using \<D> to_g by (auto intro!: tendsto_sum tendsto_scaleR)
```
```   102     then have "Cauchy (\<lambda>n. \<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x)"
```
```   103       by (meson convergent_eq_Cauchy)
```
```   104     with e3 obtain M where
```
```   105       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)
```
```   106                       < e/3"
```
```   107       unfolding Cauchy_def by blast
```
```   108     have "\<And>m n. \<lbrakk>m\<ge>M; n\<ge>M;
```
```   109                  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>
```
```   110                 \<Longrightarrow> dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e"
```
```   111        by (metis \<delta>T dist_commute dist_triangle_third [OF _ _ \<delta>T])
```
```   112     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"
```
```   113       using M by auto
```
```   114   qed
```
```   115   then obtain L where L: "(\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> L"
```
```   116     by (meson convergent_eq_Cauchy)
```
```   117   have "(g has_integral L) (cbox a b)"
```
```   118   proof (clarsimp simp: has_integral)
```
```   119     fix e::real assume "0 < e"
```
```   120     then have e2: "0 < e/2"
```
```   121       by simp
```
```   122     then obtain \<gamma> where "gauge \<gamma>"
```
```   123       and \<gamma>: "\<And>n \<D>. \<lbrakk>\<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
```
```   124                     \<Longrightarrow> norm((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) < e/2"
```
```   125       using feq unfolding equiintegrable_on_def
```
```   126       by (meson image_eqI iso_tuple_UNIV_I)
```
```   127     moreover
```
```   128     have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L) < e"
```
```   129               if "\<D> tagged_division_of cbox a b" "\<gamma> fine \<D>" for \<D>
```
```   130     proof -
```
```   131       have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L) \<le> e/2"
```
```   132       proof (rule Lim_norm_ubound)
```
```   133         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"
```
```   134           using to_g that L
```
```   135           by (intro tendsto_diff tendsto_sum) (auto simp: tag_in_interval tendsto_scaleR)
```
```   136         show "\<forall>\<^sub>F n in sequentially.
```
```   137                 norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) \<le> e/2"
```
```   138           by (intro eventuallyI less_imp_le \<gamma> that)
```
```   139       qed auto
```
```   140       with \<open>0 < e\<close> show ?thesis
```
```   141         by linarith
```
```   142     qed
```
```   143     ultimately
```
```   144     show "\<exists>\<gamma>. gauge \<gamma> \<and>
```
```   145              (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
```
```   146                   norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - L) < e)"
```
```   147       by meson
```
```   148   qed
```
```   149   with L show ?thesis
```
```   150     by (simp add: \<open>(\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> L\<close> has_integral_integrable_integral)
```
```   151 qed
```
```   152
```
```   153
```
```   154 lemma equiintegrable_reflect:
```
```   155   assumes "F equiintegrable_on cbox a b"
```
```   156   shows "(\<lambda>f. f \<circ> uminus) ` F equiintegrable_on cbox (-b) (-a)"
```
```   157 proof -
```
```   158   have "\<exists>\<gamma>. gauge \<gamma> \<and>
```
```   159             (\<forall>f \<D>. f \<in> (\<lambda>f. f \<circ> uminus) ` F \<and> \<D> tagged_division_of cbox (- b) (- a) \<and> \<gamma> fine \<D> \<longrightarrow>
```
```   160                    norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)"
```
```   161        if "gauge \<gamma>" and
```
```   162            \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk> \<Longrightarrow>
```
```   163                      norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f) < e" for e \<gamma>
```
```   164   proof (intro exI, safe)
```
```   165     show "gauge (\<lambda>x. uminus ` \<gamma> (-x))"
```
```   166       by (metis \<open>gauge \<gamma>\<close> gauge_reflect)
```
```   167     show "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R (f \<circ> uminus) x) - integral (cbox (- b) (- a)) (f \<circ> uminus)) < e"
```
```   168       if "f \<in> F" and tag: "\<D> tagged_division_of cbox (- b) (- a)"
```
```   169          and fine: "(\<lambda>x. uminus ` \<gamma> (- x)) fine \<D>" for f \<D>
```
```   170     proof -
```
```   171       have 1: "(\<lambda>(x,K). (- x, uminus ` K)) ` \<D> tagged_partial_division_of cbox a b"
```
```   172         if "\<D> tagged_partial_division_of cbox (- b) (- a)"
```
```   173       proof -
```
```   174         have "- y \<in> cbox a b"
```
```   175           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)"
```
```   176              "(x, Y) \<in> \<D>" "y \<in> Y" for x Y y
```
```   177         proof -
```
```   178           have "y \<in> uminus ` cbox a b"
```
```   179             using that by auto
```
```   180           then show "- y \<in> cbox a b"
```
```   181             by force
```
```   182         qed
```
```   183         with that show ?thesis
```
```   184           by (fastforce simp: tagged_partial_division_of_def interior_negations image_iff)
```
```   185       qed
```
```   186       have 2: "\<exists>K. (\<exists>x. (x,K) \<in> (\<lambda>(x,K). (- x, uminus ` K)) ` \<D>) \<and> x \<in> K"
```
```   187               if "\<Union>{K. \<exists>x. (x,K) \<in> \<D>} = cbox (- b) (- a)" "x \<in> cbox a b" for x
```
```   188       proof -
```
```   189         have xm: "x \<in> uminus ` \<Union>{A. \<exists>a. (a, A) \<in> \<D>}"
```
```   190           by (simp add: that)
```
```   191         then obtain a X where "-x \<in> X" "(a, X) \<in> \<D>"
```
```   192           by auto
```
```   193         then show ?thesis
```
```   194           by (metis (no_types, lifting) add.inverse_inverse image_iff pair_imageI)
```
```   195       qed
```
```   196       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"
```
```   197         by (metis (no_types, lifting) equation_minus_iff imageE subsetD tagged_partial_division_ofD(3) uminus_interval_vector)
```
```   198       have tag': "(\<lambda>(x,K). (- x, uminus ` K)) ` \<D> tagged_division_of cbox a b"
```
```   199         using tag  by (auto simp: tagged_division_of_def dest: 1 2 3)
```
```   200       have fine': "\<gamma> fine (\<lambda>(x,K). (- x, uminus ` K)) ` \<D>"
```
```   201         using fine by (fastforce simp: fine_def)
```
```   202       have inj: "inj_on (\<lambda>(x,K). (- x, uminus ` K)) \<D>"
```
```   203         unfolding inj_on_def by force
```
```   204       have eq: "content (uminus ` I) = content I"
```
```   205                if I: "(x, I) \<in> \<D>" and fnz: "f (- x) \<noteq> 0" for x I
```
```   206       proof -
```
```   207         obtain a b where "I = cbox a b"
```
```   208           using tag I that by (force simp: tagged_division_of_def tagged_partial_division_of_def)
```
```   209         then show ?thesis
```
```   210           using content_image_affinity_cbox [of "-1" 0] by auto
```
```   211       qed
```
```   212       have "(\<Sum>(x,K) \<in> (\<lambda>(x,K). (- x, uminus ` K)) ` \<D>.  content K *\<^sub>R f x) =
```
```   213             (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f (- x))"
```
```   214         apply (simp add: sum.reindex [OF inj])
```
```   215         apply (auto simp: eq intro!: sum.cong)
```
```   216         done
```
```   217       then show ?thesis
```
```   218         using \<gamma> [OF \<open>f \<in> F\<close> tag' fine'] integral_reflect
```
```   219         by (metis (mono_tags, lifting) Henstock_Kurzweil_Integration.integral_cong comp_apply split_def sum.cong)
```
```   220     qed
```
```   221   qed
```
```   222   then show ?thesis
```
```   223     using assms
```
```   224     apply (auto simp: equiintegrable_on_def)
```
```   225     apply (rule integrable_eq)
```
```   226     by auto
```
```   227 qed
```
```   228
```
```   229 subsection\<open>Subinterval restrictions for equiintegrable families\<close>
```
```   230
```
```   231 text\<open>First, some technical lemmas about minimizing a "flat" part of a sum over a division.\<close>
```
```   232
```
```   233 lemma lemma0:
```
```   234   assumes "i \<in> Basis"
```
```   235     shows "content (cbox u v) / (interval_upperbound (cbox u v) \<bullet> i - interval_lowerbound (cbox u v) \<bullet> i) =
```
```   236            (if content (cbox u v) = 0 then 0
```
```   237             else \<Prod>j \<in> Basis - {i}. interval_upperbound (cbox u v) \<bullet> j - interval_lowerbound (cbox u v) \<bullet> j)"
```
```   238 proof (cases "content (cbox u v) = 0")
```
```   239   case True
```
```   240   then show ?thesis by simp
```
```   241 next
```
```   242   case False
```
```   243   then show ?thesis
```
```   244     using prod.subset_diff [of "{i}" Basis] assms
```
```   245       by (force simp: content_cbox_if divide_simps  split: if_split_asm)
```
```   246 qed
```
```   247
```
```   248
```
```   249 lemma content_division_lemma1:
```
```   250   assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
```
```   251       and mt: "\<And>K. K \<in> \<D> \<Longrightarrow> content K \<noteq> 0"
```
```   252       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> {})"
```
```   253    shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
```
```   254           \<le> content(cbox a b)"   (is "?lhs \<le> ?rhs")
```
```   255 proof -
```
```   256   have "finite \<D>"
```
```   257     using div by blast
```
```   258   define extend where
```
```   259     "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)
```
```   260                        (\<Sum>j \<in> Basis. if j = i then (b \<bullet> i) *\<^sub>R i else (interval_upperbound K \<bullet> j) *\<^sub>R j)"
```
```   261   have div_subset_cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<subseteq> cbox a b"
```
```   262     using S div by auto
```
```   263   have "\<And>K. K \<in> \<D> \<Longrightarrow> K \<noteq> {}"
```
```   264     using div by blast
```
```   265   have extend: "extend K \<noteq> {}" "extend K \<subseteq> cbox a b" if K: "K \<in> \<D>" for K
```
```   266   proof -
```
```   267     obtain u v where K: "K = cbox u v" "K \<noteq> {}" "K \<subseteq> cbox a b"
```
```   268       using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
```
```   269     with i show "extend K \<noteq> {}" "extend K \<subseteq> cbox a b"
```
```   270       apply (auto simp: extend_def subset_box box_ne_empty sum_if_inner)
```
```   271       by fastforce
```
```   272   qed
```
```   273   have int_extend_disjoint:
```
```   274        "interior(extend K1) \<inter> interior(extend K2) = {}" if K: "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2" for K1 K2
```
```   275   proof -
```
```   276     obtain u v where K1: "K1 = cbox u v" "K1 \<noteq> {}" "K1 \<subseteq> cbox a b"
```
```   277       using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
```
```   278     obtain w z where K2: "K2 = cbox w z" "K2 \<noteq> {}" "K2 \<subseteq> cbox a b"
```
```   279       using K cbox_division_memE [OF _ div] by (meson div_subset_cbox)
```
```   280     have cboxes: "cbox u v \<in> \<D>" "cbox w z \<in> \<D>" "cbox u v \<noteq> cbox w z"
```
```   281       using K1 K2 that by auto
```
```   282     with div have "interior (cbox u v) \<inter> interior (cbox w z) = {}"
```
```   283       by blast
```
```   284     moreover
```
```   285     have "\<exists>x. x \<in> box u v \<and> x \<in> box w z"
```
```   286          if "x \<in> interior (extend K1)" "x \<in> interior (extend K2)" for x
```
```   287     proof -
```
```   288       have "a \<bullet> i < x \<bullet> i" "x \<bullet> i < b \<bullet> i"
```
```   289        and ux: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> u \<bullet> k < x \<bullet> k"
```
```   290        and xv: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> x \<bullet> k < v \<bullet> k"
```
```   291        and wx: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> w \<bullet> k < x \<bullet> k"
```
```   292        and xz: "\<And>k. k \<in> Basis - {i} \<Longrightarrow> x \<bullet> k < z \<bullet> k"
```
```   293         using that K1 K2 i by (auto simp: extend_def box_ne_empty sum_if_inner mem_box)
```
```   294       have "box u v \<noteq> {}" "box w z \<noteq> {}"
```
```   295         using cboxes interior_cbox by (auto simp: content_eq_0_interior dest: mt)
```
```   296       then obtain q s
```
```   297         where q: "\<And>k. k \<in> Basis \<Longrightarrow> w \<bullet> k < q \<bullet> k \<and> q \<bullet> k < z \<bullet> k"
```
```   298           and s: "\<And>k. k \<in> Basis \<Longrightarrow> u \<bullet> k < s \<bullet> k \<and> s \<bullet> k < v \<bullet> k"
```
```   299         by (meson all_not_in_conv mem_box(1))
```
```   300       show ?thesis  using disj
```
```   301       proof
```
```   302         assume "\<forall>K\<in>\<D>. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}"
```
```   303         then have uva: "(cbox u v) \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}"
```
```   304              and  wza: "(cbox w z) \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}"
```
```   305           using cboxes by (auto simp: content_eq_0_interior)
```
```   306         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"
```
```   307                         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"
```
```   308           by (fastforce simp: mem_box)
```
```   309         have u: "u \<bullet> i < q \<bullet> i"
```
```   310           using i K2(1) K2(3) \<open>t \<bullet> i = a \<bullet> i\<close> q s t [OF i] by (force simp: subset_box)
```
```   311         have w: "w \<bullet> i < s \<bullet> i"
```
```   312           using i K1(1) K1(3) \<open>r \<bullet> i = a \<bullet> i\<close> s r [OF i] by (force simp: subset_box)
```
```   313         let ?x = "(\<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)"
```
```   314         show ?thesis
```
```   315         proof (intro exI conjI)
```
```   316           show "?x \<in> box u v"
```
```   317             using \<open>i \<in> Basis\<close> s apply (clarsimp simp: mem_box)
```
```   318             apply (subst sum_if_inner; simp)+
```
```   319             apply (fastforce simp: u ux xv)
```
```   320             done
```
```   321           show "?x \<in> box w z"
```
```   322             using \<open>i \<in> Basis\<close> q apply (clarsimp simp: mem_box)
```
```   323             apply (subst sum_if_inner; simp)+
```
```   324             apply (fastforce simp: w wx xz)
```
```   325             done
```
```   326         qed
```
```   327       next
```
```   328         assume "\<forall>K\<in>\<D>. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {}"
```
```   329         then have uva: "(cbox u v) \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {}"
```
```   330              and  wza: "(cbox w z) \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {}"
```
```   331           using cboxes by (auto simp: content_eq_0_interior)
```
```   332         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"
```
```   333                         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"
```
```   334           by (fastforce simp: mem_box)
```
```   335         have z: "s \<bullet> i < z \<bullet> i"
```
```   336           using K1(1) K1(3) \<open>r \<bullet> i = b \<bullet> i\<close> r [OF i] i s  by (force simp: subset_box)
```
```   337         have v: "q \<bullet> i < v \<bullet> i"
```
```   338           using K2(1) K2(3) \<open>t \<bullet> i = b \<bullet> i\<close> t [OF i] i q  by (force simp: subset_box)
```
```   339         let ?x = "(\<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)"
```
```   340         show ?thesis
```
```   341         proof (intro exI conjI)
```
```   342           show "?x \<in> box u v"
```
```   343             using \<open>i \<in> Basis\<close> s apply (clarsimp simp: mem_box)
```
```   344             apply (subst sum_if_inner; simp)+
```
```   345             apply (fastforce simp: v ux xv)
```
```   346             done
```
```   347           show "?x \<in> box w z"
```
```   348             using \<open>i \<in> Basis\<close> q apply (clarsimp simp: mem_box)
```
```   349             apply (subst sum_if_inner; simp)+
```
```   350             apply (fastforce simp: z wx xz)
```
```   351             done
```
```   352         qed
```
```   353       qed
```
```   354     qed
```
```   355     ultimately show ?thesis by auto
```
```   356   qed
```
```   357   have "?lhs = (\<Sum>K\<in>\<D>. (b \<bullet> i - a \<bullet> i) * content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
```
```   358     by (simp add: sum_distrib_left)
```
```   359   also have "\<dots> = sum (content \<circ> extend) \<D>"
```
```   360   proof (rule sum.cong [OF refl])
```
```   361     fix K assume "K \<in> \<D>"
```
```   362     then obtain u v where K: "K = cbox u v" "cbox u v \<noteq> {}" "K \<subseteq> cbox a b"
```
```   363       using cbox_division_memE [OF _ div] div_subset_cbox by metis
```
```   364     then have uv: "u \<bullet> i < v \<bullet> i"
```
```   365       using mt [OF \<open>K \<in> \<D>\<close>] \<open>i \<in> Basis\<close> content_eq_0 by fastforce
```
```   366     have "insert i (Basis \<inter> -{i}) = Basis"
```
```   367       using \<open>i \<in> Basis\<close> by auto
```
```   368     then have "(b \<bullet> i - a \<bullet> i) * content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)
```
```   369              = (b \<bullet> i - a \<bullet> i) * (\<Prod>i \<in> insert i (Basis \<inter> -{i}). v \<bullet> i - u \<bullet> i) / (interval_upperbound (cbox u v) \<bullet> i - interval_lowerbound (cbox u v) \<bullet> i)"
```
```   370       using K box_ne_empty(1) content_cbox by fastforce
```
```   371     also have "... = (\<Prod>x\<in>Basis. if x = i then b \<bullet> x - a \<bullet> x
```
```   372                       else (interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) \<bullet> x)"
```
```   373       using \<open>i \<in> Basis\<close> K uv by (simp add: prod.If_cases) (simp add: algebra_simps)
```
```   374     also have "... = (\<Prod>k\<in>Basis.
```
```   375                         (\<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)"
```
```   376       using \<open>i \<in> Basis\<close> by (subst prod.cong [OF refl sum_if_inner]; simp)
```
```   377     also have "... = (\<Prod>k\<in>Basis.
```
```   378                         (\<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 -
```
```   379                         (\<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)"
```
```   380       apply (rule prod.cong [OF refl])
```
```   381       using \<open>i \<in> Basis\<close>
```
```   382       apply (subst sum_if_inner; simp add: algebra_simps)+
```
```   383       done
```
```   384     also have "... = (content \<circ> extend) K"
```
```   385       using \<open>i \<in> Basis\<close> K box_ne_empty
```
```   386       apply (simp add: extend_def)
```
```   387       apply (subst content_cbox, auto)
```
```   388       done
```
```   389     finally show "(b \<bullet> i - a \<bullet> i) * content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)
```
```   390          = (content \<circ> extend) K" .
```
```   391   qed
```
```   392   also have "... = sum content (extend ` \<D>)"
```
```   393   proof -
```
```   394     have "\<lbrakk>K1 \<in> \<D>; K2 \<in> \<D>; K1 \<noteq> K2; extend K1 = extend K2\<rbrakk> \<Longrightarrow> content (extend K1) = 0" for K1 K2
```
```   395       using int_extend_disjoint [of K1 K2] extend_def by (simp add: content_eq_0_interior)
```
```   396     then show ?thesis
```
```   397       by (simp add: comm_monoid_add_class.sum.reindex_nontrivial [OF \<open>finite \<D>\<close>])
```
```   398   qed
```
```   399   also have "... \<le> ?rhs"
```
```   400   proof (rule subadditive_content_division)
```
```   401     show "extend ` \<D> division_of \<Union> (extend ` \<D>)"
```
```   402       using int_extend_disjoint apply (auto simp: division_of_def \<open>finite \<D>\<close> extend)
```
```   403       using extend_def apply blast
```
```   404       done
```
```   405     show "\<Union> (extend ` \<D>) \<subseteq> cbox a b"
```
```   406       using extend by fastforce
```
```   407   qed
```
```   408   finally show ?thesis .
```
```   409 qed
```
```   410
```
```   411
```
```   412 proposition sum_content_area_over_thin_division:
```
```   413   assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
```
```   414     and "a \<bullet> i \<le> c" "c \<le> b \<bullet> i"
```
```   415     and nonmt: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<inter> {x. x \<bullet> i = c} \<noteq> {}"
```
```   416   shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
```
```   417           \<le> 2 * content(cbox a b)"
```
```   418 proof (cases "content(cbox a b) = 0")
```
```   419   case True
```
```   420   have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) = 0"
```
```   421     using S div by (force intro!: sum.neutral content_0_subset [OF True])
```
```   422   then show ?thesis
```
```   423     by (auto simp: True)
```
```   424 next
```
```   425   case False
```
```   426   then have "content(cbox a b) > 0"
```
```   427     using zero_less_measure_iff by blast
```
```   428   then have "a \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
```
```   429     using content_pos_lt_eq that by blast
```
```   430   have "finite \<D>"
```
```   431     using div by blast
```
```   432   define Dlec where "Dlec \<equiv> {L \<in> (\<lambda>L. L \<inter> {x. x \<bullet> i \<le> c}) ` \<D>. content L \<noteq> 0}"
```
```   433   define Dgec where "Dgec \<equiv> {L \<in> (\<lambda>L. L \<inter> {x. x \<bullet> i \<ge> c}) ` \<D>. content L \<noteq> 0}"
```
```   434   define a' where "a' \<equiv> (\<Sum>j\<in>Basis. (if j = i then c else a \<bullet> j) *\<^sub>R j)"
```
```   435   define b' where "b' \<equiv> (\<Sum>j\<in>Basis. (if j = i then c else b \<bullet> j) *\<^sub>R j)"
```
```   436   have Dlec_cbox: "\<And>K. K \<in> Dlec \<Longrightarrow> \<exists>a b. K = cbox a b"
```
```   437     using interval_split [OF i] div by (fastforce simp: Dlec_def division_of_def)
```
```   438   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
```
```   439     using Dlec_def by blast
```
```   440   have Dgec_cbox: "\<And>K. K \<in> Dgec \<Longrightarrow> \<exists>a b. K = cbox a b"
```
```   441     using interval_split [OF i] div by (fastforce simp: Dgec_def division_of_def)
```
```   442   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
```
```   443     using Dgec_def by blast
```
```   444   have "(b' \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>Dlec. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<le> content(cbox a b')"
```
```   445   proof (rule content_division_lemma1)
```
```   446     show "Dlec division_of \<Union>Dlec"
```
```   447       unfolding division_of_def
```
```   448     proof (intro conjI ballI Dlec_cbox)
```
```   449       show "\<And>K1 K2. \<lbrakk>K1 \<in> Dlec; K2 \<in> Dlec\<rbrakk> \<Longrightarrow> K1 \<noteq> K2 \<longrightarrow> interior K1 \<inter> interior K2 = {}"
```
```   450         by (clarsimp simp: Dlec_def) (use div in auto)
```
```   451     qed (use \<open>finite \<D>\<close> Dlec_def in auto)
```
```   452     show "\<Union>Dlec \<subseteq> cbox a b'"
```
```   453       using Dlec_def div S by (auto simp: b'_def division_of_def mem_box)
```
```   454     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> {})"
```
```   455       using nonmt by (fastforce simp: Dlec_def b'_def sum_if_inner i)
```
```   456   qed (use i Dlec_def in auto)
```
```   457   moreover
```
```   458   have "(\<Sum>K\<in>Dlec. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) =
```
```   459         (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)"
```
```   460     apply (subst sum.reindex_nontrivial [OF \<open>finite \<D>\<close>, symmetric], simp)
```
```   461      apply (metis division_split_left_inj [OF div] lec_is_cbox content_eq_0_interior)
```
```   462     unfolding Dlec_def using \<open>finite \<D>\<close> apply (auto simp: sum.mono_neutral_left)
```
```   463     done
```
```   464   moreover have "(b' \<bullet> i - a \<bullet> i) = (c - a \<bullet> i)"
```
```   465     by (simp add: b'_def sum_if_inner i)
```
```   466   ultimately
```
```   467   have lec: "(c - a \<bullet> i) * (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
```
```   468              \<le> content(cbox a b')"
```
```   469     by simp
```
```   470
```
```   471   have "(b \<bullet> i - a' \<bullet> i) * (\<Sum>K\<in>Dgec. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<le> content(cbox a' b)"
```
```   472   proof (rule content_division_lemma1)
```
```   473     show "Dgec division_of \<Union>Dgec"
```
```   474       unfolding division_of_def
```
```   475     proof (intro conjI ballI Dgec_cbox)
```
```   476       show "\<And>K1 K2. \<lbrakk>K1 \<in> Dgec; K2 \<in> Dgec\<rbrakk> \<Longrightarrow> K1 \<noteq> K2 \<longrightarrow> interior K1 \<inter> interior K2 = {}"
```
```   477         by (clarsimp simp: Dgec_def) (use div in auto)
```
```   478     qed (use \<open>finite \<D>\<close> Dgec_def in auto)
```
```   479     show "\<Union>Dgec \<subseteq> cbox a' b"
```
```   480       using Dgec_def div S by (auto simp: a'_def division_of_def mem_box)
```
```   481     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> {})"
```
```   482       using nonmt by (fastforce simp: Dgec_def a'_def sum_if_inner i)
```
```   483   qed (use i Dgec_def in auto)
```
```   484   moreover
```
```   485   have "(\<Sum>K\<in>Dgec. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) =
```
```   486         (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
```
```   487     apply (subst sum.reindex_nontrivial [OF \<open>finite \<D>\<close>, symmetric], simp)
```
```   488      apply (metis division_split_right_inj [OF div] gec_is_cbox content_eq_0_interior)
```
```   489     unfolding Dgec_def using \<open>finite \<D>\<close> apply (auto simp: sum.mono_neutral_left)
```
```   490     done
```
```   491   moreover have "(b \<bullet> i - a' \<bullet> i) = (b \<bullet> i - c)"
```
```   492     by (simp add: a'_def sum_if_inner i)
```
```   493   ultimately
```
```   494   have gec: "(b \<bullet> i - c) * (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
```
```   495              \<le> content(cbox a' b)"
```
```   496     by simp
```
```   497   show ?thesis
```
```   498   proof (cases "c = a \<bullet> i \<or> c = b \<bullet> i")
```
```   499     case True
```
```   500     then show ?thesis
```
```   501     proof
```
```   502       assume c: "c = a \<bullet> i"
```
```   503       then have "a' = a"
```
```   504         apply (simp add: sum_if_inner i a'_def cong: if_cong)
```
```   505         using euclidean_representation [of a] sum.cong [OF refl, of Basis "\<lambda>i. (a \<bullet> i) *\<^sub>R i"] by presburger
```
```   506       then have "content (cbox a' b) \<le> 2 * content (cbox a b)"  by simp
```
```   507       moreover
```
```   508       have eq: "(\<Sum>K\<in>\<D>. content (K \<inter> {x. a \<bullet> i \<le> x \<bullet> i}) /
```
```   509                   (interval_upperbound (K \<inter> {x. a \<bullet> i \<le> x \<bullet> i}) \<bullet> i - interval_lowerbound (K \<inter> {x. a \<bullet> i \<le> x \<bullet> i}) \<bullet> i))
```
```   510               = (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
```
```   511                (is "sum ?f _ = sum ?g _")
```
```   512       proof (rule sum.cong [OF refl])
```
```   513         fix K assume "K \<in> \<D>"
```
```   514         then have "a \<bullet> i \<le> x \<bullet> i" if "x \<in> K" for x
```
```   515           by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
```
```   516         then have "K \<inter> {x. a \<bullet> i \<le> x \<bullet> i} = K"
```
```   517           by blast
```
```   518         then show "?f K = ?g K"
```
```   519           by simp
```
```   520       qed
```
```   521       ultimately show ?thesis
```
```   522         using gec c eq by auto
```
```   523     next
```
```   524       assume c: "c = b \<bullet> i"
```
```   525       then have "b' = b"
```
```   526         apply (simp add: sum_if_inner i b'_def cong: if_cong)
```
```   527         using euclidean_representation [of b] sum.cong [OF refl, of Basis "\<lambda>i. (b \<bullet> i) *\<^sub>R i"] by presburger
```
```   528       then have "content (cbox a b') \<le> 2 * content (cbox a b)"  by simp
```
```   529       moreover
```
```   530       have eq: "(\<Sum>K\<in>\<D>. content (K \<inter> {x. x \<bullet> i \<le> b \<bullet> i}) /
```
```   531                   (interval_upperbound (K \<inter> {x. x \<bullet> i \<le> b \<bullet> i}) \<bullet> i - interval_lowerbound (K \<inter> {x. x \<bullet> i \<le> b \<bullet> i}) \<bullet> i))
```
```   532               = (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
```
```   533                (is "sum ?f _ = sum ?g _")
```
```   534       proof (rule sum.cong [OF refl])
```
```   535         fix K assume "K \<in> \<D>"
```
```   536         then have "x \<bullet> i \<le> b \<bullet> i" if "x \<in> K" for x
```
```   537           by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
```
```   538         then have "K \<inter> {x. x \<bullet> i \<le> b \<bullet> i} = K"
```
```   539           by blast
```
```   540         then show "?f K = ?g K"
```
```   541           by simp
```
```   542       qed
```
```   543       ultimately show ?thesis
```
```   544         using lec c eq by auto
```
```   545     qed
```
```   546   next
```
```   547     case False
```
```   548     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
```
```   549       using that mk_disjoint_insert [OF i]
```
```   550       apply (clarsimp simp add: divide_simps)
```
```   551       by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf mult.commute order_refl prod.insert subset_Compl_singleton)
```
```   552     have abc: "a \<bullet> i < c" "c < b \<bullet> i"
```
```   553       using False assms by auto
```
```   554     then have "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K)
```
```   555                   \<le> content(cbox a b') / (c - a \<bullet> i)"
```
```   556               "(\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)
```
```   557                  \<le> content(cbox a' b) / (b \<bullet> i - c)"
```
```   558       using lec gec by (simp_all add: divide_simps mult.commute)
```
```   559     moreover
```
```   560     have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
```
```   561           \<le> (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K) +
```
```   562             (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
```
```   563            (is "?lhs \<le> ?rhs")
```
```   564     proof -
```
```   565       have "?lhs \<le>
```
```   566             (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K +
```
```   567                     ((\<lambda>K. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
```
```   568             (is "sum ?f _ \<le> sum ?g _")
```
```   569       proof (rule sum_mono)
```
```   570         fix K assume "K \<in> \<D>"
```
```   571         then obtain u v where uv: "K = cbox u v"
```
```   572           using div by blast
```
```   573         obtain u' v' where uv': "cbox u v \<inter> {x. x \<bullet> i \<le> c} = cbox u v'"
```
```   574                                 "cbox u v \<inter> {x. c \<le> x \<bullet> i} = cbox u' v"
```
```   575                                 "\<And>k. k \<in> Basis \<Longrightarrow> u' \<bullet> k = (if k = i then max (u \<bullet> i) c else u \<bullet> k)"
```
```   576                                 "\<And>k. k \<in> Basis \<Longrightarrow> v' \<bullet> k = (if k = i then min (v \<bullet> i) c else v \<bullet> k)"
```
```   577           using i by (auto simp: interval_split)
```
```   578         have *: "\<lbrakk>content (cbox u v') = 0; content (cbox u' v) = 0\<rbrakk> \<Longrightarrow> content (cbox u v) = 0"
```
```   579                 "content (cbox u' v) \<noteq> 0 \<Longrightarrow> content (cbox u v) \<noteq> 0"
```
```   580                 "content (cbox u v') \<noteq> 0 \<Longrightarrow> content (cbox u v) \<noteq> 0"
```
```   581           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)
```
```   582         show "?f K \<le> ?g K"
```
```   583           using i uv uv' apply (clarsimp simp add: lemma0 * intro!: prod_nonneg)
```
```   584           by (metis content_eq_0 le_less_linear order.strict_implies_order)
```
```   585       qed
```
```   586       also have "... = ?rhs"
```
```   587         by (simp add: sum.distrib)
```
```   588       finally show ?thesis .
```
```   589     qed
```
```   590     moreover have "content (cbox a b') / (c - a \<bullet> i) = content (cbox a b) / (b \<bullet> i - a \<bullet> i)"
```
```   591       using i abc
```
```   592       apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff)
```
```   593       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)
```
```   594       done
```
```   595     moreover have "content (cbox a' b) / (b \<bullet> i - c) = content (cbox a b) / (b \<bullet> i - a \<bullet> i)"
```
```   596       using i abc
```
```   597       apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff)
```
```   598       apply (auto simp: if_distrib prod.If_cases [of Basis "\<lambda>x. x = i", simplified] prod_if field_simps)
```
```   599       done
```
```   600     ultimately
```
```   601     have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
```
```   602           \<le> 2 * content (cbox a b) / (b \<bullet> i - a \<bullet> i)"
```
```   603       by linarith
```
```   604     then show ?thesis
```
```   605       using abc by (simp add: divide_simps mult.commute)
```
```   606   qed
```
```   607 qed
```
```   608
```
```   609
```
```   610
```
```   611
```
```   612 proposition bounded_equiintegral_over_thin_tagged_partial_division:
```
```   613   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   614   assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F" and "0 < \<epsilon>"
```
```   615       and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
```
```   616   obtains \<gamma> where "gauge \<gamma>"
```
```   617              "\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
```
```   618                          \<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>
```
```   619                         \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
```
```   620 proof (cases "content(cbox a b) = 0")
```
```   621   case True
```
```   622   show ?thesis
```
```   623   proof
```
```   624     show "gauge (\<lambda>x. ball x 1)"
```
```   625       by (simp add: gauge_trivial)
```
```   626     show "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
```
```   627          if "S tagged_partial_division_of cbox a b" "(\<lambda>x. ball x 1) fine S" for S and h:: "'a \<Rightarrow> 'b"
```
```   628     proof -
```
```   629       have "(\<Sum>(x,K) \<in> S. norm (integral K h)) = 0"
```
```   630           using that True content_0_subset
```
```   631           by (fastforce simp: tagged_partial_division_of_def intro: sum.neutral)
```
```   632       with \<open>0 < \<epsilon>\<close> show ?thesis
```
```   633         by simp
```
```   634     qed
```
```   635   qed
```
```   636 next
```
```   637   case False
```
```   638   then have contab_gt0:  "content(cbox a b) > 0"
```
```   639     by (simp add: zero_less_measure_iff)
```
```   640   then have a_less_b: "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
```
```   641     by (auto simp: content_pos_lt_eq)
```
```   642   obtain \<gamma>0 where "gauge \<gamma>0"
```
```   643             and \<gamma>0: "\<And>S h. \<lbrakk>S tagged_partial_division_of cbox a b; \<gamma>0 fine S; h \<in> F\<rbrakk>
```
```   644                            \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
```
```   645   proof -
```
```   646     obtain \<gamma> where "gauge \<gamma>"
```
```   647                and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
```
```   648                               \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f)
```
```   649                                   < \<epsilon>/(5 * (Suc DIM('b)))"
```
```   650     proof -
```
```   651       have e5: "\<epsilon>/(5 * (Suc DIM('b))) > 0"
```
```   652         using \<open>\<epsilon> > 0\<close> by auto
```
```   653       then show ?thesis
```
```   654         using F that by (auto simp: equiintegrable_on_def)
```
```   655     qed
```
```   656     show ?thesis
```
```   657     proof
```
```   658       show "gauge \<gamma>"
```
```   659         by (rule \<open>gauge \<gamma>\<close>)
```
```   660       show "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
```
```   661            if "S tagged_partial_division_of cbox a b" "\<gamma> fine S" "h \<in> F" for S h
```
```   662       proof -
```
```   663         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)))"
```
```   664         proof (rule Henstock_lemma_part2 [of h a b])
```
```   665           show "h integrable_on cbox a b"
```
```   666             using that F equiintegrable_on_def by metis
```
```   667           show "gauge \<gamma>"
```
```   668             by (rule \<open>gauge \<gamma>\<close>)
```
```   669         qed (use that \<open>\<epsilon> > 0\<close> \<gamma> in auto)
```
```   670         also have "... < \<epsilon>/2"
```
```   671           using \<open>\<epsilon> > 0\<close> by (simp add: divide_simps)
```
```   672         finally show ?thesis .
```
```   673       qed
```
```   674     qed
```
```   675   qed
```
```   676   define \<gamma> where "\<gamma> \<equiv> \<lambda>x. \<gamma>0 x \<inter>
```
```   677                           ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
```
```   678   have "gauge (\<lambda>x. ball x
```
```   679                     (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
```
```   680     using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b
```
```   681     apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
```
```   682     apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral)
```
```   683     done
```
```   684   then have "gauge \<gamma>"
```
```   685     unfolding \<gamma>_def using \<open>gauge \<gamma>0\<close> gauge_Int by auto
```
```   686   moreover
```
```   687   have "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
```
```   688        if "c \<in> cbox a b" "i \<in> Basis" and S: "S tagged_partial_division_of cbox a b"
```
```   689           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
```
```   690   proof -
```
```   691     have "cbox c b \<subseteq> cbox a b"
```
```   692       by (meson mem_box(2) order_refl subset_box(1) that(1))
```
```   693     have "finite S"
```
```   694       using S by blast
```
```   695     have "\<gamma>0 fine S" and fineS:
```
```   696          "(\<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"
```
```   697       using \<open>\<gamma> fine S\<close> by (auto simp: \<gamma>_def fine_Int)
```
```   698     then have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
```
```   699       by (intro \<gamma>0 that fineS)
```
```   700     moreover have "(\<Sum>(x,K) \<in> S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h)) \<le> \<epsilon>/2"
```
```   701     proof -
```
```   702       have "(\<Sum>(x,K) \<in> S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h))
```
```   703             \<le> (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x))"
```
```   704       proof (clarify intro!: sum_mono)
```
```   705         fix x K
```
```   706         assume xK: "(x,K) \<in> S"
```
```   707         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))"
```
```   708           by (metis norm_minus_commute norm_triangle_ineq2)
```
```   709         also have "... \<le> norm (content K *\<^sub>R h x)"
```
```   710           by simp
```
```   711         finally show "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \<le> norm (content K *\<^sub>R h x)" .
```
```   712       qed
```
```   713       also have "... \<le> (\<Sum>(x,K) \<in> S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) *
```
```   714                                     content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
```
```   715       proof (clarify intro!: sum_mono)
```
```   716         fix x K
```
```   717         assume xK: "(x,K) \<in> S"
```
```   718         then have x: "x \<in> cbox a b"
```
```   719           using S unfolding tagged_partial_division_of_def by (meson subset_iff)
```
```   720         let ?\<Delta> = "interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i"
```
```   721         show "norm (content K *\<^sub>R h x) \<le> \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K / ?\<Delta>"
```
```   722         proof (cases "content K = 0")
```
```   723           case True
```
```   724           then show ?thesis by simp
```
```   725         next
```
```   726           case False
```
```   727           then have Kgt0: "content K > 0"
```
```   728             using zero_less_measure_iff by blast
```
```   729           moreover
```
```   730           obtain u v where uv: "K = cbox u v"
```
```   731             using S \<open>(x,K) \<in> S\<close> by blast
```
```   732           then have u_less_v: "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i < v \<bullet> i"
```
```   733             using content_pos_lt_eq uv Kgt0 by blast
```
```   734           then have dist_uv: "dist u v > 0"
```
```   735             using that by auto
```
```   736           ultimately have "norm (h x) \<le> (\<epsilon> * (b \<bullet> i - a \<bullet> i)) / (4 * content (cbox a b) * ?\<Delta>)"
```
```   737           proof -
```
```   738             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"
```
```   739                  "dist x v < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
```
```   740               using fineS u_less_v uv xK
```
```   741               by (force simp: fine_def mem_box field_simps dest!: bspec)+
```
```   742             moreover have "\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
```
```   743                   \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
```
```   744               apply (intro mult_left_mono divide_right_mono)
```
```   745               using \<open>i \<in> Basis\<close> \<open>0 < \<epsilon>\<close> apply (auto simp: intro!: cInf_le_finite)
```
```   746               done
```
```   747             ultimately
```
```   748             have "dist x u < \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
```
```   749                  "dist x v < \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
```
```   750               by linarith+
```
```   751             then have duv: "dist u v < \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b))"
```
```   752               using dist_triangle_half_r by blast
```
```   753             have uvi: "\<bar>v \<bullet> i - u \<bullet> i\<bar> \<le> norm (v - u)"
```
```   754               by (metis inner_commute inner_diff_right \<open>i \<in> Basis\<close> Basis_le_norm)
```
```   755             have "norm (h x) \<le> norm (f x)"
```
```   756               using x that by (auto simp: norm_f)
```
```   757             also have "... < (norm (f x) + 1)"
```
```   758               by simp
```
```   759             also have "... < \<epsilon> * (b \<bullet> i - a \<bullet> i) / dist u v / (4 * content (cbox a b))"
```
```   760               using duv dist_uv contab_gt0
```
```   761               apply (simp add: divide_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm)
```
```   762               by (meson add_nonneg_nonneg linorder_not_le measure_nonneg mult_nonneg_nonneg norm_ge_zero zero_le_numeral)
```
```   763             also have "... = \<epsilon> * (b \<bullet> i - a \<bullet> i) / norm (v - u) / (4 * content (cbox a b))"
```
```   764               by (simp add: dist_norm norm_minus_commute)
```
```   765             also have "... \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / \<bar>v \<bullet> i - u \<bullet> i\<bar> / (4 * content (cbox a b))"
```
```   766               apply (intro mult_right_mono divide_left_mono divide_right_mono uvi)
```
```   767               using \<open>0 < \<epsilon>\<close> a_less_b [OF \<open>i \<in> Basis\<close>] u_less_v [OF \<open>i \<in> Basis\<close>] contab_gt0
```
```   768               by (auto simp: less_eq_real_def zero_less_mult_iff that)
```
```   769             also have "... = \<epsilon> * (b \<bullet> i - a \<bullet> i)
```
```   770                        / (4 * content (cbox a b) * ?\<Delta>)"
```
```   771               using uv False that(2) u_less_v by fastforce
```
```   772             finally show ?thesis by simp
```
```   773           qed
```
```   774           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)) / ?\<Delta>)"
```
```   775             using mult_left_mono by fastforce
```
```   776           also have "... = \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) *
```
```   777                            content K / ?\<Delta>"
```
```   778             by (simp add: divide_simps)
```
```   779           finally show ?thesis .
```
```   780         qed
```
```   781       qed
```
```   782       also have "... = (\<Sum>K\<in>snd ` S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K
```
```   783                                      / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
```
```   784         apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]])
```
```   785         apply (simp add: box_eq_empty(1) content_eq_0)
```
```   786         done
```
```   787       also have "... = \<epsilon>/2 * ((b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)))"
```
```   788         by (simp add: sum_distrib_left mult.assoc)
```
```   789       also have "... \<le> (\<epsilon>/2) * 1"
```
```   790       proof (rule mult_left_mono)
```
```   791         have "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
```
```   792               \<le> 2 * content (cbox a b)"
```
```   793         proof (rule sum_content_area_over_thin_division)
```
```   794           show "snd ` S division_of \<Union>(snd ` S)"
```
```   795             by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
```
```   796           show "\<Union>(snd ` S) \<subseteq> cbox a b"
```
```   797             using S by force
```
```   798           show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
```
```   799             using mem_box(2) that by blast+
```
```   800         qed (use that in auto)
```
```   801         then show "(b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<le> 1"
```
```   802           by (simp add: contab_gt0)
```
```   803       qed (use \<open>0 < \<epsilon>\<close> in auto)
```
```   804       finally show ?thesis by simp
```
```   805     qed
```
```   806     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"
```
```   807       by (simp add: Groups_Big.sum_subtractf [symmetric])
```
```   808     ultimately show "(\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
```
```   809       by linarith
```
```   810   qed
```
```   811   ultimately show ?thesis using that by auto
```
```   812 qed
```
```   813
```
```   814
```
```   815
```
```   816 proposition equiintegrable_halfspace_restrictions_le:
```
```   817   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```   818   assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
```
```   819     and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
```
```   820   shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<le> c then h x else 0)})
```
```   821          equiintegrable_on cbox a b"
```
```   822 proof (cases "content(cbox a b) = 0")
```
```   823   case True
```
```   824   then show ?thesis by simp
```
```   825 next
```
```   826   case False
```
```   827   then have "content(cbox a b) > 0"
```
```   828     using zero_less_measure_iff by blast
```
```   829   then have "a \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
```
```   830     using content_pos_lt_eq that by blast
```
```   831   have int_F: "f integrable_on cbox a b" if "f \<in> F" for f
```
```   832     using F that by (simp add: equiintegrable_on_def)
```
```   833   let ?CI = "\<lambda>K h x. content K *\<^sub>R h x - integral K h"
```
```   834   show ?thesis
```
```   835     unfolding equiintegrable_on_def
```
```   836   proof (intro conjI; clarify)
```
```   837     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
```
```   838       using integrable_restrict_Int [of "{x. x \<bullet> i \<le> c}" h]
```
```   839       apply (auto simp: interval_split Int_commute mem_box intro!: integrable_on_subcbox int_F)
```
```   840       by (metis (full_types, hide_lams) min.bounded_iff)
```
```   841     show "\<exists>\<gamma>. gauge \<gamma> \<and>
```
```   842               (\<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>
```
```   843                      T tagged_division_of cbox a b \<and> \<gamma> fine T \<longrightarrow>
```
```   844                      norm ((\<Sum>(x,K) \<in> T. content K *\<^sub>R f x) - integral (cbox a b) f) < \<epsilon>)"
```
```   845       if "\<epsilon> > 0" for \<epsilon>
```
```   846     proof -
```
```   847       obtain \<gamma>0 where "gauge \<gamma>0" and \<gamma>0:
```
```   848         "\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
```
```   849                         \<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>
```
```   850                        \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>/12"
```
```   851         apply (rule bounded_equiintegral_over_thin_tagged_partial_division [OF F f, of \<open>\<epsilon>/12\<close>])
```
```   852         using \<open>\<epsilon> > 0\<close> by (auto simp: norm_f)
```
```   853       obtain \<gamma>1 where "gauge \<gamma>1"
```
```   854         and \<gamma>1: "\<And>h T. \<lbrakk>h \<in> F; T tagged_division_of cbox a b; \<gamma>1 fine T\<rbrakk>
```
```   855                               \<Longrightarrow> norm ((\<Sum>(x,K) \<in> T. content K *\<^sub>R h x) - integral (cbox a b) h)
```
```   856                                   < \<epsilon>/(7 * (Suc DIM('b)))"
```
```   857       proof -
```
```   858         have e5: "\<epsilon>/(7 * (Suc DIM('b))) > 0"
```
```   859           using \<open>\<epsilon> > 0\<close> by auto
```
```   860         then show ?thesis
```
```   861           using F that by (auto simp: equiintegrable_on_def)
```
```   862       qed
```
```   863       have h_less3: "(\<Sum>(x,K) \<in> T. norm (?CI K h x)) < \<epsilon>/3"
```
```   864         if "T tagged_partial_division_of cbox a b" "\<gamma>1 fine T" "h \<in> F" for T h
```
```   865       proof -
```
```   866         have "(\<Sum>(x,K) \<in> T. norm (?CI K h x)) \<le> 2 * real DIM('b) * (\<epsilon>/(7 * Suc DIM('b)))"
```
```   867         proof (rule Henstock_lemma_part2 [of h a b])
```
```   868           show "h integrable_on cbox a b"
```
```   869             using that F equiintegrable_on_def by metis
```
```   870           show "gauge \<gamma>1"
```
```   871             by (rule \<open>gauge \<gamma>1\<close>)
```
```   872         qed (use that \<open>\<epsilon> > 0\<close> \<gamma>1 in auto)
```
```   873         also have "... < \<epsilon>/3"
```
```   874           using \<open>\<epsilon> > 0\<close> by (simp add: divide_simps)
```
```   875         finally show ?thesis .
```
```   876       qed
```
```   877       have *: "norm ((\<Sum>(x,K) \<in> T. content K *\<^sub>R f x) - integral (cbox a b) f) < \<epsilon>"
```
```   878                 if f: "f = (\<lambda>x. if x \<bullet> i \<le> c then h x else 0)"
```
```   879                 and T: "T tagged_division_of cbox a b"
```
```   880                 and fine: "(\<lambda>x. \<gamma>0 x \<inter> \<gamma>1 x) fine T" and "i \<in> Basis" "h \<in> F" for f T i c h
```
```   881       proof (cases "a \<bullet> i \<le> c \<and> c \<le> b \<bullet> i")
```
```   882         case True
```
```   883         have "finite T"
```
```   884           using T by blast
```
```   885         define T' where "T' \<equiv> {(x,K) \<in> T. K \<inter> {x. x \<bullet> i \<le> c} \<noteq> {}}"
```
```   886         then have "T' \<subseteq> T"
```
```   887           by auto
```
```   888         then have "finite T'"
```
```   889           using \<open>finite T\<close> infinite_super by blast
```
```   890         have T'_tagged: "T' tagged_partial_division_of cbox a b"
```
```   891           by (meson T \<open>T' \<subseteq> T\<close> tagged_division_of_def tagged_partial_division_subset)
```
```   892         have fine': "\<gamma>0 fine T'" "\<gamma>1 fine T'"
```
```   893           using \<open>T' \<subseteq> T\<close> fine_Int fine_subset fine by blast+
```
```   894         have int_KK': "(\<Sum>(x,K) \<in> T. integral K f) = (\<Sum>(x,K) \<in> T'. integral K f)"
```
```   895           apply (rule sum.mono_neutral_right [OF \<open>finite T\<close> \<open>T' \<subseteq> T\<close>])
```
```   896           using f \<open>finite T\<close> \<open>T' \<subseteq> T\<close>
```
```   897           using integral_restrict_Int [of _ "{x. x \<bullet> i \<le> c}" h]
```
```   898           apply (auto simp: T'_def Int_commute)
```
```   899           done
```
```   900         have "(\<Sum>(x,K) \<in> T. content K *\<^sub>R f x) = (\<Sum>(x,K) \<in> T'. content K *\<^sub>R f x)"
```
```   901           apply (rule sum.mono_neutral_right [OF \<open>finite T\<close> \<open>T' \<subseteq> T\<close>])
```
```   902           using T f \<open>finite T\<close> \<open>T' \<subseteq> T\<close> apply (force simp: T'_def)
```
```   903           done
```
```   904         moreover have "norm ((\<Sum>(x,K) \<in> T'. content K *\<^sub>R f x) - integral (cbox a b) f) < \<epsilon>"
```
```   905         proof -
```
```   906           have *: "norm y < \<epsilon>" if "norm x < \<epsilon>/3" "norm(x - y) \<le> 2 * \<epsilon>/3" for x y::'b
```
```   907           proof -
```
```   908             have "norm y \<le> norm x + norm(x - y)"
```
```   909               by (metis norm_minus_commute norm_triangle_sub)
```
```   910             also have "\<dots> < \<epsilon>/3 + 2*\<epsilon>/3"
```
```   911               using that by linarith
```
```   912             also have "... = \<epsilon>"
```
```   913               by simp
```
```   914             finally show ?thesis .
```
```   915           qed
```
```   916           have "norm (\<Sum>(x,K) \<in> T'. ?CI K h x)
```
```   917                 \<le> (\<Sum>(x,K) \<in> T'. norm (?CI K h x))"
```
```   918             by (simp add: norm_sum split_def)
```
```   919           also have "... < \<epsilon>/3"
```
```   920             by (intro h_less3 T'_tagged fine' that)
```
```   921           finally have "norm (\<Sum>(x,K) \<in> T'. ?CI K h x) < \<epsilon>/3" .
```
```   922           moreover have "integral (cbox a b) f = (\<Sum>(x,K) \<in> T. integral K f)"
```
```   923             using int_lec that by (auto simp: integral_combine_tagged_division_topdown)
```
```   924           moreover have "norm (\<Sum>(x,K) \<in> T'. ?CI K h x - ?CI K f x)
```
```   925                 \<le> 2*\<epsilon>/3"
```
```   926           proof -
```
```   927             define T'' where "T'' \<equiv> {(x,K) \<in> T'. \<not> (K \<subseteq> {x. x \<bullet> i \<le> c})}"
```
```   928             then have "T'' \<subseteq> T'"
```
```   929               by auto
```
```   930             then have "finite T''"
```
```   931               using \<open>finite T'\<close> infinite_super by blast
```
```   932             have T''_tagged: "T'' tagged_partial_division_of cbox a b"
```
```   933               using T'_tagged \<open>T'' \<subseteq> T'\<close> tagged_partial_division_subset by blast
```
```   934             have fine'': "\<gamma>0 fine T''" "\<gamma>1 fine T''"
```
```   935               using \<open>T'' \<subseteq> T'\<close> fine' by (blast intro: fine_subset)+
```
```   936             have "(\<Sum>(x,K) \<in> T'. ?CI K h x - ?CI K f x)
```
```   937                 = (\<Sum>(x,K) \<in> T''. ?CI K h x - ?CI K f x)"
```
```   938             proof (clarify intro!: sum.mono_neutral_right [OF \<open>finite T'\<close> \<open>T'' \<subseteq> T'\<close>])
```
```   939               fix x K
```
```   940               assume "(x,K) \<in> T'" "(x,K) \<notin> T''"
```
```   941               then have "x \<in> K" "x \<bullet> i \<le> c" "{x. x \<bullet> i \<le> c} \<inter> K = K"
```
```   942                 using T''_def T'_tagged by blast+
```
```   943               then show "?CI K h x - ?CI K f x = 0"
```
```   944                 using integral_restrict_Int [of _ "{x. x \<bullet> i \<le> c}" h] by (auto simp: f)
```
```   945             qed
```
```   946             moreover have "norm (\<Sum>(x,K) \<in> T''. ?CI K h x - ?CI K f x) \<le> 2*\<epsilon>/3"
```
```   947             proof -
```
```   948               define A where "A \<equiv> {(x,K) \<in> T''. x \<bullet> i \<le> c}"
```
```   949               define B where "B \<equiv> {(x,K) \<in> T''. x \<bullet> i > c}"
```
```   950               then have "A \<subseteq> T''" "B \<subseteq> T''" and disj: "A \<inter> B = {}" and T''_eq: "T'' = A \<union> B"
```
```   951                 by (auto simp: A_def B_def)
```
```   952               then have "finite A" "finite B"
```
```   953                 using \<open>finite T''\<close>  by (auto intro: finite_subset)
```
```   954               have A_tagged: "A tagged_partial_division_of cbox a b"
```
```   955                 using T''_tagged \<open>A \<subseteq> T''\<close> tagged_partial_division_subset by blast
```
```   956               have fineA: "\<gamma>0 fine A" "\<gamma>1 fine A"
```
```   957                 using \<open>A \<subseteq> T''\<close> fine'' by (blast intro: fine_subset)+
```
```   958               have B_tagged: "B tagged_partial_division_of cbox a b"
```
```   959                 using T''_tagged \<open>B \<subseteq> T''\<close> tagged_partial_division_subset by blast
```
```   960               have fineB: "\<gamma>0 fine B" "\<gamma>1 fine B"
```
```   961                 using \<open>B \<subseteq> T''\<close> fine'' by (blast intro: fine_subset)+
```
```   962               have "norm (\<Sum>(x,K) \<in> T''. ?CI K h x - ?CI K f x)
```
```   963                           \<le> (\<Sum>(x,K) \<in> T''. norm (?CI K h x - ?CI K f x))"
```
```   964                 by (simp add: norm_sum split_def)
```
```   965               also have "... = (\<Sum>(x,K) \<in> A. norm (?CI K h x - ?CI K f x)) +
```
```   966                                (\<Sum>(x,K) \<in> B. norm (?CI K h x - ?CI K f x))"
```
```   967                 by (simp add: sum.union_disjoint T''_eq disj \<open>finite A\<close> \<open>finite B\<close>)
```
```   968               also have "... = (\<Sum>(x,K) \<in> A. norm (integral K h - integral K f)) +
```
```   969                                (\<Sum>(x,K) \<in> B. norm (?CI K h x + integral K f))"
```
```   970                 by (auto simp: A_def B_def f norm_minus_commute intro!: sum.cong arg_cong2 [where f= "(+)"])
```
```   971               also have "... \<le> (\<Sum>(x,K)\<in>A. norm (integral K h)) +
```
```   972                                  (\<Sum>(x,K)\<in>(\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c})) ` A. norm (integral K h))
```
```   973                              + ((\<Sum>(x,K)\<in>B. norm (?CI K h x)) +
```
```   974                                 (\<Sum>(x,K)\<in>B. norm (integral K h)) +
```
```   975                                   (\<Sum>(x,K)\<in>(\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i})) ` B. norm (integral K h)))"
```
```   976               proof (rule add_mono)
```
```   977                 show "(\<Sum>(x,K)\<in>A. norm (integral K h - integral K f))
```
```   978                         \<le> (\<Sum>(x,K)\<in>A. norm (integral K h)) +
```
```   979                            (\<Sum>(x,K)\<in>(\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c})) ` A.
```
```   980                               norm (integral K h))"
```
```   981                 proof (subst sum.reindex_nontrivial [OF \<open>finite A\<close>], clarsimp)
```
```   982                   fix x K L
```
```   983                   assume "(x,K) \<in> A" "(x,L) \<in> A"
```
```   984                     and int_ne0: "integral (L \<inter> {x. x \<bullet> i \<le> c}) h \<noteq> 0"
```
```   985                     and eq: "K \<inter> {x. x \<bullet> i \<le> c} = L \<inter> {x. x \<bullet> i \<le> c}"
```
```   986                   have False if "K \<noteq> L"
```
```   987                   proof -
```
```   988                     obtain u v where uv: "L = cbox u v"
```
```   989                       using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
```
```   990                     have "A tagged_division_of \<Union>(snd ` A)"
```
```   991                       using A_tagged tagged_partial_division_of_Union_self by auto
```
```   992                     then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}"
```
```   993                       apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>])
```
```   994                       using that eq \<open>i \<in> Basis\<close> by auto
```
```   995                     then show False
```
```   996                       using interval_split [OF \<open>i \<in> Basis\<close>] int_ne0 content_eq_0_interior eq uv by fastforce
```
```   997                   qed
```
```   998                   then show "K = L" by blast
```
```   999                 next
```
```  1000                   show "(\<Sum>(x,K) \<in> A. norm (integral K h - integral K f))
```
```  1001                           \<le> (\<Sum>(x,K) \<in> A. norm (integral K h)) +
```
```  1002                              sum ((\<lambda>(x,K). norm (integral K h)) \<circ> (\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c}))) A"
```
```  1003                     using integral_restrict_Int [of _ "{x. x \<bullet> i \<le> c}" h] f
```
```  1004                     by (auto simp: Int_commute A_def [symmetric] sum.distrib [symmetric] intro!: sum_mono norm_triangle_ineq4)
```
```  1005                 qed
```
```  1006               next
```
```  1007                 show "(\<Sum>(x,K)\<in>B. norm (?CI K h x + integral K f))
```
```  1008                       \<le> (\<Sum>(x,K)\<in>B. norm (?CI K h x)) + (\<Sum>(x,K)\<in>B. norm (integral K h)) +
```
```  1009                          (\<Sum>(x,K)\<in>(\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i})) ` B. norm (integral K h))"
```
```  1010                 proof (subst sum.reindex_nontrivial [OF \<open>finite B\<close>], clarsimp)
```
```  1011                   fix x K L
```
```  1012                   assume "(x,K) \<in> B" "(x,L) \<in> B"
```
```  1013                     and int_ne0: "integral (L \<inter> {x. c \<le> x \<bullet> i}) h \<noteq> 0"
```
```  1014                     and eq: "K \<inter> {x. c \<le> x \<bullet> i} = L \<inter> {x. c \<le> x \<bullet> i}"
```
```  1015                   have False if "K \<noteq> L"
```
```  1016                   proof -
```
```  1017                     obtain u v where uv: "L = cbox u v"
```
```  1018                       using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
```
```  1019                     have "B tagged_division_of \<Union>(snd ` B)"
```
```  1020                       using B_tagged tagged_partial_division_of_Union_self by auto
```
```  1021                     then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}"
```
```  1022                       apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>])
```
```  1023                       using that eq \<open>i \<in> Basis\<close> by auto
```
```  1024                     then show False
```
```  1025                       using interval_split [OF \<open>i \<in> Basis\<close>] int_ne0
```
```  1026                         content_eq_0_interior eq uv by fastforce
```
```  1027                   qed
```
```  1028                   then show "K = L" by blast
```
```  1029                 next
```
```  1030                   show "(\<Sum>(x,K) \<in> B. norm (?CI K h x + integral K f))
```
```  1031                         \<le> (\<Sum>(x,K) \<in> B. norm (?CI K h x)) +
```
```  1032                            (\<Sum>(x,K) \<in> B. norm (integral K h)) + sum ((\<lambda>(x,K). norm (integral K h)) \<circ> (\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i}))) B"
```
```  1033                   proof (clarsimp simp: B_def [symmetric] sum.distrib [symmetric] intro!: sum_mono)
```
```  1034                     fix x K
```
```  1035                     assume "(x,K) \<in> B"
```
```  1036                     have *: "i = i1 + i2 \<Longrightarrow> norm(c + i1) \<le> norm c + norm i + norm(i2)"
```
```  1037                       for i::'b and c i1 i2
```
```  1038                       by (metis add.commute add.left_commute add_diff_cancel_right' dual_order.refl norm_add_rule_thm norm_triangle_ineq4)
```
```  1039                     obtain u v where uv: "K = cbox u v"
```
```  1040                       using T'_tagged \<open>(x,K) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
```
```  1041                     have "h integrable_on cbox a b"
```
```  1042                       by (simp add: int_F \<open>h \<in> F\<close>)
```
```  1043                     then have huv: "h integrable_on cbox u v"
```
```  1044                       apply (rule integrable_on_subcbox)
```
```  1045                       using B_tagged \<open>(x,K) \<in> B\<close> uv by blast
```
```  1046                     have "integral K h = integral K f + integral (K \<inter> {x. c \<le> x \<bullet> i}) h"
```
```  1047                       using integral_restrict_Int [of _ "{x. x \<bullet> i \<le> c}" h] f uv \<open>i \<in> Basis\<close>
```
```  1048                       by (simp add: Int_commute integral_split [OF huv \<open>i \<in> Basis\<close>])
```
```  1049                   then show "norm (?CI K h x + integral K f)
```
```  1050                              \<le> norm (?CI K h x) + norm (integral K h) + norm (integral (K \<inter> {x. c \<le> x \<bullet> i}) h)"
```
```  1051                     by (rule *)
```
```  1052                 qed
```
```  1053               qed
```
```  1054             qed
```
```  1055             also have "... \<le> 2*\<epsilon>/3"
```
```  1056             proof -
```
```  1057               have overlap: "K \<inter> {x. x \<bullet> i = c} \<noteq> {}" if "(x,K) \<in> T''" for x K
```
```  1058               proof -
```
```  1059                 obtain y y' where y: "y' \<in> K" "c < y' \<bullet> i" "y \<in> K" "y \<bullet> i \<le> c"
```
```  1060                   using that  T''_def T'_def \<open>(x,K) \<in> T''\<close> by fastforce
```
```  1061                 obtain u v where uv: "K = cbox u v"
```
```  1062                   using T''_tagged \<open>(x,K) \<in> T''\<close> by blast
```
```  1063                 then have "connected K"
```
```  1064                   by (simp add: is_interval_cbox is_interval_connected)
```
```  1065                 then have "(\<exists>z \<in> K. z \<bullet> i = c)"
```
```  1066                   using y connected_ivt_component by fastforce
```
```  1067                 then show ?thesis
```
```  1068                   by fastforce
```
```  1069               qed
```
```  1070               have **: "\<lbrakk>x < \<epsilon>/12; y < \<epsilon>/12; z \<le> \<epsilon>/2\<rbrakk> \<Longrightarrow> x + y + z \<le> 2 * \<epsilon>/3" for x y z
```
```  1071                 by auto
```
```  1072               show ?thesis
```
```  1073               proof (rule **)
```
```  1074                 have cb_ab: "(\<Sum>j \<in> Basis. if j = i then c *\<^sub>R i else (a \<bullet> j) *\<^sub>R j) \<in> cbox a b"
```
```  1075                   using \<open>i \<in> Basis\<close> True \<open>\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i < b \<bullet> i\<close>
```
```  1076                   apply (clarsimp simp add: mem_box)
```
```  1077                   apply (subst sum_if_inner | force)+
```
```  1078                   done
```
```  1079                 show "(\<Sum>(x,K) \<in> A. norm (integral K h)) < \<epsilon>/12"
```
```  1080                   apply (rule \<gamma>0 [OF cb_ab \<open>i \<in> Basis\<close> A_tagged fineA(1) \<open>h \<in> F\<close>])
```
```  1081                   using \<open>i \<in> Basis\<close> \<open>A \<subseteq> T''\<close> overlap
```
```  1082                   apply (subst sum_if_inner | force)+
```
```  1083                   done
```
```  1084                 have 1: "(\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c})) ` A tagged_partial_division_of cbox a b"
```
```  1085                   using \<open>finite A\<close> \<open>i \<in> Basis\<close>
```
```  1086                   apply (auto simp: tagged_partial_division_of_def)
```
```  1087                   using A_tagged apply (auto simp: A_def)
```
```  1088                   using interval_split(1) by blast
```
```  1089                 have 2: "\<gamma>0 fine (\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c})) ` A"
```
```  1090                   using fineA(1) fine_def by fastforce
```
```  1091                 show "(\<Sum>(x,K) \<in> (\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c})) ` A. norm (integral K h)) < \<epsilon>/12"
```
```  1092                   apply (rule \<gamma>0 [OF cb_ab \<open>i \<in> Basis\<close> 1 2 \<open>h \<in> F\<close>])
```
```  1093                   using \<open>i \<in> Basis\<close> apply (subst sum_if_inner | force)+
```
```  1094                   using overlap apply (auto simp: A_def)
```
```  1095                   done
```
```  1096                 have *: "\<lbrakk>x < \<epsilon>/3; y < \<epsilon>/12; z < \<epsilon>/12\<rbrakk> \<Longrightarrow> x + y + z \<le> \<epsilon>/2" for x y z
```
```  1097                   by auto
```
```  1098                 show "(\<Sum>(x,K) \<in> B. norm (?CI K h x)) +
```
```  1099                       (\<Sum>(x,K) \<in> B. norm (integral K h)) +
```
```  1100                       (\<Sum>(x,K) \<in> (\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i})) ` B. norm (integral K h))
```
```  1101                       \<le> \<epsilon>/2"
```
```  1102                 proof (rule *)
```
```  1103                   show "(\<Sum>(x,K) \<in> B. norm (?CI K h x)) < \<epsilon>/3"
```
```  1104                     by (intro h_less3 B_tagged fineB that)
```
```  1105                   show "(\<Sum>(x,K) \<in> B. norm (integral K h)) < \<epsilon>/12"
```
```  1106                     apply (rule \<gamma>0 [OF cb_ab \<open>i \<in> Basis\<close> B_tagged fineB(1) \<open>h \<in> F\<close>])
```
```  1107                     using \<open>i \<in> Basis\<close> \<open>B \<subseteq> T''\<close> overlap by (subst sum_if_inner | force)+
```
```  1108                   have 1: "(\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i})) ` B tagged_partial_division_of cbox a b"
```
```  1109                     using \<open>finite B\<close> \<open>i \<in> Basis\<close>
```
```  1110                     apply (auto simp: tagged_partial_division_of_def)
```
```  1111                     using B_tagged apply (auto simp: B_def)
```
```  1112                     using interval_split(2) by blast
```
```  1113                   have 2: "\<gamma>0 fine (\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i})) ` B"
```
```  1114                     using fineB(1) fine_def by fastforce
```
```  1115                   show "(\<Sum>(x,K) \<in> (\<lambda>(x,K). (x,K \<inter> {x. c \<le> x \<bullet> i})) ` B. norm (integral K h)) < \<epsilon>/12"
```
```  1116                     apply (rule \<gamma>0 [OF cb_ab \<open>i \<in> Basis\<close> 1 2 \<open>h \<in> F\<close>])
```
```  1117                     using \<open>i \<in> Basis\<close> apply (subst sum_if_inner | force)+
```
```  1118                     using overlap apply (auto simp: B_def)
```
```  1119                     done
```
```  1120                 qed
```
```  1121               qed
```
```  1122             qed
```
```  1123             finally show ?thesis .
```
```  1124           qed
```
```  1125           ultimately show ?thesis by metis
```
```  1126         qed
```
```  1127         ultimately show ?thesis
```
```  1128           by (simp add: sum_subtractf [symmetric] int_KK' *)
```
```  1129       qed
```
```  1130         ultimately show ?thesis by metis
```
```  1131       next
```
```  1132         case False
```
```  1133         then consider "c < a \<bullet> i" | "b \<bullet> i < c"
```
```  1134           by auto
```
```  1135         then show ?thesis
```
```  1136         proof cases
```
```  1137           case 1
```
```  1138           then have f0: "f x = 0" if "x \<in> cbox a b" for x
```
```  1139             using that f \<open>i \<in> Basis\<close> mem_box(2) by force
```
```  1140           then have int_f0: "integral (cbox a b) f = 0"
```
```  1141             by (simp add: integral_cong)
```
```  1142           have f0_tag: "f x = 0" if "(x,K) \<in> T" for x K
```
```  1143             using T f0 that by (force simp: tagged_division_of_def)
```
```  1144           then have "(\<Sum>(x,K) \<in> T. content K *\<^sub>R f x) = 0"
```
```  1145             by (metis (mono_tags, lifting) real_vector.scale_eq_0_iff split_conv sum.neutral surj_pair)
```
```  1146           then show ?thesis
```
```  1147             using \<open>0 < \<epsilon>\<close> by (simp add: int_f0)
```
```  1148       next
```
```  1149           case 2
```
```  1150           then have fh: "f x = h x" if "x \<in> cbox a b" for x
```
```  1151             using that f \<open>i \<in> Basis\<close> mem_box(2) by force
```
```  1152           then have int_f: "integral (cbox a b) f = integral (cbox a b) h"
```
```  1153             using integral_cong by blast
```
```  1154           have fh_tag: "f x = h x" if "(x,K) \<in> T" for x K
```
```  1155             using T fh that by (force simp: tagged_division_of_def)
```
```  1156           then have "(\<Sum>(x,K) \<in> T. content K *\<^sub>R f x) = (\<Sum>(x,K) \<in> T. content K *\<^sub>R h x)"
```
```  1157             by (metis (mono_tags, lifting) split_cong sum.cong)
```
```  1158           with \<open>0 < \<epsilon>\<close> show ?thesis
```
```  1159             apply (simp add: int_f)
```
```  1160             apply (rule less_trans [OF \<gamma>1])
```
```  1161             using that fine_Int apply (force simp: divide_simps)+
```
```  1162             done
```
```  1163         qed
```
```  1164       qed
```
```  1165       have  "gauge (\<lambda>x. \<gamma>0 x \<inter> \<gamma>1 x)"
```
```  1166         by (simp add: \<open>gauge \<gamma>0\<close> \<open>gauge \<gamma>1\<close> gauge_Int)
```
```  1167       then show ?thesis
```
```  1168         by (auto intro: *)
```
```  1169     qed
```
```  1170   qed
```
```  1171 qed
```
```  1172
```
```  1173
```
```  1174
```
```  1175 corollary equiintegrable_halfspace_restrictions_ge:
```
```  1176   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```  1177   assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
```
```  1178     and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
```
```  1179   shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<ge> c then h x else 0)})
```
```  1180          equiintegrable_on cbox a b"
```
```  1181 proof -
```
```  1182   have *: "(\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>(\<lambda>f. f \<circ> uminus) ` F. {\<lambda>x. if x \<bullet> i \<le> c then h x else 0})
```
```  1183            equiintegrable_on  cbox (- b) (- a)"
```
```  1184   proof (rule equiintegrable_halfspace_restrictions_le)
```
```  1185     show "(\<lambda>f. f \<circ> uminus) ` F equiintegrable_on cbox (- b) (- a)"
```
```  1186       using F equiintegrable_reflect by blast
```
```  1187     show "f \<circ> uminus \<in> (\<lambda>f. f \<circ> uminus) ` F"
```
```  1188       using f by auto
```
```  1189     show "\<And>h x. \<lbrakk>h \<in> (\<lambda>f. f \<circ> uminus) ` F; x \<in> cbox (- b) (- a)\<rbrakk> \<Longrightarrow> norm (h x) \<le> norm ((f \<circ> uminus) x)"
```
```  1190       using f apply (clarsimp simp:)
```
```  1191       by (metis add.inverse_inverse image_eqI norm_f uminus_interval_vector)
```
```  1192   qed
```
```  1193   have eq: "(\<lambda>f. f \<circ> uminus) `
```
```  1194             (\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>F. {\<lambda>x. if x \<bullet> i \<le> c then (h \<circ> uminus) x else 0}) =
```
```  1195             (\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>F. {\<lambda>x. if c \<le> x \<bullet> i then h x else 0})"
```
```  1196     apply (auto simp: o_def cong: if_cong)
```
```  1197     using minus_le_iff apply fastforce
```
```  1198     apply (rule_tac x="\<lambda>x. if c \<le> (-x) \<bullet> i then h(-x) else 0" in image_eqI)
```
```  1199     using le_minus_iff apply fastforce+
```
```  1200     done
```
```  1201   show ?thesis
```
```  1202     using equiintegrable_reflect [OF *] by (auto simp: eq)
```
```  1203 qed
```
```  1204
```
```  1205
```
```  1206 proposition equiintegrable_closed_interval_restrictions:
```
```  1207   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```  1208   assumes f: "f integrable_on cbox a b"
```
```  1209   shows "(\<Union>c d. {(\<lambda>x. if x \<in> cbox c d then f x else 0)}) equiintegrable_on cbox a b"
```
```  1210 proof -
```
```  1211   let ?g = "\<lambda>B c d x. if \<forall>i\<in>B. c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i then f x else 0"
```
```  1212   have *: "insert f (\<Union>c d. {?g B c d}) equiintegrable_on cbox a b" if "B \<subseteq> Basis" for B
```
```  1213   proof -
```
```  1214     have "finite B"
```
```  1215       using finite_Basis finite_subset \<open>B \<subseteq> Basis\<close> by blast
```
```  1216     then show ?thesis using \<open>B \<subseteq> Basis\<close>
```
```  1217     proof (induction B)
```
```  1218       case empty
```
```  1219       with f show ?case by auto
```
```  1220     next
```
```  1221       case (insert i B)
```
```  1222       then have "i \<in> Basis"
```
```  1223         by auto
```
```  1224       have *: "norm (h x) \<le> norm (f x)"
```
```  1225         if "h \<in> insert f (\<Union>c d. {?g B c d})" "x \<in> cbox a b" for h x
```
```  1226         using that by auto
```
```  1227       have "(\<Union>i\<in>Basis.
```
```  1228                 \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>i\<in>Basis. \<Union>\<psi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<psi> then h x else 0}).
```
```  1229                 {\<lambda>x. if \<xi> \<le> x \<bullet> i then h x else 0})
```
```  1230              equiintegrable_on cbox a b"
```
```  1231       proof (rule equiintegrable_halfspace_restrictions_ge [where f=f])
```
```  1232         show "insert f (\<Union>i\<in>Basis. \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}).
```
```  1233               {\<lambda>x. if x \<bullet> i \<le> \<xi> then h x else 0}) equiintegrable_on cbox a b"
```
```  1234           apply (intro * f equiintegrable_on_insert equiintegrable_halfspace_restrictions_le [OF insert.IH insertI1])
```
```  1235           using insert.prems apply auto
```
```  1236           done
```
```  1237         show"norm(h x) \<le> norm(f x)"
```
```  1238           if "h \<in> insert f (\<Union>i\<in>Basis. \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<xi> then h x else 0})"
```
```  1239              "x \<in> cbox a b" for h x
```
```  1240           using that by auto
```
```  1241       qed auto
```
```  1242       then have "insert f (\<Union>i\<in>Basis.
```
```  1243                 \<Union>\<xi>. \<Union>h\<in>insert f (\<Union>i\<in>Basis. \<Union>\<psi>. \<Union>h\<in>insert f (\<Union>c d. {?g B c d}). {\<lambda>x. if x \<bullet> i \<le> \<psi> then h x else 0}).
```
```  1244                 {\<lambda>x. if \<xi> \<le> x \<bullet> i then h x else 0})
```
```  1245              equiintegrable_on cbox a b"
```
```  1246         by (blast intro: f equiintegrable_on_insert)
```
```  1247       then show ?case
```
```  1248         apply (rule equiintegrable_on_subset, clarify)
```
```  1249         using \<open>i \<in> Basis\<close> apply simp
```
```  1250         apply (drule_tac x=i in bspec, assumption)
```
```  1251         apply (drule_tac x="c \<bullet> i" in spec, clarify)
```
```  1252         apply (drule_tac x=i in bspec, assumption)
```
```  1253         apply (drule_tac x="d \<bullet> i" in spec)
```
```  1254         apply (clarsimp simp add: fun_eq_iff)
```
```  1255         apply (drule_tac x=c in spec)
```
```  1256         apply (drule_tac x=d in spec)
```
```  1257         apply (simp add: split: if_split_asm)
```
```  1258         done
```
```  1259     qed
```
```  1260   qed
```
```  1261   show ?thesis
```
```  1262     by (rule equiintegrable_on_subset [OF * [OF subset_refl]]) (auto simp: mem_box)
```
```  1263 qed
```
```  1264
```
```  1265
```
```  1266
```
```  1267 subsection\<open>Continuity of the indefinite integral\<close>
```
```  1268
```
```  1269 proposition indefinite_integral_continuous:
```
```  1270   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
```
```  1271   assumes int_f: "f integrable_on cbox a b"
```
```  1272       and c: "c \<in> cbox a b" and d: "d \<in> cbox a b" "0 < \<epsilon>"
```
```  1273   obtains \<delta> where "0 < \<delta>"
```
```  1274               "\<And>c' d'. \<lbrakk>c' \<in> cbox a b; d' \<in> cbox a b; norm(c' - c) \<le> \<delta>; norm(d' - d) \<le> \<delta>\<rbrakk>
```
```  1275                         \<Longrightarrow> norm(integral(cbox c' d') f - integral(cbox c d) f) < \<epsilon>"
```
```  1276 proof -
```
```  1277   { assume "\<exists>c' d'. c' \<in> cbox a b \<and> d' \<in> cbox a b \<and> norm(c' - c) \<le> \<delta> \<and> norm(d' - d) \<le> \<delta> \<and>
```
```  1278                     norm(integral(cbox c' d') f - integral(cbox c d) f) \<ge> \<epsilon>"
```
```  1279                     (is "\<exists>c' d'. ?\<Phi> c' d' \<delta>") if "0 < \<delta>" for \<delta>
```
```  1280     then have "\<exists>c' d'. ?\<Phi> c' d' (1 / Suc n)" for n
```
```  1281       by simp
```
```  1282     then obtain u v where "\<And>n. ?\<Phi> (u n) (v n) (1 / Suc n)"
```
```  1283       by metis
```
```  1284     then have u: "u n \<in> cbox a b" and norm_u: "norm(u n - c) \<le> 1 / Suc n"
```
```  1285          and  v: "v n \<in> cbox a b" and norm_v: "norm(v n - d) \<le> 1 / Suc n"
```
```  1286          and \<epsilon>: "\<epsilon> \<le> norm (integral (cbox (u n) (v n)) f - integral (cbox c d) f)" for n
```
```  1287       by blast+
```
```  1288     then have False
```
```  1289     proof -
```
```  1290       have uvn: "cbox (u n) (v n) \<subseteq> cbox a b" for n
```
```  1291         by (meson u v mem_box(2) subset_box(1))
```
```  1292       define S where "S \<equiv> \<Union>i \<in> Basis. {x. x \<bullet> i = c \<bullet> i} \<union> {x. x \<bullet> i = d \<bullet> i}"
```
```  1293       have "negligible S"
```
```  1294         unfolding S_def by force
```
```  1295       then have int_f': "(\<lambda>x. if x \<in> S then 0 else f x) integrable_on cbox a b"
```
```  1296         by (force intro: integrable_spike assms)
```
```  1297       have get_n: "\<exists>n. \<forall>m\<ge>n. x \<in> cbox (u m) (v m) \<longleftrightarrow> x \<in> cbox c d" if x: "x \<notin> S" for x
```
```  1298       proof -
```
```  1299         define \<epsilon> where "\<epsilon> \<equiv> Min ((\<lambda>i. min \<bar>x \<bullet> i - c \<bullet> i\<bar> \<bar>x \<bullet> i - d \<bullet> i\<bar>) ` Basis)"
```
```  1300         have "\<epsilon> > 0"
```
```  1301           using \<open>x \<notin> S\<close> by (auto simp: S_def \<epsilon>_def)
```
```  1302         then obtain n where "n \<noteq> 0" and n: "1 / (real n) < \<epsilon>"
```
```  1303           by (metis inverse_eq_divide real_arch_inverse)
```
```  1304         have emin: "\<epsilon> \<le> min \<bar>x \<bullet> i - c \<bullet> i\<bar> \<bar>x \<bullet> i - d \<bullet> i\<bar>" if "i \<in> Basis" for i
```
```  1305           unfolding \<epsilon>_def
```
```  1306           apply (rule Min.coboundedI)
```
```  1307           using that by force+
```
```  1308         have "1 / real (Suc n) < \<epsilon>"
```
```  1309           using n \<open>n \<noteq> 0\<close> \<open>\<epsilon> > 0\<close> by (simp add: field_simps)
```
```  1310         have "x \<in> cbox (u m) (v m) \<longleftrightarrow> x \<in> cbox c d" if "m \<ge> n" for m
```
```  1311         proof -
```
```  1312           have *: "\<lbrakk>\<bar>u - c\<bar> \<le> n; \<bar>v - d\<bar> \<le> n; N < \<bar>x - c\<bar>; N < \<bar>x - d\<bar>; n \<le> N\<rbrakk>
```
```  1313                    \<Longrightarrow> u \<le> x \<and> x \<le> v \<longleftrightarrow> c \<le> x \<and> x \<le> d" for N n u v c d and x::real
```
```  1314             by linarith
```
```  1315           have "(u m \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> v m \<bullet> i) = (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i)"
```
```  1316             if "i \<in> Basis" for i
```
```  1317           proof (rule *)
```
```  1318             show "\<bar>u m \<bullet> i - c \<bullet> i\<bar> \<le> 1 / Suc m"
```
```  1319               using norm_u [of m]
```
```  1320               by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that)
```
```  1321             show "\<bar>v m \<bullet> i - d \<bullet> i\<bar> \<le> 1 / real (Suc m)"
```
```  1322               using norm_v [of m]
```
```  1323               by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that)
```
```  1324             show "1/n < \<bar>x \<bullet> i - c \<bullet> i\<bar>" "1/n < \<bar>x \<bullet> i - d \<bullet> i\<bar>"
```
```  1325               using n \<open>n \<noteq> 0\<close> emin [OF \<open>i \<in> Basis\<close>]
```
```  1326               by (simp_all add: inverse_eq_divide)
```
```  1327             show "1 / real (Suc m) \<le> 1 / real n"
```
```  1328               using \<open>n \<noteq> 0\<close> \<open>m \<ge> n\<close> by (simp add: divide_simps)
```
```  1329           qed
```
```  1330           then show ?thesis by (simp add: mem_box)
```
```  1331         qed
```
```  1332         then show ?thesis by blast
```
```  1333       qed
```
```  1334       have 1: "range (\<lambda>n x. if x \<in> cbox (u n) (v n) then if x \<in> S then 0 else f x else 0) equiintegrable_on cbox a b"
```
```  1335         by (blast intro: equiintegrable_on_subset [OF equiintegrable_closed_interval_restrictions [OF int_f']])
```
```  1336       have 2: "(\<lambda>n. if x \<in> cbox (u n) (v n) then if x \<in> S then 0 else f x else 0)
```
```  1337                \<longlonglongrightarrow> (if x \<in> cbox c d then if x \<in> S then 0 else f x else 0)" for x
```
```  1338         by (fastforce simp: dest: get_n intro: Lim_eventually eventually_sequentiallyI)
```
```  1339       have [simp]: "cbox c d \<inter> cbox a b = cbox c d"
```
```  1340         using c d by (force simp: mem_box)
```
```  1341       have [simp]: "cbox (u n) (v n) \<inter> cbox a b = cbox (u n) (v n)" for n
```
```  1342         using u v by (fastforce simp: mem_box intro: order.trans)
```
```  1343       have "\<And>y A. y \<in> A - S \<Longrightarrow> f y = (\<lambda>x. if x \<in> S then 0 else f x) y"
```
```  1344         by simp
```
```  1345       then have "\<And>A. integral A (\<lambda>x. if x \<in> S then 0 else f (x)) = integral A (\<lambda>x. f (x))"
```
```  1346         by (blast intro: integral_spike [OF \<open>negligible S\<close>])
```
```  1347       moreover
```
```  1348       obtain N where "dist (integral (cbox (u N) (v N)) (\<lambda>x. if x \<in> S then 0 else f x))
```
```  1349                            (integral (cbox c d) (\<lambda>x. if x \<in> S then 0 else f x)) < \<epsilon>"
```
```  1350         using equiintegrable_limit [OF 1 2] \<open>0 < \<epsilon>\<close> by (force simp: integral_restrict_Int lim_sequentially)
```
```  1351       ultimately have "dist (integral (cbox (u N) (v N)) f) (integral (cbox c d) f) < \<epsilon>"
```
```  1352         by simp
```
```  1353       then show False
```
```  1354         by (metis dist_norm not_le \<epsilon>)
```
```  1355     qed
```
```  1356   }
```
```  1357   then show ?thesis
```
```  1358     by (meson not_le that)
```
```  1359 qed
```
```  1360
```
```  1361 corollary indefinite_integral_uniformly_continuous:
```
```  1362   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
```
```  1363   assumes "f integrable_on cbox a b"
```
```  1364   shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (\<lambda>y. integral (cbox (fst y) (snd y)) f)"
```
```  1365 proof -
```
```  1366   show ?thesis
```
```  1367   proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff)
```
```  1368     fix c d and \<epsilon>::real
```
```  1369     assume c: "c \<in> cbox a b" and d: "d \<in> cbox a b" and "0 < \<epsilon>"
```
```  1370     obtain \<delta> where "0 < \<delta>" and \<delta>:
```
```  1371               "\<And>c' d'. \<lbrakk>c' \<in> cbox a b; d' \<in> cbox a b; norm(c' - c) \<le> \<delta>; norm(d' - d) \<le> \<delta>\<rbrakk>
```
```  1372                                   \<Longrightarrow> norm(integral(cbox c' d') f -
```
```  1373                                            integral(cbox c d) f) < \<epsilon>"
```
```  1374       using indefinite_integral_continuous \<open>0 < \<epsilon>\<close> assms c d by blast
```
```  1375     show "\<exists>\<delta> > 0. \<forall>x' \<in> cbox (a, a) (b, b).
```
```  1376                    dist x' (c, d) < \<delta> \<longrightarrow>
```
```  1377                    dist (integral (cbox (fst x') (snd x')) f)
```
```  1378                         (integral (cbox c d) f)
```
```  1379                    < \<epsilon>"
```
```  1380       using \<open>0 < \<delta>\<close>
```
```  1381       by (force simp: dist_norm intro: \<delta> order_trans [OF norm_fst_le] order_trans [OF norm_snd_le] less_imp_le)
```
```  1382   qed auto
```
```  1383 qed
```
```  1384
```
```  1385
```
```  1386 corollary bounded_integrals_over_subintervals:
```
```  1387   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
```
```  1388   assumes "f integrable_on cbox a b"
```
```  1389   shows "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> cbox a b}"
```
```  1390 proof -
```
```  1391   have "bounded ((\<lambda>y. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))"
```
```  1392        (is "bounded ?I")
```
```  1393     by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms])
```
```  1394   then obtain B where "B > 0" and B: "\<And>x. x \<in> ?I \<Longrightarrow> norm x \<le> B"
```
```  1395     by (auto simp: bounded_pos)
```
```  1396   have "norm x \<le> B" if "x = integral (cbox c d) f" "cbox c d \<subseteq> cbox a b" for x c d
```
```  1397   proof (cases "cbox c d = {}")
```
```  1398     case True
```
```  1399     with \<open>0 < B\<close> that show ?thesis by auto
```
```  1400   next
```
```  1401     case False
```
```  1402     show ?thesis
```
```  1403       apply (rule B)
```
```  1404       using that \<open>B > 0\<close> False apply (clarsimp simp: image_def)
```
```  1405       by (metis cbox_Pair_iff interval_subset_is_interval is_interval_cbox prod.sel)
```
```  1406   qed
```
```  1407   then show ?thesis
```
```  1408     by (blast intro: boundedI)
```
```  1409 qed
```
```  1410
```
```  1411
```
```  1412 text\<open>An existence theorem for "improper" integrals.
```
```  1413 Hake's theorem implies that if the integrals over subintervals have a limit, the integral exists.
```
```  1414 We only need to assume that the integrals are bounded, and we get absolute integrability,
```
```  1415 but we also need a (rather weak) bound assumption on the function.\<close>
```
```  1416
```
```  1417 theorem absolutely_integrable_improper:
```
```  1418   fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
```
```  1419   assumes int_f: "\<And>c d. cbox c d \<subseteq> box a b \<Longrightarrow> f integrable_on cbox c d"
```
```  1420       and bo: "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> box a b}"
```
```  1421       and absi: "\<And>i. i \<in> Basis
```
```  1422           \<Longrightarrow> \<exists>g. g absolutely_integrable_on cbox a b \<and>
```
```  1423                   ((\<forall>x \<in> cbox a b. f x \<bullet> i \<le> g x) \<or> (\<forall>x \<in> cbox a b. f x \<bullet> i \<ge> g x))"
```
```  1424       shows "f absolutely_integrable_on cbox a b"
```
```  1425 proof (cases "content(cbox a b) = 0")
```
```  1426   case True
```
```  1427   then show ?thesis
```
```  1428     by auto
```
```  1429 next
```
```  1430   case False
```
```  1431   then have pos: "content(cbox a b) > 0"
```
```  1432     using zero_less_measure_iff by blast
```
```  1433   show ?thesis
```
```  1434     unfolding absolutely_integrable_componentwise_iff [where f = f]
```
```  1435   proof
```
```  1436     fix j::'N
```
```  1437     assume "j \<in> Basis"
```
```  1438     then obtain g where absint_g: "g absolutely_integrable_on cbox a b"
```
```  1439                     and g: "(\<forall>x \<in> cbox a b. f x \<bullet> j \<le> g x) \<or> (\<forall>x \<in> cbox a b. f x \<bullet> j \<ge> g x)"
```
```  1440       using absi by blast
```
```  1441     have int_gab: "g integrable_on cbox a b"
```
```  1442       using absint_g set_lebesgue_integral_eq_integral(1) by blast
```
```  1443     have 1: "cbox (a + (b - a) /\<^sub>R real (Suc n)) (b - (b - a) /\<^sub>R real (Suc n)) \<subseteq> box a b" for n
```
```  1444       apply (rule subset_box_imp)
```
```  1445       using pos apply (auto simp: content_pos_lt_eq algebra_simps)
```
```  1446       done
```
```  1447     have 2: "cbox (a + (b - a) /\<^sub>R real (Suc n)) (b - (b - a) /\<^sub>R real (Suc n)) \<subseteq>
```
```  1448              cbox (a + (b - a) /\<^sub>R real (Suc n + 1)) (b - (b - a) /\<^sub>R real (Suc n + 1))" for n
```
```  1449       apply (rule subset_box_imp)
```
```  1450       using pos apply (simp add: content_pos_lt_eq algebra_simps)
```
```  1451         apply (simp add: divide_simps)
```
```  1452       apply (auto simp: field_simps)
```
```  1453       done
```
```  1454     have getN: "\<exists>N::nat. \<forall>k. k \<ge> N \<longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
```
```  1455       if x: "x \<in> box a b" for x
```
```  1456     proof -
```
```  1457       let ?\<Delta> = "(\<Union>i \<in> Basis. {((x - a) \<bullet> i) / ((b - a) \<bullet> i), (b - x) \<bullet> i / ((b - a) \<bullet> i)})"
```
```  1458       obtain N where N: "real N > 1 / Inf ?\<Delta>"
```
```  1459         using reals_Archimedean2 by blast
```
```  1460       moreover have \<Delta>: "Inf ?\<Delta> > 0"
```
```  1461         using that by (auto simp: finite_less_Inf_iff mem_box algebra_simps divide_simps)
```
```  1462       ultimately have "N > 0"
```
```  1463         using of_nat_0_less_iff by fastforce
```
```  1464       show ?thesis
```
```  1465       proof (intro exI impI allI)
```
```  1466         fix k assume "N \<le> k"
```
```  1467         with \<open>0 < N\<close> have "k > 0"
```
```  1468           by linarith
```
```  1469         have xa_gt: "(x - a) \<bullet> i > ((b - a) \<bullet> i) / (real k)" if "i \<in> Basis" for i
```
```  1470         proof -
```
```  1471           have *: "Inf ?\<Delta> \<le> ((x - a) \<bullet> i) / ((b - a) \<bullet> i)"
```
```  1472             using that by (force intro: cInf_le_finite)
```
```  1473           have "1 / Inf ?\<Delta> \<ge> ((b - a) \<bullet> i) / ((x - a) \<bullet> i)"
```
```  1474             using le_imp_inverse_le [OF * \<Delta>]
```
```  1475             by (simp add: field_simps)
```
```  1476           with N have "k > ((b - a) \<bullet> i) / ((x - a) \<bullet> i)"
```
```  1477             using \<open>N \<le> k\<close> by linarith
```
```  1478           with x that show ?thesis
```
```  1479             by (auto simp: mem_box algebra_simps divide_simps)
```
```  1480         qed
```
```  1481         have bx_gt: "(b - x) \<bullet> i > ((b - a) \<bullet> i) / k" if "i \<in> Basis" for i
```
```  1482         proof -
```
```  1483           have *: "Inf ?\<Delta> \<le> ((b - x) \<bullet> i) / ((b - a) \<bullet> i)"
```
```  1484             using that by (force intro: cInf_le_finite)
```
```  1485           have "1 / Inf ?\<Delta> \<ge> ((b - a) \<bullet> i) / ((b - x) \<bullet> i)"
```
```  1486             using le_imp_inverse_le [OF * \<Delta>]
```
```  1487             by (simp add: field_simps)
```
```  1488           with N have "k > ((b - a) \<bullet> i) / ((b - x) \<bullet> i)"
```
```  1489             using \<open>N \<le> k\<close> by linarith
```
```  1490           with x that show ?thesis
```
```  1491             by (auto simp: mem_box algebra_simps divide_simps)
```
```  1492         qed
```
```  1493         show "x \<in> cbox (a + (b - a) /\<^sub>R k) (b - (b - a) /\<^sub>R k)"
```
```  1494           using that \<Delta> \<open>k > 0\<close>
```
```  1495           by (auto simp: mem_box algebra_simps divide_inverse dest: xa_gt bx_gt)
```
```  1496       qed
```
```  1497     qed
```
```  1498     obtain Bf where "Bf > 0" and Bf: "\<And>c d. cbox c d \<subseteq> box a b \<Longrightarrow> norm (integral (cbox c d) f) \<le> Bf"
```
```  1499       using bo unfolding bounded_pos by blast
```
```  1500     obtain Bg where "Bg > 0" and Bg:"\<And>c d. cbox c d \<subseteq> cbox a b \<Longrightarrow> \<bar>integral (cbox c d) g\<bar> \<le> Bg"
```
```  1501       using bounded_integrals_over_subintervals [OF int_gab] unfolding bounded_pos real_norm_def by blast
```
```  1502     show "(\<lambda>x. f x \<bullet> j) absolutely_integrable_on cbox a b"
```
```  1503       using g
```
```  1504     proof     \<comment> \<open>A lot of duplication in the two proofs\<close>
```
```  1505       assume fg [rule_format]: "\<forall>x\<in>cbox a b. f x \<bullet> j \<le> g x"
```
```  1506       have "(\<lambda>x. (f x \<bullet> j)) = (\<lambda>x. g x - (g x - (f x \<bullet> j)))"
```
```  1507         by simp
```
```  1508       moreover have "(\<lambda>x. g x - (g x - (f x \<bullet> j))) integrable_on cbox a b"
```
```  1509       proof (rule Henstock_Kurzweil_Integration.integrable_diff [OF int_gab])
```
```  1510         let ?\<phi> = "\<lambda>k x. if x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))
```
```  1511                         then g x - f x \<bullet> j else 0"
```
```  1512         have "(\<lambda>x. g x - f x \<bullet> j) integrable_on box a b"
```
```  1513         proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1])
```
```  1514           have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \<inter> box a b
```
```  1515                  = cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k
```
```  1516             using box_subset_cbox "1" by fastforce
```
```  1517           show "?\<phi> k integrable_on box a b" for k
```
```  1518             apply (simp add: integrable_restrict_Int integral_restrict_Int *)
```
```  1519             apply (rule integrable_diff [OF integrable_on_subcbox [OF int_gab]])
```
```  1520             using "*" box_subset_cbox apply blast
```
```  1521             by (metis "1" int_f integrable_component of_nat_Suc)
```
```  1522           have cb12: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))
```
```  1523                     \<subseteq> cbox (a + (b - a) /\<^sub>R (2 + real k)) (b - (b - a) /\<^sub>R (2 + real k))" for k
```
```  1524             using False content_eq_0
```
```  1525             apply (simp add: subset_box algebra_simps)
```
```  1526             apply (simp add: divide_simps)
```
```  1527             apply (fastforce simp: field_simps)
```
```  1528             done
```
```  1529           show "?\<phi> k x \<le> ?\<phi> (Suc k) x" if "x \<in> box a b" for k x
```
```  1530             using cb12 box_subset_cbox that by (force simp: intro!: fg)
```
```  1531           show "(\<lambda>k. ?\<phi> k x) \<longlonglongrightarrow> g x - f x \<bullet> j" if x: "x \<in> box a b" for x
```
```  1532           proof (rule Lim_eventually)
```
```  1533             obtain N::nat where N: "\<And>k. k \<ge> N \<Longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
```
```  1534               using getN [OF x] by blast
```
```  1535             show "\<forall>\<^sub>F k in sequentially. ?\<phi> k x = g x - f x \<bullet> j"
```
```  1536             proof
```
```  1537               fix k::nat assume "N \<le> k"
```
```  1538               have "x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))"
```
```  1539                 by (metis \<open>N \<le> k\<close> le_Suc_eq N)
```
```  1540               then show "?\<phi> k x = g x - f x \<bullet> j"
```
```  1541                 by simp
```
```  1542             qed
```
```  1543           qed
```
```  1544           have "\<bar>integral (box a b)
```
```  1545                       (\<lambda>x. if x \<in> cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))
```
```  1546                            then g x - f x \<bullet> j else 0)\<bar> \<le> Bg + Bf" for k
```
```  1547           proof -
```
```  1548             let ?I = "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))"
```
```  1549             have I_int [simp]: "?I \<inter> box a b = ?I"
```
```  1550               using 1 by (simp add: Int_absorb2)
```
```  1551             have int_fI: "f integrable_on ?I"
```
```  1552               apply (rule integrable_subinterval [OF int_f order_refl])
```
```  1553               using "*" box_subset_cbox by blast
```
```  1554             then have "(\<lambda>x. f x \<bullet> j) integrable_on ?I"
```
```  1555               by (simp add: integrable_component)
```
```  1556             moreover have "g integrable_on ?I"
```
```  1557               apply (rule integrable_subinterval [OF int_gab])
```
```  1558               using "*" box_subset_cbox by blast
```
```  1559             moreover
```
```  1560             have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> norm (integral ?I f)"
```
```  1561               by (simp add: Basis_le_norm int_fI \<open>j \<in> Basis\<close>)
```
```  1562             with 1 I_int have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> Bf"
```
```  1563               by (blast intro: order_trans [OF _ Bf])
```
```  1564             ultimately show ?thesis
```
```  1565               apply (simp add: integral_restrict_Int integral_diff)
```
```  1566               using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
```
```  1567           qed
```
```  1568           then show "bounded (range (\<lambda>k. integral (box a b) (?\<phi> k)))"
```
```  1569             apply (simp add: bounded_pos)
```
```  1570             apply (rule_tac x="Bg+Bf" in exI)
```
```  1571             using \<open>0 < Bf\<close> \<open>0 < Bg\<close>  apply auto
```
```  1572             done
```
```  1573         qed
```
```  1574         then show "(\<lambda>x. g x - f x \<bullet> j) integrable_on cbox a b"
```
```  1575           by (simp add: integrable_on_open_interval)
```
```  1576       qed
```
```  1577       ultimately have "(\<lambda>x. f x \<bullet> j) integrable_on cbox a b"
```
```  1578         by auto
```
```  1579       then show ?thesis
```
```  1580         apply (rule absolutely_integrable_component_ubound [OF _ absint_g])
```
```  1581         by (simp add: fg)
```
```  1582     next
```
```  1583       assume gf [rule_format]: "\<forall>x\<in>cbox a b. g x \<le> f x \<bullet> j"
```
```  1584       have "(\<lambda>x. (f x \<bullet> j)) = (\<lambda>x. ((f x \<bullet> j) - g x) + g x)"
```
```  1585         by simp
```
```  1586       moreover have "(\<lambda>x. (f x \<bullet> j - g x) + g x) integrable_on cbox a b"
```
```  1587       proof (rule Henstock_Kurzweil_Integration.integrable_add [OF _ int_gab])
```
```  1588         let ?\<phi> = "\<lambda>k x. if x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))
```
```  1589                         then f x \<bullet> j - g x else 0"
```
```  1590         have "(\<lambda>x. f x \<bullet> j - g x) integrable_on box a b"
```
```  1591         proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1])
```
```  1592           have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \<inter> box a b
```
```  1593                  = cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k
```
```  1594             using box_subset_cbox "1" by fastforce
```
```  1595           show "?\<phi> k integrable_on box a b" for k
```
```  1596             apply (simp add: integrable_restrict_Int integral_restrict_Int *)
```
```  1597             apply (rule integrable_diff)
```
```  1598               apply (metis "1" int_f integrable_component of_nat_Suc)
```
```  1599              apply (rule integrable_on_subcbox [OF int_gab])
```
```  1600             using "*" box_subset_cbox apply blast
```
```  1601               done
```
```  1602           have cb12: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))
```
```  1603                     \<subseteq> cbox (a + (b - a) /\<^sub>R (2 + real k)) (b - (b - a) /\<^sub>R (2 + real k))" for k
```
```  1604             using False content_eq_0
```
```  1605             apply (simp add: subset_box algebra_simps)
```
```  1606             apply (simp add: divide_simps)
```
```  1607             apply (fastforce simp: field_simps)
```
```  1608             done
```
```  1609           show "?\<phi> k x \<le> ?\<phi> (Suc k) x" if "x \<in> box a b" for k x
```
```  1610             using cb12 box_subset_cbox that by (force simp: intro!: gf)
```
```  1611           show "(\<lambda>k. ?\<phi> k x) \<longlonglongrightarrow> f x \<bullet> j - g x" if x: "x \<in> box a b" for x
```
```  1612           proof (rule Lim_eventually)
```
```  1613             obtain N::nat where N: "\<And>k. k \<ge> N \<Longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
```
```  1614               using getN [OF x] by blast
```
```  1615             show "\<forall>\<^sub>F k in sequentially. ?\<phi> k x = f x \<bullet> j - g x"
```
```  1616             proof
```
```  1617               fix k::nat assume "N \<le> k"
```
```  1618               have "x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))"
```
```  1619                 by (metis \<open>N \<le> k\<close> le_Suc_eq N)
```
```  1620               then show "?\<phi> k x = f x \<bullet> j - g x"
```
```  1621                 by simp
```
```  1622             qed
```
```  1623           qed
```
```  1624           have "\<bar>integral (box a b)
```
```  1625                       (\<lambda>x. if x \<in> cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))
```
```  1626                            then f x \<bullet> j - g x else 0)\<bar> \<le> Bf + Bg" for k
```
```  1627           proof -
```
```  1628             let ?I = "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))"
```
```  1629             have I_int [simp]: "?I \<inter> box a b = ?I"
```
```  1630               using 1 by (simp add: Int_absorb2)
```
```  1631             have int_fI: "f integrable_on ?I"
```
```  1632               apply (rule integrable_subinterval [OF int_f order_refl])
```
```  1633               using "*" box_subset_cbox by blast
```
```  1634             then have "(\<lambda>x. f x \<bullet> j) integrable_on ?I"
```
```  1635               by (simp add: integrable_component)
```
```  1636             moreover have "g integrable_on ?I"
```
```  1637               apply (rule integrable_subinterval [OF int_gab])
```
```  1638               using "*" box_subset_cbox by blast
```
```  1639             moreover
```
```  1640             have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> norm (integral ?I f)"
```
```  1641               by (simp add: Basis_le_norm int_fI \<open>j \<in> Basis\<close>)
```
```  1642             with 1 I_int have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> Bf"
```
```  1643               by (blast intro: order_trans [OF _ Bf])
```
```  1644             ultimately show ?thesis
```
```  1645               apply (simp add: integral_restrict_Int integral_diff)
```
```  1646               using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
```
```  1647           qed
```
```  1648           then show "bounded (range (\<lambda>k. integral (box a b) (?\<phi> k)))"
```
```  1649             apply (simp add: bounded_pos)
```
```  1650             apply (rule_tac x="Bf+Bg" in exI)
```
```  1651             using \<open>0 < Bf\<close> \<open>0 < Bg\<close>  by auto
```
```  1652         qed
```
```  1653         then show "(\<lambda>x. f x \<bullet> j - g x) integrable_on cbox a b"
```
```  1654           by (simp add: integrable_on_open_interval)
```
```  1655       qed
```
```  1656       ultimately have "(\<lambda>x. f x \<bullet> j) integrable_on cbox a b"
```
```  1657         by auto
```
```  1658       then show ?thesis
```
```  1659         apply (rule absolutely_integrable_component_lbound [OF absint_g])
```
```  1660         by (simp add: gf)
```
```  1661     qed
```
```  1662   qed
```
```  1663 qed
```
```  1664
```
```  1665 end
```
```  1666
```