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