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