author huffman Wed, 18 Feb 2009 09:07:36 -0800 changeset 29975 28c5322f0df3 parent 29974 ca93255656a5 child 29976 3241eb2737b9
 src/HOL/Deriv.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Deriv.thy	Wed Feb 18 07:24:13 2009 -0800
+++ b/src/HOL/Deriv.thy	Wed Feb 18 09:07:36 2009 -0800
@@ -217,9 +217,7 @@
by (cases "n", simp, simp add: DERIV_power_Suc f)

-(* ------------------------------------------------------------------------ *)
-(* Caratheodory formulation of derivative at a point: standard proof        *)
-(* ------------------------------------------------------------------------ *)
+text {* Caratheodory formulation of derivative at a point *}

lemma CARAT_DERIV:
"(DERIV f x :> l) =
@@ -307,6 +305,9 @@
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)

+lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
+by auto
+

subsection {* Differentiability predicate *}

@@ -655,6 +656,9 @@
apply (blast intro: IVT2)
done

+
+subsection {* Boundedness of continuous functions *}
+
text{*By bisection, function continuous on closed interval is bounded above*}

lemma isCont_bounded:
@@ -773,6 +777,8 @@
done

+subsection {* Local extrema *}
+
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}

lemma DERIV_left_inc:
@@ -877,6 +883,9 @@
shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
by (auto dest!: DERIV_local_max)

+
+subsection {* Rolle's Theorem *}
+
text{*Lemma about introducing open ball in open interval*}
lemma lemma_interval_lt:
"[| a < x;  x < b |]
@@ -1163,6 +1172,8 @@
qed

+subsection {* Continuous injective functions *}
+
text{*Dull lemma: an continuous injection on an interval must have a
strict maximum at an end point, not in the middle.*}

@@ -1356,6 +1367,9 @@
using neq by (rule LIM_inverse)
qed

+
+subsection {* Generalized Mean Value Theorem *}
+
theorem GMVT:
fixes a b :: real
assumes alb: "a < b"
@@ -1442,9 +1456,6 @@
with g'cdef f'cdef cint show ?thesis by auto
qed

-lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-

subsection {* Derivatives of univariate polynomials *}
```