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