Quelle  Gauge_Integration.thy   Sprache: Isabelle

(*  Author:     Jacques D. Fleuriot, University of Edinburgh
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004

    Replaced by ~~/src/HOL/Analysis/Henstock_Kurzweil_Integration and
    Bochner_Integration.
*)

section‹Theory of Integration on real intervals›

theory Gauge_Integration
imports Complex_Main
begin

text ‹

\textbf{Attention}: This theory defines the Integration on real
intervals.  This is just a example theory for historical / expository interests.
A better replacement is found in the Multivariate Analysis library. This defines
the gauge integral on real vector spaces and in the Real Integral theory
is a specialization to the integral on arbitrary real intervals.  The
Multivariate Analysis package also provides a better support for analysis on
integrals.

›

text‹We follow John Harrison in formalizing the Gauge integral.›

subsection ‹Gauges›

definition
  gauge :: "[real set, real => real] => bool" where
  "gauge E g = (\x\E. 0 < g(x))"


subsection ‹Gauge-fine divisions›

inductive
  fine :: "[real \ real, real \ real, (real \ real \ real) list] \ bool"
for
  δ :: "real \ real"
where
  fine_Nil:
    "fine \ (a, a) []"
| fine_Cons:
    "\fine \ (b, c) D; a < b; a \ x; x \ b; b - a < \ x\
      ==> fine δ (a, c) ((a, x, b) # D)"

lemmas fine_induct [induct set: fine] =
  fine.induct [of "\" "(a,b)" "D" "case_prod P", unfolded split_conv] for δ a b D P

lemma fine_single:
  "\a < b; a \ x; x \ b; b - a < \ x\ \ fine \ (a, b) [(a, x, b)]"
by (rule fine_Cons [OF fine_Nil])

lemma fine_append:
  "\fine \ (a, b) D; fine \ (b, c) D'\ \ fine \ (a, c) (D @ D')"
by (induct set: fine, simp, simp add: fine_Cons)

lemma fine_imp_le: "fine \ (a, b) D \ a \ b"
by (induct set: fine, simp_all)

lemma nonempty_fine_imp_less: "\fine \ (a, b) D; D \ []\ \ a < b"
apply (induct set: fine, simp)
apply (drule fine_imp_le, simp)
done

lemma fine_Nil_iff: "fine \ (a, b) [] \ a = b"
by (auto elim: fine.cases intro: fine.intros)

lemma fine_same_iff: "fine \ (a, a) D \ D = []"
proof
  assume "fine \ (a, a) D" thus "D = []"
    by (metis nonempty_fine_imp_less less_irrefl)
next
  assume "D = []" thus "fine \ (a, a) D"
    by (simp add: fine_Nil)
qed

lemma empty_fine_imp_eq: "\fine \ (a, b) D; D = []\ \ a = b"
by (simp add: fine_Nil_iff)

lemma mem_fine:
  "\fine \ (a, b) D; (u, x, v) \ set D\ \ u < v \ u \ x \ x \ v"
by (induct set: fine, simp, force)

lemma mem_fine2: "\fine \ (a, b) D; (u, z, v) \ set D\ \ a \ u \ v \ b"
apply (induct arbitrary: z u v set: fine, auto)
apply (simp add: fine_imp_le)
apply (erule order_trans [OF less_imp_le], simp)
done

lemma mem_fine3: "\fine \ (a, b) D; (u, z, v) \ set D\ \ v - u < \ z"
by (induct arbitrary: z u v set: fine) auto

lemma BOLZANO:
  fixes P :: "real \ real \ bool"
  assumes 1: "a \ b"
  assumes 2: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c"
  assumes 3: "\x. \d>0. \a b. a \ x & x \ b & (b-a) < d \ P a b"
  shows "P a b"
  using 1 2 3 by (rule Bolzano)

text‹We can always find a division that is fine wrt any gauge›

lemma fine_exists:
  assumes "a \ b" and "gauge {a..b} \" shows "\D. fine \ (a, b) D"
proof -
  {
    fix u v :: real assume "u \ v"
    have "a \ u \ v \ b \ \D. fine \ (u, v) D"
      apply (induct u v rule: BOLZANO, rule ‹u ≤ v›)
       apply (simp, fast intro: fine_append)
      apply (case_tac "a \ x \ x \ b")
       apply (rule_tac x="\ x" in exI)
       apply (rule conjI)
        apply (simp add: ‹gauge {a..b} δ› [unfolded gauge_def])
       apply (clarify, rename_tac u v)
       apply (case_tac "u = v")
        apply (fast intro: fine_Nil)
       apply (subgoal_tac "u < v", fast intro: fine_single, simp)
      apply (rule_tac x="1" in exI, clarsimp)
      done
  }
  with ‹a ≤ b› show ?thesis by auto
qed

lemma fine_covers_all:
  assumes "fine \ (a, c) D" and "a < x" and "x \ c"
  shows "\ N < length D. \ d t e. D ! N = (d,t,e) \ d < x \ x \ e"
  using assms
proof (induct set: fine)
  case (2 b c D a t)
  thus ?case
  proof (cases "b < x")
    case True
    with 2 obtain N where *: "N < length D"
      and **: "D ! N = (d,t,e) \ d < x \ x \ e" for d t e by auto
    hence "Suc N < length ((a,t,b)#D) \
           (∀ d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) ⟶ d < x ∧ x ≤ e)" by auto
    thus ?thesis by auto
  next
    case False with 2
    have "0 < length ((a,t,b)#D) \
           (∀ d t' e. ((a,t,b)#D) ! 0 = (d,t',e) ⟶ d < x ∧ x ≤ e)" by auto
    thus ?thesis by auto
  qed
qed auto

lemma fine_append_split:
  assumes "fine \ (a,b) D" and "D2 \ []" and "D = D1 @ D2"
  shows "fine \ (a,fst (hd D2)) D1" (is "?fine1")
  and "fine \ (fst (hd D2), b) D2" (is "?fine2")
proof -
  from assms
  have "?fine1 \ ?fine2"
  proof (induct arbitrary: D1 D2)
    case (2 b c D a' x D1 D2)
    note induct = this

    thus ?case
    proof (cases D1)
      case Nil
      hence "fst (hd D2) = a'" using 2 by auto
      with fine_Cons[OF ‹fine δ (b,c) D› induct(3,4,5)] Nil induct
      show ?thesis by (auto intro: fine_Nil)
    next
      case (Cons d1 D1')
      with induct(2)[OF ‹D2 ≠ []›, of D1'] induct(8)
      have "fine \ (b, fst (hd D2)) D1'" and "fine \ (fst (hd D2), c) D2" and
        "d1 = (a', x, b)" by auto
      with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
      show ?thesis by auto
    qed
  qed auto
  thus ?fine1 and ?fine2 by auto
qed

lemma fine_δ_expand:
  assumes "fine \ (a,b) D"
  and "\x. a \ x \ x \ b \ \ x \ \' x"
  shows "fine \' (a,b) D"
using assms proof induct
  case 1 show ?case by (rule fine_Nil)
next
  case (2 b c D a x)
  show ?case
  proof (rule fine_Cons)
    show "fine \' (b,c) D" using 2 by auto
    from fine_imp_le[OF 2(1)] 2(6) ‹x ≤ b›
    show "b - a < \' x"
      using 2(7)[OF ‹a ≤ x›] by auto
  qed (auto simp add: 2)
qed

lemma fine_single_boundaries:
  assumes "fine \ (a,b) D" and "D = [(d, t, e)]"
  shows "a = d \ b = e"
using assms proof induct
  case (2 b c  D a x)
  hence "D = []" and "a = d" and "b = e" by auto
  moreover
  from ‹fine δ (b,c) D› ‹D = []› have "b = c"
    by (rule empty_fine_imp_eq)
  ultimately show ?case by simp
qed auto

lemma fine_sum_list_eq_diff:
  fixes f :: "real \ real"
  shows "fine \ (a, b) D \ (\(u, x, v)\D. f v - f u) = f b - f a"
by (induct set: fine) simp_all

text‹Lemmas about combining gauges›

lemma gauge_min:
     "[| gauge(E) g1; gauge(E) g2 |]
      ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
by (simp add: gauge_def)

lemma fine_min:
      "fine (%x. min (g1(x)) (g2(x))) (a,b) D
       ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
apply (erule fine.induct)
apply (simp add: fine_Nil)
apply (simp add: fine_Cons)
done

subsection ‹Riemann sum›

definition
  rsum :: "[(real \ real \ real) list, real \ real] \ real" where
  "rsum D f = (\(u, x, v)\D. f x * (v - u))"

lemma rsum_Nil [simp]: "rsum [] f = 0"
unfolding rsum_def by simp

lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
unfolding rsum_def by simp

lemma rsum_zero [simp]: "rsum D (\x. 0) = 0"
by (induct D, auto)

lemma rsum_left_distrib: "rsum D f * c = rsum D (\x. f x * c)"
by (induct D, auto simp add: algebra_simps)

lemma rsum_right_distrib: "c * rsum D f = rsum D (\x. c * f x)"
by (induct D, auto simp add: algebra_simps)

lemma rsum_add: "rsum D (\x. f x + g x) = rsum D f + rsum D g"
by (induct D, auto simp add: algebra_simps)

lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
unfolding rsum_def map_append sum_list_append ..


subsection ‹Gauge integrability (definite)›

definition
  Integral :: "[(real*real),real=>real,real] => bool" where
  "Integral = (%(a,b) f k. \e > 0.
                               (∃δ. gauge {a .. b} δ &
                               (∀D. fine δ (a,b) D -->
                                         ∣rsum D f - k∣ < e)))"

lemma Integral_eq:
  "Integral (a, b) f k \
    (∀e>0. ∃δ. gauge {a..b} δ ∧ (∀D. fine δ (a,b) D ⟶ ∣rsum D f - k∣ < e))"
unfolding Integral_def by simp

lemma IntegralI:
  assumes "\e. 0 < e \
    ∃δ. gauge {a..b} δ ∧ (∀D. fine δ (a, b) D ⟶ ∣rsum D f - k∣ < e)"
  shows "Integral (a, b) f k"
using assms unfolding Integral_def by auto

lemma IntegralE:
  assumes "Integral (a, b) f k" and "0 < e"
  obtains δ where "gauge {a..b} \" and "\D. fine \ (a, b) D \ \rsum D f - k\ < e"
using assms unfolding Integral_def by auto

lemma Integral_def2:
  "Integral = (%(a,b) f k. \e>0. (\\. gauge {a..b} \ &
                               (∀D. fine δ (a,b) D -->
                                         ∣rsum D f - k∣ ≤ e)))"
unfolding Integral_def
apply (safe intro!: ext)
apply (fast intro: less_imp_le)
apply (drule_tac x="e/2" in spec)
apply force
done

text‹The integral is unique if it exists›

lemma Integral_unique:
  assumes le: "a \ b"
  assumes 1: "Integral (a, b) f k1"
  assumes 2: "Integral (a, b) f k2"
  shows "k1 = k2"
proof (rule ccontr)
  assume "k1 \ k2"
  hence e: "0 < \k1 - k2\ / 2" by simp
  obtain d1 where "gauge {a..b} d1" and
    d1: "\D. fine d1 (a, b) D \ \rsum D f - k1\ < \k1 - k2\ / 2"
    using 1 e by (rule IntegralE)
  obtain d2 where "gauge {a..b} d2" and
    d2: "\D. fine d2 (a, b) D \ \rsum D f - k2\ < \k1 - k2\ / 2"
    using 2 e by (rule IntegralE)
  have "gauge {a..b} (\x. min (d1 x) (d2 x))"
    using ‹gauge {a..b} d1› and ‹gauge {a..b} d2›
    by (rule gauge_min)
  then obtain D where "fine (\x. min (d1 x) (d2 x)) (a, b) D"
    using fine_exists [OF le] by fast
  hence "fine d1 (a, b) D" and "fine d2 (a, b) D"
    by (auto dest: fine_min)
  hence "\rsum D f - k1\ < \k1 - k2\ / 2" and "\rsum D f - k2\ < \k1 - k2\ / 2"
    using d1 d2 by simp_all
  hence "\rsum D f - k1\ + \rsum D f - k2\ < \k1 - k2\ / 2 + \k1 - k2\ / 2"
    by (rule add_strict_mono)
  thus False by auto
qed

lemma Integral_zero: "Integral(a,a) f 0"
apply (rule IntegralI)
apply (rule_tac x = "\x. 1" in exI)
apply (simp add: fine_same_iff gauge_def)
done

lemma Integral_same_iff [simp]: "Integral (a, a) f k \ k = 0"
  by (auto intro: Integral_zero Integral_unique)

lemma Integral_zero_fun: "Integral (a,b) (\x. 0) 0"
apply (rule IntegralI)
apply (rule_tac x="\x. 1" in exI, simp add: gauge_def)
done

lemma fine_rsum_const: "fine \ (a,b) D \ rsum D (\x. c) = (c * (b - a))"
unfolding rsum_def
by (induct set: fine, auto simp add: algebra_simps)

lemma Integral_mult_const: "a \ b \ Integral(a,b) (\x. c) (c * (b - a))"
apply (cases "a = b", simp)
apply (rule IntegralI)
apply (rule_tac x = "\x. b - a" in exI)
apply (rule conjI, simp add: gauge_def)
apply (clarify)
apply (subst fine_rsum_const, assumption, simp)
done

lemma Integral_eq_diff_bounds: "a \ b \ Integral(a,b) (\x. 1) (b - a)"
  using Integral_mult_const [of a b 1] by simp

lemma Integral_mult:
     "[| a \ b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
apply (auto simp add: order_le_less)
apply (cases "c = 0", simp add: Integral_zero_fun)
apply (rule IntegralI)
apply (erule_tac e="e / \c\" in IntegralE, simp)
apply (rule_tac x="\" in exI, clarify)
apply (drule_tac x="D" in spec, clarify)
apply (simp add: pos_less_divide_eq abs_mult [symmetric]
                 algebra_simps rsum_right_distrib)
done

lemma Integral_add:
  assumes "Integral (a, b) f x1"
  assumes "Integral (b, c) f x2"
  assumes "a \ b" and "b \ c"
  shows "Integral (a, c) f (x1 + x2)"
proof (cases "a < b \ b < c", rule IntegralI)
  fix ε :: real assume "0 < \"
  hence "0 < \ / 2" by auto

  assume "a < b \ b < c"
  hence "a < b" and "b < c" by auto

  obtain δ1 where δ1_gauge: "gauge {a..b} \1"
    and I1: "fine \1 (a,b) D \ \ rsum D f - x1 \ < (\ / 2)" for D
    using IntegralE [OF ‹Integral (a, b) f x1› ‹0 < ε/2›] by auto

  obtain δ2 where δ2_gauge: "gauge {b..c} \2"
    and I2: "fine \2 (b,c) D \ \ rsum D f - x2 \ < (\ / 2)" for D
    using IntegralE [OF ‹Integral (b, c) f x2› ‹0 < ε/2›] by auto

  define δ where "\ x =
    (if x < b then min (δ1 x) (b - x)
     else if x = b then min (δ1 b) (δ2 b)
     else min (δ2 x) (x - b))" for x

  have "gauge {a..c} \"
    using δ1_gauge δ2_gauge unfolding δ_def gauge_def by auto

  moreover {
    fix D :: "(real \ real \ real) list"
    assume fine: "fine \ (a,c) D"
    from fine_covers_all[OF this ‹a < b› ‹b ≤ c›]
    obtain N where "N < length D"
      and *: "\ d t e. D ! N = (d, t, e) \ d < b \ b \ e"
      by auto
    obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
    with * have "d < b" and "b \ e" by auto
    have in_D: "(d, t, e) \ set D"
      using D_eq[symmetric] using ‹N < length D› by auto

    from mem_fine[OF fine in_D]
    have "d < e" and "d \ t" and "t \ e" by auto

    have "t = b"
    proof (rule ccontr)
      assume "t \ b"
      with mem_fine3[OF fine in_D] ‹b ≤ e› ‹d ≤ t› ‹t ≤ e› ‹d < b› δ_def
      show False by (cases "t < b") auto
    qed

    let ?D1 = "take N D"
    let ?D2 = "drop N D"
    define D1 where "D1 = take N D @ [(d, t, b)]"
    define D2 where "D2 = (if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"

    from hd_drop_conv_nth[OF ‹N < length D›]
    have "fst (hd ?D2) = d" using ‹D ! N = (d, t, e)› by auto
    with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
    have fine1: "fine \ (a,d) ?D1" and fine2: "fine \ (d,c) ?D2"
      using ‹N < length D› fine by auto

    have "fine \1 (a,b) D1" unfolding D1_def
    proof (rule fine_append)
      show "fine \1 (a, d) ?D1"
      proof (rule fine1[THEN fine_δ_expand])
        fix x assume "a \ x" "x \ d"
        hence "x \ b" using ‹d < b› ‹x ≤ d› by auto
        thus "\ x \ \1 x" unfolding δ_def by auto
      qed

      have "b - d < \1 t"
        using mem_fine3[OF fine in_D] δ_def ‹b ≤ e› ‹t = b› by auto
      from ‹d < b› ‹d ≤ t› ‹t = b› this
      show "fine \1 (d, b) [(d, t, b)]" using fine_single by auto
    qed
    note rsum1 = I1[OF this]

    have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
      using Cons_nth_drop_Suc[OF ‹N < length D›] by simp

    have fine2: "fine \2 (e,c) (drop (Suc N) D)"
    proof (cases "drop (Suc N) D = []")
      case True
      note * = fine2[simplified drop_split True D_eq append_Nil2]
      have "e = c" using fine_single_boundaries[OF * refl] by auto
      thus ?thesis unfolding True using fine_Nil by auto
    next
      case False
      note * = fine_append_split[OF fine2 False drop_split]
      from fine_single_boundaries[OF *(1)]
      have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
      with *(2) have "fine \ (e,c) (drop (Suc N) D)" by auto
      thus ?thesis
      proof (rule fine_δ_expand)
        fix x assume "e \ x" and "x \ c"
        thus "\ x \ \2 x" using ‹b ≤ e› unfolding δ_def by auto
      qed
    qed

    have "fine \2 (b, c) D2"
    proof (cases "e = b")
      case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
    next
      case False
      have "e - b < \2 b"
        using mem_fine3[OF fine in_D] δ_def ‹d < b› ‹t = b› by auto
      with False ‹t = b› ‹b ≤ e›
      show ?thesis using D2_def
        by (auto intro!: fine_append[OF _ fine2] fine_single
               simp del: append_Cons)
    qed
    note rsum2 = I2[OF this]

    have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
      using rsum_append[symmetric] Cons_nth_drop_Suc[OF ‹N < length D›] by auto
    also have "\ = rsum D1 f + rsum D2 f"
      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
    finally have "\rsum D f - (x1 + x2)\ < \"
      using add_strict_mono[OF rsum1 rsum2] by simp
  }
  ultimately show "\ \. gauge {a .. c} \ \
    (∀D. fine δ (a,c) D ⟶ ∣rsum D f - (x1 + x2)∣ < ε)"
    by blast
next
  case False
  hence "a = b \ b = c" using ‹a ≤ b› and ‹b ≤ c› by auto
  thus ?thesis
  proof (rule disjE)
    assume "a = b" hence "x1 = 0"
      using ‹Integral (a, b) f x1› by simp
    thus ?thesis using ‹a = b› ‹Integral (b, c) f x2› by simp
  next
    assume "b = c" hence "x2 = 0"
      using ‹Integral (b, c) f x2› by simp
    thus ?thesis using ‹b = c› ‹Integral (a, b) f x1› by simp
  qed
qed

text‹Fundamental theorem of calculus (Part I)›

text‹"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988›

lemma strad1:
  fixes z x s e :: real
  assumes P: "(\z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < e / 2)"
  assumes "\z - x\ < s"
  shows "\f z - f x - f' x * (z - x)\ \ e / 2 * \z - x\"
proof (cases "z = x")
  case True then show ?thesis by simp
next
  case False
  then have "inverse (z - x) * (f z - f x - f' x * (z - x)) = (f z - f x) / (z - x) - f' x"
    apply (subst mult.commute)
    apply (simp add: left_diff_distrib)
    apply (simp add: mult.assoc divide_inverse)
    apply (simp add: ring_distribs)
    done
  moreover from False ‹∣z - x∣ < s› have "\(f z - f x) / (z - x) - f' x\ < e / 2"
    by (rule P)
  ultimately have "\inverse (z - x)\ * (\f z - f x - f' x * (z - x)\ * 2)
    ≤ ∣inverse (z - x)∣ * (e * ∣z - x∣)"
    using False by (simp del: abs_inverse add: abs_mult [symmetric] ac_simps)
  with False have "\f z - f x - f' x * (z - x)\ * 2 \ e * \z - x\"
    by simp
  then show ?thesis by simp
qed

lemma lemma_straddle:
  assumes f': "\x. a \ x & x \ b --> DERIV f x :> f'(x)" and "0 < e"
  shows "\g. gauge {a..b} g &
                (∀x u v. a ≤ u & u ≤ x & x ≤ v & v ≤ b & (v - u) < g(x)
                  --> ∣(f(v) - f(u)) - (f'(x) * (v - u))\ \ e * (v - u))"
proof -
  have "\x\{a..b}.
        (∃d > 0. ∀u v. u ≤ x & x ≤ v & (v - u) < d --> 
                       ∣(f(v) - f(u)) - (f'(x) * (v - u))\ \ e * (v - u))"
  proof (clarsimp)
    fix x :: real assume "a \ x" and "x \ b"
    with f' have "DERIV f x :> f'(x)" by simp
    then have "\r>0. \s>0. \z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < r"
      by (simp add: has_field_derivative_iff LIM_eq)
    with ‹0 < e› obtain s
    where "z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < e/2" and "0 < s" for z
      by (drule_tac x="e/2" in spec, auto)
    with strad1 [of x s f f' e] have strad:
        "\z. \z - x\ < s \ \f z - f x - f' x * (z - x)\ \ e/2 * \z - x\"
      by auto
    show "\d>0. \u v. u \ x \ x \ v \ v - u < d \ \f v - f u - f' x * (v - u)\ \ e * (v - u)"
    proof (safe intro!: exI)
      show "0 < s" by fact
    next
      fix u v :: real assume "u \ x" and "x \ v" and "v - u < s"
      have "\f v - f u - f' x * (v - u)\ =
            ∣(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))∣"
        by (simp add: right_diff_distrib)
      also have "\ \ \f v - f x - f' x * (v - x)\ + \f x - f u - f' x * (x - u)\"
        by (rule abs_triangle_ineq)
      also have "\ = \f v - f x - f' x * (v - x)\ + \f u - f x - f' x * (u - x)\"
        by (simp add: right_diff_distrib)
      also have "\ \ (e/2) * \v - x\ + (e/2) * \u - x\"
        using ‹u ≤ x› ‹x ≤ v› ‹v - u < s› by (intro add_mono strad, simp_all)
      also have "\ \ e * (v - u) / 2 + e * (v - u) / 2"
        using ‹u ≤ x› ‹x ≤ v› ‹0 < e› by (intro add_mono, simp_all)
      also have "\ = e * (v - u)"
        by simp
      finally show "\f v - f u - f' x * (v - u)\ \ e * (v - u)" .
    qed
  qed
  thus ?thesis
    by (simp add: gauge_def) (drule bchoice, auto)
qed

lemma fundamental_theorem_of_calculus:
  assumes "a \ b"
  assumes f': "\x. a \ x \ x \ b \ DERIV f x :> f'(x)"
  shows "Integral (a, b) f' (f(b) - f(a))"
proof (cases "a = b")
  assume "a = b" thus ?thesis by simp
next
  assume "a \ b" with ‹a ≤ b› have "a < b" by simp
  show ?thesis
  proof (simp add: Integral_def2, clarify)
    fix e :: real assume "0 < e"
    with ‹a < b› have "0 < e / (b - a)" by simp

    from lemma_straddle [OF f' this]
    obtain δ where "gauge {a..b} \"
      and δ: "\a \ u; u \ x; x \ v; v \ b; v - u < \ x\ \
           ∣f v - f u - f' x * (v - u)\ \ e * (v - u) / (b - a)" for x u v by auto

    have "\D. fine \ (a, b) D \ \rsum D f' - (f b - f a)\ \ e"
    proof (clarify)
      fix D assume D: "fine \ (a, b) D"
      hence "(\(u, x, v)\D. f v - f u) = f b - f a"
        by (rule fine_sum_list_eq_diff)
      hence "\rsum D f' - (f b - f a)\ = \rsum D f' - (\(u, x, v)\D. f v - f u)\"
        by simp
      also have "\ = \(\(u, x, v)\D. f v - f u) - rsum D f'\"
        by (rule abs_minus_commute)
      also have "\ = \\(u, x, v)\D. (f v - f u) - f' x * (v - u)\"
        by (simp only: rsum_def sum_list_subtractf split_def)
      also have "\ \ (\(u, x, v)\D. \(f v - f u) - f' x * (v - u)\)"
        by (rule ord_le_eq_trans [OF sum_list_abs], simp add: o_def split_def)
      also have "\ \ (\(u, x, v)\D. (e / (b - a)) * (v - u))"
        apply (rule sum_list_mono, clarify, rename_tac u x v)
        using D apply (simp add: δ mem_fine mem_fine2 mem_fine3)
        done
      also have "\ = e"
        using fine_sum_list_eq_diff [OF D, where f="\x. x"]
        unfolding split_def sum_list_const_mult
        using ‹a < b› by simp
      finally show "\rsum D f' - (f b - f a)\ \ e" .
    qed

    with ‹gauge {a..b} δ›
    show "\\. gauge {a..b} \ \ (\D. fine \ (a, b) D \ \rsum D f' - (f b - f a)\ \ e)"
      by auto
  qed
qed

end