src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
author paulson <lp15@cam.ac.uk>
Tue Feb 21 15:04:01 2017 +0000 (2017-02-21)
changeset 65036 ab7e11730ad8
parent 64911 f0e07600de47
child 65204 d23eded35a33
permissions -rw-r--r--
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
wenzelm@53399
     1
(*  Author:     John Harrison
lp15@60428
     2
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
wenzelm@53399
     3
*)
wenzelm@53399
     4
hoelzl@63594
     5
section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
hoelzl@63594
     6
hoelzl@63594
     7
theory Henstock_Kurzweil_Integration
wenzelm@41413
     8
imports
hoelzl@63957
     9
  Lebesgue_Measure Tagged_Division
himmelma@35172
    10
begin
himmelma@35172
    11
lp15@65036
    12
(* try instead structured proofs below *)
hoelzl@63957
    13
lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
hoelzl@63957
    14
  \<Longrightarrow> norm(y - x) \<le> e"
hoelzl@63957
    15
  using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
hoelzl@63957
    16
  by (simp add: add_diff_add)
hoelzl@63957
    17
hoelzl@63957
    18
lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
hoelzl@63886
    19
  by auto
hoelzl@63886
    20
hoelzl@63957
    21
lemma setcomp_dot2: "{z. P (z \<bullet> (0,i))} = {(x,y). P(y \<bullet> i)}"
hoelzl@63957
    22
  by auto
hoelzl@63957
    23
hoelzl@63957
    24
lemma Sigma_Int_Paircomp1: "(Sigma A B) \<inter> {(x, y). P x} = Sigma (A \<inter> {x. P x}) B"
hoelzl@63957
    25
  by blast
hoelzl@63957
    26
hoelzl@63957
    27
lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
hoelzl@63957
    28
  by blast
hoelzl@63957
    29
(* END MOVE *)
hoelzl@59425
    30
wenzelm@60420
    31
subsection \<open>Content (length, area, volume...) of an interval.\<close>
himmelma@35172
    32
hoelzl@63886
    33
abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
hoelzl@63886
    34
  where "content s \<equiv> measure lborel s"
hoelzl@63886
    35
hoelzl@63886
    36
lemma content_cbox_cases:
nipkow@64272
    37
  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then prod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
hoelzl@63886
    38
  by (simp add: measure_lborel_cbox_eq inner_diff)
hoelzl@63886
    39
hoelzl@63886
    40
lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
hoelzl@63886
    41
  unfolding content_cbox_cases by simp
hoelzl@63886
    42
hoelzl@63886
    43
lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
hoelzl@63886
    44
  by (simp add: box_ne_empty inner_diff)
wenzelm@49970
    45
wenzelm@53408
    46
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
hoelzl@63886
    47
  by simp
immler@56188
    48
wenzelm@61945
    49
lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
paulson@61204
    50
  by (auto simp: content_real)
paulson@61204
    51
hoelzl@63886
    52
lemma content_singleton: "content {a} = 0"
hoelzl@63886
    53
  by simp
hoelzl@63886
    54
hoelzl@63886
    55
lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
hoelzl@63886
    56
  by simp
hoelzl@63886
    57
hoelzl@63886
    58
lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
hoelzl@63886
    59
  by simp
hoelzl@63886
    60
hoelzl@63886
    61
corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
hoelzl@63886
    62
  using not_le by blast
hoelzl@63886
    63
hoelzl@63886
    64
lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
nipkow@64272
    65
  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)
hoelzl@63886
    66
hoelzl@63886
    67
lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
hoelzl@63886
    68
  by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
immler@56188
    69
immler@56188
    70
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
hoelzl@63886
    71
  unfolding content_eq_0 interior_cbox box_eq_empty by auto
hoelzl@63886
    72
hoelzl@63886
    73
lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
nipkow@64272
    74
  by (auto simp add: content_cbox_cases less_le prod_nonneg)
wenzelm@49970
    75
wenzelm@53399
    76
lemma content_empty [simp]: "content {} = 0"
hoelzl@63886
    77
  by simp
himmelma@35172
    78
paulson@60762
    79
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
paulson@60762
    80
  by (simp add: content_real)
paulson@60762
    81
hoelzl@63886
    82
lemma content_subset: "cbox a b \<subseteq> cbox c d \<Longrightarrow> content (cbox a b) \<le> content (cbox c d)"
hoelzl@63886
    83
  unfolding measure_def
hoelzl@63886
    84
  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
immler@56188
    85
immler@56188
    86
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
nipkow@44890
    87
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
himmelma@35172
    88
lp15@60615
    89
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
hoelzl@63886
    90
  unfolding measure_lborel_cbox_eq Basis_prod_def
nipkow@64272
    91
  apply (subst prod.union_disjoint)
hoelzl@63886
    92
  apply (auto simp: bex_Un ball_Un)
nipkow@64272
    93
  apply (subst (1 2) prod.reindex_nontrivial)
hoelzl@63886
    94
  apply auto
hoelzl@63886
    95
  done
lp15@60615
    96
lp15@60615
    97
lemma content_cbox_pair_eq0_D:
lp15@60615
    98
   "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
lp15@60615
    99
  by (simp add: content_Pair)
lp15@60615
   100
hoelzl@63886
   101
lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
hoelzl@63886
   102
  using emeasure_mono[of s "cbox a b" lborel]
hoelzl@63886
   103
  by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
hoelzl@63593
   104
hoelzl@63593
   105
lemma content_split:
hoelzl@63593
   106
  fixes a :: "'a::euclidean_space"
hoelzl@63593
   107
  assumes "k \<in> Basis"
hoelzl@63593
   108
  shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
wenzelm@64911
   109
  \<comment> \<open>Prove using measure theory\<close>
hoelzl@63593
   110
proof cases
hoelzl@63593
   111
  note simps = interval_split[OF assms] content_cbox_cases
hoelzl@63593
   112
  have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
hoelzl@63593
   113
    using assms by auto
hoelzl@63593
   114
  have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
hoelzl@63593
   115
    "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
hoelzl@63593
   116
    apply (subst *(1))
hoelzl@63593
   117
    defer
hoelzl@63593
   118
    apply (subst *(1))
nipkow@64272
   119
    unfolding prod.insert[OF *(2-)]
hoelzl@63593
   120
    apply auto
hoelzl@63593
   121
    done
hoelzl@63593
   122
  assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
hoelzl@63593
   123
  moreover
hoelzl@63593
   124
  have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
hoelzl@63593
   125
    x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
hoelzl@63593
   126
    by  (auto simp add: field_simps)
hoelzl@63593
   127
  moreover
hoelzl@63593
   128
  have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
hoelzl@63593
   129
      (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
hoelzl@63593
   130
    "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
hoelzl@63593
   131
      (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
nipkow@64272
   132
    by (auto intro!: prod.cong)
hoelzl@63593
   133
  have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
hoelzl@63593
   134
    unfolding not_le
hoelzl@63593
   135
    using as[unfolded ,rule_format,of k] assms
hoelzl@63593
   136
    by auto
hoelzl@63593
   137
  ultimately show ?thesis
hoelzl@63593
   138
    using assms
hoelzl@63593
   139
    unfolding simps **
hoelzl@63593
   140
    unfolding *(1)[of "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
hoelzl@63593
   141
    unfolding *(2)
hoelzl@63593
   142
    by auto
hoelzl@63593
   143
next
hoelzl@63593
   144
  assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
hoelzl@63593
   145
  then have "cbox a b = {}"
hoelzl@63593
   146
    unfolding box_eq_empty by (auto simp: not_le)
hoelzl@63593
   147
  then show ?thesis
hoelzl@63593
   148
    by (auto simp: not_le)
hoelzl@63593
   149
qed
hoelzl@63593
   150
wenzelm@49970
   151
lemma division_of_content_0:
immler@56188
   152
  assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
wenzelm@49970
   153
  shows "\<forall>k\<in>d. content k = 0"
wenzelm@49970
   154
  unfolding forall_in_division[OF assms(2)]
lp15@60384
   155
  by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
wenzelm@49970
   156
nipkow@64267
   157
lemma sum_content_null:
hoelzl@63957
   158
  assumes "content (cbox a b) = 0"
hoelzl@63957
   159
    and "p tagged_division_of (cbox a b)"
nipkow@64267
   160
  shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
nipkow@64267
   161
proof (rule sum.neutral, rule)
hoelzl@63957
   162
  fix y
hoelzl@63957
   163
  assume y: "y \<in> p"
hoelzl@63957
   164
  obtain x k where xk: "y = (x, k)"
hoelzl@63957
   165
    using surj_pair[of y] by blast
hoelzl@63957
   166
  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
hoelzl@63957
   167
  from this(2) obtain c d where k: "k = cbox c d" by blast
hoelzl@63957
   168
  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
hoelzl@63957
   169
    unfolding xk by auto
hoelzl@63957
   170
  also have "\<dots> = 0"
hoelzl@63957
   171
    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
hoelzl@63957
   172
    unfolding assms(1) k
wenzelm@53399
   173
    by auto
hoelzl@63957
   174
  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
hoelzl@63593
   175
qed
hoelzl@63593
   176
hoelzl@63593
   177
lemma operative_content[intro]: "add.operative content"
hoelzl@63957
   178
  by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior)
hoelzl@63593
   179
nipkow@64267
   180
lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum content d = content (cbox a b)"
nipkow@64267
   181
  by (metis operative_content sum.operative_division)
hoelzl@63593
   182
hoelzl@63593
   183
lemma additive_content_tagged_division:
nipkow@64267
   184
  "d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<lambda>(x,l). content l) d = content (cbox a b)"
nipkow@64267
   185
  unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast
hoelzl@63593
   186
hoelzl@63593
   187
lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
hoelzl@63593
   188
  by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
hoelzl@63593
   189
hoelzl@63957
   190
lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
hoelzl@63957
   191
  using content_empty unfolding empty_as_interval by auto
hoelzl@63944
   192
hoelzl@63944
   193
subsection \<open>Gauge integral\<close>
hoelzl@63944
   194
hoelzl@63944
   195
text \<open>Case distinction to define it first on compact intervals first, then use a limit. This is only
hoelzl@63944
   196
much later unified. In Fremlin: Measure Theory, Volume 4I this is generalized using residual sets.\<close>
hoelzl@63944
   197
hoelzl@63944
   198
definition has_integral :: "('n::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> 'n set \<Rightarrow> bool"
hoelzl@63944
   199
  (infixr "has'_integral" 46)
hoelzl@63944
   200
  where "(f has_integral I) s \<longleftrightarrow>
hoelzl@63944
   201
    (if \<exists>a b. s = cbox a b
hoelzl@63944
   202
      then ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R f x) \<longlongrightarrow> I) (division_filter s)
hoelzl@63944
   203
      else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
hoelzl@63944
   204
        (\<exists>z. ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R (if x \<in> s then f x else 0)) \<longlongrightarrow> z) (division_filter (cbox a b)) \<and>
hoelzl@63944
   205
          norm (z - I) < e)))"
hoelzl@63944
   206
hoelzl@63944
   207
lemma has_integral_cbox:
hoelzl@63944
   208
  "(f has_integral I) (cbox a b) \<longleftrightarrow> ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R f x) \<longlongrightarrow> I) (division_filter (cbox a b))"
hoelzl@63944
   209
  by (auto simp add: has_integral_def)
hoelzl@63944
   210
hoelzl@63944
   211
lemma has_integral:
hoelzl@63944
   212
  "(f has_integral y) (cbox a b) \<longleftrightarrow>
hoelzl@63944
   213
    (\<forall>e>0. \<exists>d. gauge d \<and>
hoelzl@63944
   214
      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
nipkow@64267
   215
        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
hoelzl@63944
   216
  by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)
hoelzl@63944
   217
hoelzl@63944
   218
lemma has_integral_real:
hoelzl@63944
   219
  "(f has_integral y) {a .. b::real} \<longleftrightarrow>
hoelzl@63944
   220
    (\<forall>e>0. \<exists>d. gauge d \<and>
hoelzl@63944
   221
      (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow>
nipkow@64267
   222
        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
hoelzl@63944
   223
  unfolding box_real[symmetric]
hoelzl@63944
   224
  by (rule has_integral)
hoelzl@63944
   225
hoelzl@63944
   226
lemma has_integralD[dest]:
hoelzl@63944
   227
  assumes "(f has_integral y) (cbox a b)"
hoelzl@63944
   228
    and "e > 0"
hoelzl@63944
   229
  obtains d
hoelzl@63944
   230
    where "gauge d"
hoelzl@63944
   231
      and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
hoelzl@63944
   232
        norm ((\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) - y) < e"
hoelzl@63944
   233
  using assms unfolding has_integral by auto
hoelzl@63944
   234
hoelzl@63944
   235
lemma has_integral_alt:
hoelzl@63944
   236
  "(f has_integral y) i \<longleftrightarrow>
hoelzl@63944
   237
    (if \<exists>a b. i = cbox a b
hoelzl@63944
   238
     then (f has_integral y) i
hoelzl@63944
   239
     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
hoelzl@63944
   240
      (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
hoelzl@63944
   241
  by (subst has_integral_def) (auto simp add: has_integral_cbox)
hoelzl@63944
   242
hoelzl@63944
   243
lemma has_integral_altD:
hoelzl@63944
   244
  assumes "(f has_integral y) i"
hoelzl@63944
   245
    and "\<not> (\<exists>a b. i = cbox a b)"
hoelzl@63944
   246
    and "e>0"
hoelzl@63944
   247
  obtains B where "B > 0"
hoelzl@63944
   248
    and "\<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
hoelzl@63944
   249
      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - y) < e)"
hoelzl@63944
   250
  using assms has_integral_alt[of f y i] by auto
hoelzl@63944
   251
hoelzl@63944
   252
definition integrable_on (infixr "integrable'_on" 46)
hoelzl@63944
   253
  where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
hoelzl@63944
   254
hoelzl@63944
   255
definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
hoelzl@63944
   256
hoelzl@63944
   257
lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
hoelzl@63944
   258
  unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
hoelzl@63944
   259
hoelzl@63944
   260
lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
hoelzl@63944
   261
  unfolding integrable_on_def integral_def by blast
hoelzl@63944
   262
hoelzl@63944
   263
lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
hoelzl@63944
   264
  unfolding integrable_on_def by auto
hoelzl@63944
   265
hoelzl@63944
   266
lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
hoelzl@63944
   267
  by auto
hoelzl@63944
   268
wenzelm@60420
   269
subsection \<open>Basic theorems about integrals.\<close>
himmelma@35172
   270
wenzelm@53409
   271
lemma has_integral_unique:
immler@56188
   272
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
   273
  assumes "(f has_integral k1) i"
wenzelm@53410
   274
    and "(f has_integral k2) i"
wenzelm@53409
   275
  shows "k1 = k2"
wenzelm@53410
   276
proof (rule ccontr)
wenzelm@53842
   277
  let ?e = "norm (k1 - k2) / 2"
wenzelm@61165
   278
  assume as: "k1 \<noteq> k2"
wenzelm@53410
   279
  then have e: "?e > 0"
wenzelm@53410
   280
    by auto
hoelzl@63944
   281
  have lem: "(f has_integral k1) (cbox a b) \<Longrightarrow> (f has_integral k2) (cbox a b) \<Longrightarrow> k1 = k2"
wenzelm@61165
   282
    for f :: "'n \<Rightarrow> 'a" and a b k1 k2
hoelzl@63944
   283
    by (auto simp: has_integral_cbox intro: tendsto_unique[OF division_filter_not_empty])
wenzelm@53410
   284
  {
immler@56188
   285
    presume "\<not> (\<exists>a b. i = cbox a b) \<Longrightarrow> False"
wenzelm@53410
   286
    then show False
lp15@60396
   287
      using as assms lem by blast
wenzelm@53410
   288
  }
immler@56188
   289
  assume as: "\<not> (\<exists>a b. i = cbox a b)"
wenzelm@55751
   290
  obtain B1 where B1:
wenzelm@55751
   291
      "0 < B1"
immler@56188
   292
      "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
immler@56188
   293
        \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and>
wenzelm@55751
   294
          norm (z - k1) < norm (k1 - k2) / 2"
wenzelm@55751
   295
    by (rule has_integral_altD[OF assms(1) as,OF e]) blast
wenzelm@55751
   296
  obtain B2 where B2:
wenzelm@55751
   297
      "0 < B2"
immler@56188
   298
      "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
immler@56188
   299
        \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and>
wenzelm@55751
   300
          norm (z - k2) < norm (k1 - k2) / 2"
wenzelm@55751
   301
    by (rule has_integral_altD[OF assms(2) as,OF e]) blast
immler@56188
   302
  have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> cbox a b"
immler@56188
   303
    apply (rule bounded_subset_cbox)
wenzelm@53410
   304
    using bounded_Un bounded_ball
wenzelm@53410
   305
    apply auto
wenzelm@53410
   306
    done
immler@56188
   307
  then obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
wenzelm@53410
   308
    by blast
wenzelm@53410
   309
  obtain w where w:
immler@56188
   310
    "((\<lambda>x. if x \<in> i then f x else 0) has_integral w) (cbox a b)"
wenzelm@53410
   311
    "norm (w - k1) < norm (k1 - k2) / 2"
wenzelm@53410
   312
    using B1(2)[OF ab(1)] by blast
wenzelm@53410
   313
  obtain z where z:
immler@56188
   314
    "((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b)"
wenzelm@53410
   315
    "norm (z - k2) < norm (k1 - k2) / 2"
wenzelm@53410
   316
    using B2(2)[OF ab(2)] by blast
wenzelm@53410
   317
  have "z = w"
wenzelm@53410
   318
    using lem[OF w(1) z(1)] by auto
wenzelm@53410
   319
  then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
wenzelm@53410
   320
    using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
wenzelm@53410
   321
    by (auto simp add: norm_minus_commute)
wenzelm@53410
   322
  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
wenzelm@53410
   323
    apply (rule add_strict_mono)
wenzelm@53410
   324
    apply (rule_tac[!] z(2) w(2))
wenzelm@53410
   325
    done
wenzelm@53410
   326
  finally show False by auto
wenzelm@53410
   327
qed
wenzelm@53410
   328
wenzelm@53410
   329
lemma integral_unique [intro]: "(f has_integral y) k \<Longrightarrow> integral k f = y"
wenzelm@53410
   330
  unfolding integral_def
wenzelm@53410
   331
  by (rule some_equality) (auto intro: has_integral_unique)
wenzelm@53410
   332
lp15@62463
   333
lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> ~ f integrable_on k \<and> y=0"
lp15@62463
   334
  unfolding integral_def integrable_on_def
lp15@62463
   335
  apply (erule subst)
lp15@62463
   336
  apply (rule someI_ex)
lp15@62463
   337
  by blast
lp15@62463
   338
hoelzl@63944
   339
hoelzl@63944
   340
lemma has_integral_const [intro]:
hoelzl@63944
   341
  fixes a b :: "'a::euclidean_space"
hoelzl@63944
   342
  shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)"
hoelzl@63944
   343
  using eventually_division_filter_tagged_division[of "cbox a b"]
hoelzl@63944
   344
     additive_content_tagged_division[of _ a b]
nipkow@64267
   345
  by (auto simp: has_integral_cbox split_beta' scaleR_sum_left[symmetric]
hoelzl@63944
   346
           elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const])
hoelzl@63944
   347
hoelzl@63944
   348
lemma has_integral_const_real [intro]:
hoelzl@63944
   349
  fixes a b :: real
hoelzl@63944
   350
  shows "((\<lambda>x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}"
hoelzl@63944
   351
  by (metis box_real(2) has_integral_const)
hoelzl@63944
   352
hoelzl@63944
   353
lemma integral_const [simp]:
hoelzl@63944
   354
  fixes a b :: "'a::euclidean_space"
hoelzl@63944
   355
  shows "integral (cbox a b) (\<lambda>x. c) = content (cbox a b) *\<^sub>R c"
hoelzl@63944
   356
  by (rule integral_unique) (rule has_integral_const)
hoelzl@63944
   357
hoelzl@63944
   358
lemma integral_const_real [simp]:
hoelzl@63944
   359
  fixes a b :: real
hoelzl@63944
   360
  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
hoelzl@63944
   361
  by (metis box_real(2) integral_const)
hoelzl@63944
   362
wenzelm@53410
   363
lemma has_integral_is_0:
immler@56188
   364
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
   365
  assumes "\<forall>x\<in>s. f x = 0"
wenzelm@53410
   366
  shows "(f has_integral 0) s"
wenzelm@53410
   367
proof -
hoelzl@63944
   368
  have lem: "(\<forall>x\<in>cbox a b. f x = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)" for a  b and f :: "'n \<Rightarrow> 'a"
hoelzl@63944
   369
    unfolding has_integral_cbox
hoelzl@63944
   370
    using eventually_division_filter_tagged_division[of "cbox a b"]
hoelzl@63944
   371
    by (subst tendsto_cong[where g="\<lambda>_. 0"])
nipkow@64267
   372
       (auto elim!: eventually_mono intro!: sum.neutral simp: tag_in_interval)
wenzelm@53410
   373
  {
immler@56188
   374
    presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
lp15@60396
   375
    with assms lem show ?thesis
lp15@60396
   376
      by blast
wenzelm@53410
   377
  }
wenzelm@53410
   378
  have *: "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)"
wenzelm@53410
   379
    apply (rule ext)
wenzelm@53410
   380
    using assms
wenzelm@53410
   381
    apply auto
wenzelm@53410
   382
    done
immler@56188
   383
  assume "\<not> (\<exists>a b. s = cbox a b)"
wenzelm@53410
   384
  then show ?thesis
lp15@60396
   385
    using lem
lp15@60396
   386
    by (subst has_integral_alt) (force simp add: *)
wenzelm@53410
   387
qed
himmelma@35172
   388
immler@56188
   389
lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) s"
wenzelm@53410
   390
  by (rule has_integral_is_0) auto
himmelma@35172
   391
himmelma@35172
   392
lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) s \<longleftrightarrow> i = 0"
himmelma@35172
   393
  using has_integral_unique[OF has_integral_0] by auto
himmelma@35172
   394
wenzelm@53410
   395
lemma has_integral_linear:
immler@56188
   396
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
   397
  assumes "(f has_integral y) s"
wenzelm@53410
   398
    and "bounded_linear h"
wenzelm@61736
   399
  shows "((h \<circ> f) has_integral ((h y))) s"
wenzelm@53410
   400
proof -
wenzelm@53410
   401
  interpret bounded_linear h
wenzelm@53410
   402
    using assms(2) .
wenzelm@53410
   403
  from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
wenzelm@53410
   404
    by blast
hoelzl@63944
   405
  have lem: "\<And>a b y f::'n\<Rightarrow>'a. (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> f) has_integral h y) (cbox a b)"
nipkow@64267
   406
    unfolding has_integral_cbox by (drule tendsto) (simp add: sum scaleR split_beta')
wenzelm@53410
   407
  {
immler@56188
   408
    presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
wenzelm@53410
   409
    then show ?thesis
lp15@60396
   410
      using assms(1) lem by blast
wenzelm@53410
   411
  }
immler@56188
   412
  assume as: "\<not> (\<exists>a b. s = cbox a b)"
wenzelm@53410
   413
  then show ?thesis
lp15@60396
   414
  proof (subst has_integral_alt, clarsimp)
wenzelm@53410
   415
    fix e :: real
wenzelm@53410
   416
    assume e: "e > 0"
nipkow@56541
   417
    have *: "0 < e/B" using e B(1) by simp
wenzelm@53410
   418
    obtain M where M:
wenzelm@53410
   419
      "M > 0"
immler@56188
   420
      "\<And>a b. ball 0 M \<subseteq> cbox a b \<Longrightarrow>
immler@56188
   421
        \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e / B"
wenzelm@53410
   422
      using has_integral_altD[OF assms(1) as *] by blast
immler@56188
   423
    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
immler@56188
   424
      (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
wenzelm@61166
   425
    proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases)
wenzelm@61167
   426
      case prems: (1 a b)
wenzelm@53410
   427
      obtain z where z:
immler@56188
   428
        "((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
wenzelm@53410
   429
        "norm (z - y) < e / B"
wenzelm@61167
   430
        using M(2)[OF prems(1)] by blast
wenzelm@53410
   431
      have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
lp15@60396
   432
        using zero by auto
wenzelm@53410
   433
      show ?case
wenzelm@53410
   434
        apply (rule_tac x="h z" in exI)
hoelzl@63944
   435
        apply (simp add: * lem[OF z(1)])
wenzelm@61165
   436
        apply (metis B diff le_less_trans pos_less_divide_eq z(2))
wenzelm@61165
   437
        done
wenzelm@53410
   438
    qed
wenzelm@53410
   439
  qed
wenzelm@53410
   440
qed
wenzelm@53410
   441
lp15@60615
   442
lemma has_integral_scaleR_left:
hoelzl@57447
   443
  "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
hoelzl@57447
   444
  using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
hoelzl@57447
   445
hoelzl@57447
   446
lemma has_integral_mult_left:
lp15@62463
   447
  fixes c :: "_ :: real_normed_algebra"
hoelzl@57447
   448
  shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
hoelzl@57447
   449
  using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
hoelzl@57447
   450
lp15@62463
   451
text\<open>The case analysis eliminates the condition @{term "f integrable_on s"} at the cost
wenzelm@62837
   452
     of the type class constraint \<open>division_ring\<close>\<close>
lp15@62463
   453
corollary integral_mult_left [simp]:
lp15@62463
   454
  fixes c:: "'a::{real_normed_algebra,division_ring}"
lp15@62463
   455
  shows "integral s (\<lambda>x. f x * c) = integral s f * c"
lp15@62463
   456
proof (cases "f integrable_on s \<or> c = 0")
lp15@62463
   457
  case True then show ?thesis
lp15@62463
   458
    by (force intro: has_integral_mult_left)
lp15@62463
   459
next
lp15@62463
   460
  case False then have "~ (\<lambda>x. f x * c) integrable_on s"
lp15@62463
   461
    using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ s "inverse c"]
lp15@62463
   462
    by (force simp add: mult.assoc)
lp15@62463
   463
  with False show ?thesis by (simp add: not_integrable_integral)
lp15@62463
   464
qed
lp15@62463
   465
lp15@62463
   466
corollary integral_mult_right [simp]:
lp15@62463
   467
  fixes c:: "'a::{real_normed_field}"
lp15@62463
   468
  shows "integral s (\<lambda>x. c * f x) = c * integral s f"
lp15@62463
   469
by (simp add: mult.commute [of c])
lp15@60615
   470
lp15@62533
   471
corollary integral_divide [simp]:
lp15@62533
   472
  fixes z :: "'a::real_normed_field"
lp15@62533
   473
  shows "integral S (\<lambda>x. f x / z) = integral S (\<lambda>x. f x) / z"
lp15@62533
   474
using integral_mult_left [of S f "inverse z"]
lp15@62533
   475
  by (simp add: divide_inverse_commute)
lp15@62533
   476
paulson@60762
   477
lemma has_integral_mult_right:
paulson@60762
   478
  fixes c :: "'a :: real_normed_algebra"
paulson@60762
   479
  shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
paulson@60762
   480
  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)
wenzelm@61165
   481
wenzelm@53410
   482
lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
wenzelm@53410
   483
  unfolding o_def[symmetric]
lp15@60396
   484
  by (metis has_integral_linear bounded_linear_scaleR_right)
himmelma@35172
   485
hoelzl@50104
   486
lemma has_integral_cmult_real:
hoelzl@50104
   487
  fixes c :: real
hoelzl@50104
   488
  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
hoelzl@50104
   489
  shows "((\<lambda>x. c * f x) has_integral c * x) A"
wenzelm@53410
   490
proof (cases "c = 0")
wenzelm@53410
   491
  case True
wenzelm@53410
   492
  then show ?thesis by simp
wenzelm@53410
   493
next
wenzelm@53410
   494
  case False
hoelzl@50104
   495
  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
hoelzl@50104
   496
    unfolding real_scaleR_def .
wenzelm@53410
   497
qed
wenzelm@53410
   498
lp15@62463
   499
lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) s"
lp15@60396
   500
  by (drule_tac c="-1" in has_integral_cmul) auto
wenzelm@53410
   501
wenzelm@53410
   502
lemma has_integral_add:
immler@56188
   503
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53410
   504
  assumes "(f has_integral k) s"
wenzelm@53410
   505
    and "(g has_integral l) s"
himmelma@35172
   506
  shows "((\<lambda>x. f x + g x) has_integral (k + l)) s"
wenzelm@53410
   507
proof -
hoelzl@63944
   508
  have lem: "(f has_integral k) (cbox a b) \<Longrightarrow> (g has_integral l) (cbox a b) \<Longrightarrow>
hoelzl@63944
   509
    ((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
wenzelm@61165
   510
    for f :: "'n \<Rightarrow> 'a" and g a b k l
hoelzl@63944
   511
    unfolding has_integral_cbox
nipkow@64267
   512
    by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add)
wenzelm@53410
   513
  {
immler@56188
   514
    presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
wenzelm@53410
   515
    then show ?thesis
lp15@60396
   516
      using assms lem by force
wenzelm@53410
   517
  }
immler@56188
   518
  assume as: "\<not> (\<exists>a b. s = cbox a b)"
wenzelm@53410
   519
  then show ?thesis
wenzelm@61166
   520
  proof (subst has_integral_alt, clarsimp, goal_cases)
wenzelm@61165
   521
    case (1 e)
wenzelm@61165
   522
    then have *: "e / 2 > 0"
wenzelm@53410
   523
      by auto
wenzelm@55751
   524
    from has_integral_altD[OF assms(1) as *]
wenzelm@55751
   525
    obtain B1 where B1:
wenzelm@55751
   526
        "0 < B1"
immler@56188
   527
        "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
immler@56188
   528
          \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - k) < e / 2"
wenzelm@55751
   529
      by blast
wenzelm@55751
   530
    from has_integral_altD[OF assms(2) as *]
wenzelm@55751
   531
    obtain B2 where B2:
wenzelm@55751
   532
        "0 < B2"
immler@56188
   533
        "\<And>a b. ball 0 B2 \<subseteq> (cbox a b) \<Longrightarrow>
immler@56188
   534
          \<exists>z. ((\<lambda>x. if x \<in> s then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e / 2"
wenzelm@55751
   535
      by blast
wenzelm@53410
   536
    show ?case
lp15@60396
   537
    proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1)
wenzelm@53410
   538
      fix a b
immler@56188
   539
      assume "ball 0 (max B1 B2) \<subseteq> cbox a (b::'n)"
immler@56188
   540
      then have *: "ball 0 B1 \<subseteq> cbox a (b::'n)" "ball 0 B2 \<subseteq> cbox a (b::'n)"
wenzelm@53410
   541
        by auto
wenzelm@53410
   542
      obtain w where w:
immler@56188
   543
        "((\<lambda>x. if x \<in> s then f x else 0) has_integral w) (cbox a b)"
wenzelm@53410
   544
        "norm (w - k) < e / 2"
wenzelm@53410
   545
        using B1(2)[OF *(1)] by blast
wenzelm@53410
   546
      obtain z where z:
immler@56188
   547
        "((\<lambda>x. if x \<in> s then g x else 0) has_integral z) (cbox a b)"
wenzelm@53410
   548
        "norm (z - l) < e / 2"
wenzelm@53410
   549
        using B2(2)[OF *(2)] by blast
wenzelm@53410
   550
      have *: "\<And>x. (if x \<in> s then f x + g x else 0) =
wenzelm@53410
   551
        (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)"
wenzelm@53410
   552
        by auto
immler@56188
   553
      show "\<exists>z. ((\<lambda>x. if x \<in> s then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
wenzelm@53410
   554
        apply (rule_tac x="w + z" in exI)
lp15@60396
   555
        apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]])
wenzelm@53410
   556
        using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2)
wenzelm@53410
   557
        apply (auto simp add: field_simps)
wenzelm@53410
   558
        done
wenzelm@53410
   559
    qed
wenzelm@53410
   560
  qed
wenzelm@53410
   561
qed
himmelma@35172
   562
himmelma@35172
   563
lemma has_integral_sub:
wenzelm@53410
   564
  "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
wenzelm@53410
   565
    ((\<lambda>x. f x - g x) has_integral (k - l)) s"
wenzelm@53410
   566
  using has_integral_add[OF _ has_integral_neg, of f k s g l]
lp15@63469
   567
  by (auto simp: algebra_simps)
wenzelm@53410
   568
lp15@62463
   569
lemma integral_0 [simp]:
immler@56188
   570
  "integral s (\<lambda>x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
wenzelm@53410
   571
  by (rule integral_unique has_integral_0)+
wenzelm@53410
   572
wenzelm@53410
   573
lemma integral_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
wenzelm@53410
   574
    integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
lp15@60396
   575
  by (rule integral_unique) (metis integrable_integral has_integral_add)
wenzelm@53410
   576
lp15@62463
   577
lemma integral_cmul [simp]: "integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
lp15@62463
   578
proof (cases "f integrable_on s \<or> c = 0")
lp15@62463
   579
  case True with has_integral_cmul show ?thesis by force
lp15@62463
   580
next
lp15@62463
   581
  case False then have "~ (\<lambda>x. c *\<^sub>R f x) integrable_on s"
lp15@62463
   582
    using has_integral_cmul [of "(\<lambda>x. c *\<^sub>R f x)" _ s "inverse c"]
lp15@62463
   583
    by force
lp15@62463
   584
  with False show ?thesis by (simp add: not_integrable_integral)
lp15@62463
   585
qed
lp15@62463
   586
lp15@62463
   587
lemma integral_neg [simp]: "integral s (\<lambda>x. - f x) = - integral s f"
lp15@62463
   588
proof (cases "f integrable_on s")
lp15@62463
   589
  case True then show ?thesis
lp15@62463
   590
    by (simp add: has_integral_neg integrable_integral integral_unique)
lp15@62463
   591
next
lp15@62463
   592
  case False then have "~ (\<lambda>x. - f x) integrable_on s"
lp15@62463
   593
    using has_integral_neg [of "(\<lambda>x. - f x)" _ s ]
lp15@62463
   594
    by force
lp15@62463
   595
  with False show ?thesis by (simp add: not_integrable_integral)
lp15@62463
   596
qed
wenzelm@53410
   597
lp15@61806
   598
lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
wenzelm@53410
   599
    integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
lp15@60396
   600
  by (rule integral_unique) (metis integrable_integral has_integral_sub)
himmelma@35172
   601
himmelma@35172
   602
lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
himmelma@35172
   603
  unfolding integrable_on_def using has_integral_0 by auto
himmelma@35172
   604
wenzelm@53410
   605
lemma integrable_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) integrable_on s"
himmelma@35172
   606
  unfolding integrable_on_def by(auto intro: has_integral_add)
himmelma@35172
   607
wenzelm@53410
   608
lemma integrable_cmul: "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
himmelma@35172
   609
  unfolding integrable_on_def by(auto intro: has_integral_cmul)
himmelma@35172
   610
hoelzl@50104
   611
lemma integrable_on_cmult_iff:
wenzelm@53410
   612
  fixes c :: real
wenzelm@53410
   613
  assumes "c \<noteq> 0"
hoelzl@50104
   614
  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
wenzelm@60420
   615
  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] \<open>c \<noteq> 0\<close>
hoelzl@50104
   616
  by auto
hoelzl@50104
   617
lp15@62533
   618
lemma integrable_on_cmult_left:
lp15@62533
   619
  assumes "f integrable_on s"
lp15@62533
   620
  shows "(\<lambda>x. of_real c * f x) integrable_on s"
lp15@62533
   621
    using integrable_cmul[of f s "of_real c"] assms
lp15@62533
   622
    by (simp add: scaleR_conv_of_real)
lp15@62533
   623
wenzelm@53410
   624
lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
himmelma@35172
   625
  unfolding integrable_on_def by(auto intro: has_integral_neg)
himmelma@35172
   626
lp15@61806
   627
lemma integrable_diff:
wenzelm@53410
   628
  "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
himmelma@35172
   629
  unfolding integrable_on_def by(auto intro: has_integral_sub)
himmelma@35172
   630
himmelma@35172
   631
lemma integrable_linear:
wenzelm@53410
   632
  "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) integrable_on s"
himmelma@35172
   633
  unfolding integrable_on_def by(auto intro: has_integral_linear)
himmelma@35172
   634
himmelma@35172
   635
lemma integral_linear:
wenzelm@53410
   636
  "f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h \<circ> f) = h (integral s f)"
lp15@60396
   637
  apply (rule has_integral_unique [where i=s and f = "h \<circ> f"])
lp15@60396
   638
  apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
wenzelm@53410
   639
  done
wenzelm@53410
   640
wenzelm@53410
   641
lemma integral_component_eq[simp]:
immler@56188
   642
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
wenzelm@53410
   643
  assumes "f integrable_on s"
wenzelm@53410
   644
  shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
lp15@63938
   645
  unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..
himmelma@36243
   646
nipkow@64267
   647
lemma has_integral_sum:
wenzelm@53410
   648
  assumes "finite t"
wenzelm@53410
   649
    and "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
nipkow@64267
   650
  shows "((\<lambda>x. sum (\<lambda>a. f a x) t) has_integral (sum i t)) s"
wenzelm@53410
   651
  using assms(1) subset_refl[of t]
wenzelm@53410
   652
proof (induct rule: finite_subset_induct)
wenzelm@53410
   653
  case empty
wenzelm@53410
   654
  then show ?case by auto
wenzelm@53410
   655
next
wenzelm@53410
   656
  case (insert x F)
lp15@60396
   657
  with assms show ?case
lp15@60396
   658
    by (simp add: has_integral_add)
lp15@60396
   659
qed
lp15@60396
   660
nipkow@64267
   661
lemma integral_sum:
lp15@60396
   662
  "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow>
nipkow@64267
   663
   integral s (\<lambda>x. sum (\<lambda>a. f a x) t) = sum (\<lambda>a. integral s (f a)) t"
nipkow@64267
   664
  by (auto intro: has_integral_sum integrable_integral)
nipkow@64267
   665
nipkow@64267
   666
lemma integrable_sum:
nipkow@64267
   667
  "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) t) integrable_on s"
wenzelm@53410
   668
  unfolding integrable_on_def
wenzelm@53410
   669
  apply (drule bchoice)
nipkow@64267
   670
  using has_integral_sum[of t]
wenzelm@53410
   671
  apply auto
wenzelm@53410
   672
  done
himmelma@35172
   673
himmelma@35172
   674
lemma has_integral_eq:
lp15@60615
   675
  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
wenzelm@53410
   676
    and "(f has_integral k) s"
wenzelm@53410
   677
  shows "(g has_integral k) s"
himmelma@35172
   678
  using has_integral_sub[OF assms(2), of "\<lambda>x. f x - g x" 0]
wenzelm@53410
   679
  using has_integral_is_0[of s "\<lambda>x. f x - g x"]
wenzelm@53410
   680
  using assms(1)
wenzelm@53410
   681
  by auto
wenzelm@53410
   682
lp15@60615
   683
lemma integrable_eq: "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
wenzelm@53410
   684
  unfolding integrable_on_def
lp15@60615
   685
  using has_integral_eq[of s f g] has_integral_eq by blast
lp15@60615
   686
lp15@60615
   687
lemma has_integral_cong:
lp15@60615
   688
  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
lp15@60615
   689
  shows "(f has_integral i) s = (g has_integral i) s"
lp15@60615
   690
  using has_integral_eq[of s f g] has_integral_eq[of s g f] assms
wenzelm@53410
   691
  by auto
wenzelm@53410
   692
lp15@60615
   693
lemma integral_cong:
lp15@60615
   694
  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
lp15@60615
   695
  shows "integral s f = integral s g"
lp15@60615
   696
  unfolding integral_def
lp15@62463
   697
by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)
lp15@60615
   698
lp15@62533
   699
lemma integrable_on_cmult_left_iff [simp]:
lp15@62533
   700
  assumes "c \<noteq> 0"
lp15@62533
   701
  shows "(\<lambda>x. of_real c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
lp15@62533
   702
        (is "?lhs = ?rhs")
lp15@62533
   703
proof
lp15@62533
   704
  assume ?lhs
lp15@62533
   705
  then have "(\<lambda>x. of_real (1 / c) * (of_real c * f x)) integrable_on s"
lp15@62533
   706
    using integrable_cmul[of "\<lambda>x. of_real c * f x" s "1 / of_real c"]
lp15@62533
   707
    by (simp add: scaleR_conv_of_real)
lp15@62533
   708
  then have "(\<lambda>x. (of_real (1 / c) * of_real c * f x)) integrable_on s"
lp15@62533
   709
    by (simp add: algebra_simps)
lp15@62533
   710
  with \<open>c \<noteq> 0\<close> show ?rhs
lp15@62533
   711
    by (metis (no_types, lifting) integrable_eq mult.left_neutral nonzero_divide_eq_eq of_real_1 of_real_mult)
lp15@62533
   712
qed (blast intro: integrable_on_cmult_left)
lp15@62533
   713
lp15@62533
   714
lemma integrable_on_cmult_right:
lp15@62533
   715
  fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
lp15@62533
   716
  assumes "f integrable_on s"
lp15@62533
   717
  shows "(\<lambda>x. f x * of_real c) integrable_on s"
lp15@62533
   718
using integrable_on_cmult_left [OF assms] by (simp add: mult.commute)
lp15@62533
   719
lp15@62533
   720
lemma integrable_on_cmult_right_iff [simp]:
lp15@62533
   721
  fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
lp15@62533
   722
  assumes "c \<noteq> 0"
lp15@62533
   723
  shows "(\<lambda>x. f x * of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
lp15@62533
   724
using integrable_on_cmult_left_iff [OF assms] by (simp add: mult.commute)
lp15@62533
   725
lp15@62533
   726
lemma integrable_on_cdivide:
lp15@62533
   727
  fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
lp15@62533
   728
  assumes "f integrable_on s"
lp15@62533
   729
  shows "(\<lambda>x. f x / of_real c) integrable_on s"
lp15@62533
   730
by (simp add: integrable_on_cmult_right divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
lp15@62533
   731
lp15@62533
   732
lemma integrable_on_cdivide_iff [simp]:
lp15@62533
   733
  fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
lp15@62533
   734
  assumes "c \<noteq> 0"
lp15@62533
   735
  shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
lp15@62533
   736
by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
lp15@62533
   737
hoelzl@63944
   738
lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
hoelzl@63944
   739
  unfolding has_integral_cbox
hoelzl@63944
   740
  using eventually_division_filter_tagged_division[of "cbox a b"]
nipkow@64267
   741
  by (subst tendsto_cong[where g="\<lambda>_. 0"]) (auto elim: eventually_mono intro: sum_content_null)
hoelzl@63944
   742
hoelzl@63944
   743
lemma has_integral_null_real [intro]: "content {a .. b::real} = 0 \<Longrightarrow> (f has_integral 0) {a .. b}"
hoelzl@63944
   744
  by (metis box_real(2) has_integral_null)
immler@56188
   745
immler@56188
   746
lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0"
lp15@60396
   747
  by (auto simp add: has_integral_null dest!: integral_unique)
wenzelm@53410
   748
lp15@60615
   749
lemma integral_null [simp]: "content (cbox a b) = 0 \<Longrightarrow> integral (cbox a b) f = 0"
lp15@60396
   750
  by (metis has_integral_null integral_unique)
wenzelm@53410
   751
lp15@60615
   752
lemma integrable_on_null [intro]: "content (cbox a b) = 0 \<Longrightarrow> f integrable_on (cbox a b)"
lp15@60615
   753
  by (simp add: has_integral_integrable)
wenzelm@53410
   754
wenzelm@53410
   755
lemma has_integral_empty[intro]: "(f has_integral 0) {}"
lp15@60396
   756
  by (simp add: has_integral_is_0)
wenzelm@53410
   757
wenzelm@53410
   758
lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \<longleftrightarrow> i = 0"
lp15@60396
   759
  by (auto simp add: has_integral_empty has_integral_unique)
wenzelm@53410
   760
wenzelm@53410
   761
lemma integrable_on_empty[intro]: "f integrable_on {}"
wenzelm@53410
   762
  unfolding integrable_on_def by auto
wenzelm@53410
   763
wenzelm@53410
   764
lemma integral_empty[simp]: "integral {} f = 0"
wenzelm@53410
   765
  by (rule integral_unique) (rule has_integral_empty)
wenzelm@53410
   766
wenzelm@53410
   767
lemma has_integral_refl[intro]:
immler@56188
   768
  fixes a :: "'a::euclidean_space"
immler@56188
   769
  shows "(f has_integral 0) (cbox a a)"
wenzelm@53410
   770
    and "(f has_integral 0) {a}"
wenzelm@53410
   771
proof -
immler@56188
   772
  have *: "{a} = cbox a a"
wenzelm@53410
   773
    apply (rule set_eqI)
immler@56188
   774
    unfolding mem_box singleton_iff euclidean_eq_iff[where 'a='a]
wenzelm@53410
   775
    apply safe
wenzelm@53410
   776
    prefer 3
wenzelm@53410
   777
    apply (erule_tac x=b in ballE)
wenzelm@53410
   778
    apply (auto simp add: field_simps)
wenzelm@53410
   779
    done
immler@56188
   780
  show "(f has_integral 0) (cbox a a)" "(f has_integral 0) {a}"
wenzelm@53410
   781
    unfolding *
wenzelm@53410
   782
    apply (rule_tac[!] has_integral_null)
wenzelm@53410
   783
    unfolding content_eq_0_interior
immler@56188
   784
    unfolding interior_cbox
immler@56188
   785
    using box_sing
immler@56188
   786
    apply auto
immler@56188
   787
    done
immler@56188
   788
qed
immler@56188
   789
immler@56188
   790
lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
wenzelm@53410
   791
  unfolding integrable_on_def by auto
wenzelm@53410
   792
paulson@60762
   793
lemma integral_refl [simp]: "integral (cbox a a) f = 0"
wenzelm@53410
   794
  by (rule integral_unique) auto
wenzelm@53410
   795
paulson@60762
   796
lemma integral_singleton [simp]: "integral {a} f = 0"
paulson@60762
   797
  by auto
paulson@60762
   798
immler@61915
   799
lemma integral_blinfun_apply:
immler@61915
   800
  assumes "f integrable_on s"
immler@61915
   801
  shows "integral s (\<lambda>x. blinfun_apply h (f x)) = blinfun_apply h (integral s f)"
immler@61915
   802
  by (subst integral_linear[symmetric, OF assms blinfun.bounded_linear_right]) (simp add: o_def)
immler@61915
   803
immler@61915
   804
lemma blinfun_apply_integral:
immler@61915
   805
  assumes "f integrable_on s"
immler@61915
   806
  shows "blinfun_apply (integral s f) x = integral s (\<lambda>y. blinfun_apply (f y) x)"
immler@61915
   807
  by (metis (no_types, lifting) assms blinfun.prod_left.rep_eq integral_blinfun_apply integral_cong)
immler@61915
   808
eberlm@63295
   809
lemma has_integral_componentwise_iff:
eberlm@63295
   810
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
eberlm@63295
   811
  shows "(f has_integral y) A \<longleftrightarrow> (\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
eberlm@63295
   812
proof safe
eberlm@63295
   813
  fix b :: 'b assume "(f has_integral y) A"
lp15@63938
   814
  from has_integral_linear[OF this(1) bounded_linear_inner_left, of b]
eberlm@63295
   815
    show "((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A" by (simp add: o_def)
eberlm@63295
   816
next
eberlm@63295
   817
  assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
eberlm@63295
   818
  hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral ((y \<bullet> b) *\<^sub>R b)) A"
eberlm@63295
   819
    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
eberlm@63295
   820
  hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. (y \<bullet> b) *\<^sub>R b)) A"
nipkow@64267
   821
    by (intro has_integral_sum) (simp_all add: o_def)
eberlm@63295
   822
  thus "(f has_integral y) A" by (simp add: euclidean_representation)
eberlm@63295
   823
qed
eberlm@63295
   824
eberlm@63295
   825
lemma has_integral_componentwise:
eberlm@63295
   826
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
eberlm@63295
   827
  shows "(\<And>b. b \<in> Basis \<Longrightarrow> ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A) \<Longrightarrow> (f has_integral y) A"
eberlm@63295
   828
  by (subst has_integral_componentwise_iff) blast
eberlm@63295
   829
eberlm@63295
   830
lemma integrable_componentwise_iff:
eberlm@63295
   831
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
eberlm@63295
   832
  shows "f integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)"
eberlm@63295
   833
proof
eberlm@63295
   834
  assume "f integrable_on A"
eberlm@63295
   835
  then obtain y where "(f has_integral y) A" by (auto simp: integrable_on_def)
eberlm@63295
   836
  hence "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
eberlm@63295
   837
    by (subst (asm) has_integral_componentwise_iff)
eberlm@63295
   838
  thus "(\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)" by (auto simp: integrable_on_def)
eberlm@63295
   839
next
eberlm@63295
   840
  assume "(\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)"
eberlm@63295
   841
  then obtain y where "\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral y b) A"
eberlm@63295
   842
    unfolding integrable_on_def by (subst (asm) bchoice_iff) blast
eberlm@63295
   843
  hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral (y b *\<^sub>R b)) A"
eberlm@63295
   844
    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
eberlm@63295
   845
  hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. y b *\<^sub>R b)) A"
nipkow@64267
   846
    by (intro has_integral_sum) (simp_all add: o_def)
eberlm@63295
   847
  thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation)
eberlm@63295
   848
qed
eberlm@63295
   849
eberlm@63295
   850
lemma integrable_componentwise:
eberlm@63295
   851
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
eberlm@63295
   852
  shows "(\<And>b. b \<in> Basis \<Longrightarrow> (\<lambda>x. f x \<bullet> b) integrable_on A) \<Longrightarrow> f integrable_on A"
eberlm@63295
   853
  by (subst integrable_componentwise_iff) blast
eberlm@63295
   854
eberlm@63295
   855
lemma integral_componentwise:
eberlm@63295
   856
  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
eberlm@63295
   857
  assumes "f integrable_on A"
eberlm@63295
   858
  shows "integral A f = (\<Sum>b\<in>Basis. integral A (\<lambda>x. (f x \<bullet> b) *\<^sub>R b))"
eberlm@63295
   859
proof -
eberlm@63295
   860
  from assms have integrable: "\<forall>b\<in>Basis. (\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. (f x \<bullet> b)) integrable_on A"
eberlm@63295
   861
    by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI)
eberlm@63295
   862
       (simp_all add: bounded_linear_scaleR_left)
eberlm@63295
   863
  have "integral A f = integral A (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b)"
eberlm@63295
   864
    by (simp add: euclidean_representation)
eberlm@63295
   865
  also from integrable have "\<dots> = (\<Sum>a\<in>Basis. integral A (\<lambda>x. (f x \<bullet> a) *\<^sub>R a))"
nipkow@64267
   866
    by (subst integral_sum) (simp_all add: o_def)
eberlm@63295
   867
  finally show ?thesis .
eberlm@63295
   868
qed
eberlm@63295
   869
eberlm@63295
   870
lemma integrable_component:
eberlm@63295
   871
  "f integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (y :: 'b :: euclidean_space)) integrable_on A"
lp15@63938
   872
  by (drule integrable_linear[OF _ bounded_linear_inner_left[of y]]) (simp add: o_def)
eberlm@63295
   873
eberlm@63295
   874
himmelma@35172
   875
wenzelm@60420
   876
subsection \<open>Cauchy-type criterion for integrability.\<close>
himmelma@35172
   877
hoelzl@37489
   878
(* XXXXXXX *)
wenzelm@53442
   879
lemma integrable_cauchy:
immler@56188
   880
  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
immler@56188
   881
  shows "f integrable_on cbox a b \<longleftrightarrow>
hoelzl@63944
   882
    (\<forall>e>0. \<exists>d. gauge d \<and>
immler@56188
   883
      (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<and> d fine p1 \<and>
immler@56188
   884
        p2 tagged_division_of (cbox a b) \<and> d fine p2 \<longrightarrow>
hoelzl@63944
   885
        norm ((\<Sum>(x,k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x,k)\<in>p2. content k *\<^sub>R f x)) < e))"
wenzelm@53442
   886
  (is "?l = (\<forall>e>0. \<exists>d. ?P e d)")
wenzelm@53442
   887
proof
wenzelm@53442
   888
  assume ?l
himmelma@35172
   889
  then guess y unfolding integrable_on_def has_integral .. note y=this
wenzelm@53442
   890
  show "\<forall>e>0. \<exists>d. ?P e d"
wenzelm@61166
   891
  proof (clarify, goal_cases)
wenzelm@61165
   892
    case (1 e)
wenzelm@53442
   893
    then have "e/2 > 0" by auto
wenzelm@53494
   894
    then guess d
wenzelm@53494
   895
      apply -
wenzelm@53494
   896
      apply (drule y[rule_format])
wenzelm@53494
   897
      apply (elim exE conjE)
wenzelm@53494
   898
      done
wenzelm@53494
   899
    note d=this[rule_format]
wenzelm@53442
   900
    show ?case
lp15@60396
   901
    proof (rule_tac x=d in exI, clarsimp simp: d)
wenzelm@53442
   902
      fix p1 p2
immler@56188
   903
      assume as: "p1 tagged_division_of (cbox a b)" "d fine p1"
lp15@60396
   904
                 "p2 tagged_division_of (cbox a b)" "d fine p2"
himmelma@35172
   905
      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
wenzelm@53442
   906
        apply (rule dist_triangle_half_l[where y=y,unfolded dist_norm])
himmelma@35172
   907
        using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .
wenzelm@53442
   908
    qed
wenzelm@53442
   909
  qed
wenzelm@53442
   910
next
wenzelm@53442
   911
  assume "\<forall>e>0. \<exists>d. ?P e d"
lp15@60487
   912
  then have "\<forall>n::nat. \<exists>d. ?P (inverse(of_nat (n + 1))) d"
wenzelm@53442
   913
    by auto
himmelma@35172
   914
  from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
wenzelm@53442
   915
  have "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})"
wenzelm@53442
   916
    apply (rule gauge_inters)
wenzelm@53442
   917
    using d(1)
wenzelm@53442
   918
    apply auto
wenzelm@53442
   919
    done
immler@56188
   920
  then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p"
lp15@60425
   921
    by (meson fine_division_exists)
himmelma@35172
   922
  from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]]
wenzelm@53442
   923
  have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
wenzelm@53442
   924
    using p(2) unfolding fine_inters by auto
nipkow@64267
   925
  have "Cauchy (\<lambda>n. sum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
wenzelm@61166
   926
  proof (rule CauchyI, goal_cases)
wenzelm@61165
   927
    case (1 e)
lp15@62623
   928
    then guess N unfolding real_arch_inverse[of e] .. note N=this
wenzelm@53442
   929
    show ?case
wenzelm@53442
   930
      apply (rule_tac x=N in exI)
lp15@60425
   931
    proof clarify
wenzelm@53442
   932
      fix m n
wenzelm@53442
   933
      assume mn: "N \<le> m" "N \<le> n"
wenzelm@53442
   934
      have *: "N = (N - 1) + 1" using N by auto
himmelma@35172
   935
      show "norm ((\<Sum>(x, k)\<in>p m. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p n. content k *\<^sub>R f x)) < e"
wenzelm@53442
   936
        apply (rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]])
wenzelm@53442
   937
        apply(subst *)
lp15@61609
   938
        using dp p(1) mn d(2) by auto
wenzelm@53442
   939
    qed
wenzelm@53442
   940
  qed
lp15@64287
   941
  then guess y unfolding convergent_eq_Cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
wenzelm@53442
   942
  show ?l
wenzelm@53442
   943
    unfolding integrable_on_def has_integral
lp15@60425
   944
  proof (rule_tac x=y in exI, clarify)
wenzelm@53442
   945
    fix e :: real
wenzelm@53442
   946
    assume "e>0"
lp15@60615
   947
    then have *:"e/2 > 0" by auto
lp15@62623
   948
    then guess N1 unfolding real_arch_inverse[of "e/2"] .. note N1=this
wenzelm@53442
   949
    then have N1': "N1 = N1 - 1 + 1"
wenzelm@53442
   950
      by auto
himmelma@35172
   951
    guess N2 using y[OF *] .. note N2=this
lp15@60425
   952
    have "gauge (d (N1 + N2))"
lp15@60425
   953
      using d by auto
lp15@60425
   954
    moreover
lp15@60425
   955
    {
wenzelm@53442
   956
      fix q
immler@56188
   957
      assume as: "q tagged_division_of (cbox a b)" "d (N1 + N2) fine q"
lp15@60487
   958
      have *: "inverse (of_nat (N1 + N2 + 1)) < e / 2"
wenzelm@53442
   959
        apply (rule less_trans)
wenzelm@53442
   960
        using N1
wenzelm@53442
   961
        apply auto
wenzelm@53442
   962
        done
lp15@60425
   963
      have "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e"
wenzelm@53442
   964
        apply (rule norm_triangle_half_r)
wenzelm@53442
   965
        apply (rule less_trans[OF _ *])
wenzelm@53442
   966
        apply (subst N1', rule d(2)[of "p (N1+N2)"])
lp15@60615
   967
        using N1' as(1) as(2) dp
wenzelm@61222
   968
        apply (simp add: \<open>\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x\<close>)
lp15@60425
   969
        using N2 le_add2 by blast
lp15@60425
   970
    }
lp15@60425
   971
    ultimately show "\<exists>d. gauge d \<and>
lp15@60425
   972
      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
lp15@60425
   973
        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e)"
lp15@60425
   974
      by (rule_tac x="d (N1 + N2)" in exI) auto
wenzelm@53442
   975
  qed
wenzelm@53442
   976
qed
wenzelm@53442
   977
himmelma@35172
   978
wenzelm@60420
   979
subsection \<open>Additivity of integral on abutting intervals.\<close>
himmelma@35172
   980
hoelzl@63957
   981
lemma tagged_division_split_left_inj_content:
lp15@60425
   982
  assumes d: "d tagged_division_of i"
hoelzl@63957
   983
    and "(x1, k1) \<in> d" "(x2, k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}" "k \<in> Basis"
wenzelm@53443
   984
  shows "content (k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
wenzelm@53443
   985
proof -
hoelzl@63957
   986
  from tagged_division_ofD(4)[OF d \<open>(x1, k1) \<in> d\<close>] obtain a b where k1: "k1 = cbox a b"
hoelzl@63957
   987
    by auto
wenzelm@53443
   988
  show ?thesis
hoelzl@63957
   989
    unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
hoelzl@63957
   990
    unfolding content_eq_0_interior
hoelzl@63957
   991
    unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
hoelzl@63957
   992
    by (rule tagged_division_split_left_inj[OF assms])
wenzelm@53443
   993
qed
wenzelm@53443
   994
hoelzl@63957
   995
lemma tagged_division_split_right_inj_content:
lp15@60425
   996
  assumes d: "d tagged_division_of i"
hoelzl@63957
   997
    and "(x1, k1) \<in> d" "(x2, k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}" "k \<in> Basis"
wenzelm@53494
   998
  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
wenzelm@53443
   999
proof -
hoelzl@63957
  1000
  from tagged_division_ofD(4)[OF d \<open>(x1, k1) \<in> d\<close>] obtain a b where k1: "k1 = cbox a b"
hoelzl@63957
  1001
    by auto
wenzelm@53443
  1002
  show ?thesis
hoelzl@63957
  1003
    unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
hoelzl@63957
  1004
    unfolding content_eq_0_interior
hoelzl@63957
  1005
    unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
hoelzl@63957
  1006
    by (rule tagged_division_split_right_inj[OF assms])
wenzelm@53443
  1007
qed
himmelma@35172
  1008
wenzelm@53468
  1009
lemma has_integral_split:
immler@56188
  1010
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@60435
  1011
  assumes fi: "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
lp15@60435
  1012
      and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
lp15@60435
  1013
      and k: "k \<in> Basis"
immler@56188
  1014
  shows "(f has_integral (i + j)) (cbox a b)"
wenzelm@61166
  1015
proof (unfold has_integral, rule, rule, goal_cases)
wenzelm@61165
  1016
  case (1 e)
wenzelm@53468
  1017
  then have e: "e/2 > 0"
wenzelm@53468
  1018
    by auto
lp15@60615
  1019
    obtain d1
lp15@60435
  1020
    where d1: "gauge d1"
lp15@60615
  1021
      and d1norm:
lp15@60435
  1022
        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c};
lp15@60435
  1023
               d1 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - i) < e / 2"
lp15@60435
  1024
       apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
lp15@60435
  1025
       apply (simp add: interval_split[symmetric] k)
lp15@60435
  1026
       done
lp15@60615
  1027
    obtain d2
lp15@60435
  1028
    where d2: "gauge d2"
lp15@60615
  1029
      and d2norm:
lp15@60435
  1030
        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k};
lp15@60435
  1031
               d2 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e / 2"
lp15@60435
  1032
       apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
lp15@60435
  1033
       apply (simp add: interval_split[symmetric] k)
lp15@60435
  1034
       done
wenzelm@61945
  1035
  let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x \<bar>x\<bullet>k - c\<bar> \<inter> d1 x \<inter> d2 x"
lp15@60440
  1036
  have "gauge ?d"
lp15@60440
  1037
    using d1 d2 unfolding gauge_def by auto
lp15@60440
  1038
  then show ?case
lp15@60440
  1039
  proof (rule_tac x="?d" in exI, safe)
wenzelm@53468
  1040
    fix p
immler@56188
  1041
    assume "p tagged_division_of (cbox a b)" "?d fine p"
wenzelm@53494
  1042
    note p = this tagged_division_ofD[OF this(1)]
lp15@60435
  1043
    have xk_le_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
lp15@60435
  1044
    proof -
lp15@60435
  1045
      fix x kk
lp15@60440
  1046
      assume as: "(x, kk) \<in> p" and kk: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
lp15@60435
  1047
      show "x\<bullet>k \<le> c"
lp15@60435
  1048
      proof (rule ccontr)
lp15@60435
  1049
        assume **: "\<not> ?thesis"
lp15@60435
  1050
        from this[unfolded not_le]
lp15@60435
  1051
        have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
lp15@60440
  1052
          using p(2)[unfolded fine_def, rule_format,OF as] by auto
lp15@60440
  1053
        with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
lp15@60435
  1054
          by blast
lp15@60615
  1055
        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
lp15@60435
  1056
          using Basis_le_norm[OF k, of "x - y"]
lp15@60440
  1057
          by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
lp15@60440
  1058
        with y show False
lp15@60440
  1059
          using ** by (auto simp add: field_simps)
lp15@60615
  1060
      qed
lp15@60435
  1061
    qed
lp15@60440
  1062
    have xk_ge_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
wenzelm@53468
  1063
    proof -
wenzelm@53468
  1064
      fix x kk
lp15@60440
  1065
      assume as: "(x, kk) \<in> p" and kk: "kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
lp15@60435
  1066
      show "x\<bullet>k \<ge> c"
lp15@60435
  1067
      proof (rule ccontr)
lp15@60435
  1068
        assume **: "\<not> ?thesis"
lp15@60435
  1069
        from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
lp15@60435
  1070
          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
lp15@60440
  1071
        with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
lp15@60435
  1072
          by blast
lp15@60615
  1073
        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
lp15@60435
  1074
          using Basis_le_norm[OF k, of "x - y"]
lp15@60440
  1075
          by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
lp15@60440
  1076
        with y show False
lp15@60440
  1077
          using ** by (auto simp add: field_simps)
lp15@60435
  1078
      qed
wenzelm@53468
  1079
    qed
wenzelm@53468
  1080
wenzelm@53468
  1081
    have lem1: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
lp15@60615
  1082
                         (\<forall>x k. P x k \<longrightarrow> Q x (f k))"
lp15@60440
  1083
      by auto
hoelzl@63957
  1084
    have fin_finite: "finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
hoelzl@63957
  1085
      if "finite s" for s and f :: "'a set \<Rightarrow> 'a set" and P :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"
wenzelm@53468
  1086
    proof -
wenzelm@61165
  1087
      from that have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
lp15@60425
  1088
        by auto
wenzelm@61165
  1089
      then show ?thesis
lp15@60425
  1090
        by (rule rev_finite_subset) auto
wenzelm@53468
  1091
    qed
lp15@60435
  1092
    { fix g :: "'a set \<Rightarrow> 'a set"
wenzelm@53468
  1093
      fix i :: "'a \<times> 'a set"
wenzelm@53468
  1094
      assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
wenzelm@53468
  1095
      then obtain x k where xk:
lp15@60435
  1096
              "i = (x, g k)"  "(x, k) \<in> p"
lp15@60435
  1097
              "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
lp15@60435
  1098
          by auto
wenzelm@53468
  1099
      have "content (g k) = 0"
wenzelm@53468
  1100
        using xk using content_empty by auto
lp15@60435
  1101
      then have "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
wenzelm@53468
  1102
        unfolding xk split_conv by auto
lp15@60435
  1103
    } note [simp] = this
lp15@60435
  1104
    have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
nipkow@64267
  1105
                  sum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
nipkow@64267
  1106
                  sum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
nipkow@64267
  1107
      by (rule sum.mono_neutral_left) auto
wenzelm@53468
  1108
    let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
lp15@60435
  1109
    have d1_fine: "d1 fine ?M1"
nipkow@62390
  1110
      by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
wenzelm@53468
  1111
    have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2"
lp15@60435
  1112
    proof (rule d1norm [OF tagged_division_ofI d1_fine])
lp15@60435
  1113
      show "finite ?M1"
lp15@60435
  1114
        by (rule fin_finite p(3))+
immler@56188
  1115
      show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = cbox a b \<inter> {x. x\<bullet>k \<le> c}"
wenzelm@53468
  1116
        unfolding p(8)[symmetric] by auto
wenzelm@53468
  1117
      fix x l
wenzelm@53468
  1118
      assume xl: "(x, l) \<in> ?M1"
haftmann@61424
  1119
      then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
immler@56188
  1120
      show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
wenzelm@53468
  1121
        unfolding xl'
wenzelm@53468
  1122
        using p(4-6)[OF xl'(3)] using xl'(4)
lp15@60435
  1123
        using xk_le_c[OF xl'(3-4)] by auto
immler@56188
  1124
      show "\<exists>a b. l = cbox a b"
wenzelm@53468
  1125
        unfolding xl'
wenzelm@53468
  1126
        using p(6)[OF xl'(3)]
wenzelm@53468
  1127
        by (fastforce simp add: interval_split[OF k,where c=c])
wenzelm@53468
  1128
      fix y r
wenzelm@53468
  1129
      let ?goal = "interior l \<inter> interior r = {}"
wenzelm@53468
  1130
      assume yr: "(y, r) \<in> ?M1"
haftmann@61424
  1131
      then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
wenzelm@53468
  1132
      assume as: "(x, l) \<noteq> (y, r)"
wenzelm@53468
  1133
      show "interior l \<inter> interior r = {}"
wenzelm@53468
  1134
      proof (cases "l' = r' \<longrightarrow> x' = y'")
wenzelm@53468
  1135
        case False
wenzelm@53468
  1136
        then show ?thesis
wenzelm@53468
  1137
          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
wenzelm@53468
  1138
      next
wenzelm@53468
  1139
        case True
wenzelm@53468
  1140
        then have "l' \<noteq> r'"
wenzelm@53468
  1141
          using as unfolding xl' yr' by auto
wenzelm@53468
  1142
        then show ?thesis
wenzelm@53468
  1143
          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
himmelma@35172
  1144
      qed
himmelma@35172
  1145
    qed
wenzelm@53468
  1146
    moreover
wenzelm@53399
  1147
    let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
lp15@60435
  1148
    have d2_fine: "d2 fine ?M2"
nipkow@62390
  1149
      by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
wenzelm@53468
  1150
    have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2"
lp15@60435
  1151
    proof (rule d2norm [OF tagged_division_ofI d2_fine])
lp15@60435
  1152
      show "finite ?M2"
lp15@60435
  1153
        by (rule fin_finite p(3))+
immler@56188
  1154
      show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = cbox a b \<inter> {x. x\<bullet>k \<ge> c}"
wenzelm@53468
  1155
        unfolding p(8)[symmetric] by auto
wenzelm@53468
  1156
      fix x l
wenzelm@53468
  1157
      assume xl: "(x, l) \<in> ?M2"
haftmann@61424
  1158
      then guess x' l' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note xl'=this
immler@56188
  1159
      show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
wenzelm@53468
  1160
        unfolding xl'
lp15@60435
  1161
        using p(4-6)[OF xl'(3)] xl'(4) xk_ge_c[OF xl'(3-4)]
wenzelm@53468
  1162
        by auto
immler@56188
  1163
      show "\<exists>a b. l = cbox a b"
wenzelm@53468
  1164
        unfolding xl'
wenzelm@53468
  1165
        using p(6)[OF xl'(3)]
wenzelm@53468
  1166
        by (fastforce simp add: interval_split[OF k, where c=c])
wenzelm@53468
  1167
      fix y r
wenzelm@53468
  1168
      let ?goal = "interior l \<inter> interior r = {}"
wenzelm@53468
  1169
      assume yr: "(y, r) \<in> ?M2"
haftmann@61424
  1170
      then guess y' r' unfolding mem_Collect_eq unfolding prod.inject by (elim exE conjE) note yr'=this
wenzelm@53468
  1171
      assume as: "(x, l) \<noteq> (y, r)"
wenzelm@53468
  1172
      show "interior l \<inter> interior r = {}"
wenzelm@53468
  1173
      proof (cases "l' = r' \<longrightarrow> x' = y'")
wenzelm@53468
  1174
        case False
wenzelm@53468
  1175
        then show ?thesis
wenzelm@53468
  1176
          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
wenzelm@53468
  1177
      next
wenzelm@53468
  1178
        case True
wenzelm@53468
  1179
        then have "l' \<noteq> r'"
wenzelm@53468
  1180
          using as unfolding xl' yr' by auto
wenzelm@53468
  1181
        then show ?thesis
wenzelm@53468
  1182
          using p(7)[OF xl'(3) yr'(3)] using as unfolding xl' yr' by auto
wenzelm@53468
  1183
      qed
wenzelm@53468
  1184
    qed
wenzelm@53468
  1185
    ultimately
himmelma@35172
  1186
    have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
lp15@60425
  1187
      using norm_add_less by blast
wenzelm@53468
  1188
    also {
lp15@60435
  1189
      have eq0: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
wenzelm@53468
  1190
        using scaleR_zero_left by auto
lp15@60435
  1191
      have cont_eq: "\<And>g. (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l)) = (\<lambda>(x,l). content (g l) *\<^sub>R f x)"
lp15@60435
  1192
        by auto
wenzelm@53468
  1193
      have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) =
wenzelm@53468
  1194
        (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)"
wenzelm@53468
  1195
        by auto
hoelzl@50526
  1196
      also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
hoelzl@50526
  1197
        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
wenzelm@53468
  1198
        unfolding lem3[OF p(3)]
nipkow@64267
  1199
        by (subst (1 2) sum.reindex_nontrivial[OF p(3)])
hoelzl@63957
  1200
           (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)]
hoelzl@63957
  1201
                 simp: cont_eq)+
nipkow@64267
  1202
      also note sum.distrib[symmetric]
lp15@60435
  1203
      also have "\<And>x. x \<in> p \<Longrightarrow>
lp15@60435
  1204
                    (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
lp15@60435
  1205
                    (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
lp15@60435
  1206
                    (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
lp15@60435
  1207
      proof clarify
wenzelm@53468
  1208
        fix a b
wenzelm@53468
  1209
        assume "(a, b) \<in> p"
wenzelm@53468
  1210
        from p(6)[OF this] guess u v by (elim exE) note uv=this
wenzelm@53468
  1211
        then show "content (b \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f a + content (b \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f a =
wenzelm@53468
  1212
          content b *\<^sub>R f a"
wenzelm@53468
  1213
          unfolding scaleR_left_distrib[symmetric]
wenzelm@53468
  1214
          unfolding uv content_split[OF k,of u v c]
wenzelm@53468
  1215
          by auto
wenzelm@53468
  1216
      qed
nipkow@64267
  1217
      note sum.cong [OF _ this]
hoelzl@50526
  1218
      finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x \<bullet> k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i +
hoelzl@50526
  1219
        ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x \<bullet> k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}. content k *\<^sub>R f x) - j) =
wenzelm@53468
  1220
        (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)"
wenzelm@53468
  1221
        by auto
wenzelm@53468
  1222
    }
wenzelm@53468
  1223
    finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e"
wenzelm@53468
  1224
      by auto
wenzelm@53468
  1225
  qed
wenzelm@53468
  1226
qed
wenzelm@53468
  1227
himmelma@35172
  1228
wenzelm@60420
  1229
subsection \<open>A sort of converse, integrability on subintervals.\<close>
himmelma@35172
  1230
wenzelm@53494
  1231
lemma has_integral_separate_sides:
immler@56188
  1232
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
immler@56188
  1233
  assumes "(f has_integral i) (cbox a b)"
wenzelm@53494
  1234
    and "e > 0"
wenzelm@53494
  1235
    and k: "k \<in> Basis"
wenzelm@53494
  1236
  obtains d where "gauge d"
immler@56188
  1237
    "\<forall>p1 p2. p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<and> d fine p1 \<and>
immler@56188
  1238
        p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
nipkow@64267
  1239
        norm ((sum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + sum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
wenzelm@53494
  1240
proof -
wenzelm@53494
  1241
  guess d using has_integralD[OF assms(1-2)] . note d=this
lp15@60428
  1242
  { fix p1 p2
immler@56188
  1243
    assume "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
wenzelm@53494
  1244
    note p1=tagged_division_ofD[OF this(1)] this
immler@56188
  1245
    assume "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" "d fine p2"
wenzelm@53494
  1246
    note p2=tagged_division_ofD[OF this(1)] this
himmelma@35172
  1247
    note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this
lp15@60428
  1248
    { fix a b
wenzelm@53494
  1249
      assume ab: "(a, b) \<in> p1 \<inter> p2"
wenzelm@53494
  1250
      have "(a, b) \<in> p1"
wenzelm@53494
  1251
        using ab by auto
lp15@60428
  1252
      with p1 obtain u v where uv: "b = cbox u v" by auto
wenzelm@53494
  1253
      have "b \<subseteq> {x. x\<bullet>k = c}"
wenzelm@53494
  1254
        using ab p1(3)[of a b] p2(3)[of a b] by fastforce
wenzelm@53494
  1255
      moreover
wenzelm@53494
  1256
      have "interior {x::'a. x \<bullet> k = c} = {}"
wenzelm@53494
  1257
      proof (rule ccontr)
wenzelm@53494
  1258
        assume "\<not> ?thesis"
wenzelm@53494
  1259
        then obtain x where x: "x \<in> interior {x::'a. x\<bullet>k = c}"
wenzelm@53494
  1260
          by auto
himmelma@35172
  1261
        then guess e unfolding mem_interior .. note e=this
wenzelm@53494
  1262
        have x: "x\<bullet>k = c"
wenzelm@53494
  1263
          using x interior_subset by fastforce
wenzelm@53494
  1264
        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)"
wenzelm@53494
  1265
          using e k by (auto simp: inner_simps inner_not_same_Basis)
hoelzl@50526
  1266
        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
lp15@60425
  1267
              (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
nipkow@64267
  1268
          using "*" by (blast intro: sum.cong)
wenzelm@53494
  1269
        also have "\<dots> < e"
nipkow@64267
  1270
          apply (subst sum.delta)
wenzelm@53494
  1271
          using e
wenzelm@53494
  1272
          apply auto
wenzelm@53494
  1273
          done
hoelzl@50526
  1274
        finally have "x + (e/2) *\<^sub>R k \<in> ball x e"
hoelzl@50526
  1275
          unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1])
wenzelm@53494
  1276
        then have "x + (e/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
wenzelm@53494
  1277
          using e by auto
wenzelm@53494
  1278
        then show False
wenzelm@53494
  1279
          unfolding mem_Collect_eq using e x k by (auto simp: inner_simps)
wenzelm@53494
  1280
      qed
wenzelm@53494
  1281
      ultimately have "content b = 0"
wenzelm@53494
  1282
        unfolding uv content_eq_0_interior
lp15@60428
  1283
        using interior_mono by blast
lp15@60428
  1284
      then have "content b *\<^sub>R f a = 0"
wenzelm@53494
  1285
        by auto
lp15@60428
  1286
    }
lp15@60428
  1287
    then have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) =
lp15@60428
  1288
               norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
nipkow@64267
  1289
      by (subst sum.union_inter_neutral) (auto simp: p1 p2)
wenzelm@53494
  1290
    also have "\<dots> < e"
wenzelm@53494
  1291
      by (rule k d(2) p12 fine_union p1 p2)+
lp15@60428
  1292
    finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
lp15@60615
  1293
   }
lp15@60428
  1294
  then show ?thesis
lp15@60428
  1295
    by (auto intro: that[of d] d elim: )
wenzelm@53494
  1296
qed
himmelma@35172
  1297
hoelzl@50526
  1298
lemma integrable_split[intro]:
immler@56188
  1299
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
immler@56188
  1300
  assumes "f integrable_on cbox a b"
wenzelm@53494
  1301
    and k: "k \<in> Basis"
immler@56188
  1302
  shows "f integrable_on (cbox a b \<inter> {x. x\<bullet>k \<le> c})" (is ?t1)
immler@56188
  1303
    and "f integrable_on (cbox a b \<inter> {x. x\<bullet>k \<ge> c})" (is ?t2)
wenzelm@53494
  1304
proof -
wenzelm@53494
  1305
  guess y using assms(1) unfolding integrable_on_def .. note y=this
wenzelm@63040
  1306
  define b' where "b' = (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i)*\<^sub>R i)"
wenzelm@63040
  1307
  define a' where "a' = (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i)*\<^sub>R i)"
wenzelm@53494
  1308
  show ?t1 ?t2
wenzelm@53494
  1309
    unfolding interval_split[OF k] integrable_cauchy
wenzelm@53494
  1310
    unfolding interval_split[symmetric,OF k]
wenzelm@53494
  1311
  proof (rule_tac[!] allI impI)+
wenzelm@53494
  1312
    fix e :: real
wenzelm@53494
  1313
    assume "e > 0"
wenzelm@53494
  1314
    then have "e/2>0"
wenzelm@53494
  1315
      by auto
hoelzl@37489
  1316
    from has_integral_separate_sides[OF y this k,of c] guess d . note d=this[rule_format]
immler@56188
  1317
    let ?P = "\<lambda>A. \<exists>d. gauge d \<and> (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<inter> A \<and> d fine p1 \<and>
immler@56188
  1318
      p2 tagged_division_of (cbox a b) \<inter> A \<and> d fine p2 \<longrightarrow>
hoelzl@37489
  1319
      norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e)"
wenzelm@53494
  1320
    show "?P {x. x \<bullet> k \<le> c}"
lp15@60428
  1321
    proof (rule_tac x=d in exI, clarsimp simp add: d)
wenzelm@53494
  1322
      fix p1 p2
lp15@60428
  1323
      assume as: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
lp15@60428
  1324
                 "p2 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p2"
himmelma@35172
  1325
      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
lp15@60428
  1326
      proof (rule fine_division_exists[OF d(1), of a' b] )
lp15@60428
  1327
        fix p
lp15@60428
  1328
        assume "p tagged_division_of cbox a' b" "d fine p"
lp15@60428
  1329
        then show ?thesis
lp15@60428
  1330
          using as norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]]
lp15@60428
  1331
          unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
wenzelm@53494
  1332
          by (auto simp add: algebra_simps)
wenzelm@53494
  1333
      qed
wenzelm@53494
  1334
    qed
wenzelm@53494
  1335
    show "?P {x. x \<bullet> k \<ge> c}"
lp15@60428
  1336
    proof (rule_tac x=d in exI, clarsimp simp add: d)
wenzelm@53494
  1337
      fix p1 p2
lp15@60428
  1338
      assume as: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<ge> c}" "d fine p1"
lp15@60428
  1339
                 "p2 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<ge> c}" "d fine p2"
himmelma@35172
  1340
      show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
lp15@60428
  1341
      proof (rule fine_division_exists[OF d(1), of a b'] )
lp15@60428
  1342
        fix p
lp15@60428
  1343
        assume "p tagged_division_of cbox a b'" "d fine p"
lp15@60428
  1344
        then show ?thesis
lp15@60428
  1345
          using as norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]]
wenzelm@53494
  1346
          unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
wenzelm@53520
  1347
          by (auto simp add: algebra_simps)
wenzelm@53494
  1348
      qed
wenzelm@53494
  1349
    qed
wenzelm@53494
  1350
  qed
wenzelm@53494
  1351
qed
wenzelm@53494
  1352
wenzelm@53494
  1353
lemma operative_integral:
immler@56188
  1354
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
haftmann@63659
  1355
  shows "comm_monoid.operative (lift_option op +) (Some 0)
haftmann@63659
  1356
    (\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
haftmann@63659
  1357
proof -
haftmann@63659
  1358
  interpret comm_monoid "lift_option plus" "Some (0::'b)"
haftmann@63659
  1359
    by (rule comm_monoid_lift_option)
haftmann@63659
  1360
      (rule add.comm_monoid_axioms)
haftmann@63659
  1361
  show ?thesis
haftmann@63659
  1362
  proof (unfold operative_def, safe)
haftmann@63659
  1363
    fix a b c
haftmann@63659
  1364
    fix k :: 'a
haftmann@63659
  1365
    assume k: "k \<in> Basis"
haftmann@63659
  1366
    show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) =
haftmann@63659
  1367
          lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
haftmann@63659
  1368
          (if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
haftmann@63659
  1369
    proof (cases "f integrable_on cbox a b")
haftmann@63659
  1370
      case True
haftmann@63659
  1371
      with k show ?thesis
haftmann@63659
  1372
        apply (simp add: integrable_split)
haftmann@63659
  1373
        apply (rule integral_unique [OF has_integral_split[OF _ _ k]])
lp15@60440
  1374
        apply (auto intro: integrable_integral)
wenzelm@53494
  1375
        done
haftmann@63659
  1376
    next
haftmann@63659
  1377
    case False
haftmann@63659
  1378
      have "\<not> (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
haftmann@63659
  1379
      proof (rule ccontr)
haftmann@63659
  1380
        assume "\<not> ?thesis"
haftmann@63659
  1381
        then have "f integrable_on cbox a b"
haftmann@63659
  1382
          unfolding integrable_on_def
haftmann@63659
  1383
          apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
haftmann@63659
  1384
          apply (rule has_integral_split[OF _ _ k])
haftmann@63659
  1385
          apply (auto intro: integrable_integral)
haftmann@63659
  1386
          done
haftmann@63659
  1387
        then show False
haftmann@63659
  1388
          using False by auto
haftmann@63659
  1389
      qed
haftmann@63659
  1390
      then show ?thesis
wenzelm@53494
  1391
        using False by auto
wenzelm@53494
  1392
    qed
haftmann@63659
  1393
  next
haftmann@63659
  1394
    fix a b :: 'a
hoelzl@63957
  1395
    assume "box a b = {}"
haftmann@63659
  1396
    then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
haftmann@63659
  1397
      using has_integral_null_eq
hoelzl@63957
  1398
      by (auto simp: integrable_on_null content_eq_0_interior)
haftmann@63659
  1399
  qed
wenzelm@53494
  1400
qed
wenzelm@53494
  1401
wenzelm@60420
  1402
subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close>
himmelma@35172
  1403
wenzelm@53494
  1404
lemma dsum_bound:
immler@56188
  1405
  assumes "p division_of (cbox a b)"
wenzelm@53494
  1406
    and "norm c \<le> e"
nipkow@64267
  1407
  shows "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)"
lp15@60467
  1408
proof -
nipkow@64267
  1409
  have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = sum content p"
nipkow@64267
  1410
    apply (rule sum.cong)
lp15@60467
  1411
    using assms
lp15@60467
  1412
    apply simp
lp15@60467
  1413
    apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4))
lp15@60467
  1414
    done
lp15@60467
  1415
  have e: "0 \<le> e"
lp15@60467
  1416
    using assms(2) norm_ge_zero order_trans by blast
nipkow@64267
  1417
  have "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
nipkow@64267
  1418
    using norm_sum by blast
lp15@60467
  1419
  also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
nipkow@64267
  1420
    by (simp add: sum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono sum_nonneg)
lp15@60467
  1421
  also have "... \<le> e * content (cbox a b)"
lp15@60467
  1422
    apply (rule mult_left_mono [OF _ e])
lp15@60467
  1423
    apply (simp add: sumeq)
lp15@60467
  1424
    using additive_content_division assms(1) eq_iff apply blast
lp15@60467
  1425
    done
lp15@60467
  1426
  finally show ?thesis .
lp15@60467
  1427
qed
wenzelm@53494
  1428
wenzelm@53494
  1429
lemma rsum_bound:
lp15@60472
  1430
  assumes p: "p tagged_division_of (cbox a b)"
lp15@60472
  1431
      and "\<forall>x\<in>cbox a b. norm (f x) \<le> e"
nipkow@64267
  1432
    shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content (cbox a b)"
immler@56188
  1433
proof (cases "cbox a b = {}")
lp15@60472
  1434
  case True show ?thesis
lp15@60472
  1435
    using p unfolding True tagged_division_of_trivial by auto
wenzelm@53494
  1436
next
wenzelm@53494
  1437
  case False
lp15@60472
  1438
  then have e: "e \<ge> 0"
lp15@63018
  1439
    by (meson ex_in_conv assms(2) norm_ge_zero order_trans)
nipkow@64267
  1440
  have sum_le: "sum (content \<circ> snd) p \<le> content (cbox a b)"
lp15@60472
  1441
    unfolding additive_content_tagged_division[OF p, symmetric] split_def
lp15@60472
  1442
    by (auto intro: eq_refl)
lp15@60472
  1443
  have con: "\<And>xk. xk \<in> p \<Longrightarrow> 0 \<le> content (snd xk)"
lp15@60472
  1444
    using tagged_division_ofD(4) [OF p] content_pos_le
lp15@60472
  1445
    by force
lp15@60472
  1446
  have norm: "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e"
lp15@60472
  1447
    unfolding fst_conv using tagged_division_ofD(2,3)[OF p] assms
lp15@60472
  1448
    by (metis prod.collapse subset_eq)
nipkow@64267
  1449
  have "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))"
nipkow@64267
  1450
    by (rule norm_sum)
lp15@60472
  1451
  also have "...  \<le> e * content (cbox a b)"
wenzelm@53494
  1452
    unfolding split_def norm_scaleR
nipkow@64267
  1453
    apply (rule order_trans[OF sum_mono])
wenzelm@53494
  1454
    apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e])
lp15@60472
  1455
    apply (metis norm)
nipkow@64267
  1456
    unfolding sum_distrib_right[symmetric]
nipkow@64267
  1457
    using con sum_le
lp15@60472
  1458
    apply (auto simp: mult.commute intro: mult_left_mono [OF _ e])
lp15@60472
  1459
    done
lp15@60472
  1460
  finally show ?thesis .
wenzelm@53494
  1461
qed
himmelma@35172
  1462
himmelma@35172
  1463
lemma rsum_diff_bound:
immler@56188
  1464
  assumes "p tagged_division_of (cbox a b)"
immler@56188
  1465
    and "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e"
nipkow@64267
  1466
  shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - sum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le>
lp15@60472
  1467
         e * content (cbox a b)"
wenzelm@53494
  1468
  apply (rule order_trans[OF _ rsum_bound[OF assms]])
nipkow@64267
  1469
  apply (simp add: split_def scaleR_diff_right sum_subtractf eq_refl)
wenzelm@53494
  1470
  done
wenzelm@53494
  1471
wenzelm@53494
  1472
lemma has_integral_bound:
immler@56188
  1473
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
wenzelm@53494
  1474
  assumes "0 \<le> B"
hoelzl@63944
  1475
      and *: "(f has_integral i) (cbox a b)"
lp15@60472
  1476
      and "\<forall>x\<in>cbox a b. norm (f x) \<le> B"
lp15@60472
  1477
    shows "norm i \<le> B * content (cbox a b)"
lp15@60472
  1478
proof (rule ccontr)
wenzelm@53494
  1479
  assume "\<not> ?thesis"
immler@56188
  1480
  then have *: "norm i - B * content (cbox a b) > 0"
wenzelm@53494
  1481
    by auto
wenzelm@53494
  1482
  from assms(2)[unfolded has_integral,rule_format,OF *]
wenzelm@53494
  1483
  guess d by (elim exE conjE) note d=this[rule_format]
himmelma@35172
  1484
  from fine_division_exists[OF this(1), of a b] guess p . note p=this
wenzelm@53494
  1485
  have *: "\<And>s B. norm s \<le> B \<Longrightarrow> \<not> norm (s - i) < norm i - B"
lp15@60472
  1486
    unfolding not_less
lp15@60472
  1487
    by (metis norm_triangle_sub[of i] add.commute le_less_trans less_diff_eq linorder_not_le norm_minus_commute)
wenzelm@53494
  1488
  show False
wenzelm@53494
  1489
    using d(2)[OF conjI[OF p]] *[OF rsum_bound[OF p(1) assms(3)]] by auto
wenzelm@53494
  1490
qed
wenzelm@53494
  1491
lp15@60615
  1492
corollary has_integral_bound_real:
immler@56188
  1493
  fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
immler@56188
  1494
  assumes "0 \<le> B"
lp15@60472
  1495
      and "(f has_integral i) {a .. b}"
lp15@60472
  1496
      and "\<forall>x\<in>{a .. b}. norm (f x) \<le> B"
lp15@60472
  1497
    shows "norm i \<le> B * content {a .. b}"
lp15@60615
  1498
  by (metis assms box_real(2) has_integral_bound)
lp15@60615
  1499
lp15@60615
  1500
corollary integrable_bound:
lp15@60615
  1501
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@60615
  1502
  assumes "0 \<le> B"
lp15@60615
  1503
      and "f integrable_on (cbox a b)"
lp15@60615
  1504
      and "\<And>x. x\<in>cbox a b \<Longrightarrow> norm (f x) \<le> B"
lp15@60615
  1505
    shows "norm (integral (cbox a b) f) \<le> B * content (cbox a b)"
lp15@60615
  1506
by (metis integrable_integral has_integral_bound assms)
immler@56188
  1507
himmelma@35172
  1508
wenzelm@60420
  1509
subsection \<open>Similar theorems about relationship among components.\<close>
himmelma@35172
  1510
wenzelm@53494
  1511
lemma rsum_component_le:
immler@56188
  1512
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@56188
  1513
  assumes "p tagged_division_of (cbox a b)"
lp15@60472
  1514
      and "\<forall>x\<in>cbox a b. (f x)\<bullet>i \<le> (g x)\<bullet>i"
nipkow@64267
  1515
    shows "(sum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (sum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i"
nipkow@64267
  1516
unfolding inner_sum_left
nipkow@64267
  1517
proof (rule sum_mono, clarify)
wenzelm@53494
  1518
  fix a b
wenzelm@53494
  1519
  assume ab: "(a, b) \<in> p"
lp15@60466
  1520
  note tagged = tagged_division_ofD(2-4)[OF assms(1) ab]
wenzelm@53494
  1521
  from this(3) guess u v by (elim exE) note b=this
wenzelm@53494
  1522
  show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i"
lp15@60472
  1523
    unfolding b inner_simps real_scaleR_def
wenzelm@53494
  1524
    apply (rule mult_left_mono)
lp15@60615
  1525
    using assms(2) tagged
lp15@60472
  1526
    by (auto simp add: content_pos_le)
wenzelm@53494
  1527
qed
himmelma@35172
  1528
hoelzl@50526
  1529
lemma has_integral_component_le:
immler@56188
  1530
  fixes f g :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
hoelzl@50526
  1531
  assumes k: "k \<in> Basis"
wenzelm@53494
  1532
  assumes "(f has_integral i) s" "(g has_integral j) s"
wenzelm@53494
  1533
    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
hoelzl@50526
  1534
  shows "i\<bullet>k \<le> j\<bullet>k"
hoelzl@50348
  1535
proof -
wenzelm@61165
  1536
  have lem: "i\<bullet>k \<le> j\<bullet>k"
wenzelm@61165
  1537
    if f_i: "(f has_integral i) (cbox a b)"
wenzelm@61165
  1538
    and g_j: "(g has_integral j) (cbox a b)"
wenzelm@61165
  1539
    and le: "\<forall>x\<in>cbox a b. (f x)\<bullet>k \<le> (g x)\<bullet>k"
wenzelm@61165
  1540
    for a b i and j :: 'b and f g :: "'a \<Rightarrow> 'b"
hoelzl@50348
  1541
  proof (rule ccontr)
wenzelm@61165
  1542
    assume "\<not> ?thesis"
wenzelm@53494
  1543
    then have *: "0 < (i\<bullet>k - j\<bullet>k) / 3"
wenzelm@53494
  1544
      by auto
wenzelm@61165
  1545
    guess d1 using f_i[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
wenzelm@61165
  1546
    guess d2 using g_j[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
lp15@60615
  1547
    obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p"
lp15@60615
  1548
       using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter
lp15@60615
  1549
       by metis
hoelzl@50526
  1550
    note le_less_trans[OF Basis_le_norm[OF k]]
lp15@60474
  1551
    then have "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
lp15@60474
  1552
              "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
lp15@60474
  1553
      using  k norm_bound_Basis_lt d1 d2 p
lp15@60474
  1554
      by blast+
wenzelm@53494
  1555
    then show False
hoelzl@50526
  1556
      unfolding inner_simps
wenzelm@61165
  1557
      using rsum_component_le[OF p(1) le]
nipkow@62390
  1558
      by (simp add: abs_real_def split: if_split_asm)
wenzelm@53494
  1559
  qed
lp15@60474
  1560
  show ?thesis
lp15@60474
  1561
  proof (cases "\<exists>a b. s = cbox a b")
lp15@60474
  1562
    case True
lp15@60474
  1563
    with lem assms show ?thesis
lp15@60474
  1564
      by auto
lp15@60474
  1565
  next
lp15@60474
  1566
    case False
lp15@60474
  1567
    show ?thesis
lp15@60474
  1568
    proof (rule ccontr)
lp15@60474
  1569
      assume "\<not> i\<bullet>k \<le> j\<bullet>k"
lp15@60474
  1570
      then have ij: "(i\<bullet>k - j\<bullet>k) / 3 > 0"
lp15@60474
  1571
        by auto
lp15@60474
  1572
      note has_integral_altD[OF _ False this]
lp15@60474
  1573
      from this[OF assms(2)] this[OF assms(3)] guess B1 B2 . note B=this[rule_format]
lp15@60474
  1574
      have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
lp15@60474
  1575
        unfolding bounded_Un by(rule conjI bounded_ball)+
lp15@60474
  1576
      from bounded_subset_cbox[OF this] guess a b by (elim exE)
lp15@60474
  1577
      note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
lp15@60474
  1578
      guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
lp15@60474
  1579
      guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
lp15@60474
  1580
      have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
nipkow@62390
  1581
        by (simp add: abs_real_def split: if_split_asm)
lp15@60474
  1582
      note le_less_trans[OF Basis_le_norm[OF k]]
lp15@60474
  1583
      note this[OF w1(2)] this[OF w2(2)]
lp15@60474
  1584
      moreover
lp15@60474
  1585
      have "w1\<bullet>k \<le> w2\<bullet>k"
lp15@60474
  1586
        by (rule lem[OF w1(1) w2(1)]) (simp add: assms(4))
lp15@60474
  1587
      ultimately show False
lp15@60474
  1588
        unfolding inner_simps by(rule *)
lp15@60474
  1589
    qed
lp15@60474
  1590
  qed
hoelzl@50526
  1591
qed
hoelzl@37489
  1592
wenzelm@53494
  1593
lemma integral_component_le:
immler@56188
  1594
  fixes g f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53494
  1595
  assumes "k \<in> Basis"
wenzelm@53494
  1596
    and "f integrable_on s" "g integrable_on s"
wenzelm@53494
  1597
    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
hoelzl@50526
  1598
  shows "(integral s f)\<bullet>k \<le> (integral s g)\<bullet>k"
wenzelm@53494
  1599
  apply (rule has_integral_component_le)
wenzelm@53494
  1600
  using integrable_integral assms
wenzelm@53494
  1601
  apply auto
wenzelm@53494
  1602
  done
wenzelm@53494
  1603
wenzelm@53494
  1604
lemma has_integral_component_nonneg:
immler@56188
  1605
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53494
  1606
  assumes "k \<in> Basis"
wenzelm@53494
  1607
    and "(f has_integral i) s"
wenzelm@53494
  1608
    and "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
wenzelm@53494
  1609
  shows "0 \<le> i\<bullet>k"
wenzelm@53494
  1610
  using has_integral_component_le[OF assms(1) has_integral_0 assms(2)]
wenzelm@53494
  1611
  using assms(3-)
wenzelm@53494
  1612
  by auto
wenzelm@53494
  1613
wenzelm@53494
  1614
lemma integral_component_nonneg:
immler@56188
  1615
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53494
  1616
  assumes "k \<in> Basis"
lp15@62463
  1617
    and  "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
wenzelm@53494
  1618
  shows "0 \<le> (integral s f)\<bullet>k"
lp15@62463
  1619
proof (cases "f integrable_on s")
lp15@62463
  1620
  case True show ?thesis
lp15@62463
  1621
    apply (rule has_integral_component_nonneg)
lp15@62463
  1622
    using assms True
lp15@62463
  1623
    apply auto
lp15@62463
  1624
    done
lp15@62463
  1625
next
lp15@62463
  1626
  case False then show ?thesis by (simp add: not_integrable_integral)
lp15@62463
  1627
qed
wenzelm@53494
  1628
wenzelm@53494
  1629
lemma has_integral_component_neg:
immler@56188
  1630
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
wenzelm@53494
  1631
  assumes "k \<in> Basis"
wenzelm@53494
  1632
    and "(f has_integral i) s"
wenzelm@53494
  1633
    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> 0"
wenzelm@53494
  1634
  shows "i\<bullet>k \<le> 0"
wenzelm@53494
  1635
  using has_integral_component_le[OF assms(1,2) has_integral_0] assms(2-)
wenzelm@53494
  1636
  by auto
hoelzl@50526
  1637
hoelzl@50526
  1638
lemma has_integral_component_lbound:
immler@56188
  1639
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@56188
  1640
  assumes "(f has_integral i) (cbox a b)"
immler@56188
  1641
    and "\<forall>x\<in>cbox a b. B \<le> f(x)\<bullet>k"
wenzelm@53494
  1642
    and "k \<in> Basis"
immler@56188
  1643
  shows "B * content (cbox a b) \<le> i\<bullet>k"
hoelzl@50526
  1644
  using has_integral_component_le[OF assms(3) has_integral_const assms(1),of "(\<Sum>i\<in>Basis. B *\<^sub>R i)::'b"] assms(2-)
wenzelm@53494
  1645
  by (auto simp add: field_simps)
hoelzl@50526
  1646
hoelzl@50526
  1647
lemma has_integral_component_ubound:
immler@56188
  1648
  fixes f::"'a::euclidean_space => 'b::euclidean_space"
immler@56188
  1649
  assumes "(f has_integral i) (cbox a b)"
immler@56188
  1650
    and "\<forall>x\<in>cbox a b. f x\<bullet>k \<le> B"
wenzelm@53494
  1651
    and "k \<in> Basis"
immler@56188
  1652
  shows "i\<bullet>k \<le> B * content (cbox a b)"
wenzelm@53494
  1653
  using has_integral_component_le[OF assms(3,1) has_integral_const, of "\<Sum>i\<in>Basis. B *\<^sub>R i"] assms(2-)
wenzelm@53494
  1654
  by (auto simp add: field_simps)
wenzelm@53494
  1655
wenzelm@53494
  1656
lemma integral_component_lbound:
immler@56188
  1657
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@56188
  1658
  assumes "f integrable_on cbox a b"
immler@56188
  1659
    and "\<forall>x\<in>cbox a b. B \<le> f(x)\<bullet>k"
wenzelm@53494
  1660
    and "k \<in> Basis"
immler@56188
  1661
  shows "B * content (cbox a b) \<le> (integral(cbox a b) f)\<bullet>k"
wenzelm@53494
  1662
  apply (rule has_integral_component_lbound)
wenzelm@53494
  1663
  using assms
wenzelm@53494
  1664
  unfolding has_integral_integral
wenzelm@53494
  1665
  apply auto
wenzelm@53494
  1666
  done
wenzelm@53494
  1667
immler@56190
  1668
lemma integral_component_lbound_real:
immler@56190
  1669
  assumes "f integrable_on {a ::real .. b}"
immler@56190
  1670
    and "\<forall>x\<in>{a .. b}. B \<le> f(x)\<bullet>k"
immler@56190
  1671
    and "k \<in> Basis"
immler@56190
  1672
  shows "B * content {a .. b} \<le> (integral {a .. b} f)\<bullet>k"
immler@56190
  1673
  using assms
immler@56190
  1674
  by (metis box_real(2) integral_component_lbound)
immler@56190
  1675
wenzelm@53494
  1676
lemma integral_component_ubound:
immler@56188
  1677
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
immler@56188
  1678
  assumes "f integrable_on cbox a b"
immler@56188
  1679
    and "\<forall>x\<in>cbox a b. f x\<bullet>k \<le> B"
wenzelm@53494
  1680
    and "k \<in> Basis"
immler@56188
  1681
  shows "(integral (cbox a b) f)\<bullet>k \<le> B * content (cbox a b)"
wenzelm@53494
  1682
  apply (rule has_integral_component_ubound)
wenzelm@53494
  1683
  using assms
wenzelm@53494
  1684
  unfolding has_integral_integral
wenzelm@53494
  1685
  apply auto
wenzelm@53494
  1686
  done
wenzelm@53494
  1687
immler@56190
  1688
lemma integral_component_ubound_real:
immler@56190
  1689
  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
immler@56190
  1690
  assumes "f integrable_on {a .. b}"
immler@56190
  1691
    and "\<forall>x\<in>{a .. b}. f x\<bullet>k \<le> B"
immler@56190
  1692
    and "k \<in> Basis"
immler@56190
  1693
  shows "(integral {a .. b} f)\<bullet>k \<le> B * content {a .. b}"
immler@56190
  1694
  using assms
immler@56190
  1695
  by (metis box_real(2) integral_component_ubound)
himmelma@35172
  1696
wenzelm@60420
  1697
subsection \<open>Uniform limit of integrable functions is integrable.\<close>
himmelma@35172
  1698
lp15@62626
  1699
lemma real_arch_invD:
lp15@62626
  1700
  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
lp15@62626
  1701
  by (subst(asm) real_arch_inverse)
lp15@62626
  1702
wenzelm@53494
  1703
lemma integrable_uniform_limit:
immler@56188
  1704
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
immler@56188
  1705
  assumes "\<forall>e>0. \<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
immler@56188
  1706
  shows "f integrable_on cbox a b"
lp15@60487
  1707
proof (cases "content (cbox a b) > 0")
lp15@60487
  1708
  case False then show ?thesis
wenzelm@53494
  1709
      using has_integral_null
lp15@60487
  1710
      by (simp add: content_lt_nz integrable_on_def)
lp15@60487
  1711
next
lp15@60487
  1712
  case True
wenzelm@53494
  1713
  have *: "\<And>P. \<forall>e>(0::real). P e \<Longrightarrow> \<forall>n::nat. P (inverse (real n + 1))"
wenzelm@53494
  1714
    by auto
himmelma@35172
  1715
  from choice[OF *[OF assms]] guess g .. note g=conjunctD2[OF this[rule_format],rule_format]
lp15@60615
  1716
  from choice[OF allI[OF g(2)[unfolded integrable_on_def], of "\<lambda>x. x"]]
lp15@60487
  1717
  obtain i where i: "\<And>x. (g x has_integral i x) (cbox a b)"
lp15@60487
  1718
      by auto
wenzelm@53494
  1719
  have "Cauchy i"
wenzelm@53494
  1720
    unfolding Cauchy_def
lp15@60487
  1721
  proof clarify
wenzelm@53494
  1722
    fix e :: real
wenzelm@53494
  1723
    assume "e>0"
immler@56188
  1724
    then have "e / 4 / content (cbox a b) > 0"
lp15@60487
  1725
      using True by (auto simp add: field_simps)
lp15@60487
  1726
    then obtain M :: nat
lp15@60487
  1727
         where M: "M \<noteq> 0" "0 < inverse (real_of_nat M)" "inverse (of_nat M) < e / 4 / content (cbox a b)"
lp15@62623
  1728
      by (subst (asm) real_arch_inverse) auto
wenzelm@53494
  1729
    show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (i m) (i n) < e"
lp15@60487
  1730
    proof (rule exI [where x=M], clarify)
lp15@60487
  1731
      fix m n
lp15@60487
  1732
      assume m: "M \<le> m" and n: "M \<le> n"
wenzelm@60420
  1733
      have "e/4>0" using \<open>e>0\<close> by auto
wenzelm@53494
  1734
      note * = i[unfolded has_integral,rule_format,OF this]
wenzelm@53494
  1735
      from *[of m] guess gm by (elim conjE exE) note gm=this[rule_format]
wenzelm@53494
  1736
      from *[of n] guess gn by (elim conjE exE) note gn=this[rule_format]
lp15@60615
  1737
      from fine_division_exists[OF gauge_inter[OF gm(1) gn(1)], of a b]
lp15@60487
  1738
      obtain p where p: "p tagged_division_of cbox a b" "(\<lambda>x. gm x \<inter> gn x) fine p"
lp15@60487
  1739
        by auto
lp15@60487
  1740
      { fix s1 s2 i1 and i2::'b
lp15@60487
  1741
        assume no: "norm(s2 - s1) \<le> e/2" "norm (s1 - i1) < e/4" "norm (s2 - i2) < e/4"
wenzelm@53494
  1742
        have "norm (i1 - i2) \<le> norm (i1 - s1) + norm (s1 - s2) + norm (s2 - i2)"
himmelma@35172
  1743
          using norm_triangle_ineq[of "i1 - s1" "s1 - i2"]
wenzelm@53494
  1744
          using norm_triangle_ineq[of "s1 - s2" "s2 - i2"]
wenzelm@53494
  1745
          by (auto simp add: algebra_simps)
wenzelm@53494
  1746
        also have "\<dots> < e"
lp15@60487
  1747
          using no
wenzelm@53494
  1748
          unfolding norm_minus_commute
wenzelm@53494
  1749
          by (auto simp add: algebra_simps)
lp15@60487
  1750
        finally have "norm (i1 - i2) < e" .
lp15@60487
  1751
      } note triangle3 = this
lp15@60487
  1752
      have finep: "gm fine p" "gn fine p"
lp15@60487
  1753
        using fine_inter p  by auto
lp15@60487
  1754
      { fix x
immler@56188
  1755
        assume x: "x \<in> cbox a b"
wenzelm@53399
  1756
        have "norm (f x - g n x) + norm (f x - g m x) \<le> inverse (real n + 1) + inverse (real m + 1)"
wenzelm@53494
  1757
          using g(1)[OF x, of n] g(1)[OF x, of m] by auto
wenzelm@53494
  1758
        also have "\<dots> \<le> inverse (real M) + inverse (real M)"
wenzelm@53494
  1759
          apply (rule add_mono)
lp15@60487
  1760
          using M(2) m n by auto
wenzelm@53494
  1761
        also have "\<dots> = 2 / real M"
wenzelm@53494
  1762
          unfolding divide_inverse by auto
lp15@60487
  1763
        finally have "norm (g n x - g m x) \<le> 2 / real M"
himmelma@35172
  1764
          using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
wenzelm@53494
  1765
          by (auto simp add: algebra_simps simp add: norm_minus_commute)
lp15@60487
  1766
      } note norm_le = this
lp15@60487
  1767
      have le_e2: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g n x) - (\<Sum>(x, k)\<in>p. content k *\<^sub>R g m x)) \<le> e / 2"
lp15@60487
  1768
        apply (rule order_trans [OF rsum_diff_bound[OF p(1), where e="2 / real M"]])
lp15@60487
  1769
        apply (blast intro: norm_le)
lp15@60487
  1770
        using M True
lp15@60487
  1771
        by (auto simp add: field_simps)
lp15@60487
  1772
      then show "dist (i m) (i n) < e"
lp15@60487
  1773
        unfolding dist_norm
lp15@60487
  1774
        using gm gn p finep
lp15@60487
  1775
        by (auto intro!: triangle3)
lp15@60487
  1776
    qed
lp15@60487
  1777
  qed
wenzelm@61969
  1778
  then obtain s where s: "i \<longlonglongrightarrow> s"
lp15@64287
  1779
    using convergent_eq_Cauchy[symmetric] by blast
wenzelm@53494
  1780
  show ?thesis
lp15@60487
  1781
    unfolding integrable_on_def has_integral
lp15@60487
  1782
  proof (rule_tac x=s in exI, clarify)
lp15@60487
  1783
    fix e::real
lp15@60487
  1784
    assume e: "0 < e"
wenzelm@53494
  1785
    then have *: "e/3 > 0" by auto
lp15@60487
  1786
    then obtain N1 where N1: "\<forall>n\<ge>N1. norm (i n - s) < e / 3"
lp15@60487
  1787
      using LIMSEQ_D [OF s] by metis
lp15@60487
  1788
    from e True have "e / 3 / content (cbox a b) > 0"
wenzelm@53494
  1789
      by (auto simp add: field_simps)
wenzelm@53494
  1790
    from real_arch_invD[OF this] guess N2 by (elim exE conjE) note N2=this
himmelma@35172
  1791
    from i[of "N1 + N2",unfolded has_integral,rule_format,OF *] guess g' .. note g'=conjunctD2[OF this,rule_format]
lp15@60487
  1792
    { fix sf sg i
lp15@60487
  1793
      assume no: "norm (sf - sg) \<le> e / 3"
lp15@60487
  1794
                 "norm(i - s) < e / 3"
lp15@60487
  1795
                 "norm (sg - i) < e / 3"
wenzelm@53494
  1796
      have "norm (sf - s) \<le> norm (sf - sg) + norm (sg - i) + norm (i - s)"
himmelma@35172
  1797
        using norm_triangle_ineq[of "sf - sg" "sg - s"]
wenzelm@53494
  1798
        using norm_triangle_ineq[of "sg -  i" " i - s"]
wenzelm@53494
  1799
        by (auto simp add: algebra_simps)
wenzelm@53494
  1800
      also have "\<dots> < e"
lp15@60487
  1801
        using no
wenzelm@53494
  1802
        unfolding norm_minus_commute
wenzelm@53494
  1803
        by (auto simp add: algebra_simps)
lp15@60487
  1804
      finally have "norm (sf - s) < e" .
lp15@60615
  1805
    } note lem = this
lp15@60487
  1806
    { fix p
immler@56188
  1807
      assume p: "p tagged_division_of (cbox a b) \<and> g' fine p"
lp15@60487
  1808
      then have norm_less: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g (N1 + N2) x) - i (N1 + N2)) < e / 3"
lp15@60487
  1809
        using g' by blast
lp15@60487
  1810
      have "content (cbox a b) < e / 3 * (of_nat N2)"
lp15@60487
  1811
        using N2 unfolding inverse_eq_divide using True by (auto simp add: field_simps)
lp15@60487
  1812
      moreover have "e / 3 * of_nat N2 \<le> e / 3 * (of_nat (N1 + N2) + 1)"
lp15@60487
  1813
        using \<open>e>0\<close> by auto
lp15@60487
  1814
      ultimately have "content (cbox a b) < e / 3 * (of_nat (N1 + N2) + 1)"
lp15@60487
  1815
        by linarith
lp15@60487
  1816
      then have le_e3: "inverse (real (N1 + N2) + 1) * content (cbox a b) \<le> e / 3"
lp15@60487
  1817
        unfolding inverse_eq_divide
lp15@60487
  1818
        by (auto simp add: field_simps)
lp15@60487
  1819
      have ne3: "norm (i (N1 + N2) - s) < e / 3"
lp15@60487
  1820
        using N1 by auto
lp15@60487
  1821
      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - s) < e"
lp15@60487
  1822
        apply (rule lem[OF order_trans [OF _ le_e3] ne3 norm_less])
wenzelm@53494
  1823
        apply (rule rsum_diff_bound[OF p[THEN conjunct1]])
lp15@60487
  1824
        apply (blast intro: g)
lp15@60487
  1825
        done }
lp15@60487
  1826
    then show "\<exists>d. gauge d \<and>
lp15@60487
  1827
             (\<forall>p. p tagged_division_of cbox a b \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - s) < e)"
lp15@60487
  1828
      by (blast intro: g')
wenzelm@53494
  1829
  qed
wenzelm@53494
  1830
qed
wenzelm@53494
  1831
lp15@61806
  1832
lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified]
lp15@61806
  1833
himmelma@35172
  1834
wenzelm@60420
  1835
subsection \<open>Negligible sets.\<close>
himmelma@35172
  1836
immler@56188
  1837
definition "negligible (s:: 'a::euclidean_space set) \<longleftrightarrow>
immler@56188
  1838
  (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) (cbox a b))"
wenzelm@53494
  1839
himmelma@35172
  1840
wenzelm@60420
  1841
subsection \<open>Negligibility of hyperplane.\<close>
himmelma@35172
  1842
wenzelm@53495
  1843
lemma content_doublesplit:
immler@56188
  1844
  fixes a :: "'a::euclidean_space"
wenzelm@53495
  1845
  assumes "0 < e"
wenzelm@53495
  1846
    and k: "k \<in> Basis"
wenzelm@61945
  1847
  obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
hoelzl@63886
  1848
proof cases
hoelzl@63886
  1849
  assume *: "a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j)"
hoelzl@63886
  1850
  define a' where "a' d = (\<Sum>j\<in>Basis. (if j = k then max (a\<bullet>j) (c - d) else a\<bullet>j) *\<^sub>R j)" for d
hoelzl@63886
  1851
  define b' where "b' d = (\<Sum>j\<in>Basis. (if j = k then min (b\<bullet>j) (c + d) else b\<bullet>j) *\<^sub>R j)" for d
hoelzl@63886
  1852
hoelzl@63886
  1853
  have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)"
hoelzl@63886
  1854
    by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
hoelzl@63886
  1855
  also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
hoelzl@63886
  1856
    using k *
nipkow@64272
  1857
    by (intro prod_zero bexI[OF _ k])
nipkow@64267
  1858
       (auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong)
hoelzl@63886
  1859
  also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
hoelzl@63886
  1860
    ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
hoelzl@63886
  1861
  proof (intro tendsto_cong eventually_at_rightI)
hoelzl@63886
  1862
    fix d :: real assume d: "d \<in> {0<..<1}"
hoelzl@63886
  1863
    have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d
hoelzl@63886
  1864
      using * d k by (auto simp add: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
hoelzl@63886
  1865
    moreover have "j \<in> Basis \<Longrightarrow> a' d \<bullet> j \<le> b' d \<bullet> j" for j
hoelzl@63886
  1866
      using * d k by (auto simp: a'_def b'_def)
hoelzl@63886
  1867
    ultimately show "(\<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) = content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})"
hoelzl@63886
  1868
      by simp
hoelzl@63886
  1869
  qed simp
hoelzl@63886
  1870
  finally have "((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" .
hoelzl@63886
  1871
  from order_tendstoD(2)[OF this \<open>0<e\<close>]
hoelzl@63886
  1872
  obtain d' where "0 < d'" and d': "\<And>y. y > 0 \<Longrightarrow> y < d' \<Longrightarrow> content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> y}) < e"
hoelzl@63886
  1873
    by (subst (asm) eventually_at_right[of _ 1]) auto
wenzelm@53495
  1874
  show ?thesis
hoelzl@63886
  1875
    by (rule that[of "d'/2"], insert \<open>0<d'\<close> d'[of "d'/2"], auto)
wenzelm@53495
  1876
next
hoelzl@63886
  1877
  assume *: "\<not> (a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j))"
hoelzl@63886
  1878
  then have "(\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j) \<or> (c < a \<bullet> k \<or> b \<bullet> k < c)"
hoelzl@63886
  1879
    by (auto simp: not_le)
hoelzl@63886
  1880
  show thesis
hoelzl@63886
  1881
  proof cases
hoelzl@63886
  1882
    assume "\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j"
hoelzl@63886
  1883
    then have [simp]: "cbox a b = {}"
hoelzl@63886
  1884
      using box_ne_empty(1)[of a b] by auto
hoelzl@63886
  1885
    show ?thesis
hoelzl@63886
  1886
      by (rule that[of 1]) (simp_all add: \<open>0<e\<close>)
hoelzl@63886
  1887
  next
hoelzl@63886
  1888
    assume "\<not> (\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j)"
hoelzl@63886
  1889
    with * have "c < a \<bullet> k \<or> b \<bullet> k < c"
hoelzl@63886
  1890
      by auto
hoelzl@63886
  1891
    then show thesis
hoelzl@63886
  1892
    proof
hoelzl@63886
  1893
      assume c: "c < a \<bullet> k"
hoelzl@63886
  1894
      moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
hoelzl@63886
  1895
        using k c by (auto simp: cbox_def)
hoelzl@63886
  1896
      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
hoelzl@63886
  1897
        using k by (auto simp: cbox_def)
hoelzl@63886
  1898
      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
wenzelm@53495
  1899
        by auto
lp15@60492
  1900
    next
hoelzl@63886
  1901
      assume c: "b \<bullet> k < c"
hoelzl@63886
  1902
      moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
hoelzl@63886
  1903
        using k c by (auto simp: cbox_def)
hoelzl@63886
  1904
      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
hoelzl@63886
  1905
        using k by (auto simp: cbox_def)
hoelzl@63886
  1906
      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
hoelzl@63886
  1907
        by auto
hoelzl@63886
  1908
    qed
hoelzl@63886
  1909
  qed
hoelzl@63886
  1910
qed
hoelzl@63886
  1911
hoelzl@50526
  1912
wenzelm@53399
  1913
lemma negligible_standard_hyperplane[intro]:
immler@56188
  1914
  fixes k :: "'a::euclidean_space"
hoelzl@50526
  1915
  assumes k: "k \<in> Basis"
wenzelm@53399
  1916
  shows "negligible {x. x\<bullet>k = c}"
wenzelm@53495
  1917
  unfolding negligible_def has_integral
wenzelm@61166
  1918
proof (clarify, goal_cases)
wenzelm@61165
  1919
  case (1 a b e)
wenzelm@61165
  1920
  from this and k obtain d where d: "0 < d" "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
wenzelm@61165
  1921
    by (rule content_doublesplit)
hoelzl@50526
  1922
  let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"
wenzelm@53495
  1923
  show ?case
wenzelm@53495
  1924
    apply (rule_tac x="\<lambda>x. ball x d" in exI)
wenzelm@53495
  1925
    apply rule
wenzelm@53495
  1926
    apply (rule gauge_ball)
wenzelm@53495
  1927
    apply (rule d)
wenzelm@53495
  1928
  proof (rule, rule)
wenzelm@53495
  1929
    fix p
immler@56188
  1930
    assume p: "p tagged_division_of (cbox a b) \<and> (\<lambda>x. ball x d) fine p"
wenzelm@53495
  1931
    have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
wenzelm@61945
  1932
      (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
nipkow@64267
  1933
      apply (rule sum.cong)
haftmann@57418
  1934
      apply (rule refl)
wenzelm@53495
  1935
      unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
wenzelm@53495
  1936
      apply cases
wenzelm@53495
  1937
      apply (rule disjI1)
wenzelm@53495
  1938
      apply assumption
wenzelm@53495
  1939
      apply (rule disjI2)
wenzelm@53495
  1940
    proof -
wenzelm@53495
  1941
      fix x l
wenzelm@53495
  1942
      assume as: "(x, l) \<in> p" "?i x \<noteq> 0"
wenzelm@53495
  1943
      then have xk: "x\<bullet>k = c"
wenzelm@53495
  1944
        unfolding indicator_def
wenzelm@53495
  1945
        apply -
wenzelm@53495
  1946
        apply (rule ccontr)
wenzelm@53495
  1947
        apply auto
wenzelm@53495
  1948
        done
wenzelm@53495
  1949
      show "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
wenzelm@53495
  1950
        apply (rule arg_cong[where f=content])
wenzelm@53495
  1951
        apply (rule set_eqI)
wenzelm@53495
  1952
        apply rule
wenzelm@53495
  1953
        apply rule
wenzelm@53495
  1954
        unfolding mem_Collect_eq
wenzelm@53495
  1955
      proof -
wenzelm@53495
  1956
        fix y
wenzelm@53495
  1957
        assume y: "y \<in> l"
wenzelm@53495
  1958
        note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
wenzelm@53495
  1959
        note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y]
wenzelm@53495
  1960
        note le_less_trans[OF Basis_le_norm[OF k] this]
wenzelm@53495
  1961
        then show "\<bar>y \<bullet> k - c\<bar> \<le> d"
wenzelm@53495
  1962
          unfolding inner_simps xk by auto
wenzelm@53495
  1963
      qed auto
wenzelm@53495
  1964
    qed
himmelma@35172
  1965
    note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
wenzelm@53495
  1966
    show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
wenzelm@53495
  1967
      unfolding diff_0_right *
wenzelm@53495
  1968
      unfolding real_scaleR_def real_norm_def
wenzelm@53495
  1969
      apply (subst abs_of_nonneg)
nipkow@64267
  1970
      apply (rule sum_nonneg)
wenzelm@53495
  1971
      apply rule
wenzelm@53495
  1972
      unfolding split_paired_all split_conv
wenzelm@53495
  1973
      apply (rule mult_nonneg_nonneg)
wenzelm@53495
  1974
      apply (drule p'(4))
wenzelm@53495
  1975
      apply (erule exE)+
wenzelm@53495
  1976
      apply(rule_tac b=b in back_subst)
wenzelm@53495
  1977
      prefer 2
wenzelm@53495
  1978
      apply (subst(asm) eq_commute)
wenzelm@53495
  1979
      apply assumption
wenzelm@53495
  1980
      apply (subst interval_doublesplit[OF k])
wenzelm@53495
  1981
      apply (rule content_pos_le)
wenzelm@53495
  1982
      apply (rule indicator_pos_le)
wenzelm@53495
  1983
    proof -
wenzelm@53495
  1984
      have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
wenzelm@53495
  1985
        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
nipkow@64267
  1986
        apply (rule sum_mono)
wenzelm@53495
  1987
        unfolding split_paired_all split_conv
wenzelm@53495
  1988
        apply (rule mult_right_le_one_le)
wenzelm@53495
  1989
        apply (drule p'(4))
wenzelm@53495
  1990
        apply (auto simp add:interval_doublesplit[OF k])
wenzelm@53495
  1991
        done
wenzelm@53495
  1992
      also have "\<dots> < e"
nipkow@64267
  1993
      proof (subst sum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
wenzelm@61167
  1994
        case prems: (1 u v)
hoelzl@63957
  1995
        then have *: "content (cbox u v) = 0"
hoelzl@63957
  1996
          unfolding content_eq_0_interior by simp
immler@56188
  1997
        have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
wenzelm@53495
  1998
          unfolding interval_doublesplit[OF k]
wenzelm@53495
  1999
          apply (rule content_subset)
wenzelm@53495
  2000
          unfolding interval_doublesplit[symmetric,OF k]
wenzelm@53495
  2001
          apply auto
wenzelm@53495
  2002
          done
wenzelm@53495
  2003
        then show ?case
hoelzl@63957
  2004
          unfolding * interval_doublesplit[OF k]
hoelzl@50348
  2005
          by (blast intro: antisym)
wenzelm@53495
  2006
      next
hoelzl@63593
  2007
        have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
nipkow@64267
  2008
          sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
nipkow@64267
  2009
        proof (subst (2) sum.reindex_nontrivial)
hoelzl@63593
  2010
          fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
hoelzl@63593
  2011
            "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
hoelzl@63593
  2012
          then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
hoelzl@63593
  2013
            by (auto)
hoelzl@63593
  2014
          from p'(5)[OF \<open>(x', x) \<in> p\<close> \<open>(y', y) \<in> p\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}"
hoelzl@63593
  2015
            by auto
hoelzl@63593
  2016
          moreover have "interior ((x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<subseteq> interior (x \<inter> y)"
hoelzl@63593
  2017
            by (auto intro: interior_mono)
hoelzl@63593
  2018
          ultimately have "interior (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
hoelzl@63593
  2019
            by (auto simp: eq)
hoelzl@63593
  2020
          then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
hoelzl@63593
  2021
            using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
nipkow@64267
  2022
        qed (insert p'(1), auto intro!: sum.mono_neutral_right)
hoelzl@63593
  2023
        also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
hoelzl@63593
  2024
          by simp
hoelzl@63593
  2025
        also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
hoelzl@63593
  2026
          using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]]
hoelzl@63593
  2027
          unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto
hoelzl@63593
  2028
        also have "\<dots> < e"
hoelzl@63593
  2029
          using d(2) by simp
hoelzl@63593
  2030
        finally show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
wenzelm@53495
  2031
      qed
hoelzl@50526
  2032
      finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
wenzelm@53495
  2033
    qed
wenzelm@53495
  2034
  qed
wenzelm@53495
  2035
qed
wenzelm@53495
  2036
himmelma@35172
  2037
himmelma@35172
  2038
wenzelm@60420
  2039
subsection \<open>Hence the main theorem about negligible sets.\<close>
himmelma@35172
  2040
wenzelm@53495
  2041
lemma has_integral_negligible:
immler@56188
  2042
  fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53495
  2043
  assumes "negligible s"
wenzelm@53495
  2044
    and "\<forall>x\<in>(t - s). f x = 0"
himmelma@35172
  2045
  shows "(f has_integral 0) t"
wenzelm@53495
  2046
proof -
immler@56188
  2047
  presume P: "\<And>f::'b::euclidean_space \<Rightarrow> 'a.
immler@56188
  2048
    \<And>a b. \<forall>x. x \<notin> s \<longrightarrow> f x = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
himmelma@35172
  2049
  let ?f = "(\<lambda>x. if x \<in> t then f x else 0)"
wenzelm@53495
  2050
  show ?thesis
wenzelm@53495
  2051
    apply (rule_tac f="?f" in has_integral_eq)
wenzelm@53495
  2052
    unfolding if_P
wenzelm@53495
  2053
    apply (rule refl)
wenzelm@53495
  2054
    apply (subst has_integral_alt)
wenzelm@53495
  2055
    apply cases
wenzelm@53495
  2056
    apply (subst if_P, assumption)
wenzelm@53495
  2057
    unfolding if_not_P
wenzelm@53495
  2058
  proof -
immler@56188
  2059
    assume "\<exists>a b. t = cbox a b"
wenzelm@53495
  2060
    then guess a b apply - by (erule exE)+ note t = this
wenzelm@53495
  2061
    show "(?f has_integral 0) t"
wenzelm@53495
  2062
      unfolding t
wenzelm@53495
  2063
      apply (rule P)
wenzelm@53495
  2064
      using assms(2)
wenzelm@53495
  2065
      unfolding t
wenzelm@53495
  2066
      apply auto
wenzelm@53495
  2067
      done
wenzelm@53495
  2068
  next
immler@56188
  2069
    show "\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
immler@56188
  2070
      (\<exists>z. ((\<lambda>x. if x \<in> t then ?f x else 0) has_integral z) (cbox a b) \<and> norm (z - 0) < e)"
wenzelm@53495
  2071
      apply safe
wenzelm@53495
  2072
      apply (rule_tac x=1 in exI)
wenzelm@53495
  2073
      apply rule
wenzelm@53495
  2074
      apply (rule zero_less_one)
wenzelm@53495
  2075
      apply safe
wenzelm@53495
  2076
      apply (rule_tac x=0 in exI)
wenzelm@53495
  2077
      apply rule
wenzelm@53495
  2078
      apply (rule P)
wenzelm@53495
  2079
      using assms(2)
wenzelm@53495
  2080
      apply auto
wenzelm@53495
  2081
      done
himmelma@35172
  2082
  qed
wenzelm@53495
  2083
next
wenzelm@53495
  2084
  fix f :: "'b \<Rightarrow> 'a"
wenzelm@53495
  2085
  fix a b :: 'b
wenzelm@53495
  2086
  assume assm: "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
immler@56188
  2087
  show "(f has_integral 0) (cbox a b)"
wenzelm@53495
  2088
    unfolding has_integral
wenzelm@61166
  2089
  proof (safe, goal_cases)
wenzelm@61167
  2090
    case prems: (1 e)
wenzelm@53495
  2091
    then have "\<And>n. e / 2 / ((real n+1) * (2 ^ n)) > 0"
wenzelm@53495
  2092
      apply -
wenzelm@53495
  2093
      apply (rule divide_pos_pos)
wenzelm@53495
  2094
      defer
wenzelm@53495
  2095
      apply (rule mult_pos_pos)
wenzelm@53495
  2096
      apply (auto simp add:field_simps)
wenzelm@53495
  2097
      done
wenzelm@53495
  2098
    note assms(1)[unfolded negligible_def has_integral,rule_format,OF this,of a b]
wenzelm@53495
  2099
    note allI[OF this,of "\<lambda>x. x"]
himmelma@35172
  2100
    from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format]]
wenzelm@53495
  2101
    show ?case
wenzelm@53495
  2102
      apply (rule_tac x="\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x" in exI)
wenzelm@53495
  2103
    proof safe
wenzelm@53495
  2104
      show "gauge (\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x)"
wenzelm@53495
  2105
        using d(1) unfolding gauge_def by auto
wenzelm@53495
  2106
      fix p
immler@56188
  2107
      assume as: "p tagged_division_of (cbox a b)" "(\<lambda>x. d (nat \<lfloor>norm (f x)\<rfloor>) x) fine p"
himmelma@35172
  2108
      let ?goal = "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
wenzelm@53495
  2109
      {
wenzelm@53495
  2110
        presume "p \<noteq> {} \<Longrightarrow> ?goal"
wenzelm@53495
  2111
        then show ?goal
wenzelm@53495
  2112
          apply (cases "p = {}")
wenzelm@61167
  2113
          using prems
wenzelm@53495
  2114
          apply auto
wenzelm@53495
  2115
          done
wenzelm@53495
  2116
      }
wenzelm@53495
  2117
      assume as': "p \<noteq> {}"
lp15@61824
  2118
      from real_arch_simple[of "Max((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
wenzelm@53495
  2119
      then have N: "\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N"
lp15@61824
  2120
        by (meson Max_ge as(1) dual_order.trans finite_imageI tagged_division_of_finite)
immler@56188
  2121
      have "\<forall>i. \<exists>q. q tagged_division_of (cbox a b) \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
lp15@61824
  2122
        by (auto intro: tagged_division_finer[OF as(1) d(1)])
himmelma@35172
  2123
      from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
wenzelm@53495
  2124
      have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)"
nipkow@64267
  2125
        apply (rule sum_nonneg)
wenzelm@53495
  2126
        apply safe
wenzelm@53495
  2127
        unfolding real_scaleR_def
wenzelm@53495
  2128
        apply (drule tagged_division_ofD(4)[OF q(1)])
nipkow@56536
  2129
        apply (auto intro: mult_nonneg_nonneg)
wenzelm@53495
  2130
        done
wenzelm@61165
  2131
      have **: "finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
nipkow@64267
  2132
        (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> sum f s \<le> sum g t" for f g s t
nipkow@64267
  2133
        apply (rule sum_le_included[of s t g snd f])
wenzelm@61165
  2134
        prefer 4
wenzelm@61165
  2135
        apply safe
wenzelm@61165
  2136
        apply (erule_tac x=x in ballE)
wenzelm@61165
  2137
        apply (erule exE)
wenzelm@61165
  2138
        apply (rule_tac x="(xa,x)" in bexI)
wenzelm@61165
  2139
        apply auto
wenzelm@61165
  2140
        done
nipkow@64267
  2141
      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> sum (\<lambda>i. (real i + 1) *
nipkow@64267
  2142
        norm (sum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}"
nipkow@64267
  2143
        unfolding real_norm_def sum_distrib_left abs_of_nonneg[OF *] diff_0_right
wenzelm@53495
  2144
        apply (rule order_trans)
nipkow@64267
  2145
        apply (rule norm_sum)
wenzelm@53495
  2146
        apply (subst sum_sum_product)
wenzelm@53495
  2147
        prefer 3
wenzelm@53495
  2148
      proof (rule **, safe)
hoelzl@56193
  2149
        show "finite {(i, j) |i j. i \<in> {..N + 1} \<and> j \<in> q i}"
wenzelm@53495
  2150
          apply (rule finite_product_dependent)
wenzelm@53495
  2151
          using q
wenzelm@53495
  2152
          apply auto
wenzelm@53495
  2153
          done
wenzelm@53495
  2154
        fix i a b
wenzelm@53495
  2155
        assume as'': "(a, b) \<in> q i"
wenzelm@53495
  2156
        show "0 \<le> (real i + 1) * (content b *\<^sub>R indicator s a)"
wenzelm@53495
  2157
          unfolding real_scaleR_def
wenzelm@53495
  2158
          using tagged_division_ofD(4)[OF q(1) as'']
nipkow@56536
  2159
          by (auto intro!: mult_nonneg_nonneg)
wenzelm@53495
  2160
      next
wenzelm@53495
  2161
        fix i :: nat
wenzelm@53495
  2162
        show "finite (q i)"
wenzelm@53495
  2163
          using q by auto
wenzelm@53495
  2164
      next
wenzelm@53495
  2165
        fix x k
wenzelm@53495
  2166
        assume xk: "(x, k) \<in> p"
wenzelm@63040
  2167
        define n where "n = nat \<lfloor>norm (f x)\<rfloor>"
wenzelm@53495
  2168
        have *: "norm (f x) \<in> (\<lambda>(x, k). norm (f x)) ` p"
wenzelm@53495
  2169
          using xk by auto
wenzelm@53495
  2170
        have nfx: "real n \<le> norm (f x)" "norm (f x) \<le> real n + 1"
wenzelm@53495
  2171
          unfolding n_def by auto
wenzelm@53495
  2172
        then have "n \<in> {0..N + 1}"
wenzelm@53495
  2173
          using N[rule_format,OF *] by auto
wenzelm@53495
  2174
        moreover
wenzelm@53495
  2175
        note as(2)[unfolded fine_def,rule_format,OF xk,unfolded split_conv]
wenzelm@53495
  2176
        note q(3)[rule_format,OF xk,unfolded split_conv,rule_format,OF this]
wenzelm@53495
  2177
        note this[unfolded n_def[symmetric]]
wenzelm@53495
  2178
        moreover
wenzelm@53495
  2179
        have "norm (content k *\<^sub>R f x) \<le> (real n + 1) * (content k * indicator s x)"
wenzelm@53495
  2180
        proof (cases "x \<in> s")
wenzelm@53495
  2181
          case False
wenzelm@53495
  2182
          then show ?thesis
wenzelm@53495
  2183
            using assm by auto
wenzelm@53495
  2184
        next
wenzelm@53495
  2185
          case True
wenzelm@53495
  2186
          have *: "content k \<ge> 0"
wenzelm@53495
  2187
            using tagged_division_ofD(4)[OF as(1) xk] by auto
wenzelm@53495
  2188
          moreover
wenzelm@53495
  2189
          have "content k * norm (f x) \<le> content k * (real n + 1)"
wenzelm@53495
  2190
            apply (rule mult_mono)
wenzelm@53495
  2191
            using nfx *
wenzelm@53495
  2192
            apply auto
wenzelm@53495
  2193
            done
wenzelm@53495
  2194
          ultimately
wenzelm@53495
  2195
          show ?thesis
wenzelm@53495
  2196
            unfolding abs_mult
wenzelm@53495
  2197
            using nfx True
wenzelm@53495
  2198
            by (auto simp add: field_simps)
wenzelm@53495
  2199
        qed
hoelzl@56193
  2200
        ultimately show "\<exists>y. (y, x, k) \<in> {(i, j) |i j. i \<in> {..N + 1} \<and> j \<in> q i} \<and> norm (content k *\<^sub>R f x) \<le>
wenzelm@53495
  2201
          (real y + 1) * (content k *\<^sub>R indicator s x)"
wenzelm@53495
  2202
          apply (rule_tac x=n in exI)
wenzelm@53495
  2203
          apply safe
wenzelm@53495
  2204
          apply (rule_tac x=n in exI)
wenzelm@53495
  2205
          apply (rule_tac x="(x,k)" in exI)
wenzelm@53495
  2206
          apply safe
wenzelm@53495
  2207
          apply auto
wenzelm@53495
  2208
          done
wenzelm@53495
  2209
      qed (insert as, auto)
nipkow@64267
  2210
      also have "\<dots> \<le> sum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
nipkow@64267
  2211
      proof (rule sum_mono, goal_cases)
wenzelm@61165
  2212
        case (1 i)
wenzelm@53495
  2213
        then show ?case
haftmann@57512
  2214
          apply (subst mult.commute, subst pos_le_divide_eq[symmetric])
wenzelm@61165
  2215
          using d(2)[rule_format, of "q i" i]
wenzelm@53495
  2216
          using q[rule_format]
wenzelm@53495
  2217
          apply (auto simp add: field_simps)
wenzelm@53495
  2218
          done
wenzelm@53495
  2219
      qed
wenzelm@53495
  2220
      also have "\<dots> < e * inverse 2 * 2"
nipkow@64267
  2221
        unfolding divide_inverse sum_distrib_left[symmetric]
wenzelm@53495
  2222
        apply (rule mult_strict_left_mono)
haftmann@60867
  2223
        unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric]
hoelzl@56193
  2224
        apply (subst geometric_sum)
wenzelm@61167
  2225
        using prems
wenzelm@53495
  2226
        apply auto
wenzelm@53495
  2227
        done
wenzelm@53495
  2228
      finally show "?goal" by auto
wenzelm@53495
  2229
    qed
wenzelm@53495
  2230
  qed
wenzelm@53495
  2231
qed
wenzelm@53495
  2232
wenzelm@53495
  2233
lemma has_integral_spike:
immler@56188
  2234
  fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
wenzelm@53495
  2235
  assumes "negligible s"
wenzelm@53495
  2236
    and "(\<forall>x\<in>(t - s). g x = f x)"
wenzelm@53495
  2237
    and "(f has_integral y) t"
himmelma@35172
  2238
  shows "(g has_integral y) t"
wenzelm@53495
  2239
proof -
wenzelm@53495
  2240
  {
wenzelm@53495
  2241
    fix a b :: 'b
wenzelm@53495
  2242
    fix f g :: "'b \<Rightarrow> 'a"
wenzelm@53495
  2243
    fix y :: 'a
immler@56188
  2244
    assume as: "\<forall>x \<in> cbox a b - s. g x = f x" "(f has_integral y) (cbox a b)"
immler@56188
  2245
    have "((\<lambda>x. f x + (g x - f x)) has_integral (y + 0)) (cbox a b)"
wenzelm@53495
  2246
      apply (rule has_integral_add[OF as(2)])
wenzelm@53495
  2247
      apply (rule has_integral_negligible[OF assms(1)])
wenzelm@53495
  2248
      using as
wenzelm@53495
  2249
      apply auto
wenzelm@53495
  2250
      done
immler@56188
  2251
    then have "(g has_integral y) (cbox a b)"
wenzelm@53495
  2252
      by auto
wenzelm@53495
  2253
  } note * = this
wenzelm@53495
  2254
  show ?thesis
wenzelm@53495
  2255
    apply (subst has_integral_alt)
wenzelm@53495
  2256
    using assms(2-)
wenzelm@53495
  2257
    apply -
wenzelm@53495
  2258
    apply (rule cond_cases)
wenzelm@53495
  2259
    apply safe
wenzelm@53495
  2260
    apply (rule *)
wenzelm@53495
  2261
    apply assumption+
wenzelm@53495
  2262
    apply (subst(asm) has_integral_alt)
wenzelm@53495
  2263
    unfolding if_not_P
wenzelm@53495
  2264
    apply (erule_tac x=e in allE)
wenzelm@53495
  2265
    apply safe
wenzelm@53495
  2266
    apply (rule_tac x=B in exI)
wenzelm@53495
  2267
    apply safe
wenzelm@53495
  2268
    apply (erule_tac x=a in allE)
wenzelm@53495
  2269
    apply (erule_tac x=b in allE)
wenzelm@53495
  2270
    apply safe
wenzelm@53495
  2271
    apply (rule_tac x=z in exI)
wenzelm@53495
  2272
    apply safe
wenzelm@53495
  2273
    apply (rule *[where fa2="\<lambda>x. if x\<in>t then f x else 0"])
wenzelm@53495
  2274
    apply auto
wenzelm@53495
  2275
    done
wenzelm@53495
  2276
qed
himmelma@35172
  2277
himmelma@35172
  2278
lemma has_integral_spike_eq:
wenzelm@53495
  2279
  assumes "negligible s"
wenzelm@53495
  2280
    and "\<forall>x\<in>(t - s). g x = f x"
himmelma@35172
  2281
  shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
wenzelm@53495
  2282
  apply rule
wenzelm@53495
  2283
  apply (rule_tac[!] has_integral_spike[OF assms(1)])
wenzelm@53495
  2284
  using assms(2)
wenzelm@53495
  2285
  apply auto
wenzelm@53495
  2286
  done
wenzelm@53495
  2287
wenzelm@53495
  2288
lemma integrable_spike:
wenzelm@53495
  2289
  assumes "negligible s"
wenzelm@53495
  2290
    and "\<forall>x\<in>(t - s). g x = f x"
wenzelm@53495
  2291
    and "f integrable_on t"
himmelma@35172
  2292
  shows "g integrable_on  t"
wenzelm@53495
  2293
  using assms
wenzelm@53495
  2294
  unfolding integrable_on_def
wenzelm@53495
  2295
  apply -
wenzelm@53495
  2296
  apply (erule exE)
wenzelm@53495
  2297
  apply rule
wenzelm@53495
  2298
  apply (rule has_integral_spike)
wenzelm@53495
  2299
  apply fastforce+
wenzelm@53495
  2300
  done
wenzelm@53495
  2301
wenzelm@53495
  2302
lemma integral_spike:
wenzelm@53495
  2303
  assumes "negligible s"
wenzelm@53495
  2304
    and "\<forall>x\<in>(t - s). g x = f x"
himmelma@35172
  2305
  shows "integral t f = integral t g"
lp15@62463
  2306
  using has_integral_spike_eq[OF assms] by (simp add: integral_def integrable_on_def)
wenzelm@53495
  2307
himmelma@35172
  2308
wenzelm@60420
  2309
subsection \<open>Some other trivialities about negligible sets.\<close>
himmelma@35172
  2310
lp15@63945
  2311
lemma negligible_subset:
lp15@63945
  2312
  assumes "negligible s" "t \<subseteq> s"
wenzelm@53495
  2313
  shows "negligible t"
wenzelm@53495
  2314
  unfolding negligible_def
lp15@63945
  2315
    by (metis (no_types) Diff_iff assms contra_subsetD has_integral_negligible indicator_simps(2))
wenzelm@53495
  2316
wenzelm@53495
  2317
lemma negligible_diff[intro?]:
wenzelm@53495
  2318
  assumes "negligible s"
wenzelm@53495
  2319
  shows "negligible (s - t)"
lp15@63945
  2320
  using assms by (meson Diff_subset negligible_subset)
wenzelm@53495
  2321
lp15@63492
  2322
lemma negligible_Int:
wenzelm@53495
  2323
  assumes "negligible s \<or> negligible t"
wenzelm@53495
  2324
  shows "negligible (s \<inter> t)"
lp15@63945
  2325
  using assms negligible_subset by force
wenzelm@53495
  2326
lp15@63492
  2327
lemma negligible_Un:
wenzelm@53495
  2328
  assumes "negligible s"
wenzelm@53495
  2329
    and "negligible t"
wenzelm@53495
  2330
  shows "negligible (s \<union> t)"
wenzelm@53495
  2331
  unfolding negligible_def
wenzelm@61166
  2332
proof (safe, goal_cases)
wenzelm@61165
  2333
  case (1 a b)
wenzelm@53495
  2334
  note assm = assms[unfolded negligible_def,rule_format,of a b]
wenzelm@53495
  2335
  then show ?case
wenzelm@53495
  2336
    apply (subst has_integral_spike_eq[OF assms(2)])
wenzelm@53495
  2337
    defer
wenzelm@53495
  2338
    apply assumption
wenzelm@53495
  2339
    unfolding indicator_def
wenzelm@53495
  2340
    apply auto
wenzelm@53495
  2341
    done
wenzelm@53495
  2342
qed
wenzelm@53495
  2343
lp15@63492
  2344
lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
hoelzl@63956
  2345
  using negligible_Un negligible_subset by blast
himmelma@35172
  2346
immler@56188
  2347
lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
lp15@63945
  2348
  using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
himmelma@35172
  2349
wenzelm@53495
  2350
lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
wenzelm@53495
  2351
  apply (subst insert_is_Un)
lp15@63492
  2352
  unfolding negligible_Un_eq
wenzelm@53495
  2353
  apply auto
wenzelm@53495
  2354
  done
wenzelm@53495
  2355
paulson@60762
  2356
lemma negligible_empty[iff]: "negligible {}"
lp15@63945
  2357
  using negligible_insert by blast
wenzelm@53495
  2358
wenzelm@53495
  2359
lemma negligible_finite[intro]:
wenzelm@53495
  2360
  assumes "finite s"
wenzelm@53495
  2361
  shows "negligible s"
wenzelm@53495
  2362
  using assms by (induct s) auto
wenzelm@53495
  2363
lp15@63469
  2364
lemma negligible_Union[intro]:
wenzelm@53495
  2365
  assumes "finite s"
wenzelm@53495
  2366
    and "\<forall>t\<in>s. negligible t"
wenzelm@53495
  2367
  shows "negligible(\<Union>s)"
wenzelm@53495
  2368
  using assms by induct auto
wenzelm@53495
  2369
wenzelm@53495
  2370
lemma negligible:
immler@56188
  2371
  "negligible s \<longleftrightarrow> (\<forall>t::('a::euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
wenzelm@53495
  2372
  apply safe
wenzelm@53495
  2373
  defer
wenzelm@53495
  2374
  apply (subst negligible_def)
wenzelm@46905
  2375
proof -
wenzelm@53495
  2376
  fix t :: "'a set"
wenzelm@53495
  2377
  assume as: "negligible s"
wenzelm@53495
  2378
  have *: "(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
wenzelm@46905
  2379
    by auto
wenzelm@46905
  2380
  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
wenzelm@53495
  2381
    apply (subst has_integral_alt)
wenzelm@53495
  2382
    apply cases
wenzelm@53495
  2383
    apply (subst if_P,assumption)
wenzelm@46905
  2384
    unfolding if_not_P
wenzelm@53495
  2385
    apply safe
wenzelm@53495
  2386
    apply (rule as[unfolded negligible_def,rule_format])
wenzelm@53495
  2387
    apply (rule_tac x=1 in exI)