products/sources/formale Sprachen/Isabelle/Pure/System/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Relation_Operators.v   Sprache: Unknown

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

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

theory "Improper_Integral"
  imports Equivalence_Lebesgue_Henstock_Integration
begin

subsection \<open>Equiintegrability\<close>

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

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

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

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

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

lemma equiintegrable_on_Un:
  assumes "F equiintegrable_on I" "G equiintegrable_on I"
  shows "(F \ G) equiintegrable_on I"
  unfolding equiintegrable_on_def
proof (intro conjI impI allI)
  show "\f\F \ G. f integrable_on I"
    using assms unfolding equiintegrable_on_def by blast
  show "\\. gauge \ \
            (\<forall>f \<D>. f \<in> F \<union> G \<and>
                   \<D> tagged_division_of I \<and> \<gamma> fine \<D> \<longrightarrow>
                   norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
         if "\ > 0" for \
  proof -
    obtain \<gamma>1 where "gauge \<gamma>1"
      and \<gamma>1: "\<And>f \<D>. f \<in> F \<and> \<D> tagged_division_of I \<and> \<gamma>1 fine \<D>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by auto
    obtain \<gamma>2 where  "gauge \<gamma>2"
      and \<gamma>2: "\<And>f \<D>. f \<in> G \<and> \<D> tagged_division_of I \<and> \<gamma>2 fine \<D>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by auto
    have "gauge (\x. \1 x \ \2 x)"
      using \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close> by blast
    moreover have "\f \. f \ F \ G \ \ tagged_division_of I \ (\x. \1 x \ \2 x) fine \ \
          norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>"
      using \<gamma>1 \<gamma>2 by (auto simp: fine_Int)
    ultimately show ?thesis
      by (intro exI conjI) assumption+
  qed
qed


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


lemma equiintegrable_cmul:
  assumes F: "F equiintegrable_on I"
  shows "(\c \ {-k..k}. \f \ F. {(\x. c *\<^sub>R f x)}) equiintegrable_on I"
  unfolding equiintegrable_on_def
  proof (intro conjI impI allI ballI)
  show "f integrable_on I"
    if "f \ (\c\{- k..k}. \f\F. {\x. c *\<^sub>R f x})"
    for f :: "'a \ 'b"
    using that assms equiintegrable_on_integrable integrable_cmul by blast
  show "\\. gauge \ \ (\f \. f \ (\c\{- k..k}. \f\F. {\x. c *\<^sub>R f x}) \ \ tagged_division_of I
          \<and> \<gamma> fine \<D> \<longrightarrow> norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
    if "\ > 0" for \
  proof -
    obtain \<gamma> where "gauge \<gamma>"
      and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of I; \<gamma> fine \<D>\<rbrakk>
                    \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon> / (\<bar>k\<bar> + 1)"
      using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def
      by (metis add.commute add.right_neutral add_strict_mono divide_pos_pos norm_eq_zero real_norm_def zero_less_norm_iff zero_less_one)
    moreover have "norm ((\(x, K)\\. content K *\<^sub>R c *\<^sub>R (f x)) - integral I (\x. c *\<^sub>R f x)) < \"
      if c: "c \ {- k..k}"
        and "f \ F" "\ tagged_division_of I" "\ fine \"
      for \<D> c f
    proof -
      have "norm ((\x\\. case x of (x, K) \ content K *\<^sub>R c *\<^sub>R f x) - integral I (\x. c *\<^sub>R f x))
          = \<bar>c\<bar> * norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R f x) - integral I f)"
        by (simp add: algebra_simps scale_sum_right case_prod_unfold flip: norm_scaleR)
      also have "\ \ (\k\ + 1) * norm ((\x\\. case x of (x, K) \ content K *\<^sub>R f x) - integral I f)"
        using c by (auto simp: mult_right_mono)
      also have "\ < (\k\ + 1) * (\ / (\k\ + 1))"
        by (rule mult_strict_left_mono) (use \<gamma> less_eq_real_def that in auto)
      also have "\ = \"
        by auto
      finally show ?thesis .
    qed
    ultimately show ?thesis
      by (rule_tac x="\" in exI) auto
  qed
qed


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

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

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


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

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


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

lemma equiintegrable_on_null [simp]:
   "content(cbox a b) = 0 \ F equiintegrable_on cbox a b"
  unfolding equiintegrable_on_def 
  by (metis diff_zero gauge_trivial integrable_on_null integral_null norm_zero sum_content_null)


text\<open> Main limit theorem for an equiintegrable sequence.\<close>

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


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

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

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

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


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


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

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

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

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

  show ?thesis
  proof (cases "c = a \ i \ c = b \ i")
    case True
    then show ?thesis
    proof
      assume c: "c = a \ i"
      moreover
      have "(\j\Basis. (if j = i then a \ i else a \ j) *\<^sub>R j) = a"
        using euclidean_representation [of a] sum.cong [OF refl, of Basis "\i. (a \ i) *\<^sub>R i"] by presburger
      ultimately have "a' = a"
        by (simp add: i a'_def cong: if_cong)
      then have "content (cbox a' b) \ 2 * content (cbox a b)" by simp
      moreover
      have eq: "(\K\\. content (K \ {x. a \ i \ x \ i}) / interv_diff (K \ {x. a \ i \ x \ i}) i)
              = (\<Sum>K\<in>\<D>. content K / interv_diff K i)"
        (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K \ \"
        then have "a \ i \ x \ i" if "x \ K" for x
          by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
        then have "K \ {x. a \ i \ x \ i} = K"
          by blast
        then show "?f K = ?g K"
          by simp
      qed
      ultimately show ?thesis
        using gec c eq interv_diff_def by auto
    next
      assume c: "c = b \ i"
      moreover have "(\j\Basis. (if j = i then b \ i else b \ j) *\<^sub>R j) = b"
        using euclidean_representation [of b] sum.cong [OF refl, of Basis "\i. (b \ i) *\<^sub>R i"] by presburger
      ultimately have "b' = b"
        by (simp add: i b'_def cong: if_cong)
      then have "content (cbox a b') \ 2 * content (cbox a b)" by simp
      moreover
      have eq: "(\K\\. content (K \ {x. x \ i \ b \ i}) / interv_diff (K \ {x. x \ i \ b \ i}) i)
              = (\<Sum>K\<in>\<D>. content K / interv_diff K i)"
               (is "sum ?f _ = sum ?g _")
      proof (rule sum.cong [OF refl])
        fix K assume "K \ \"
        then have "x \ i \ b \ i" if "x \ K" for x
          by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that)
        then have "K \ {x. x \ i \ b \ i} = K"
          by blast
        then show "?f K = ?g K"
          by simp
      qed
      ultimately show ?thesis
        using lec c eq interv_diff_def by auto
    qed
  next
    case False
    have prod_if: "(\k\Basis \ - {i}. f k) = (\k\Basis. f k) / f i" if "f i \ (0::real)" for f
    proof -
      have "f i * prod f (Basis \ - {i}) = prod f Basis"
        using that mk_disjoint_insert [OF i]
        by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf order_refl prod.insert subset_Compl_singleton)
      then show ?thesis
        by (metis nonzero_mult_div_cancel_left that)
    qed
    have abc: "a \ i < c" "c < b \ i"
      using False assms by auto
    then have "(\K\\. ((\K. content K / (interv_diff K i)) \ ((\K. K \ {x. x \ i \ c}))) K)
                  \<le> content(cbox a b') / (c - a \<bullet> i)"
              "(\K\\. ((\K. content K / (interv_diff K i)) \ ((\K. K \ {x. x \ i \ c}))) K)
                 \<le> content(cbox a' b) / (b \<bullet> i - c)"
      using lec gec by (simp_all add: field_split_simps)
    moreover
    have "(\K\\. content K / (interv_diff K i))
          \<le> (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K) +
            (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
           (is "?lhs \ ?rhs")
    proof -
      have "?lhs \
            (\<Sum>K\<in>\<D>. ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<le> c}))) K +
                    ((\<lambda>K. content K / (interv_diff K i)) \<circ> ((\<lambda>K. K \<inter> {x. x \<bullet> i \<ge> c}))) K)"
            (is "sum ?f _ \ sum ?g _")
      proof (rule sum_mono)
        fix K assume "K \ \"
        then obtain u v where uv: "K = cbox u v"
          using div by blast
        obtain u' v' where uv': "cbox u v \ {x. x \ i \ c} = cbox u v'"
                                "cbox u v \ {x. c \ x \ i} = cbox u' v"
                                "\k. k \ Basis \ u' \ k = (if k = i then max (u \ i) c else u \ k)"
                                "\k. k \ Basis \ v' \ k = (if k = i then min (v \ i) c else v \ k)"
          using i by (auto simp: interval_split)
        have *: "\content (cbox u v') = 0; content (cbox u' v) = 0\ \ content (cbox u v) = 0"
                "content (cbox u' v) \ 0 \ content (cbox u v) \ 0"
                "content (cbox u v') \ 0 \ content (cbox u v) \ 0"
          using i uv uv' by (auto simp: content_eq_0 le_max_iff_disj min_le_iff_disj split: if_split_asm intro: order_trans)
        have uniq: "\j. \j \ Basis; \ u \ j \ v \ j\ \ j = i"
          by (metis \<open>K \<in> \<D>\<close> box_ne_empty(1) div division_of_def uv)
        show "?f K \ ?g K"
          using i uv uv' by (auto simp add: interv_diff_def lemma0 dest: uniq * intro!: prod_nonneg)
      qed
      also have "... = ?rhs"
        by (simp add: sum.distrib)
      finally show ?thesis .
    qed
    moreover have "content (cbox a b') / (c - a \ i) = content (cbox a b) / (b \ i - a \ i)"
      using i abc
      apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff)
      apply (auto simp: if_distrib if_distrib [of "\f. f x" for x] prod.If_cases [of Basis "\x. x = i", simplified] prod_if field_simps)
      done
    moreover have "content (cbox a' b) / (b \ i - c) = content (cbox a b) / (b \ i - a \ i)"
      using i abc
      apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff)
      apply (auto simp: if_distrib prod.If_cases [of Basis "\x. x = i", simplified] prod_if field_simps)
      done
    ultimately
    have "(\K\\. content K / (interv_diff K i)) \ 2 * content (cbox a b) / (b \ i - a \ i)"
      by linarith
    then show ?thesis
      using abc interv_diff_def by (simp add: field_split_simps)
  qed
qed


proposition bounded_equiintegral_over_thin_tagged_partial_division:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" and "0 < \"
      and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)"
  obtains \<gamma> where "gauge \<gamma>"
             "\c i S h. \c \ cbox a b; i \ Basis; S tagged_partial_division_of cbox a b;
                         \<gamma> fine S; h \<in> F; \<And>x K. (x,K) \<in> S \<Longrightarrow> (K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {})\<rbrakk>
                        \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
proof (cases "content(cbox a b) = 0")
  case True
  show ?thesis
  proof
    show "gauge (\x. ball x 1)"
      by (simp add: gauge_trivial)
    show "(\(x,K) \ S. norm (integral K h)) < \"
         if "S tagged_partial_division_of cbox a b" "(\x. ball x 1) fine S" for S and h:: "'a \ 'b"
    proof -
      have "(\(x,K) \ S. norm (integral K h)) = 0"
          using that True content_0_subset
          by (fastforce simp: tagged_partial_division_of_def intro: sum.neutral)
      with \<open>0 < \<epsilon>\<close> show ?thesis
        by simp
    qed
  qed
next
  case False
  then have contab_gt0:  "content(cbox a b) > 0"
    by (simp add: zero_less_measure_iff)
  then have a_less_b: "\i. i \ Basis \ a\i < b\i"
    by (auto simp: content_pos_lt_eq)
  obtain \<gamma>0 where "gauge \<gamma>0"
            and \<gamma>0: "\<And>S h. \<lbrakk>S tagged_partial_division_of cbox a b; \<gamma>0 fine S; h \<in> F\<rbrakk>
                           \<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
  proof -
    obtain \<gamma> where "gauge \<gamma>"
               and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
                              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f)
                                  < \<epsilon>/(5 * (Suc DIM('b)))"
    proof -
      have e5: "\/(5 * (Suc DIM('b))) > 0"
        using \<open>\<epsilon> > 0\<close> by auto
      then show ?thesis
        using F that by (auto simp: equiintegrable_on_def)
    qed
    show ?thesis
    proof
      show "gauge \"
        by (rule \<open>gauge \<gamma>\<close>)
      show "(\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) < \/2"
           if "S tagged_partial_division_of cbox a b" "\ fine S" "h \ F" for S h
      proof -
        have "(\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) \ 2 * real DIM('b) * (\/(5 * Suc DIM('b)))"
        proof (rule Henstock_lemma_part2 [of h a b])
          show "h integrable_on cbox a b"
            using that F equiintegrable_on_def by metis
          show "gauge \"
            by (rule \<open>gauge \<gamma>\<close>)
        qed (use that \<open>\<epsilon> > 0\<close> \<gamma> in auto)
        also have "... < \/2"
          using \<open>\<epsilon> > 0\<close> by (simp add: divide_simps)
        finally show ?thesis .
      qed
    qed
  qed
  define \<gamma> where "\<gamma> \<equiv> \<lambda>x. \<gamma>0 x \<inter>
                          ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
  define interv_diff where "interv_diff \ \K. \i::'a. interval_upperbound K \ i - interval_lowerbound K \ i"
  have "8 * content (cbox a b) + norm (f x) * (8 * content (cbox a b)) > 0" for x
    by (metis add.right_neutral add_pos_pos contab_gt0 mult_pos_pos mult_zero_left norm_eq_zero zero_less_norm_iff zero_less_numeral)
  then have "gauge (\x. ball x
                    (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
    using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b 
    by (auto simp add: gauge_def field_split_simps add_nonneg_eq_0_iff finite_less_Inf_iff)
  then have "gauge \"
    unfolding \<gamma>_def using \<open>gauge \<gamma>0\<close> gauge_Int by auto
  moreover
  have "(\(x,K) \ S. norm (integral K h)) < \"
       if "c \ cbox a b" "i \ Basis" and S: "S tagged_partial_division_of cbox a b"
          and "\ fine S" "h \ F" and ne: "\x K. (x,K) \ S \ K \ {x. x \ i = c \ i} \ {}" for c i S h
  proof -
    have "cbox c b \ cbox a b"
      by (meson mem_box(2) order_refl subset_box(1) that(1))
    have "finite S"
      using S unfolding tagged_partial_division_of_def by blast
    have "\0 fine S" and fineS:
         "(\x. ball x (\ * (INF m\Basis. b \ m - a \ m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
      using \<open>\<gamma> fine S\<close> by (auto simp: \<gamma>_def fine_Int)
    then have "(\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) < \/2"
      by (intro \<gamma>0 that fineS)
    moreover have "(\(x,K) \ S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h)) \ \/2"
    proof -
      have "(\(x,K) \ S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h))
            \<le> (\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x))"
      proof (clarify intro!: sum_mono)
        fix x K
        assume xK: "(x,K) \ S"
        have "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \ norm (integral K h - (integral K h - content K *\<^sub>R h x))"
          by (metis norm_minus_commute norm_triangle_ineq2)
        also have "... \ norm (content K *\<^sub>R h x)"
          by simp
        finally show "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \ norm (content K *\<^sub>R h x)" .
      qed
      also have "... \ (\(x,K) \ S. \/4 * (b \ i - a \ i) / content (cbox a b) * content K / interv_diff K i)"
      proof (clarify intro!: sum_mono)
        fix x K
        assume xK: "(x,K) \ S"
        then have x: "x \ cbox a b"
          using S unfolding tagged_partial_division_of_def by (meson subset_iff)
        show "norm (content K *\<^sub>R h x) \ \/4 * (b \ i - a \ i) / content (cbox a b) * content K / interv_diff K i"
        proof (cases "content K = 0")
          case True
          then show ?thesis by simp
        next
          case False
          then have Kgt0: "content K > 0"
            using zero_less_measure_iff by blast
          moreover
          obtain u v where uv: "K = cbox u v"
            using S \<open>(x,K) \<in> S\<close> unfolding tagged_partial_division_of_def by blast
          then have u_less_v: "\i. i \ Basis \ u \ i < v \ i"
            using content_pos_lt_eq uv Kgt0 by blast
          then have dist_uv: "dist u v > 0"
            using that by auto
          ultimately have "norm (h x) \ (\ * (b \ i - a \ i)) / (4 * content (cbox a b) * interv_diff K i)"
          proof -
            have "dist x u < \ * (INF m\Basis. b \ m - a \ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
                 "dist x v < \ * (INF m\Basis. b \ m - a \ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
              using fineS u_less_v uv xK
              by (force simp: fine_def mem_box field_simps dest!: bspec)+
            moreover have "\ * (INF m\Basis. b \ m - a \ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
                  \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
            proof (intro mult_left_mono divide_right_mono)
              show "(INF m\Basis. b \ m - a \ m) \ b \ i - a \ i"
                using \<open>i \<in> Basis\<close> by (auto intro!: cInf_le_finite)
            qed (use \<open>0 < \<epsilon>\<close> in auto)
            ultimately
            have "dist x u < \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
                 "dist x v < \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
              by linarith+
            then have duv: "dist u v < \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b))"
              using dist_triangle_half_r by blast
            have uvi: "\v \ i - u \ i\ \ norm (v - u)"
              by (metis inner_commute inner_diff_right \<open>i \<in> Basis\<close> Basis_le_norm)
            have "norm (h x) \ norm (f x)"
              using x that by (auto simp: norm_f)
            also have "... < (norm (f x) + 1)"
              by simp
            also have "... < \ * (b \ i - a \ i) / dist u v / (4 * content (cbox a b))"
            proof -
              have "0 < norm (f x) + 1"
                by (simp add: add.commute add_pos_nonneg)
              then show ?thesis
                using duv dist_uv contab_gt0
                by (simp only: mult_ac divide_simps) auto
            qed
            also have "... = \ * (b \ i - a \ i) / norm (v - u) / (4 * content (cbox a b))"
              by (simp add: dist_norm norm_minus_commute)
            also have "... \ \ * (b \ i - a \ i) / \v \ i - u \ i\ / (4 * content (cbox a b))"
            proof (intro mult_right_mono divide_left_mono divide_right_mono uvi)
              show "norm (v - u) * \v \ i - u \ i\ > 0"
                using u_less_v [OF \<open>i \<in> Basis\<close>] 
                by (auto simp: less_eq_real_def zero_less_mult_iff that)
              show "\ * (b \ i - a \ i) \ 0"
                using a_less_b \<open>0 < \<epsilon>\<close> \<open>i \<in> Basis\<close> by force
            qed auto
            also have "... = \ * (b \ i - a \ i) / (4 * content (cbox a b) * interv_diff K i)"
              using uv False that(2) u_less_v interv_diff_def by fastforce
            finally show ?thesis by simp
          qed
          with Kgt0 have "norm (content K *\<^sub>R h x) \ content K * ((\/4 * (b \ i - a \ i) / content (cbox a b)) / interv_diff K i)"
            using mult_left_mono by fastforce
          also have "... = \/4 * (b \ i - a \ i) / content (cbox a b) * content K / interv_diff K i"
            by (simp add: field_split_simps)
          finally show ?thesis .
        qed
      qed
      also have "... = (\K\snd ` S. \/4 * (b \ i - a \ i) / content (cbox a b) * content K / interv_diff K i)"
        unfolding interv_diff_def
        apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]])
        apply (simp add: box_eq_empty(1) content_eq_0)
        done
      also have "... = \/2 * ((b \ i - a \ i) / (2 * content (cbox a b)) * (\K\snd ` S. content K / interv_diff K i))"
        by (simp add: interv_diff_def sum_distrib_left mult.assoc)
      also have "... \ (\/2) * 1"
      proof (rule mult_left_mono)
        have "(b \ i - a \ i) * (\K\snd ` S. content K / interv_diff K i) \ 2 * content (cbox a b)"
          unfolding interv_diff_def
        proof (rule sum_content_area_over_thin_division)
          show "snd ` S division_of \(snd ` S)"
            by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
          show "\(snd ` S) \ cbox a b"
            using S unfolding tagged_partial_division_of_def by force
          show "a \ i \ c \ i" "c \ i \ b \ i"
            using mem_box(2) that by blast+
        qed (use that in auto)
        then show "(b \ i - a \ i) / (2 * content (cbox a b)) * (\K\snd ` S. content K / interv_diff K i) \ 1"
          by (simp add: contab_gt0)
      qed (use \<open>0 < \<epsilon>\<close> in auto)
      finally show ?thesis by simp
    qed
    then have "(\(x,K) \ S. norm (integral K h)) - (\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) \ \/2"
      by (simp add: Groups_Big.sum_subtractf [symmetric])
    ultimately show "(\(x,K) \ S. norm (integral K h)) < \"
      by linarith
  qed
  ultimately show ?thesis using that by auto
qed



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

--> maximum size reached

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

[ zur Elbe Produktseite wechseln0.25Quellennavigators  Analyse erneut starten  ]