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