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