Theory HOL-Analysis.Interval_Integral

(*  Title:      HOL/Analysis/Interval_Integral.thy
    Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)

Lebesgue integral over an interval (with endpoints possibly +-∞)
*)

theory Interval_Integral (*FIX ME rename? Lebesgue  *)
  imports Equivalence_Lebesgue_Henstock_Integration
begin

definition "einterval a b = {x. a < ereal x  ereal x < b}"

lemma einterval_eq[simp]:
  shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
    and einterval_eq_Ici: "einterval (ereal a)  = {a <..}"
    and einterval_eq_Iic: "einterval (- ) (ereal b) = {..< b}"
    and einterval_eq_UNIV: "einterval (- )  = UNIV"
  by (auto simp: einterval_def)

lemma einterval_same: "einterval a a = {}"
  by (auto simp: einterval_def)

lemma einterval_iff: "x  einterval a b  a < ereal x  ereal x < b"
  by (simp add: einterval_def)

lemma einterval_nonempty: "a < b  c. c  einterval a b"
  by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex)

lemma open_einterval[simp]: "open (einterval a b)"
  by (cases a b rule: ereal2_cases)
     (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros)

lemma borel_einterval[measurable]: "einterval a b  sets borel"
  unfolding einterval_def by measurable

subsection ‹Approximating a (possibly infinite) interval›

lemma filterlim_sup1: "(LIM x F. f x :> G1)  (LIM x F. f x :> (sup G1 G2))"
 unfolding filterlim_def by (auto intro: le_supI1)

lemma ereal_incseq_approx:
  fixes a b :: ereal
  assumes "a < b"
  obtains X :: "nat  real" where "incseq X" "i. a < X i" "i. X i < b" "X  b"
proof (cases b)
  case PInf
  with a < b have "a = -  (r. a = ereal r)"
    by (cases a) auto
  moreover have "(λx. ereal (real (Suc x)))  "
    by (simp add: Lim_PInfty filterlim_sequentially_Suc) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)
  moreover have "r. (λx. ereal (r + real (Suc x)))  "
    by (simp add: filterlim_sequentially_Suc Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq)
  ultimately show thesis
    by (intro that[of "λi. real_of_ereal a + Suc i"])
       (auto simp: incseq_def PInf)
next
  case (real b')
  define d where "d = b' - (if a = - then b' - 1 else real_of_ereal a)"
  with a < b have a': "0 < d"
    by (cases a) (auto simp: real)
  moreover
  have "i r. r < b'  (b' - r) * 1 < (b' - r) * real (Suc (Suc i))"
    by (intro mult_strict_left_mono) auto
  with a < b a' have "i. a < ereal (b' - d / real (Suc (Suc i)))"
    by (cases a) (auto simp: real d_def field_simps)
  moreover
  have "(λi. b' - d / real i)  b'"
    by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1
              simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
  then have "(λi. b' - d / Suc (Suc i))  b'"
    by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2])
  ultimately show thesis
    by (intro that[of "λi. b' - d / Suc (Suc i)"])
       (auto simp: real incseq_def intro!: divide_left_mono)
qed (use a < b in auto)

lemma ereal_decseq_approx:
  fixes a b :: ereal
  assumes "a < b"
  obtains X :: "nat  real" where
    "decseq X" "i. a < X i" "i. X i < b" "X  a"
proof -
  have "-b < -a" using a < b by simp
  from ereal_incseq_approx[OF this] obtain X where
    "incseq X"
    "i. - b < ereal (X i)"
    "i. ereal (X i) < - a"
    "(λx. ereal (X x))  - a"
    by auto
  then show thesis
    apply (intro that[of "λi. - X i"])
    apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
    apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
    done
qed

proposition einterval_Icc_approximation:
  fixes a b :: ereal
  assumes "a < b"
  obtains u l :: "nat  real" where
    "einterval a b = (i. {l i .. u i})"
    "incseq u" "decseq l" "i. l i < u i" "i. a < l i" "i. u i < b"
    "l  a" "u  b"
proof -
  from dense[OF a < b] obtain c where "a < c" "c < b" by safe
  from ereal_incseq_approx[OF c < b] obtain u where u:
    "incseq u"
    "i. c < ereal (u i)"
    "i. ereal (u i) < b"
    "(λx. ereal (u x))  b"
    by auto
  from ereal_decseq_approx[OF a < c] obtain l where l:
    "decseq l"
    "i. a < ereal (l i)"
    "i. ereal (l i) < c"
    "(λx. ereal (l x))  a"
    by auto
  have "einterval a b = (i. {l i .. u i})"
  proof (auto simp: einterval_iff)
    fix x assume "a < ereal x" "ereal x < b"
    have "eventually (λi. ereal (l i) < ereal x) sequentially"
      using l(4) a < ereal x by (rule order_tendstoD)
    moreover
    have "eventually (λi. ereal x < ereal (u i)) sequentially"
      using u(4) ereal x< b by (rule order_tendstoD)
    ultimately have "eventually (λi. l i < x  x < u i) sequentially"
      by eventually_elim auto
    then show "i. l i  x  x  u i"
      by (auto intro: less_imp_le simp: eventually_sequentially)
  next
    fix x i assume "l i  x" "x  u i"
    with a < ereal (l i) ereal (u i) < b
    show "a < ereal x" "ereal x < b"
      by (auto simp flip: ereal_less_eq(3))
  qed
  moreover { fix i from less_trans[OF l i < c c < u i] have "l i < u i" by simp }
  ultimately show thesis
    by (simp add: l that u)
qed

(* TODO: in this definition, it would be more natural if einterval a b included a and b when
   they are real. *)
definitiontag important› interval_lebesgue_integral :: "real measure  ereal  ereal  (real  'a)  'a::{banach, second_countable_topology}" where
  "interval_lebesgue_integral M a b f =
    (if a  b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"

syntax
  "_ascii_interval_lebesgue_integral" :: "pttrn  real  real  real measure  real  real"
  ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)

translations
  "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (λx. f)"

definitiontag important› interval_lebesgue_integrable :: "real measure  ereal  ereal  (real  'a::{banach, second_countable_topology})  bool" where
  "interval_lebesgue_integrable M a b f =
    (if a  b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"

syntax
  "_ascii_interval_lebesgue_borel_integral" :: "pttrn  real  real  real  real"
  ("(4LBINT _=_.._. _)" [0,60,60,61] 60)

translations
  "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (λx. f)"

subsection‹Basic properties of integration over an interval›

lemma interval_lebesgue_integral_cong:
  "a  b  (x. x  einterval a b  f x = g x)  einterval a b  sets M 
    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
  by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def)

lemma interval_lebesgue_integral_cong_AE:
  "f  borel_measurable M  g  borel_measurable M 
    a  b  AE x  einterval a b in M. f x = g x  einterval a b  sets M 
    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
  by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def)

lemma interval_integrable_mirror:
  shows "interval_lebesgue_integrable lborel a b (λx. f (-x)) 
    interval_lebesgue_integrable lborel (-b) (-a) f"
proof -
  have *: "indicator (einterval a b) (- x) = (indicator (einterval (-b) (-a)) x :: real)"
    for a b :: ereal and x :: real
    by (cases a b rule: ereal2_cases) (auto simp: einterval_def split: split_indicator)
  show ?thesis
    unfolding interval_lebesgue_integrable_def
    using lborel_integrable_real_affine_iff[symmetric, of "-1" "λx. indicator (einterval _ _) x *R f x" 0]
    by (simp add: * set_integrable_def)
qed

lemma interval_lebesgue_integral_add [intro, simp]:
  fixes M a b f
  assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
  shows "interval_lebesgue_integrable M a b (λx. f x + g x)"
    and "interval_lebesgue_integral M a b (λx. f x + g x) =
         interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
    field_simps)

lemma interval_lebesgue_integral_diff [intro, simp]:
  fixes M a b f
  assumes "interval_lebesgue_integrable M a b f"
    "interval_lebesgue_integrable M a b g"
  shows "interval_lebesgue_integrable M a b (λx. f x - g x)" and
    "interval_lebesgue_integral M a b (λx. f x - g x) =
   interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def
    field_simps)

lemma interval_lebesgue_integrable_mult_right [intro, simp]:
  fixes M a b c and f :: "real  'a::{banach, real_normed_field, second_countable_topology}"
  shows "(c  0  interval_lebesgue_integrable M a b f) 
    interval_lebesgue_integrable M a b (λx. c * f x)"
  by (simp add: interval_lebesgue_integrable_def)

lemma interval_lebesgue_integrable_mult_left [intro, simp]:
  fixes M a b c and f :: "real  'a::{banach, real_normed_field, second_countable_topology}"
  shows "(c  0  interval_lebesgue_integrable M a b f) 
    interval_lebesgue_integrable M a b (λx. f x * c)"
  by (simp add: interval_lebesgue_integrable_def)

lemma interval_lebesgue_integrable_divide [intro, simp]:
  fixes M a b c and f :: "real  'a::{banach, real_normed_field, field, second_countable_topology}"
  shows "(c  0  interval_lebesgue_integrable M a b f) 
    interval_lebesgue_integrable M a b (λx. f x / c)"
  by (simp add: interval_lebesgue_integrable_def)

lemma interval_lebesgue_integral_mult_right [simp]:
  fixes M a b c and f :: "real  'a::{banach, real_normed_field, second_countable_topology}"
  shows "interval_lebesgue_integral M a b (λx. c * f x) =
    c * interval_lebesgue_integral M a b f"
  by (simp add: interval_lebesgue_integral_def)

lemma interval_lebesgue_integral_mult_left [simp]:
  fixes M a b c and f :: "real  'a::{banach, real_normed_field, second_countable_topology}"
  shows "interval_lebesgue_integral M a b (λx. f x * c) =
    interval_lebesgue_integral M a b f * c"
  by (simp add: interval_lebesgue_integral_def)

lemma interval_lebesgue_integral_divide [simp]:
  fixes M a b c and f :: "real  'a::{banach, real_normed_field, field, second_countable_topology}"
  shows "interval_lebesgue_integral M a b (λx. f x / c) =
    interval_lebesgue_integral M a b f / c"
  by (simp add: interval_lebesgue_integral_def)

lemma interval_lebesgue_integral_uminus:
  "interval_lebesgue_integral M a b (λx. - f x) = - interval_lebesgue_integral M a b f"
  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)

lemma interval_lebesgue_integral_of_real:
  "interval_lebesgue_integral M a b (λx. complex_of_real (f x)) =
    of_real (interval_lebesgue_integral M a b f)"
  unfolding interval_lebesgue_integral_def
  by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)

lemma interval_lebesgue_integral_le_eq:
  fixes a b f
  assumes "a  b"
  shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
  using assms by (auto simp: interval_lebesgue_integral_def)

lemma interval_lebesgue_integral_gt_eq:
  fixes a b f
  assumes "a > b"
  shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)

lemma interval_lebesgue_integral_gt_eq':
  fixes a b f
  assumes "a > b"
  shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def)

lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
  by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)

lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)

lemma interval_integrable_endpoints_reverse:
  "interval_lebesgue_integrable lborel a b f 
    interval_lebesgue_integrable lborel b a f"
  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)

lemma interval_integral_reflect:
  "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
proof (induct a b rule: linorder_wlog)
  case (sym a b) then show ?case
    by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
             split: if_split_asm)
next
  case (le a b) 
  have "(LBINT x:{x. - x  einterval a b}. f (- x)) = (LBINT x:einterval (- b) (- a). f (- x))"
    unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def
    by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1))
  then show ?case
    unfolding interval_lebesgue_integral_def 
    by (subst set_integral_reflect) (simp add: le)
qed

lemma interval_lebesgue_integral_0_infty:
  "interval_lebesgue_integrable M 0  f  set_integrable M {0<..} f"
  "interval_lebesgue_integral M 0  f = (LINT x:{0<..}|M. f x)"
  unfolding zero_ereal_def
  by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def)

lemma interval_integral_to_infinity_eq: "(LINT x=ereal a.. | M. f x) = (LINT x : {a<..} | M. f x)"
  unfolding interval_lebesgue_integral_def by auto

proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a  f) =
  (set_integrable M {a<..} f)"
  unfolding interval_lebesgue_integrable_def by auto

subsection‹Basic properties of integration over an interval wrt lebesgue measure›

lemma interval_integral_zero [simp]:
  fixes a b :: ereal
  shows "(LBINT x=a..b. 0) = 0"
unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
by simp

lemma interval_integral_const [intro, simp]:
  fixes a b c :: real
  shows "interval_lebesgue_integrable lborel a b (λx. c)" and "(LBINT x=a..b. c) = c * (b - a)"
  unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
  by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)

lemma interval_integral_cong_AE:
  assumes [measurable]: "f  borel_measurable borel" "g  borel_measurable borel"
  assumes "AE x  einterval (min a b) (max a b) in lborel. f x = g x"
  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
  using assms
  by (auto simp: interval_lebesgue_integral_def max_def min_def intro!: set_lebesgue_integral_cong_AE)

lemma interval_integral_cong:
  assumes "x. x  einterval (min a b) (max a b)  f x = g x"
  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
  using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_cong)

lemma interval_lebesgue_integrable_cong_AE:
    "f  borel_measurable lborel  g  borel_measurable lborel 
    AE x  einterval (min a b) (max a b) in lborel. f x = g x 
    interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
  apply (simp add: interval_lebesgue_integrable_def)
  apply (intro conjI impI set_integrable_cong_AE)
  apply (auto simp: min_def max_def)
  done

lemma interval_integrable_abs_iff:
  fixes f :: "real  real"
  shows  "f  borel_measurable lborel 
    interval_lebesgue_integrable lborel a b (λx. ¦f x¦) = interval_lebesgue_integrable lborel a b f"
  unfolding interval_lebesgue_integrable_def
  by (simp add: set_integrable_abs_iff')

lemma interval_integral_Icc:
  fixes a b :: real
  shows "a  b  (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)"
  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
           simp add: interval_lebesgue_integral_def)

lemma interval_integral_Icc':
  "a  b  (LBINT x=a..b. f x) = (LBINT x : {x. a  ereal x  ereal x  b}. f x)"
  by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"]
           simp add: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_Ioc:
  "a  b  (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)"
  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
           simp add: interval_lebesgue_integral_def einterval_iff)

(* TODO: other versions as well? *) (* Yes: I need the Icc' version. *)
lemma interval_integral_Ioc':
  "a  b  (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x  ereal x  b}. f x)"
  by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"]
           simp add: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_Ico:
  "a  b  (LBINT x=a..b. f x) = (LBINT x : {a..<b}. f x)"
  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
           simp add: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_Ioi:
  "¦a¦ <   (LBINT x=a... f x) = (LBINT x : {real_of_ereal a <..}. f x)"
  by (auto simp: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_Ioo:
  "a  b  ¦a¦ <  ==> ¦b¦ <   (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
  by (auto simp: interval_lebesgue_integral_def einterval_iff)

lemma interval_integral_discrete_difference:
  fixes f :: "real  'b::{banach, second_countable_topology}" and a b :: ereal
  assumes "countable X"
  and eq: "x. a  b  a < x  x < b  x  X  f x = g x"
  and anti_eq: "x. b  a  b < x  x < a  x  X  f x = g x"
  assumes "x. x  X  emeasure M {x} = 0" "x. x  X  {x}  sets M"
  shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
  unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
  apply (intro if_cong refl arg_cong[where f="λx. - x"] integral_discrete_difference[of X] assms)
  apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
  done

lemma interval_integral_sum:
  fixes a b c :: ereal
  assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
  shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
proof -
  let ?I = "λa b. LBINT x=a..b. f x"
  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a  b" "b  c"
    then have ord: "a  b" "b  c" "a  c" and f': "set_integrable lborel (einterval a c) f"
      by (auto simp: interval_lebesgue_integrable_def)
    then have f: "set_borel_measurable borel (einterval a c) f"
      unfolding set_integrable_def set_borel_measurable_def
      by (drule_tac borel_measurable_integrable) simp
    have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b  einterval b c. f x)"
    proof (rule set_integral_cong_set)
      show "AE x in lborel. (x  einterval a b  einterval b c) = (x  einterval a c)"
        using AE_lborel_singleton[of "real_of_ereal b"] ord
        by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
      show "set_borel_measurable lborel (einterval a c) f" "set_borel_measurable lborel (einterval a b  einterval b c) f"
        unfolding set_borel_measurable_def
        using ord by (auto simp: einterval_iff intro!: set_borel_measurable_subset[OF f, unfolded set_borel_measurable_def])
    qed
    also have " = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
      using ord
      by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
    finally have "?I a b + ?I b c = ?I a c"
      using ord by (simp add: interval_lebesgue_integral_def)
  } note 1 = this
  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a  b" "b  c"
    from 1[OF this] have "?I b c + ?I a b = ?I a c"
      by (metis add.commute)
  } note 2 = this
  have 3: "a b. b  a  (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)"
    by (rule interval_integral_endpoints_reverse)
  show ?thesis
    using integrable
    apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
    apply simp_all (* remove some looping cases *)
    by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
qed

lemma interval_integrable_isCont:
  fixes a b and f :: "real  'a::{banach, second_countable_topology}"
  shows "(x. min a b  x  x  max a b  isCont f x) 
    interval_lebesgue_integrable lborel a b f"
proof (induct a b rule: linorder_wlog)
  case (le a b) then show ?case
    unfolding interval_lebesgue_integrable_def set_integrable_def
    by (auto simp: interval_lebesgue_integrable_def
        intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]]
        continuous_at_imp_continuous_on)
qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])

lemma interval_integrable_continuous_on:
  fixes a b :: real and f
  assumes "a  b" and "continuous_on {a..b} f"
  shows "interval_lebesgue_integrable lborel a b f"
using assms unfolding interval_lebesgue_integrable_def apply simp
  by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto)

lemma interval_integral_eq_integral:
  fixes f :: "real  'a::euclidean_space"
  shows "a  b  set_integrable lborel {a..b} f  LBINT x=a..b. f x = integral {a..b} f"
  by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral)

lemma interval_integral_eq_integral':
  fixes f :: "real  'a::euclidean_space"
  shows "a  b  set_integrable lborel (einterval a b) f  LBINT x=a..b. f x = integral (einterval a b) f"
  by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)


subsection‹General limit approximation arguments›

proposition interval_integral_Icc_approx_nonneg:
  fixes a b :: ereal
  assumes "a < b"
  fixes u l :: "nat  real"
  assumes  approx: "einterval a b = (i. {l i .. u i})"
    "incseq u" "decseq l" "i. l i < u i" "i. a < l i" "i. u i < b"
    "l  a" "u  b"
  fixes f :: "real  real"
  assumes f_integrable: "i. set_integrable lborel {l i..u i} f"
  assumes f_nonneg: "AE x in lborel. a < ereal x  ereal x < b  0  f x"
  assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
  assumes lbint_lim: "(λi. LBINT x=l i.. u i. f x)  C"
  shows
    "set_integrable lborel (einterval a b) f"
    "(LBINT x=a..b. f x) = C"
proof -
  have 1 [unfolded set_integrable_def]: "i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
  have 2: "AE x in lborel. mono (λn. indicator {l n..u n} x *R f x)"
  proof -
     from f_nonneg have "AE x in lborel. i. l i  x  x  u i  0  f x"
      by eventually_elim
         (metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans)
    then show ?thesis
      apply eventually_elim
      apply (auto simp: mono_def split: split_indicator)
      apply (metis approx(3) decseqD order_trans)
      apply (metis approx(2) incseqD order_trans)
      done
  qed
  have 3: "AE x in lborel. (λi. indicator {l i..u i} x *R f x)  indicator (einterval a b) x *R f x"
  proof -
    { fix x i assume "l i  x" "x  u i"
      then have "eventually (λi. l i  x  x  u i) sequentially"
        apply (auto simp: eventually_sequentially intro!: exI[of _ i])
        apply (metis approx(3) decseqD order_trans)
        apply (metis approx(2) incseqD order_trans)
        done
      then have "eventually (λi. f x * indicator {l i..u i} x = f x) sequentially"
        by eventually_elim auto }
    then show ?thesis
      unfolding approx(1) by (auto intro!: AE_I2 tendsto_eventually split: split_indicator)
  qed
  have 4: "(λi.  x. indicator {l i..u i} x *R f x lborel)  C"
    using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
  have 5: "(λx. indicat_real (einterval a b) x *R f x)  borel_measurable lborel"
    using f_measurable set_borel_measurable_def by blast
  have "(LBINT x=a..b. f x) = lebesgue_integral lborel (λx. indicator (einterval a b) x *R f x)"
    using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
  also have " = C"
    by (rule integral_monotone_convergence [OF 1 2 3 4 5])
  finally show "(LBINT x=a..b. f x) = C" .
  show "set_integrable lborel (einterval a b) f"
    unfolding set_integrable_def
    by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
qed

proposition interval_integral_Icc_approx_integrable:
  fixes u l :: "nat  real" and a b :: ereal
  fixes f :: "real  'a::{banach, second_countable_topology}"
  assumes "a < b"
  assumes  approx: "einterval a b = (i. {l i .. u i})"
    "incseq u" "decseq l" "i. l i < u i" "i. a < l i" "i. u i < b"
    "l  a" "u  b"
  assumes f_integrable: "set_integrable lborel (einterval a b) f"
  shows "(λi. LBINT x=l i.. u i. f x)  (LBINT x=a..b. f x)"
proof -
  have "(λi. LBINT x:{l i.. u i}. f x)  (LBINT x:einterval a b. f x)"
    unfolding set_lebesgue_integral_def
  proof (rule integral_dominated_convergence)
    show "integrable lborel (λx. norm (indicator (einterval a b) x *R f x))"
      using f_integrable integrable_norm set_integrable_def by blast
    show "(λx. indicat_real (einterval a b) x *R f x)  borel_measurable lborel"
      using f_integrable by (simp add: set_integrable_def)
    then show "i. (λx. indicat_real {l i..u i} x *R f x)  borel_measurable lborel"
      by (rule set_borel_measurable_subset [unfolded set_borel_measurable_def]) (auto simp: approx)
    show "i. AE x in lborel. norm (indicator {l i..u i} x *R f x)  norm (indicator (einterval a b) x *R f x)"
      by (intro AE_I2) (auto simp: approx split: split_indicator)
    show "AE x in lborel. (λi. indicator {l i..u i} x *R f x)  indicator (einterval a b) x *R f x"
    proof (intro AE_I2 tendsto_intros tendsto_eventually)
      fix x
      { fix i assume "l i  x" "x  u i"
        with incseq u[THEN incseqD, of i] decseq l[THEN decseqD, of i]
        have "eventually (λi. l i  x  x  u i) sequentially"
          by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
      then show "eventually (λxa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially"
        using approx order_tendstoD(2)[OF l  a, of x] order_tendstoD(1)[OF u  b, of x]
        by (auto split: split_indicator)
    qed
  qed
  with a < b i. l i < u i show ?thesis
    by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
qed

subsection‹A slightly stronger Fundamental Theorem of Calculus›

text‹Three versions: first, for finite intervals, and then two versions for
    arbitrary intervals.›

(*
  TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
*)

lemma interval_integral_FTC_finite:
  fixes f F :: "real  'a::euclidean_space" and a b :: real
  assumes f: "continuous_on {min a b..max a b} f"
  assumes F: "x. min a b  x  x  max a b  (F has_vector_derivative (f x)) (at x within
    {min a b..max a b})"
  shows "(LBINT x=a..b. f x) = F b - F a"
proof (cases "a  b")
  case True
  have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *R f x)"
    by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
  also have " = F b - F a"
  proof (rule integral_FTC_atLeastAtMost [OF True])
    show "continuous_on {a..b} f"
      using True f by linarith
    show "x. a  x; x  b  (F has_vector_derivative f x) (at x within {a..b})"
      by (metis F True max.commute max_absorb1 min_def)
  qed
  finally show ?thesis .
next
  case False
  then have "b  a"
    by simp
  have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *R f x)"
    by (simp add: b  a interval_integral_Icc set_lebesgue_integral_def)
  also have " = F b - F a"
  proof (subst integral_FTC_atLeastAtMost [OF b  a])
    show "continuous_on {b..a} f"
      using False f by linarith
    show "x. b  x; x  a
          (F has_vector_derivative f x) (at x within {b..a})"
      by (metis F False max_def min_def)
  qed auto
  finally show ?thesis
    by (metis interval_integral_endpoints_reverse)
qed


lemma interval_integral_FTC_nonneg:
  fixes f F :: "real  real" and a b :: ereal
  assumes "a < b"
  assumes F: "x. a < ereal x  ereal x < b  DERIV F x :> f x"
  assumes f: "x. a < ereal x  ereal x < b  isCont f x"
  assumes f_nonneg: "AE x in lborel. a < ereal x  ereal x < b  0  f x"
  assumes A: "((F  real_of_ereal)  A) (at_right a)"
  assumes B: "((F  real_of_ereal)  B) (at_left b)"
  shows
    "set_integrable lborel (einterval a b) f"
    "(LBINT x=a..b. f x) = B - A"
proof -
  obtain u l where approx:
    "einterval a b = (i. {l i .. u i})"
    "incseq u" "decseq l" "i. l i < u i" "i. a < l i" "i. u i < b"
    "l  a" "u  b" 
    by (blast intro: einterval_Icc_approximation[OF a < b])
  have aless[simp]: "x i. l i  x  a < ereal x"
    by (rule order_less_le_trans, rule approx, force)
  have lessb[simp]: "x i. x  u i  ereal x < b"
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
  have cf: "i. continuous_on {min (l i) (u i)..max (l i) (u i)} f"
    using approx f by (intro continuous_at_imp_continuous_on strip) auto
  have FTCi: "i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
    apply (intro interval_integral_FTC_finite cf DERIV_subset [OF F])
    by (smt (verit) F aless approx(4) has_real_derivative_iff_has_vector_derivative has_vector_derivative_at_within lessb)
  have 1: "i. set_integrable lborel {l i..u i} f"
    by (meson aless lessb assms(3) atLeastAtMost_iff borel_integrable_atLeastAtMost' continuous_at_imp_continuous_on)
  have 2: "set_borel_measurable lborel (einterval a b) f"
    unfolding set_borel_measurable_def
    by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
             simp: continuous_on_eq_continuous_at einterval_iff f)
  have "(λx. F (l x))  A"
    using A approx unfolding tendsto_at_iff_sequentially comp_def
    by (force elim!: allE[of _ "λi. ereal (l i)"])
  moreover have "(λx. F (u x))  B"
    using B approx unfolding tendsto_at_iff_sequentially comp_def
    by (force elim!: allE[of _ "λi. ereal (u i)"])
  ultimately have 3: "(λi. LBINT x=l i..u i. f x)  B - A"
    by (simp add: FTCi tendsto_diff)
  show "(LBINT x=a..b. f x) = B - A"
    by (rule interval_integral_Icc_approx_nonneg [OF a < b approx 1 f_nonneg 2 3])
  show "set_integrable lborel (einterval a b) f"
    by (rule interval_integral_Icc_approx_nonneg [OF a < b approx 1 f_nonneg 2 3])
qed

theorem interval_integral_FTC_integrable:
  fixes f F :: "real  'a::euclidean_space" and a b :: ereal
  assumes "a < b"
  assumes F: "x. a < ereal x  ereal x < b  (F has_vector_derivative f x) (at x)"
  assumes f: "x. a < ereal x  ereal x < b  isCont f x"
  assumes f_integrable: "set_integrable lborel (einterval a b) f"
  assumes A: "((F  real_of_ereal)  A) (at_right a)"
  assumes B: "((F  real_of_ereal)  B) (at_left b)"
  shows "(LBINT x=a..b. f x) = B - A"
proof -
  obtain u l where approx:
    "einterval a b = (i. {l i .. u i})"
    "incseq u" "decseq l" "i. l i < u i" "i. a < l i" "i. u i < b"
    "l  a" "u  b" 
    by (blast intro: einterval_Icc_approximation[OF a < b])
  have [simp]: "x i. l i  x  a < ereal x"
    by (rule order_less_le_trans, rule approx, force)
  have [simp]: "x i. x  u i  ereal x < b"
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
  have FTCi: "i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
    using assms approx
    by (auto simp: less_imp_le min_def max_def
             intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
             intro: has_vector_derivative_at_within)
  have "(λi. LBINT x=l i..u i. f x)  B - A"
    unfolding FTCi
  proof (intro tendsto_intros)
    show "(λx. F (l x))  A"
      using A approx unfolding tendsto_at_iff_sequentially comp_def
      by (elim allE[of _ "λi. ereal (l i)"], auto)
    show "(λx. F (u x))  B"
      using B approx unfolding tendsto_at_iff_sequentially comp_def
      by (elim allE[of _ "λi. ereal (u i)"], auto)
  qed
  moreover have "(λi. LBINT x=l i..u i. f x)  (LBINT x=a..b. f x)"
    by (rule interval_integral_Icc_approx_integrable [OF a < b approx f_integrable])
  ultimately show ?thesis
    by (elim LIMSEQ_unique)
qed

(*
  The second Fundamental Theorem of Calculus and existence of antiderivatives on an
  einterval.
*)

theorem interval_integral_FTC2:
  fixes a b c :: real and f :: "real  'a::euclidean_space"
  assumes "a  c" "c  b"
  and contf: "continuous_on {a..b} f"
  fixes x :: real
  assumes "a  x" and "x  b"
  shows "((λu. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
proof -
  let ?F = "(λu. LBINT y=a..u. f y)"
  have intf: "set_integrable lborel {a..b} f"
    by (rule borel_integrable_atLeastAtMost', rule contf)
  have "((λu. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
    using a  x x  b 
    by (auto intro: integral_has_vector_derivative continuous_on_subset [OF contf])
  then have "((λu. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
    by simp
  then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
    by (rule has_vector_derivative_weaken)
       (auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf])
  then have "((λx. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})"
    by (auto intro!: derivative_eq_intros)
  then show ?thesis
  proof (rule has_vector_derivative_weaken)
    fix u assume "u  {a .. b}"
    then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
      using assms
      apply (intro interval_integral_sum)
      apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def)
      by (rule set_integrable_subset [OF intf], auto simp: min_def max_def)
  qed (insert assms, auto)
qed

proposition einterval_antiderivative:
  fixes a b :: ereal and f :: "real  'a::euclidean_space"
  assumes "a < b" and contf: "x :: real. a < x  x < b  isCont f x"
  shows "F. x :: real. a < x  x < b  (F has_vector_derivative f x) (at x)"
proof -
  from einterval_nonempty [OF a < b] obtain c :: real where [simp]: "a < c" "c < b"
    by (auto simp: einterval_def)
  let ?F = "(λu. LBINT y=c..u. f y)"
  show ?thesis
  proof (rule exI, clarsimp)
    fix x :: real
    assume [simp]: "a < x" "x < b"
    have 1: "a < min c x" by simp
    from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x"
      by (auto simp: einterval_def)
    have 2: "max c x < b" by simp
    from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
      by (auto simp: einterval_def)
    have "(?F has_vector_derivative f x) (at x within {d<..<e})"
    proof (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
      have "continuous_on {d..e} f"
      proof (intro continuous_at_imp_continuous_on ballI contf; clarsimp)
        show "x. d  x; x  e  a < ereal x"
          using a < ereal d ereal_less_ereal_Ex by auto
        show "x. d  x; x  e  ereal x < b"
          using ereal e < b ereal_less_eq(3) le_less_trans by blast
      qed
      then show "(?F has_vector_derivative f x) (at x within {d..e})"
        by (intro interval_integral_FTC2) (use d < c c < e d < x x < e in linarith+)
    qed auto
    then show "(?F has_vector_derivative f x) (at x)"
      by (force simp: has_vector_derivative_within_open [of _ "{d<..<e}"])
  qed
qed

subsection‹The substitution theorem›

text‹Once again, three versions: first, for finite intervals, and then two versions for
    arbitrary intervals.›

theorem interval_integral_substitution_finite:
  fixes a b :: real and f :: "real  'a::euclidean_space"
  assumes "a  b"
  and derivg: "x. a  x  x  b  (g has_real_derivative (g' x)) (at x within {a..b})"
  and contf : "continuous_on (g ` {a..b}) f"
  and contg': "continuous_on {a..b} g'"
  shows "(LBINT x=a..b. g' x *R f (g x)) = (LBINT y=g a..g b. f y)"
proof-
  have v_derivg: "x. a  x  x  b  (g has_vector_derivative (g' x)) (at x within {a..b})"
    using derivg unfolding has_real_derivative_iff_has_vector_derivative .
  then have contg [simp]: "continuous_on {a..b} g"
    by (rule continuous_on_vector_derivative) auto
  have 1: "x{a..b}. u = g x" if "min (g a) (g b)  u" "u  max (g a) (g b)" for u
    by (cases "g a  g b") (use that assms IVT' [of g a u b]  IVT2' [of g b u a]  in auto simp: min_def max_def)
  obtain c d where g_im: "g ` {a..b} = {c..d}" and "c  d"
    by (metis continuous_image_closed_interval contg a  b)
  obtain F where derivF:
         "x. a  x; x  b  (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" 
    using continuous_on_subset [OF contf] g_im
      by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset)
  have contfg: "continuous_on {a..b} (λx. f (g x))"
    by (blast intro: continuous_on_compose2 contf contg)
  have "continuous_on {a..b} (λx. g' x *R f (g x))"
    by (auto intro!: continuous_on_scaleR contg' contfg)
  then have "(LBINT x. indicat_real {a..b} x *R g' x *R f (g x)) = F (g b) - F (g a)"
    using integral_FTC_atLeastAtMost [OF a  b vector_diff_chain_within[OF v_derivg derivF]]
    by force
  then have "LBINT x=a..b. g' x *R f (g x) = F (g b) - F (g a)"
    by (simp add: assms interval_integral_Icc set_lebesgue_integral_def)
  moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
  proof (rule interval_integral_FTC_finite)
    show "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
      by (rule continuous_on_subset [OF contf]) (auto simp: image_def 1)
    show "(F has_vector_derivative f y) (at y within {min (g a) (g b)..max (g a) (g b)})" 
      if y: "min (g a) (g b)  y" "y  max (g a) (g b)" for y
    proof -
      obtain x where "a  x" "x  b" "y = g x"
        using 1 y by force
      then show ?thesis
        by (auto simp: image_def intro!: 1  has_vector_derivative_within_subset [OF derivF])
    qed
  qed
  ultimately show ?thesis by simp
qed

(* TODO: is it possible to lift the assumption here that g' is nonnegative? *)

theorem interval_integral_substitution_integrable:
  fixes f :: "real  'a::euclidean_space" and a b u v :: ereal
  assumes "a < b"
  and deriv_g: "x. a < ereal x  ereal x < b  DERIV g x :> g' x"
  and contf: "x. a < ereal x  ereal x < b  isCont f (g x)"
  and contg': "x. a < ereal x  ereal x < b  isCont g' x"
  and g'_nonneg: "x. a  ereal x  ereal x  b  0  g' x"
  and A: "((ereal  g  real_of_ereal)  A) (at_right a)"
  and B: "((ereal  g  real_of_ereal)  B) (at_left b)"
  and integrable: "set_integrable lborel (einterval a b) (λx. g' x *R f (g x))"
  and integrable2: "set_integrable lborel (einterval A B) (λx. f x)"
  shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *R f (g x))"
proof -
  obtain u l where approx [simp]:
    "einterval a b = (i. {l i .. u i})"
    "incseq u" "decseq l" "i. l i < u i" "i. a < l i" "i. u i < b"
    "l  a" "u  b" 
    by (blast intro: einterval_Icc_approximation[OF a < b])
  note less_imp_le [simp]
  have [simp]: "x i. l i  x  a < ereal x"
    by (rule order_less_le_trans, rule approx, force)
  have [simp]: "x i. x  u i  ereal x < b"
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
  then have lessb[simp]: "i. l i < b"
    using approx(4) less_eq_real_def by blast
  have [simp]: "i. a < u i"
    by (rule order_less_trans, rule approx, auto, rule approx)
  have lle[simp]: "i j. i  j  l j  l i" by (rule decseqD, rule approx)
  have [simp]: "i j. i  j  u i  u j" by (rule incseqD, rule approx)
  have g_nondec [simp]: "g x  g y" if "a < x" "x  y" "y < b" for x y
  proof (rule DERIV_nonneg_imp_nondecreasing [OF x  y], intro exI conjI)
    show "u. x  u  u  y  (g has_real_derivative g' u) (at u)"
      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
    show "u. x  u  u  y  0  g' u"
      by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
  qed
  have "A  B" and un: "einterval A B = (i. {g(l i)<..<g(u i)})"
  proof -
    have A2: "(λi. g (l i))  A"
      using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
      by (drule_tac x = "λi. ereal (l i)" in spec, auto)
    hence A3: "i. g (l i)  A"
      by (intro decseq_ge, auto simp: decseq_def)
    have B2: "(λi. g (u i))  B"
      using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
      by (drule_tac x = "λi. ereal (u i)" in spec, auto)
    hence B3: "i. g (u i)  B"
      by (intro incseq_le, auto simp: incseq_def)
    have "ereal (g (l 0))  ereal (g (u 0))"
      by auto
    then show "A  B"
      by (meson A3 B3 order.trans)
    { fix x :: real
      assume "A < x" and "x < B"
      then have "eventually (λi. ereal (g (l i)) < x  x < ereal (g (u i))) sequentially"
        by (fast intro: eventually_conj order_tendstoD A2 B2)
      hence "i. g (l i) < x  x < g (u i)"
        by (simp add: eventually_sequentially, auto)
    } note AB = this
    show "einterval A B = (i. {g(l i)<..<g(u i)})"
    proof
      show "einterval A B  (i. {g(l i)<..<g(u i)})"
        by (auto simp: einterval_def AB)
      show "(i. {g(l i)<..<g(u i)})  einterval A B"
      proof (clarsimp simp add: einterval_def, intro conjI)
        show "x i. g (l i) < x; x < g (u i)  A < ereal x"
          using A3 le_ereal_less by blast
        show "x i. g (l i) < x; x < g (u i)  ereal x < B"
          using B3 ereal_le_less by blast
      qed
    qed
  qed
  (* finally, the main argument *)
  have eq1: "(LBINT x=l i.. u i. g' x *R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
    apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
    unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
         apply (auto intro!: continuous_at_imp_continuous_on contf contg')
    done
  have "(λi. LBINT x=l i..u i. g' x *R f (g x))  (LBINT x=a..b. g' x *R f (g x))"
    using approx(4) a < b integrable interval_integral_Icc_approx_integrable by fastforce
  hence 2: "(λi. (LBINT y=g (l i)..g (u i). f y))  (LBINT x=a..b. g' x *R f (g x))"
    by (simp add: eq1)
  have incseq: "incseq (λi. {g (l i)<..<g (u i)})"
    apply (clarsimp simp: incseq_def, intro conjI)
    using lessb lle approx(5) g_nondec le_less_trans apply blast
    by (force intro: less_le_trans)
  have "(λi. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)
         set_lebesgue_integral lborel (einterval A B) f"
    unfolding un  by (rule set_integral_cont_up) (use incseq  integrable2 un in auto)
  then have "(λi. (LBINT y=g (l i)..g (u i). f y))  (LBINT x = A..B. f x)"
    by (simp add: interval_lebesgue_integral_le_eq A  B)
  thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
qed

(* TODO: the last two proofs are only slightly different. Factor out common part?
   An alternative: make the second one the main one, and then have another lemma
   that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)

theorem interval_integral_substitution_nonneg:
  fixes f g g':: "real  real" and a b u v :: ereal
  assumes "a < b"
  and deriv_g: "x. a < ereal x  ereal x < b  DERIV g x :> g' x"
  and contf: "x. a < ereal x  ereal x < b  isCont f (g x)"
  and contg': "x. a < ereal x  ereal x < b  isCont g' x"
  and f_nonneg: "x. a < ereal x  ereal x < b  0  f (g x)" (* TODO: make this AE? *)
  and g'_nonneg: "x. a  ereal x  ereal x  b  0  g' x"
  and A: "((ereal  g  real_of_ereal)  A) (at_right a)"
  and B: "((ereal  g  real_of_ereal)  B) (at_left b)"
  and integrable_fg: "set_integrable lborel (einterval a b) (λx. f (g x) * g' x)"
  shows
    "set_integrable lborel (einterval A B) f"
    "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
proof -
  from einterval_Icc_approximation[OF a < b] obtain u l where approx [simp]:
    "einterval a b = (i. {l i..u i})"
    "incseq u"
    "decseq l"
    "i. l i < u i"
    "i. a < ereal (l i)"
    "i. ereal (u i) < b"
    "(λx. ereal (l x))  a"
    "(λx. ereal (u x))  b" by this auto
  have aless[simp]: "x i. l i  x  a < ereal x"
    by (rule order_less_le_trans, rule approx, force)
  have lessb[simp]: "x i. x  u i  ereal x < b"
    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
  have llb[simp]: "i. l i < b"
    using lessb approx(4) less_eq_real_def by blast
  have alu[simp]: "i. a < u i"
    by (rule order_less_trans, rule approx, auto, rule approx)
  have [simp]: "i j. i  j  l j  l i" by (rule decseqD, rule approx)
  have uleu[simp]: "i j. i  j  u i  u j" by (rule incseqD, rule approx)
  have g_nondec [simp]: "g x  g y" if "a < x" "x  y" "y < b" for x y
  proof (rule DERIV_nonneg_imp_nondecreasing [OF x  y], intro exI conjI)
    show "u. x  u  u  y  (g has_real_derivative g' u) (at u)"
      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
    show "u. x  u  u  y  0  g' u"
      by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
  qed
  have "A  B" and un: "einterval A B = (i. {g(l i)<..<g(u i)})"
  proof -
    have A2: "(λi. g (l i))  A"
      using A by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "λi. ereal (l i)"])
    hence A3: "i. g (l i)  A"
      by (intro decseq_ge, auto simp: decseq_def)
    have B2: "(λi. g (u i))  B"
      using B by (force simp: einterval_def tendsto_at_iff_sequentially comp_def elim!: allE[where x = "λi. ereal (u i)"])
    hence B3: "i. g (u i)  B"
      by (intro incseq_le, auto simp: incseq_def)
    have "ereal (g (l 0))  ereal (g (u 0))"
      by (auto simp: less_imp_le)
    then show "A  B"
      by (meson A3 B3 order.trans)
    { fix x :: real
      assume "A < x" and "x < B"
      then have "eventually (λi. ereal (g (l i)) < x  x < ereal (g (u i))) sequentially"
        by (fast intro: eventually_conj order_tendstoD A2 B2)
      hence "i. g (l i) < x  x < g (u i)"
        by (simp add: eventually_sequentially, auto)
    } note AB = this
    show "einterval A B = (i. {g(l i)<..<g(u i)})"
    proof
      show "einterval A B  (i. {g (l i)<..<g (u i)})"
        by (auto simp: einterval_def AB)
      show "(i. {g (l i)<..<g (u i)})  einterval A B"
        using A3 B3 by (force simp: einterval_def intro: le_ereal_less ereal_le_less)
    qed
  qed
    (* finally, the main argument *)
  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
  proof -
    have "(LBINT x=l i.. u i. g' x *R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
      apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
      unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
           apply (auto simp: less_imp_le intro!: continuous_at_imp_continuous_on contf contg')
      done
    then show ?thesis
      by (simp add: ac_simps)
  qed
  have incseq: "incseq (λi. {g (l i)<..<g (u i)})"
    apply (clarsimp simp: incseq_def, intro conjI)
    apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
    using alu uleu approx(6) g_nondec less_le_trans by blast
  have img: "c  l i. c  u i  x = g c" if "g (l i)  x" "x  g (u i)" for x i
  proof -
    have "continuous_on {l i..u i} g"
      by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on)
    with that show ?thesis
      using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
  qed
  have "continuous_on {g (l i)..g (u i)} f" for i
    using contf img by (force simp add: intro!: continuous_at_imp_continuous_on)
  then have int_f: "i. set_integrable lborel {g (l i)<..<g (u i)} f"
    by (rule set_integrable_subset [OF borel_integrable_atLeastAtMost']) (auto intro: less_imp_le)
  have integrable: "set_integrable lborel (i. {g (l i)<..<g (u i)}) f"
  proof (intro pos_integrable_to_top incseq int_f)
    let ?l = "(LBINT x=a..b. f (g x) * g' x)"
    have "(λi. LBINT x=l i..u i. f (g x) * g' x)  ?l"
      by (intro assms interval_integral_Icc_approx_integrable [OF a < b approx])
    hence "(λi. (LBINT y=g (l i)..g (u i). f y))  ?l"
      by (simp add: eq1)
    then show "(λi. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f)  ?l"
      unfolding interval_lebesgue_integral_def by (auto simp: less_imp_le)
    have "x i. g (l i)  x  x  g (u i)  0  f x"
      using aless f_nonneg img lessb by blast
    then show "x i. x  {g (l i)<..<g (u i)}  0  f x"
      using less_eq_real_def by auto
  qed (auto simp: greaterThanLessThan_borel)
  thus "set_integrable lborel (einterval A B) f"
    by (simp add: un)

  have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *R f (g x))"
  proof (rule interval_integral_substitution_integrable)
    show "set_integrable lborel (einterval a b) (λx. g' x *R f (g x))"
      using integrable_fg by (simp add: ac_simps)
  qed fact+
  then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
    by (simp add: ac_simps)
qed


syntax "_complex_lebesgue_borel_integral" :: "pttrn  real  complex"
  ("(2CLBINT _. _)" [0,60] 60)

translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (λx. f)"

syntax "_complex_set_lebesgue_borel_integral" :: "pttrn  real set  real  complex"
  ("(3CLBINT _:_. _)" [0,60,61] 60)

translations
  "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (λx. f)"

abbreviation complex_interval_lebesgue_integral ::
    "real measure  ereal  ereal  (real  complex)  complex" where
  "complex_interval_lebesgue_integral M a b f  interval_lebesgue_integral M a b f"

abbreviation complex_interval_lebesgue_integrable ::
  "real measure  ereal  ereal  (real  complex)  bool" where
  "complex_interval_lebesgue_integrable M a b f  interval_lebesgue_integrable M a b f"

syntax
  "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn  ereal  ereal  real  complex"
  ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)

translations
  "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (λx. f)"

proposition interval_integral_norm:
  fixes f :: "real  'a :: {banach, second_countable_topology}"
  shows "interval_lebesgue_integrable lborel a b f  a  b 
    norm (LBINT t=a..b. f t)  LBINT t=a..b. norm (f t)"
  using integral_norm_bound[of lborel "λx. indicator (einterval a b) x *R f x"]
  by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)

proposition interval_integral_norm2:
  "interval_lebesgue_integrable lborel a b f 
    norm (LBINT t=a..b. f t)  ¦LBINT t=a..b. norm (f t)¦"
proof (induct a b rule: linorder_wlog)
  case (sym a b) then show ?case
    by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
next
  case (le a b)
  then have "¦LBINT t=a..b. norm (f t)¦ = LBINT t=a..b. norm (f t)"
    using integrable_norm[of lborel "λx. indicator (einterval a b) x *R f x"]
    by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
             intro!: integral_nonneg_AE abs_of_nonneg)
  then show ?case
    using le by (simp add: interval_integral_norm)
qed

(* TODO: should we have a library of facts like these? *)
lemma integral_cos: "t  0  LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
  apply (intro interval_integral_FTC_finite continuous_intros)
  by (auto intro!: derivative_eq_intros simp: has_real_derivative_iff_has_vector_derivative[symmetric])

end