src/HOL/Deriv.thy
changeset 29975 28c5322f0df3
parent 29803 c56a5571f60a
child 29982 6ec97eba1ee3
     1.1 --- a/src/HOL/Deriv.thy	Wed Feb 18 07:24:13 2009 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Wed Feb 18 09:07:36 2009 -0800
     1.3 @@ -217,9 +217,7 @@
     1.4  by (cases "n", simp, simp add: DERIV_power_Suc f)
     1.5  
     1.6  
     1.7 -(* ------------------------------------------------------------------------ *)
     1.8 -(* Caratheodory formulation of derivative at a point: standard proof        *)
     1.9 -(* ------------------------------------------------------------------------ *)
    1.10 +text {* Caratheodory formulation of derivative at a point *}
    1.11  
    1.12  lemma CARAT_DERIV:
    1.13       "(DERIV f x :> l) =
    1.14 @@ -307,6 +305,9 @@
    1.15         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
    1.16  by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
    1.17  
    1.18 +lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    1.19 +by auto
    1.20 +
    1.21  
    1.22  subsection {* Differentiability predicate *}
    1.23  
    1.24 @@ -655,6 +656,9 @@
    1.25  apply (blast intro: IVT2)
    1.26  done
    1.27  
    1.28 +
    1.29 +subsection {* Boundedness of continuous functions *}
    1.30 +
    1.31  text{*By bisection, function continuous on closed interval is bounded above*}
    1.32  
    1.33  lemma isCont_bounded:
    1.34 @@ -773,6 +777,8 @@
    1.35  done
    1.36  
    1.37  
    1.38 +subsection {* Local extrema *}
    1.39 +
    1.40  text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
    1.41  
    1.42  lemma DERIV_left_inc:
    1.43 @@ -877,6 +883,9 @@
    1.44    shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
    1.45  by (auto dest!: DERIV_local_max)
    1.46  
    1.47 +
    1.48 +subsection {* Rolle's Theorem *}
    1.49 +
    1.50  text{*Lemma about introducing open ball in open interval*}
    1.51  lemma lemma_interval_lt:
    1.52       "[| a < x;  x < b |]
    1.53 @@ -1163,6 +1172,8 @@
    1.54  qed
    1.55  
    1.56  
    1.57 +subsection {* Continuous injective functions *}
    1.58 +
    1.59  text{*Dull lemma: an continuous injection on an interval must have a
    1.60  strict maximum at an end point, not in the middle.*}
    1.61  
    1.62 @@ -1356,6 +1367,9 @@
    1.63      using neq by (rule LIM_inverse)
    1.64  qed
    1.65  
    1.66 +
    1.67 +subsection {* Generalized Mean Value Theorem *}
    1.68 +
    1.69  theorem GMVT:
    1.70    fixes a b :: real
    1.71    assumes alb: "a < b"
    1.72 @@ -1442,9 +1456,6 @@
    1.73    with g'cdef f'cdef cint show ?thesis by auto
    1.74  qed
    1.75  
    1.76 -lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    1.77 -by auto
    1.78 -
    1.79  
    1.80  subsection {* Derivatives of univariate polynomials *}
    1.81