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