src/HOL/Analysis/Interval_Integral.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69683 8b3458ca0762
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Interval_Integral.thy
hoelzl@63329
     2
    Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
hoelzl@59092
     3
hoelzl@59092
     4
Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
hoelzl@59092
     5
*)
hoelzl@59092
     6
immler@69681
     7
theory Interval_Integral (*FIX ME rename? Lebesgue  *)
hoelzl@63941
     8
  imports Equivalence_Lebesgue_Henstock_Integration
hoelzl@59092
     9
begin
hoelzl@59092
    10
immler@69681
    11
lemma continuous_on_vector_derivative:
hoelzl@59092
    12
  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
immler@69681
    13
  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
hoelzl@59092
    14
immler@69681
    15
definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
hoelzl@59092
    16
hoelzl@59092
    17
lemma einterval_eq[simp]:
hoelzl@59092
    18
  shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
hoelzl@59092
    19
    and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}"
hoelzl@59092
    20
    and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}"
hoelzl@59092
    21
    and einterval_eq_UNIV: "einterval (- \<infinity>) \<infinity> = UNIV"
hoelzl@59092
    22
  by (auto simp: einterval_def)
hoelzl@59092
    23
hoelzl@59092
    24
lemma einterval_same: "einterval a a = {}"
lp15@68096
    25
  by (auto simp: einterval_def)
hoelzl@59092
    26
hoelzl@59092
    27
lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b"
hoelzl@59092
    28
  by (simp add: einterval_def)
hoelzl@59092
    29
hoelzl@59092
    30
lemma einterval_nonempty: "a < b \<Longrightarrow> \<exists>c. c \<in> einterval a b"
hoelzl@59092
    31
  by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex)
hoelzl@59092
    32
hoelzl@59092
    33
lemma open_einterval[simp]: "open (einterval a b)"
hoelzl@59092
    34
  by (cases a b rule: ereal2_cases)
hoelzl@59092
    35
     (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros)
hoelzl@59092
    36
hoelzl@59092
    37
lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
hoelzl@59092
    38
  unfolding einterval_def by measurable
hoelzl@59092
    39
immler@69683
    40
subsection \<open>Approximating a (possibly infinite) interval\<close>
hoelzl@59092
    41
hoelzl@59092
    42
lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
hoelzl@59092
    43
 unfolding filterlim_def by (auto intro: le_supI1)
hoelzl@59092
    44
immler@69681
    45
lemma ereal_incseq_approx:
hoelzl@59092
    46
  fixes a b :: ereal
hoelzl@59092
    47
  assumes "a < b"
lp15@68095
    48
  obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
immler@69681
    49
proof (cases b)
hoelzl@59092
    50
  case PInf
wenzelm@61808
    51
  with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
hoelzl@59092
    52
    by (cases a) auto
wenzelm@61969
    53
  moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>"
lp15@68096
    54
    by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
wenzelm@61969
    55
  moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) \<longlonglongrightarrow> \<infinity>"
lp15@68096
    56
    by (simp add: LIMSEQ_Suc_iff Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
hoelzl@59092
    57
  ultimately show thesis
lp15@61609
    58
    by (intro that[of "\<lambda>i. real_of_ereal a + Suc i"])
hoelzl@59092
    59
       (auto simp: incseq_def PInf)
hoelzl@59092
    60
next
hoelzl@59092
    61
  case (real b')
wenzelm@63040
    62
  define d where "d = b' - (if a = -\<infinity> then b' - 1 else real_of_ereal a)"
wenzelm@61808
    63
  with \<open>a < b\<close> have a': "0 < d"
hoelzl@59092
    64
    by (cases a) (auto simp: real)
hoelzl@59092
    65
  moreover
hoelzl@59092
    66
  have "\<And>i r. r < b' \<Longrightarrow> (b' - r) * 1 < (b' - r) * real (Suc (Suc i))"
hoelzl@59092
    67
    by (intro mult_strict_left_mono) auto
wenzelm@61808
    68
  with \<open>a < b\<close> a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
hoelzl@59092
    69
    by (cases a) (auto simp: real d_def field_simps)
lp15@68095
    70
  moreover
lp15@68095
    71
  have "(\<lambda>i. b' - d / real i) \<longlonglongrightarrow> b'"
lp15@68095
    72
    by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1
lp15@68095
    73
              simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
lp15@68095
    74
  then have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
lp15@68095
    75
    by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2])
hoelzl@59092
    76
  ultimately show thesis
hoelzl@59092
    77
    by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
lp15@68096
    78
       (auto simp: real incseq_def intro!: divide_left_mono)
wenzelm@61808
    79
qed (insert \<open>a < b\<close>, auto)
hoelzl@59092
    80
immler@69681
    81
lemma ereal_decseq_approx:
hoelzl@59092
    82
  fixes a b :: ereal
hoelzl@59092
    83
  assumes "a < b"
hoelzl@63329
    84
  obtains X :: "nat \<Rightarrow> real" where
wenzelm@61969
    85
    "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
immler@69681
    86
proof -
wenzelm@61808
    87
  have "-b < -a" using \<open>a < b\<close> by simp
hoelzl@59092
    88
  from ereal_incseq_approx[OF this] guess X .
hoelzl@59092
    89
  then show thesis
hoelzl@59092
    90
    apply (intro that[of "\<lambda>i. - X i"])
nipkow@68403
    91
    apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
hoelzl@59092
    92
    apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
hoelzl@59092
    93
    done
hoelzl@59092
    94
qed
hoelzl@59092
    95
immler@69681
    96
proposition einterval_Icc_approximation:
hoelzl@59092
    97
  fixes a b :: ereal
hoelzl@59092
    98
  assumes "a < b"
hoelzl@63329
    99
  obtains u l :: "nat \<Rightarrow> real" where
hoelzl@59092
   100
    "einterval a b = (\<Union>i. {l i .. u i})"
hoelzl@59092
   101
    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
wenzelm@61969
   102
    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
immler@69681
   103
proof -
wenzelm@61808
   104
  from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
wenzelm@61808
   105
  from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
wenzelm@61808
   106
  from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
wenzelm@61808
   107
  { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
hoelzl@59092
   108
  have "einterval a b = (\<Union>i. {l i .. u i})"
hoelzl@59092
   109
  proof (auto simp: einterval_iff)
hoelzl@59092
   110
    fix x assume "a < ereal x" "ereal x < b"
hoelzl@59092
   111
    have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially"
wenzelm@61808
   112
      using l(4) \<open>a < ereal x\<close> by (rule order_tendstoD)
hoelzl@63329
   113
    moreover
hoelzl@59092
   114
    have "eventually (\<lambda>i. ereal x < ereal (u i)) sequentially"
wenzelm@61808
   115
      using u(4) \<open>ereal x< b\<close> by (rule order_tendstoD)
hoelzl@59092
   116
    ultimately have "eventually (\<lambda>i. l i < x \<and> x < u i) sequentially"
hoelzl@59092
   117
      by eventually_elim auto
hoelzl@59092
   118
    then show "\<exists>i. l i \<le> x \<and> x \<le> u i"
hoelzl@59092
   119
      by (auto intro: less_imp_le simp: eventually_sequentially)
hoelzl@59092
   120
  next
hoelzl@63329
   121
    fix x i assume "l i \<le> x" "x \<le> u i"
wenzelm@61808
   122
    with \<open>a < ereal (l i)\<close> \<open>ereal (u i) < b\<close>
hoelzl@59092
   123
    show "a < ereal x" "ereal x < b"
nipkow@68403
   124
      by (auto simp flip: ereal_less_eq(3))
hoelzl@59092
   125
  qed
hoelzl@59092
   126
  show thesis
hoelzl@59092
   127
    by (intro that) fact+
hoelzl@59092
   128
qed
hoelzl@59092
   129
hoelzl@63329
   130
(* TODO: in this definition, it would be more natural if einterval a b included a and b when
hoelzl@59092
   131
   they are real. *)
ak2110@69173
   132
definition%important interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where
hoelzl@59092
   133
  "interval_lebesgue_integral M a b f =
hoelzl@59092
   134
    (if a \<le> b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"
hoelzl@59092
   135
hoelzl@59092
   136
syntax
hoelzl@59092
   137
  "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
hoelzl@59092
   138
  ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
hoelzl@59092
   139
hoelzl@59092
   140
translations
hoelzl@59092
   141
  "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
hoelzl@59092
   142
ak2110@69173
   143
definition%important interval_lebesgue_integrable :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a::{banach, second_countable_topology}) \<Rightarrow> bool" where
hoelzl@59092
   144
  "interval_lebesgue_integrable M a b f =
hoelzl@59092
   145
    (if a \<le> b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"
hoelzl@59092
   146
hoelzl@59092
   147
syntax
hoelzl@59092
   148
  "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
hoelzl@59092
   149
  ("(4LBINT _=_.._. _)" [0,60,60,61] 60)
hoelzl@59092
   150
hoelzl@59092
   151
translations
hoelzl@59092
   152
  "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
hoelzl@59092
   153
immler@69683
   154
subsection\<open>Basic properties of integration over an interval\<close>
hoelzl@59092
   155
hoelzl@59092
   156
lemma interval_lebesgue_integral_cong:
hoelzl@59092
   157
  "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
hoelzl@59092
   158
    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
hoelzl@59092
   159
  by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def)
hoelzl@59092
   160
hoelzl@59092
   161
lemma interval_lebesgue_integral_cong_AE:
hoelzl@59092
   162
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
hoelzl@59092
   163
    a \<le> b \<Longrightarrow> AE x \<in> einterval a b in M. f x = g x \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
hoelzl@59092
   164
    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
hoelzl@59092
   165
  by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def)
hoelzl@59092
   166
hoelzl@62083
   167
lemma interval_integrable_mirror:
hoelzl@62083
   168
  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. f (-x)) \<longleftrightarrow>
hoelzl@62083
   169
    interval_lebesgue_integrable lborel (-b) (-a) f"
hoelzl@62083
   170
proof -
hoelzl@62083
   171
  have *: "indicator (einterval a b) (- x) = (indicator (einterval (-b) (-a)) x :: real)"
hoelzl@62083
   172
    for a b :: ereal and x :: real
hoelzl@62083
   173
    by (cases a b rule: ereal2_cases) (auto simp: einterval_def split: split_indicator)
hoelzl@62083
   174
  show ?thesis
hoelzl@62083
   175
    unfolding interval_lebesgue_integrable_def
hoelzl@62083
   176
    using lborel_integrable_real_affine_iff[symmetric, of "-1" "\<lambda>x. indicator (einterval _ _) x *\<^sub>R f x" 0]
lp15@67974
   177
    by (simp add: * set_integrable_def)
hoelzl@62083
   178
qed
hoelzl@62083
   179
hoelzl@63329
   180
lemma interval_lebesgue_integral_add [intro, simp]:
hoelzl@63329
   181
  fixes M a b f
hoelzl@59092
   182
  assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
hoelzl@63329
   183
  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and
hoelzl@63329
   184
    "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) =
hoelzl@59092
   185
   interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
lp15@68096
   186
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
hoelzl@59092
   187
    field_simps)
hoelzl@59092
   188
hoelzl@63329
   189
lemma interval_lebesgue_integral_diff [intro, simp]:
hoelzl@63329
   190
  fixes M a b f
hoelzl@59092
   191
  assumes "interval_lebesgue_integrable M a b f"
hoelzl@59092
   192
    "interval_lebesgue_integrable M a b g"
hoelzl@63329
   193
  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and
hoelzl@63329
   194
    "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) =
hoelzl@59092
   195
   interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
lp15@68096
   196
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
hoelzl@59092
   197
    field_simps)
hoelzl@59092
   198
hoelzl@59092
   199
lemma interval_lebesgue_integrable_mult_right [intro, simp]:
hoelzl@59092
   200
  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
hoelzl@59092
   201
  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
hoelzl@59092
   202
    interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
hoelzl@59092
   203
  by (simp add: interval_lebesgue_integrable_def)
hoelzl@59092
   204
immler@69681
   205
lemma interval_lebesgue_integrable_mult_left [intro, simp]:
hoelzl@59092
   206
  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
hoelzl@59092
   207
  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
hoelzl@59092
   208
    interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
immler@69681
   209
  by (simp add: interval_lebesgue_integrable_def)
hoelzl@59092
   210
immler@69681
   211
lemma interval_lebesgue_integrable_divide [intro, simp]:
haftmann@59867
   212
  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
hoelzl@59092
   213
  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
hoelzl@59092
   214
    interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
immler@69681
   215
  by (simp add: interval_lebesgue_integrable_def)
hoelzl@59092
   216
hoelzl@59092
   217
lemma interval_lebesgue_integral_mult_right [simp]:
hoelzl@59092
   218
  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
hoelzl@59092
   219
  shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) =
hoelzl@59092
   220
    c * interval_lebesgue_integral M a b f"
hoelzl@59092
   221
  by (simp add: interval_lebesgue_integral_def)
hoelzl@59092
   222
immler@69681
   223
lemma interval_lebesgue_integral_mult_left [simp]:
hoelzl@59092
   224
  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
hoelzl@59092
   225
  shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
hoelzl@59092
   226
    interval_lebesgue_integral M a b f * c"
immler@69681
   227
  by (simp add: interval_lebesgue_integral_def)
hoelzl@59092
   228
hoelzl@59092
   229
lemma interval_lebesgue_integral_divide [simp]:
haftmann@59867
   230
  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
hoelzl@59092
   231
  shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
hoelzl@59092
   232
    interval_lebesgue_integral M a b f / c"
hoelzl@59092
   233
  by (simp add: interval_lebesgue_integral_def)
hoelzl@59092
   234
hoelzl@59092
   235
lemma interval_lebesgue_integral_uminus:
hoelzl@59092
   236
  "interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
lp15@68096
   237
  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
hoelzl@59092
   238
hoelzl@59092
   239
lemma interval_lebesgue_integral_of_real:
hoelzl@59092
   240
  "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
hoelzl@59092
   241
    of_real (interval_lebesgue_integral M a b f)"
hoelzl@59092
   242
  unfolding interval_lebesgue_integral_def
lp15@68096
   243
  by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
hoelzl@59092
   244
immler@69681
   245
lemma interval_lebesgue_integral_le_eq:
hoelzl@59092
   246
  fixes a b f
hoelzl@59092
   247
  assumes "a \<le> b"
hoelzl@59092
   248
  shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
immler@69681
   249
  using assms by (auto simp: interval_lebesgue_integral_def)
hoelzl@59092
   250
hoelzl@63329
   251
lemma interval_lebesgue_integral_gt_eq:
hoelzl@59092
   252
  fixes a b f
hoelzl@59092
   253
  assumes "a > b"
hoelzl@59092
   254
  shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
lp15@68096
   255
using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)
hoelzl@59092
   256
hoelzl@59092
   257
lemma interval_lebesgue_integral_gt_eq':
hoelzl@59092
   258
  fixes a b f
hoelzl@59092
   259
  assumes "a > b"
hoelzl@59092
   260
  shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
lp15@68096
   261
using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)
hoelzl@59092
   262
hoelzl@59092
   263
lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
lp15@67974
   264
  by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
hoelzl@59092
   265
hoelzl@59092
   266
lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
lp15@67974
   267
  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
hoelzl@59092
   268
hoelzl@59092
   269
lemma interval_integrable_endpoints_reverse:
hoelzl@59092
   270
  "interval_lebesgue_integrable lborel a b f \<longleftrightarrow>
hoelzl@59092
   271
    interval_lebesgue_integrable lborel b a f"
hoelzl@59092
   272
  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
hoelzl@59092
   273
immler@69681
   274
lemma interval_integral_reflect:
hoelzl@59092
   275
  "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
immler@69681
   276
proof (induct a b rule: linorder_wlog)
hoelzl@59092
   277
  case (sym a b) then show ?case
lp15@68096
   278
    by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
nipkow@62390
   279
             split: if_split_asm)
hoelzl@59092
   280
next
lp15@67974
   281
  case (le a b) 
lp15@67974
   282
  have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
lp15@67974
   283
    unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
lp15@67974
   284
    apply (rule Bochner_Integration.integral_cong [OF refl])
nipkow@68046
   285
    by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
nipkow@68403
   286
             simp flip: uminus_ereal.simps
hoelzl@59092
   287
             split: split_indicator)
lp15@67974
   288
  then show ?case
lp15@67974
   289
    unfolding interval_lebesgue_integral_def 
lp15@67974
   290
    by (subst set_integral_reflect) (simp add: le)
hoelzl@59092
   291
qed
hoelzl@59092
   292
hoelzl@61897
   293
lemma interval_lebesgue_integral_0_infty:
hoelzl@61897
   294
  "interval_lebesgue_integrable M 0 \<infinity> f \<longleftrightarrow> set_integrable M {0<..} f"
hoelzl@61897
   295
  "interval_lebesgue_integral M 0 \<infinity> f = (LINT x:{0<..}|M. f x)"
hoelzl@63329
   296
  unfolding zero_ereal_def
hoelzl@61897
   297
  by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def)
hoelzl@61897
   298
hoelzl@61897
   299
lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
hoelzl@61897
   300
  unfolding interval_lebesgue_integral_def by auto
hoelzl@61897
   301
immler@69681
   302
proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
hoelzl@61897
   303
  (set_integrable M {a<..} f)"
ak2110@69173
   304
  unfolding%unimportant interval_lebesgue_integrable_def by auto
hoelzl@61897
   305
immler@69683
   306
subsection\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
hoelzl@59092
   307
hoelzl@59092
   308
lemma interval_integral_zero [simp]:
hoelzl@59092
   309
  fixes a b :: ereal
lp15@68096
   310
  shows "LBINT x=a..b. 0 = 0"
lp15@67974
   311
unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
hoelzl@59092
   312
by simp
hoelzl@59092
   313
hoelzl@59092
   314
lemma interval_integral_const [intro, simp]:
hoelzl@59092
   315
  fixes a b c :: real
hoelzl@63329
   316
  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
lp15@67974
   317
  unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
lp15@68096
   318
  by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
hoelzl@59092
   319
immler@69681
   320
lemma interval_integral_cong_AE:
hoelzl@59092
   321
  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
hoelzl@59092
   322
  assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
hoelzl@59092
   323
  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
hoelzl@59092
   324
  using assms
immler@69681
   325
proof (induct a b rule: linorder_wlog)
hoelzl@59092
   326
  case (sym a b) then show ?case
hoelzl@59092
   327
    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
hoelzl@59092
   328
next
hoelzl@59092
   329
  case (le a b) then show ?case
hoelzl@59092
   330
    by (auto simp: interval_lebesgue_integral_def max_def min_def
hoelzl@59092
   331
             intro!: set_lebesgue_integral_cong_AE)
hoelzl@59092
   332
qed
hoelzl@59092
   333
immler@69681
   334
lemma interval_integral_cong:
hoelzl@63329
   335
  assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
hoelzl@59092
   336
  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
hoelzl@59092
   337
  using assms
immler@69681
   338
proof (induct a b rule: linorder_wlog)
hoelzl@59092
   339
  case (sym a b) then show ?case
hoelzl@59092
   340
    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
hoelzl@59092
   341
next
hoelzl@59092
   342
  case (le a b) then show ?case
hoelzl@59092
   343
    by (auto simp: interval_lebesgue_integral_def max_def min_def
hoelzl@59092
   344
             intro!: set_lebesgue_integral_cong)
hoelzl@59092
   345
qed
hoelzl@59092
   346
hoelzl@59092
   347
lemma interval_lebesgue_integrable_cong_AE:
hoelzl@59092
   348
    "f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
hoelzl@59092
   349
    AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x \<Longrightarrow>
hoelzl@59092
   350
    interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
lp15@68096
   351
  apply (simp add: interval_lebesgue_integrable_def)
hoelzl@59092
   352
  apply (intro conjI impI set_integrable_cong_AE)
hoelzl@59092
   353
  apply (auto simp: min_def max_def)
hoelzl@59092
   354
  done
hoelzl@59092
   355
hoelzl@59092
   356
lemma interval_integrable_abs_iff:
hoelzl@59092
   357
  fixes f :: "real \<Rightarrow> real"
hoelzl@59092
   358
  shows  "f \<in> borel_measurable lborel \<Longrightarrow>
hoelzl@59092
   359
    interval_lebesgue_integrable lborel a b (\<lambda>x. \<bar>f x\<bar>) = interval_lebesgue_integrable lborel a b f"
hoelzl@59092
   360
  unfolding interval_lebesgue_integrable_def
hoelzl@59092
   361
  by (subst (1 2) set_integrable_abs_iff') simp_all
hoelzl@59092
   362
hoelzl@59092
   363
lemma interval_integral_Icc:
hoelzl@59092
   364
  fixes a b :: real
hoelzl@59092
   365
  shows "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)"
hoelzl@59092
   366
  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
hoelzl@59092
   367
           simp add: interval_lebesgue_integral_def)
hoelzl@59092
   368
hoelzl@59092
   369
lemma interval_integral_Icc':
hoelzl@59092
   370
  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a \<le> ereal x \<and> ereal x \<le> b}. f x)"
lp15@61609
   371
  by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"]
hoelzl@59092
   372
           simp add: interval_lebesgue_integral_def einterval_iff)
hoelzl@59092
   373
hoelzl@59092
   374
lemma interval_integral_Ioc:
hoelzl@59092
   375
  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)"
hoelzl@59092
   376
  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
hoelzl@59092
   377
           simp add: interval_lebesgue_integral_def einterval_iff)
hoelzl@59092
   378
hoelzl@59092
   379
(* TODO: other versions as well? *) (* Yes: I need the Icc' version. *)
hoelzl@59092
   380
lemma interval_integral_Ioc':
hoelzl@59092
   381
  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x \<and> ereal x \<le> b}. f x)"
lp15@61609
   382
  by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"]
hoelzl@59092
   383
           simp add: interval_lebesgue_integral_def einterval_iff)
hoelzl@59092
   384
hoelzl@59092
   385
lemma interval_integral_Ico:
hoelzl@59092
   386
  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..<b}. f x)"
hoelzl@59092
   387
  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
hoelzl@59092
   388
           simp add: interval_lebesgue_integral_def einterval_iff)
hoelzl@59092
   389
hoelzl@59092
   390
lemma interval_integral_Ioi:
hoelzl@61882
   391
  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real_of_ereal a <..}. f x)"
lp15@68096
   392
  by (auto simp: interval_lebesgue_integral_def einterval_iff)
hoelzl@59092
   393
hoelzl@59092
   394
lemma interval_integral_Ioo:
hoelzl@61882
   395
  "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
lp15@68096
   396
  by (auto simp: interval_lebesgue_integral_def einterval_iff)
hoelzl@59092
   397
hoelzl@59092
   398
lemma interval_integral_discrete_difference:
hoelzl@59092
   399
  fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
hoelzl@59092
   400
  assumes "countable X"
hoelzl@59092
   401
  and eq: "\<And>x. a \<le> b \<Longrightarrow> a < x \<Longrightarrow> x < b \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
hoelzl@59092
   402
  and anti_eq: "\<And>x. b \<le> a \<Longrightarrow> b < x \<Longrightarrow> x < a \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
hoelzl@59092
   403
  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
hoelzl@59092
   404
  shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
lp15@67974
   405
  unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
hoelzl@59092
   406
  apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms)
hoelzl@59092
   407
  apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
hoelzl@59092
   408
  done
hoelzl@59092
   409
immler@69681
   410
lemma interval_integral_sum:
hoelzl@59092
   411
  fixes a b c :: ereal
hoelzl@63329
   412
  assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
hoelzl@59092
   413
  shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
immler@69681
   414
proof -
hoelzl@59092
   415
  let ?I = "\<lambda>a b. LBINT x=a..b. f x"
hoelzl@59092
   416
  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
hoelzl@59092
   417
    then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
hoelzl@59092
   418
      by (auto simp: interval_lebesgue_integrable_def)
hoelzl@59092
   419
    then have f: "set_borel_measurable borel (einterval a c) f"
lp15@67974
   420
      unfolding set_integrable_def set_borel_measurable_def
hoelzl@59092
   421
      by (drule_tac borel_measurable_integrable) simp
hoelzl@59092
   422
    have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \<union> einterval b c. f x)"
hoelzl@59092
   423
    proof (rule set_integral_cong_set)
hoelzl@59092
   424
      show "AE x in lborel. (x \<in> einterval a b \<union> einterval b c) = (x \<in> einterval a c)"
lp15@61609
   425
        using AE_lborel_singleton[of "real_of_ereal b"] ord
hoelzl@59092
   426
        by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
lp15@67974
   427
      show "set_borel_measurable lborel (einterval a c) f" "set_borel_measurable lborel (einterval a b \<union> einterval b c) f"
lp15@67974
   428
        unfolding set_borel_measurable_def
lp15@67974
   429
        using ord by (auto simp: einterval_iff intro!: set_borel_measurable_subset[OF f, unfolded set_borel_measurable_def])
lp15@67974
   430
    qed
hoelzl@59092
   431
    also have "\<dots> = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
hoelzl@59092
   432
      using ord
hoelzl@59092
   433
      by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
hoelzl@59092
   434
    finally have "?I a b + ?I b c = ?I a c"
hoelzl@59092
   435
      using ord by (simp add: interval_lebesgue_integral_def)
hoelzl@59092
   436
  } note 1 = this
hoelzl@59092
   437
  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
hoelzl@59092
   438
    from 1[OF this] have "?I b c + ?I a b = ?I a c"
hoelzl@59092
   439
      by (metis add.commute)
hoelzl@59092
   440
  } note 2 = this
hoelzl@59092
   441
  have 3: "\<And>a b. b \<le> a \<Longrightarrow> (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)"
hoelzl@59092
   442
    by (rule interval_integral_endpoints_reverse)
hoelzl@59092
   443
  show ?thesis
hoelzl@59092
   444
    using integrable
hoelzl@59092
   445
    by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
hoelzl@59092
   446
       (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
hoelzl@59092
   447
qed
hoelzl@59092
   448
immler@69681
   449
lemma interval_integrable_isCont:
hoelzl@59092
   450
  fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
hoelzl@59092
   451
  shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
hoelzl@59092
   452
    interval_lebesgue_integrable lborel a b f"
immler@69681
   453
proof (induct a b rule: linorder_wlog)
hoelzl@59092
   454
  case (le a b) then show ?case
lp15@67974
   455
    unfolding interval_lebesgue_integrable_def set_integrable_def
hoelzl@59092
   456
    by (auto simp: interval_lebesgue_integrable_def
lp15@67974
   457
        intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]]
lp15@67974
   458
        continuous_at_imp_continuous_on)
hoelzl@59092
   459
qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])
hoelzl@59092
   460
hoelzl@59092
   461
lemma interval_integrable_continuous_on:
hoelzl@59092
   462
  fixes a b :: real and f
hoelzl@59092
   463
  assumes "a \<le> b" and "continuous_on {a..b} f"
hoelzl@59092
   464
  shows "interval_lebesgue_integrable lborel a b f"
hoelzl@59092
   465
using assms unfolding interval_lebesgue_integrable_def apply simp
hoelzl@59092
   466
  by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto)
hoelzl@59092
   467
hoelzl@63329
   468
lemma interval_integral_eq_integral:
hoelzl@59092
   469
  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
hoelzl@59092
   470
  shows "a \<le> b \<Longrightarrow> set_integrable lborel {a..b} f \<Longrightarrow> LBINT x=a..b. f x = integral {a..b} f"
hoelzl@59092
   471
  by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral)
hoelzl@59092
   472
hoelzl@63329
   473
lemma interval_integral_eq_integral':
hoelzl@59092
   474
  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
hoelzl@59092
   475
  shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f"
hoelzl@59092
   476
  by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
hoelzl@63329
   477
lp15@67974
   478
immler@69683
   479
subsection\<open>General limit approximation arguments\<close>
hoelzl@59092
   480
immler@69681
   481
proposition interval_integral_Icc_approx_nonneg:
hoelzl@59092
   482
  fixes a b :: ereal
hoelzl@59092
   483
  assumes "a < b"
hoelzl@59092
   484
  fixes u l :: "nat \<Rightarrow> real"
hoelzl@59092
   485
  assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
hoelzl@59092
   486
    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
wenzelm@61969
   487
    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
hoelzl@59092
   488
  fixes f :: "real \<Rightarrow> real"
hoelzl@59092
   489
  assumes f_integrable: "\<And>i. set_integrable lborel {l i..u i} f"
hoelzl@59092
   490
  assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
hoelzl@59092
   491
  assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
wenzelm@61969
   492
  assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C"
hoelzl@63329
   493
  shows
hoelzl@59092
   494
    "set_integrable lborel (einterval a b) f"
hoelzl@59092
   495
    "(LBINT x=a..b. f x) = C"
immler@69681
   496
proof -
lp15@67974
   497
  have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
hoelzl@59092
   498
  have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
hoelzl@59092
   499
  proof -
hoelzl@59092
   500
     from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x"
hoelzl@59092
   501
      by eventually_elim
hoelzl@59092
   502
         (metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans)
hoelzl@59092
   503
    then show ?thesis
hoelzl@59092
   504
      apply eventually_elim
hoelzl@59092
   505
      apply (auto simp: mono_def split: split_indicator)
hoelzl@59092
   506
      apply (metis approx(3) decseqD order_trans)
hoelzl@59092
   507
      apply (metis approx(2) incseqD order_trans)
hoelzl@59092
   508
      done
hoelzl@59092
   509
  qed
wenzelm@61969
   510
  have 3: "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
hoelzl@59092
   511
  proof -
hoelzl@59092
   512
    { fix x i assume "l i \<le> x" "x \<le> u i"
hoelzl@59092
   513
      then have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
hoelzl@59092
   514
        apply (auto simp: eventually_sequentially intro!: exI[of _ i])
hoelzl@59092
   515
        apply (metis approx(3) decseqD order_trans)
hoelzl@59092
   516
        apply (metis approx(2) incseqD order_trans)
hoelzl@59092
   517
        done
hoelzl@59092
   518
      then have "eventually (\<lambda>i. f x * indicator {l i..u i} x = f x) sequentially"
hoelzl@59092
   519
        by eventually_elim auto }
hoelzl@59092
   520
    then show ?thesis
hoelzl@59092
   521
      unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
hoelzl@59092
   522
  qed
wenzelm@61969
   523
  have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) \<longlonglongrightarrow> C"
lp15@67974
   524
    using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
lp15@67974
   525
  have 5: "(\<lambda>x. indicat_real (einterval a b) x *\<^sub>R f x) \<in> borel_measurable lborel"
lp15@67974
   526
    using f_measurable set_borel_measurable_def by blast
hoelzl@59092
   527
  have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
lp15@67974
   528
    using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
lp15@68096
   529
  also have "\<dots> = C"
lp15@67974
   530
    by (rule integral_monotone_convergence [OF 1 2 3 4 5])
hoelzl@59092
   531
  finally show "(LBINT x=a..b. f x) = C" .
hoelzl@63329
   532
  show "set_integrable lborel (einterval a b) f"
lp15@67974
   533
    unfolding set_integrable_def
hoelzl@59092
   534
    by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
hoelzl@59092
   535
qed
hoelzl@59092
   536
immler@69681
   537
proposition interval_integral_Icc_approx_integrable:
hoelzl@59092
   538
  fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
hoelzl@59092
   539
  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
hoelzl@59092
   540
  assumes "a < b"
hoelzl@59092
   541
  assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
hoelzl@59092
   542
    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
wenzelm@61969
   543
    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
hoelzl@59092
   544
  assumes f_integrable: "set_integrable lborel (einterval a b) f"
wenzelm@61969
   545
  shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
immler@69681
   546
proof -
wenzelm@61969
   547
  have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
lp15@67974
   548
    unfolding set_lebesgue_integral_def
hoelzl@59092
   549
  proof (rule integral_dominated_convergence)
hoelzl@59092
   550
    show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
lp15@67974
   551
      using f_integrable integrable_norm set_integrable_def by blast
lp15@67974
   552
    show "(\<lambda>x. indicat_real (einterval a b) x *\<^sub>R f x) \<in> borel_measurable lborel"
lp15@67974
   553
      using f_integrable by (simp add: set_integrable_def)
lp15@67974
   554
    then show "\<And>i. (\<lambda>x. indicat_real {l i..u i} x *\<^sub>R f x) \<in> borel_measurable lborel"
lp15@67974
   555
      by (rule set_borel_measurable_subset [unfolded set_borel_measurable_def]) (auto simp: approx)
hoelzl@59092
   556
    show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
hoelzl@59092
   557
      by (intro AE_I2) (auto simp: approx split: split_indicator)
wenzelm@61969
   558
    show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
hoelzl@59092
   559
    proof (intro AE_I2 tendsto_intros Lim_eventually)
hoelzl@59092
   560
      fix x
hoelzl@63329
   561
      { fix i assume "l i \<le> x" "x \<le> u i"
wenzelm@61808
   562
        with \<open>incseq u\<close>[THEN incseqD, of i] \<open>decseq l\<close>[THEN decseqD, of i]
hoelzl@59092
   563
        have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
hoelzl@59092
   564
          by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
hoelzl@59092
   565
      then show "eventually (\<lambda>xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially"
wenzelm@61969
   566
        using approx order_tendstoD(2)[OF \<open>l \<longlonglongrightarrow> a\<close>, of x] order_tendstoD(1)[OF \<open>u \<longlonglongrightarrow> b\<close>, of x]
hoelzl@59092
   567
        by (auto split: split_indicator)
hoelzl@59092
   568
    qed
hoelzl@59092
   569
  qed
wenzelm@61808
   570
  with \<open>a < b\<close> \<open>\<And>i. l i < u i\<close> show ?thesis
hoelzl@59092
   571
    by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
hoelzl@59092
   572
qed
hoelzl@59092
   573
immler@69683
   574
subsection\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
lp15@67974
   575
lp15@67974
   576
text\<open>Three versions: first, for finite intervals, and then two versions for
lp15@67974
   577
    arbitrary intervals.\<close>
lp15@67974
   578
hoelzl@59092
   579
(*
hoelzl@59092
   580
  TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
hoelzl@59092
   581
*)
hoelzl@59092
   582
immler@69681
   583
lemma interval_integral_FTC_finite:
hoelzl@59092
   584
  fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
hoelzl@59092
   585
  assumes f: "continuous_on {min a b..max a b} f"
hoelzl@63329
   586
  assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
hoelzl@63329
   587
    {min a b..max a b})"
hoelzl@59092
   588
  shows "(LBINT x=a..b. f x) = F b - F a"
immler@69681
   589
proof (cases "a \<le> b")
lp15@67974
   590
  case True
lp15@67974
   591
  have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
lp15@67974
   592
    by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
lp15@68096
   593
  also have "\<dots> = F b - F a"
lp15@67974
   594
  proof (rule integral_FTC_atLeastAtMost [OF True])
lp15@67974
   595
    show "continuous_on {a..b} f"
lp15@67974
   596
      using True f by linarith
lp15@67974
   597
    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (F has_vector_derivative f x) (at x within {a..b})"
lp15@67974
   598
      by (metis F True max.commute max_absorb1 min_def)
lp15@67974
   599
  qed
lp15@67974
   600
  finally show ?thesis .
lp15@67974
   601
next
lp15@67974
   602
  case False
lp15@67974
   603
  then have "b \<le> a"
lp15@67974
   604
    by simp
lp15@67974
   605
  have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *\<^sub>R f x)"
lp15@67974
   606
    by (simp add: \<open>b \<le> a\<close> interval_integral_Icc set_lebesgue_integral_def)
lp15@68096
   607
  also have "\<dots> = F b - F a"
lp15@67974
   608
  proof (subst integral_FTC_atLeastAtMost [OF \<open>b \<le> a\<close>])
lp15@67974
   609
    show "continuous_on {b..a} f"
lp15@67974
   610
      using False f by linarith
lp15@67974
   611
    show "\<And>x. \<lbrakk>b \<le> x; x \<le> a\<rbrakk>
lp15@67974
   612
         \<Longrightarrow> (F has_vector_derivative f x) (at x within {b..a})"
lp15@67974
   613
      by (metis F False max_def min_def)
lp15@67974
   614
  qed auto
lp15@67974
   615
  finally show ?thesis
lp15@67974
   616
    by (metis interval_integral_endpoints_reverse)
lp15@67974
   617
qed
lp15@67974
   618
lp15@67974
   619
immler@69681
   620
lemma interval_integral_FTC_nonneg:
hoelzl@59092
   621
  fixes f F :: "real \<Rightarrow> real" and a b :: ereal
hoelzl@59092
   622
  assumes "a < b"
hoelzl@63329
   623
  assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
hoelzl@63329
   624
  assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
hoelzl@59092
   625
  assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
wenzelm@61973
   626
  assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
wenzelm@61973
   627
  assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
hoelzl@59092
   628
  shows
hoelzl@63329
   629
    "set_integrable lborel (einterval a b) f"
hoelzl@59092
   630
    "(LBINT x=a..b. f x) = B - A"
immler@69681
   631
proof -
lp15@68095
   632
  obtain u l where approx:
lp15@68095
   633
    "einterval a b = (\<Union>i. {l i .. u i})"
lp15@68095
   634
    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
lp15@68095
   635
    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
lp15@68095
   636
    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
hoelzl@59092
   637
  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
hoelzl@59092
   638
    by (rule order_less_le_trans, rule approx, force)
hoelzl@59092
   639
  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
hoelzl@59092
   640
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
hoelzl@59092
   641
  have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
hoelzl@59092
   642
    using assms approx apply (intro interval_integral_FTC_finite)
lp15@68096
   643
    apply (auto simp: less_imp_le min_def max_def
hoelzl@59092
   644
      has_field_derivative_iff_has_vector_derivative[symmetric])
hoelzl@59092
   645
    apply (rule continuous_at_imp_continuous_on, auto intro!: f)
hoelzl@59092
   646
    by (rule DERIV_subset [OF F], auto)
hoelzl@59092
   647
  have 1: "\<And>i. set_integrable lborel {l i..u i} f"
hoelzl@59092
   648
  proof -
hoelzl@59092
   649
    fix i show "set_integrable lborel {l i .. u i} f"
lp15@67974
   650
      using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
hoelzl@59092
   651
      by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
nipkow@68403
   652
         (auto simp flip: ereal_less_eq)
hoelzl@59092
   653
  qed
hoelzl@59092
   654
  have 2: "set_borel_measurable lborel (einterval a b) f"
lp15@67974
   655
    unfolding set_borel_measurable_def
lp15@66164
   656
    by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
hoelzl@59092
   657
             simp: continuous_on_eq_continuous_at einterval_iff f)
wenzelm@61969
   658
  have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
hoelzl@59092
   659
    apply (subst FTCi)
hoelzl@59092
   660
    apply (intro tendsto_intros)
hoelzl@59092
   661
    using B approx unfolding tendsto_at_iff_sequentially comp_def
hoelzl@59092
   662
    using tendsto_at_iff_sequentially[where 'a=real]
hoelzl@59092
   663
    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
hoelzl@59092
   664
    using A approx unfolding tendsto_at_iff_sequentially comp_def
hoelzl@59092
   665
    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
hoelzl@59092
   666
  show "(LBINT x=a..b. f x) = B - A"
wenzelm@61808
   667
    by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
hoelzl@63329
   668
  show "set_integrable lborel (einterval a b) f"
wenzelm@61808
   669
    by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
hoelzl@59092
   670
qed
hoelzl@59092
   671
immler@69681
   672
theorem interval_integral_FTC_integrable:
hoelzl@59092
   673
  fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
hoelzl@59092
   674
  assumes "a < b"
hoelzl@63329
   675
  assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
hoelzl@63329
   676
  assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
hoelzl@59092
   677
  assumes f_integrable: "set_integrable lborel (einterval a b) f"
wenzelm@61973
   678
  assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
wenzelm@61973
   679
  assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
hoelzl@59092
   680
  shows "(LBINT x=a..b. f x) = B - A"
immler@69681
   681
proof -
lp15@68095
   682
  obtain u l where approx:
lp15@68095
   683
    "einterval a b = (\<Union>i. {l i .. u i})"
lp15@68095
   684
    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
lp15@68095
   685
    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
lp15@68095
   686
    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
hoelzl@59092
   687
  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
hoelzl@59092
   688
    by (rule order_less_le_trans, rule approx, force)
hoelzl@59092
   689
  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
hoelzl@59092
   690
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
hoelzl@59092
   691
  have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
hoelzl@59092
   692
    using assms approx
lp15@68096
   693
    by (auto simp: less_imp_le min_def max_def
hoelzl@59092
   694
             intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
hoelzl@59092
   695
             intro: has_vector_derivative_at_within)
wenzelm@61969
   696
  have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
lp15@68096
   697
    unfolding FTCi
lp15@68096
   698
  proof (intro tendsto_intros)
lp15@68096
   699
    show "(\<lambda>x. F (l x)) \<longlonglongrightarrow> A"
lp15@68096
   700
      using A approx unfolding tendsto_at_iff_sequentially comp_def
lp15@68096
   701
      by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
lp15@68096
   702
    show "(\<lambda>x. F (u x)) \<longlonglongrightarrow> B"
lp15@68096
   703
      using B approx unfolding tendsto_at_iff_sequentially comp_def
lp15@68096
   704
      by (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
lp15@68096
   705
  qed
wenzelm@61969
   706
  moreover have "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
wenzelm@61808
   707
    by (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx f_integrable])
hoelzl@59092
   708
  ultimately show ?thesis
hoelzl@59092
   709
    by (elim LIMSEQ_unique)
hoelzl@59092
   710
qed
hoelzl@59092
   711
hoelzl@63329
   712
(*
hoelzl@59092
   713
  The second Fundamental Theorem of Calculus and existence of antiderivatives on an
hoelzl@59092
   714
  einterval.
hoelzl@59092
   715
*)
hoelzl@59092
   716
immler@69681
   717
theorem interval_integral_FTC2:
hoelzl@59092
   718
  fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
hoelzl@59092
   719
  assumes "a \<le> c" "c \<le> b"
hoelzl@59092
   720
  and contf: "continuous_on {a..b} f"
hoelzl@59092
   721
  fixes x :: real
hoelzl@59092
   722
  assumes "a \<le> x" and "x \<le> b"
hoelzl@59092
   723
  shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
immler@69681
   724
proof -
hoelzl@59092
   725
  let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
hoelzl@59092
   726
  have intf: "set_integrable lborel {a..b} f"
hoelzl@59092
   727
    by (rule borel_integrable_atLeastAtMost', rule contf)
hoelzl@59092
   728
  have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
lp15@68096
   729
    using \<open>a \<le> x\<close> \<open>x \<le> b\<close> 
lp15@68096
   730
    by (auto intro: integral_has_vector_derivative continuous_on_subset [OF contf])
hoelzl@59092
   731
  then have "((\<lambda>u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
hoelzl@59092
   732
    by simp
hoelzl@59092
   733
  then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
hoelzl@59092
   734
    by (rule has_vector_derivative_weaken)
hoelzl@59092
   735
       (auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf])
hoelzl@59092
   736
  then have "((\<lambda>x. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})"
hoelzl@59092
   737
    by (auto intro!: derivative_eq_intros)
hoelzl@59092
   738
  then show ?thesis
hoelzl@59092
   739
  proof (rule has_vector_derivative_weaken)
hoelzl@59092
   740
    fix u assume "u \<in> {a .. b}"
hoelzl@59092
   741
    then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
hoelzl@59092
   742
      using assms
hoelzl@59092
   743
      apply (intro interval_integral_sum)
lp15@68096
   744
      apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def)
lp15@68096
   745
      by (rule set_integrable_subset [OF intf], auto simp: min_def max_def)
hoelzl@59092
   746
  qed (insert assms, auto)
hoelzl@59092
   747
qed
hoelzl@59092
   748
immler@69681
   749
proposition einterval_antiderivative:
hoelzl@59092
   750
  fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
hoelzl@59092
   751
  assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
hoelzl@59092
   752
  shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
immler@69681
   753
proof -
hoelzl@63329
   754
  from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
lp15@68096
   755
    by (auto simp: einterval_def)
hoelzl@59092
   756
  let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
hoelzl@59092
   757
  show ?thesis
hoelzl@59092
   758
  proof (rule exI, clarsimp)
hoelzl@59092
   759
    fix x :: real
hoelzl@59092
   760
    assume [simp]: "a < x" "x < b"
hoelzl@59092
   761
    have 1: "a < min c x" by simp
hoelzl@63329
   762
    from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
lp15@68096
   763
      by (auto simp: einterval_def)
hoelzl@59092
   764
    have 2: "max c x < b" by simp
hoelzl@63329
   765
    from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
lp15@68096
   766
      by (auto simp: einterval_def)
lp15@68095
   767
    have "(?F has_vector_derivative f x) (at x within {d<..<e})"
lp15@68095
   768
    proof (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
lp15@68095
   769
      have "continuous_on {d..e} f"
lp15@68095
   770
      proof (intro continuous_at_imp_continuous_on ballI contf; clarsimp)
lp15@68095
   771
        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> a < ereal x"
lp15@68095
   772
          using \<open>a < ereal d\<close> ereal_less_ereal_Ex by auto
lp15@68095
   773
        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> ereal x < b"
lp15@68095
   774
          using \<open>ereal e < b\<close> ereal_less_eq(3) le_less_trans by blast
lp15@68095
   775
      qed
lp15@68095
   776
      then show "(?F has_vector_derivative f x) (at x within {d..e})"
lp15@68095
   777
        by (intro interval_integral_FTC2) (use \<open>d < c\<close> \<open>c < e\<close> \<open>d < x\<close> \<open>x < e\<close> in \<open>linarith+\<close>)
lp15@68095
   778
    qed auto
lp15@68095
   779
    then show "(?F has_vector_derivative f x) (at x)"
lp15@68096
   780
      by (force simp: has_vector_derivative_within_open [of _ "{d<..<e}"])
hoelzl@59092
   781
  qed
hoelzl@59092
   782
qed
hoelzl@59092
   783
immler@69683
   784
subsection\<open>The substitution theorem\<close>
hoelzl@59092
   785
lp15@67974
   786
text\<open>Once again, three versions: first, for finite intervals, and then two versions for
lp15@67974
   787
    arbitrary intervals.\<close>
hoelzl@63329
   788
immler@69681
   789
theorem interval_integral_substitution_finite:
hoelzl@59092
   790
  fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
hoelzl@59092
   791
  assumes "a \<le> b"
hoelzl@59092
   792
  and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
hoelzl@59092
   793
  and contf : "continuous_on (g ` {a..b}) f"
hoelzl@59092
   794
  and contg': "continuous_on {a..b} g'"
hoelzl@59092
   795
  shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
immler@69681
   796
proof-
hoelzl@59092
   797
  have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
hoelzl@59092
   798
    using derivg unfolding has_field_derivative_iff_has_vector_derivative .
hoelzl@59092
   799
  then have contg [simp]: "continuous_on {a..b} g"
hoelzl@59092
   800
    by (rule continuous_on_vector_derivative) auto
lp15@68096
   801
  have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u
lp15@68096
   802
    by (cases "g a \<le> g b") (use that assms IVT' [of g a u b]  IVT2' [of g b u a]  in \<open>auto simp: min_def max_def\<close>)
lp15@68096
   803
  obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d"
lp15@68096
   804
    by (metis continuous_image_closed_interval contg \<open>a \<le> b\<close>)
lp15@68096
   805
  obtain F where derivF:
lp15@68096
   806
         "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" 
lp15@68096
   807
    using continuous_on_subset [OF contf] g_im
lp15@68096
   808
      by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
hoelzl@59092
   809
  have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
hoelzl@59092
   810
    by (blast intro: continuous_on_compose2 contf contg)
lp15@68096
   811
  have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
lp15@68096
   812
    apply (rule integral_FTC_atLeastAtMost
lp15@68096
   813
                [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]])
hoelzl@59092
   814
    apply (auto intro!: continuous_on_scaleR contg' contfg)
hoelzl@59092
   815
    done
lp15@68096
   816
  then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
lp15@68096
   817
    by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
hoelzl@59092
   818
  moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
lp15@68096
   819
  proof (rule interval_integral_FTC_finite)
lp15@68096
   820
    show "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
lp15@68096
   821
      by (rule continuous_on_subset [OF contf]) (auto simp: image_def 1)
lp15@68096
   822
    show "(F has_vector_derivative f y) (at y within {min (g a) (g b)..max (g a) (g b)})" 
lp15@68096
   823
      if y: "min (g a) (g b) \<le> y" "y \<le> max (g a) (g b)" for y
lp15@68096
   824
    proof -
lp15@68096
   825
      obtain x where "a \<le> x" "x \<le> b" "y = g x"
lp15@68096
   826
        using 1 y by force
lp15@68096
   827
      then show ?thesis
lp15@68096
   828
        by (auto simp: image_def intro!: 1  has_vector_derivative_within_subset [OF derivF])
lp15@68096
   829
    qed
lp15@68096
   830
  qed
hoelzl@59092
   831
  ultimately show ?thesis by simp
hoelzl@59092
   832
qed
hoelzl@59092
   833
hoelzl@59092
   834
(* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
hoelzl@59092
   835
immler@69681
   836
theorem interval_integral_substitution_integrable:
hoelzl@59092
   837
  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
hoelzl@63329
   838
  assumes "a < b"
hoelzl@59092
   839
  and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
hoelzl@59092
   840
  and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
hoelzl@59092
   841
  and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
hoelzl@59092
   842
  and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
wenzelm@61973
   843
  and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
wenzelm@61973
   844
  and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
hoelzl@59092
   845
  and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
hoelzl@59092
   846
  and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
hoelzl@59092
   847
  shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
immler@69681
   848
proof -
lp15@68095
   849
  obtain u l where approx [simp]:
lp15@68095
   850
    "einterval a b = (\<Union>i. {l i .. u i})"
lp15@68095
   851
    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
lp15@68095
   852
    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
lp15@68095
   853
    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
hoelzl@59092
   854
  note less_imp_le [simp]
hoelzl@59092
   855
  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
hoelzl@59092
   856
    by (rule order_less_le_trans, rule approx, force)
hoelzl@59092
   857
  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
hoelzl@59092
   858
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
lp15@68095
   859
  then have lessb[simp]: "\<And>i. l i < b"
lp15@68095
   860
    using approx(4) less_eq_real_def by blast
hoelzl@63329
   861
  have [simp]: "\<And>i. a < u i"
hoelzl@59092
   862
    by (rule order_less_trans, rule approx, auto, rule approx)
lp15@68095
   863
  have lle[simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
hoelzl@59092
   864
  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
lp15@68095
   865
  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
lp15@68638
   866
  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI)
lp15@68638
   867
    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
lp15@68095
   868
      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
lp15@68638
   869
    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> 0 \<le> g' u"
lp15@68095
   870
      by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
lp15@68095
   871
  qed
hoelzl@59092
   872
  have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
hoelzl@63329
   873
  proof -
wenzelm@61969
   874
    have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
lp15@68096
   875
      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
hoelzl@59092
   876
      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hoelzl@59092
   877
    hence A3: "\<And>i. g (l i) \<ge> A"
lp15@68532
   878
      by (intro decseq_ge, auto simp: decseq_def)
wenzelm@61969
   879
    have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
lp15@68096
   880
      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
hoelzl@59092
   881
      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
hoelzl@59092
   882
    hence B3: "\<And>i. g (u i) \<le> B"
lp15@68096
   883
      by (intro incseq_le, auto simp: incseq_def)
lp15@68095
   884
    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
hoelzl@59092
   885
      by auto
lp15@68095
   886
    then show "A \<le> B"
lp15@68095
   887
      by (meson A3 B3 order.trans)
hoelzl@59092
   888
    { fix x :: real
hoelzl@63329
   889
      assume "A < x" and "x < B"
hoelzl@59092
   890
      then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
lp15@68095
   891
        by (fast intro: eventually_conj order_tendstoD A2 B2)
hoelzl@59092
   892
      hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
hoelzl@59092
   893
        by (simp add: eventually_sequentially, auto)
hoelzl@59092
   894
    } note AB = this
hoelzl@59092
   895
    show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
lp15@68095
   896
    proof
lp15@68095
   897
      show "einterval A B \<subseteq> (\<Union>i. {g(l i)<..<g(u i)})"
lp15@68096
   898
        by (auto simp: einterval_def AB)
lp15@68095
   899
      show "(\<Union>i. {g(l i)<..<g(u i)}) \<subseteq> einterval A B"
lp15@68095
   900
      proof (clarsimp simp add: einterval_def, intro conjI)
lp15@68095
   901
        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> A < ereal x"
lp15@68095
   902
          using A3 le_ereal_less by blast
lp15@68095
   903
        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> ereal x < B"
lp15@68095
   904
          using B3 ereal_le_less by blast
lp15@68095
   905
      qed
lp15@68095
   906
    qed
hoelzl@59092
   907
  qed
hoelzl@59092
   908
  (* finally, the main argument *)
lp15@68095
   909
  have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
lp15@68095
   910
    apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
lp15@68095
   911
    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
lp15@68095
   912
         apply (auto intro!: continuous_at_imp_continuous_on contf contg')
lp15@68095
   913
    done
wenzelm@61969
   914
  have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
wenzelm@61808
   915
    apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
hoelzl@59092
   916
    by (rule assms)
wenzelm@61969
   917
  hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
hoelzl@59092
   918
    by (simp add: eq1)
hoelzl@59092
   919
  have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
lp15@68096
   920
    apply (auto simp: incseq_def)
lp15@68095
   921
    using lessb lle approx(5) g_nondec le_less_trans apply blast
lp15@68095
   922
    by (force intro: less_le_trans)
lp15@68096
   923
  have "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
lp15@68096
   924
        \<longlonglongrightarrow> set_lebesgue_integral lborel (einterval A B) f"
lp15@68096
   925
    unfolding un  by (rule set_integral_cont_up) (use incseq  integrable2 un in auto)
lp15@68096
   926
  then have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
lp15@68096
   927
    by (simp add: interval_lebesgue_integral_le_eq \<open>A \<le> B\<close>)
hoelzl@59092
   928
  thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
hoelzl@59092
   929
qed
hoelzl@59092
   930
hoelzl@59092
   931
(* TODO: the last two proofs are only slightly different. Factor out common part?
hoelzl@59092
   932
   An alternative: make the second one the main one, and then have another lemma
hoelzl@59092
   933
   that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
hoelzl@59092
   934
immler@69681
   935
theorem interval_integral_substitution_nonneg:
hoelzl@59092
   936
  fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
hoelzl@63329
   937
  assumes "a < b"
hoelzl@59092
   938
  and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
hoelzl@59092
   939
  and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
hoelzl@59092
   940
  and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
hoelzl@59092
   941
  and f_nonneg: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> 0 \<le> f (g x)" (* TODO: make this AE? *)
hoelzl@59092
   942
  and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
wenzelm@61973
   943
  and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
wenzelm@61973
   944
  and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
hoelzl@59092
   945
  and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
hoelzl@63329
   946
  shows
hoelzl@59092
   947
    "set_integrable lborel (einterval A B) f"
hoelzl@59092
   948
    "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
immler@69681
   949
proof -
wenzelm@61808
   950
  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
hoelzl@59092
   951
  note less_imp_le [simp]
lp15@68096
   952
  have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
hoelzl@59092
   953
    by (rule order_less_le_trans, rule approx, force)
lp15@68095
   954
  have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
hoelzl@59092
   955
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
lp15@68095
   956
  have llb[simp]: "\<And>i. l i < b"
lp15@68095
   957
    using lessb approx(4) less_eq_real_def by blast
lp15@68095
   958
  have alu[simp]: "\<And>i. a < u i"
hoelzl@59092
   959
    by (rule order_less_trans, rule approx, auto, rule approx)
hoelzl@59092
   960
  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
lp15@68095
   961
  have uleu[simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
lp15@68095
   962
  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
lp15@68638
   963
  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI)
lp15@68638
   964
    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
lp15@68095
   965
      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
lp15@68638
   966
    show "\<And>u. x \<le> u \<Longrightarrow> u \<le> y \<Longrightarrow> 0 \<le> g' u"
lp15@68095
   967
      by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
lp15@68095
   968
  qed
hoelzl@59092
   969
  have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
hoelzl@63329
   970
  proof -
wenzelm@61969
   971
    have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
lp15@68096
   972
      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
hoelzl@59092
   973
      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hoelzl@59092
   974
    hence A3: "\<And>i. g (l i) \<ge> A"
lp15@68532
   975
      by (intro decseq_ge, auto simp: decseq_def)
wenzelm@61969
   976
    have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
lp15@68096
   977
      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
hoelzl@59092
   978
      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
hoelzl@59092
   979
    hence B3: "\<And>i. g (u i) \<le> B"
lp15@68096
   980
      by (intro incseq_le, auto simp: incseq_def)
lp15@68095
   981
    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
hoelzl@59092
   982
      by auto
lp15@68095
   983
    then show "A \<le> B"
lp15@68095
   984
      by (meson A3 B3 order.trans)
hoelzl@59092
   985
    { fix x :: real
hoelzl@63329
   986
      assume "A < x" and "x < B"
hoelzl@59092
   987
      then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
lp15@68096
   988
        by (fast intro: eventually_conj order_tendstoD A2 B2)
hoelzl@59092
   989
      hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
hoelzl@59092
   990
        by (simp add: eventually_sequentially, auto)
hoelzl@59092
   991
    } note AB = this
hoelzl@59092
   992
    show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
lp15@68095
   993
    proof
lp15@68095
   994
      show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
lp15@68096
   995
        by (auto simp: einterval_def AB)
lp15@68095
   996
      show "(\<Union>i. {g (l i)<..<g (u i)}) \<subseteq> einterval A B"
lp15@68095
   997
        apply (clarsimp simp: einterval_def, intro conjI)
lp15@68095
   998
        using A3 le_ereal_less apply blast
lp15@68095
   999
        using B3 ereal_le_less by blast
lp15@68095
  1000
    qed
hoelzl@59092
  1001
  qed
lp15@68095
  1002
    (* finally, the main argument *)
lp15@68095
  1003
  have eq1: "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" for i
lp15@68095
  1004
  proof -
lp15@68095
  1005
    have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
lp15@68095
  1006
      apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
lp15@68095
  1007
      unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
lp15@68095
  1008
           apply (auto intro!: continuous_at_imp_continuous_on contf contg')
lp15@68095
  1009
      done
lp15@68095
  1010
    then show ?thesis
lp15@68095
  1011
      by (simp add: ac_simps)
lp15@68095
  1012
  qed
hoelzl@59092
  1013
  have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
lp15@68095
  1014
    apply (clarsimp simp add: incseq_def, intro conjI)
lp15@68095
  1015
    apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
lp15@68095
  1016
    using alu uleu approx(6) g_nondec less_le_trans by blast
lp15@68095
  1017
  have img: "\<exists>c \<ge> l i. c \<le> u i \<and> x = g c" if "g (l i) \<le> x" "x \<le> g (u i)" for x i
lp15@68095
  1018
  proof -
lp15@68095
  1019
    have "continuous_on {l i..u i} g"
lp15@68095
  1020
      by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on)
lp15@68095
  1021
    with that show ?thesis
lp15@68095
  1022
      using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
lp15@68095
  1023
  qed
lp15@68096
  1024
  have "continuous_on {g (l i)..g (u i)} f" for i
lp15@68096
  1025
    apply (intro continuous_intros continuous_at_imp_continuous_on)
lp15@68096
  1026
    using contf img by force
lp15@68096
  1027
  then have int_f: "\<And>i. set_integrable lborel {g (l i)<..<g (u i)} f"
lp15@68096
  1028
    by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
hoelzl@59092
  1029
  have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
lp15@68096
  1030
  proof (intro pos_integrable_to_top incseq int_f)
lp15@68096
  1031
    let ?l = "(LBINT x=a..b. f (g x) * g' x)"
lp15@68096
  1032
    have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x) \<longlonglongrightarrow> ?l"
lp15@68096
  1033
      by (intro assms interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
lp15@68096
  1034
    hence "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> ?l"
lp15@68096
  1035
      by (simp add: eq1)
lp15@68096
  1036
    then show "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f) \<longlonglongrightarrow> ?l"
lp15@68096
  1037
      unfolding interval_lebesgue_integral_def by auto
lp15@68096
  1038
    have "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
lp15@68096
  1039
      using aless f_nonneg img lessb by blast
lp15@68096
  1040
    then show "\<And>x i. x \<in> {g (l i)<..<g (u i)} \<Longrightarrow> 0 \<le> f x"
lp15@68096
  1041
      using less_eq_real_def by auto
lp15@68096
  1042
  qed (auto simp: greaterThanLessThan_borel)
hoelzl@59092
  1043
  thus "set_integrable lborel (einterval A B) f"
hoelzl@59092
  1044
    by (simp add: un)
hoelzl@59092
  1045
hoelzl@59092
  1046
  have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
hoelzl@59092
  1047
  proof (rule interval_integral_substitution_integrable)
hoelzl@59092
  1048
    show "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
hoelzl@59092
  1049
      using integrable_fg by (simp add: ac_simps)
hoelzl@59092
  1050
  qed fact+
hoelzl@59092
  1051
  then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
hoelzl@59092
  1052
    by (simp add: ac_simps)
hoelzl@59092
  1053
qed
hoelzl@59092
  1054
hoelzl@59092
  1055
hoelzl@63941
  1056
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
hoelzl@63941
  1057
  ("(2CLBINT _. _)" [0,60] 60)
hoelzl@63941
  1058
hoelzl@63941
  1059
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
hoelzl@63941
  1060
hoelzl@63941
  1061
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
hoelzl@63941
  1062
  ("(3CLBINT _:_. _)" [0,60,61] 60)
hoelzl@59092
  1063
hoelzl@59092
  1064
translations
hoelzl@63941
  1065
  "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
hoelzl@59092
  1066
hoelzl@63329
  1067
abbreviation complex_interval_lebesgue_integral ::
hoelzl@59092
  1068
    "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
hoelzl@59092
  1069
  "complex_interval_lebesgue_integral M a b f \<equiv> interval_lebesgue_integral M a b f"
hoelzl@59092
  1070
hoelzl@63329
  1071
abbreviation complex_interval_lebesgue_integrable ::
hoelzl@59092
  1072
  "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" where
hoelzl@59092
  1073
  "complex_interval_lebesgue_integrable M a b f \<equiv> interval_lebesgue_integrable M a b f"
hoelzl@59092
  1074
hoelzl@59092
  1075
syntax
hoelzl@59092
  1076
  "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
hoelzl@59092
  1077
  ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
hoelzl@59092
  1078
hoelzl@59092
  1079
translations
hoelzl@59092
  1080
  "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
hoelzl@59092
  1081
immler@69681
  1082
proposition interval_integral_norm:
hoelzl@59092
  1083
  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
hoelzl@59092
  1084
  shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
hoelzl@59092
  1085
    norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
ak2110@69173
  1086
  using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
ak2110@69173
  1087
  by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
hoelzl@59092
  1088
immler@69681
  1089
proposition interval_integral_norm2:
hoelzl@63329
  1090
  "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
wenzelm@61945
  1091
    norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
immler@69681
  1092
proof (induct a b rule: linorder_wlog)
hoelzl@59092
  1093
  case (sym a b) then show ?case
hoelzl@59092
  1094
    by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
hoelzl@59092
  1095
next
hoelzl@63329
  1096
  case (le a b)
hoelzl@63329
  1097
  then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
hoelzl@59092
  1098
    using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
lp15@68096
  1099
    by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
hoelzl@59092
  1100
             intro!: integral_nonneg_AE abs_of_nonneg)
hoelzl@59092
  1101
  then show ?case
hoelzl@59092
  1102
    using le by (simp add: interval_integral_norm)
hoelzl@59092
  1103
qed
hoelzl@59092
  1104
hoelzl@59092
  1105
(* TODO: should we have a library of facts like these? *)
hoelzl@59092
  1106
lemma integral_cos: "t \<noteq> 0 \<Longrightarrow> LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
hoelzl@59092
  1107
  apply (intro interval_integral_FTC_finite continuous_intros)
hoelzl@59092
  1108
  by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])
hoelzl@59092
  1109
hoelzl@59092
  1110
end