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