Structure derivativeTheory

signature derivativeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val convex : thm
    val convex_on : thm
    val differentiable : thm
    val differentiable_on : thm
    val frechet_derivative : thm
    val has_derivative : thm
    val has_vector_derivative : thm
    val oabs : thm
    val vector_derivative : thm
  
  (*  Theorems  *)
    val ABS_BOUND_GENERALIZE : thm
    val CONNECTED_COMPACT_INTERVAL_1 : thm
    val CONTINUOUS_AT_EXP : thm
    val CONTINUOUS_ON_EXP : thm
    val CONTINUOUS_WITHIN_EXP : thm
    val CONVEX_ALT : thm
    val CONVEX_BALL : thm
    val CONVEX_CBALL : thm
    val CONVEX_CONNECTED : thm
    val CONVEX_DISTANCE : thm
    val CONVEX_INDEXED : thm
    val CONVEX_INTERVAL : thm
    val CONVEX_SUM : thm
    val DIFFERENTIABLE_BOUND : thm
    val DIFFERENTIABLE_IMP_CONTINUOUS_AT : thm
    val DIFFERENTIABLE_IMP_CONTINUOUS_ON : thm
    val DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN : thm
    val DIFFERENTIABLE_ON_EMPTY : thm
    val DIFFERENTIABLE_ON_SUBSET : thm
    val DIFFERENTIABLE_WITHIN_SUBSET : thm
    val DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM : thm
    val DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM : thm
    val DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN : thm
    val DIFFERENTIAL_ZERO_MAXMIN : thm
    val DIFF_CHAIN_WITHIN : thm
    val EXP_CONVERGES : thm
    val EXP_CONVERGES_UNIFORMLY : thm
    val EXP_CONVERGES_UNIFORMLY_CAUCHY : thm
    val EXP_CONVERGES_UNIQUE : thm
    val FRECHET_DERIVATIVE_WORKS : thm
    val HAS_DERIVATIVE_ADD : thm
    val HAS_DERIVATIVE_AT : thm
    val HAS_DERIVATIVE_AT_ALT : thm
    val HAS_DERIVATIVE_AT_WITHIN : thm
    val HAS_DERIVATIVE_BILINEAR_AT : thm
    val HAS_DERIVATIVE_BILINEAR_WITHIN : thm
    val HAS_DERIVATIVE_CMUL : thm
    val HAS_DERIVATIVE_CONST : thm
    val HAS_DERIVATIVE_EXP : thm
    val HAS_DERIVATIVE_ID : thm
    val HAS_DERIVATIVE_IMP_CONTINUOUS_AT : thm
    val HAS_DERIVATIVE_LINEAR : thm
    val HAS_DERIVATIVE_MUL_AT : thm
    val HAS_DERIVATIVE_MUL_WITHIN : thm
    val HAS_DERIVATIVE_NEG : thm
    val HAS_DERIVATIVE_POW : thm
    val HAS_DERIVATIVE_SEQUENCE : thm
    val HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ : thm
    val HAS_DERIVATIVE_SERIES : thm
    val HAS_DERIVATIVE_SERIES' : thm
    val HAS_DERIVATIVE_SUB : thm
    val HAS_DERIVATIVE_SUM : thm
    val HAS_DERIVATIVE_TRANSFORM_AT : thm
    val HAS_DERIVATIVE_TRANSFORM_WITHIN : thm
    val HAS_DERIVATIVE_WITHIN : thm
    val HAS_DERIVATIVE_WITHIN_ALT : thm
    val HAS_DERIVATIVE_WITHIN_OPEN : thm
    val HAS_DERIVATIVE_WITHIN_SUBSET : thm
    val HAS_VECTOR_DERIVATIVE_AT_WITHIN : thm
    val HAS_VECTOR_DERIVATIVE_BILINEAR_AT : thm
    val HAS_VECTOR_DERIVATIVE_BILINEAR_WITHIN : thm
    val HAS_VECTOR_DERIVATIVE_WITHIN_SUBSET : thm
    val IN_CONVEX_SET : thm
    val IS_INTERVAL_CONNECTED : thm
    val IS_INTERVAL_CONNECTED_1 : thm
    val IS_INTERVAL_CONVEX : thm
    val IS_INTERVAL_CONVEX_1 : thm
    val LIMPT_APPROACHABLE : thm
    val LIMPT_OF_CONVEX : thm
    val LIM_MUL_ABS_WITHIN : thm
    val LINEAR_FRECHET_DERIVATIVE : thm
    val MVT : thm
    val MVT_GENERAL : thm
    val OABS : thm
    val REAL_CONVEX_BOUND2_LT : thm
    val REAL_CONVEX_BOUND_LT : thm
    val REAL_MUL_NZ : thm
    val ROLLE : thm
    val TRIVIAL_LIMIT_WITHIN_CONVEX : thm
    val has_derivative_at : thm
    val has_derivative_within : thm
  
  val derivative_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [real_topology] Parent theory of "derivative"
   
   [convex]  Definition
      
      ⊢ ∀s. convex s ⇔
            ∀x y u v.
              x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒ u * x + v * y ∈ s
   
   [convex_on]  Definition
      
      ⊢ ∀f s.
          f convex_on s ⇔
          ∀x y u v.
            x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒
            f (u * x + v * y) ≤ u * f x + v * f y
   
   [differentiable]  Definition
      
      ⊢ ∀f net. f differentiable net ⇔ ∃f'. (f has_derivative f') net
   
   [differentiable_on]  Definition
      
      ⊢ ∀f s.
          f differentiable_on s ⇔
          ∀x. x ∈ s ⇒ f differentiable (at x within s)
   
   [frechet_derivative]  Definition
      
      ⊢ ∀f net. frechet_derivative f net = @f'. (f has_derivative f') net
   
   [has_derivative]  Definition
      
      ⊢ ∀f f' net.
          (f has_derivative f') net ⇔
          linear f' ∧
          ((λy.
                (abs (y − netlimit net))⁻¹ *
                (f y − (f (netlimit net) + f' (y − netlimit net)))) ⟶ 0)
            net
   
   [has_vector_derivative]  Definition
      
      ⊢ ∀f f' net.
          (f has_vector_derivative f') net ⇔
          (f has_derivative (λx. x * f')) net
   
   [oabs]  Definition
      
      ⊢ ∀f. oabs f = sup {abs (f x) | abs x = 1}
   
   [vector_derivative]  Definition
      
      ⊢ ∀f net.
          vector_derivative f net = @f'. (f has_vector_derivative f') net
   
   [ABS_BOUND_GENERALIZE]  Theorem
      
      ⊢ ∀f b.
          linear f ⇒
          ((∀x. abs x = 1 ⇒ abs (f x) ≤ b) ⇔ ∀x. abs (f x) ≤ b * abs x)
   
   [CONNECTED_COMPACT_INTERVAL_1]  Theorem
      
      ⊢ ∀s. connected s ∧ compact s ⇔ ∃a b. s = interval [(a,b)]
   
   [CONTINUOUS_AT_EXP]  Theorem
      
      ⊢ ∀z. exp continuous at z
   
   [CONTINUOUS_ON_EXP]  Theorem
      
      ⊢ ∀s. exp continuous_on s
   
   [CONTINUOUS_WITHIN_EXP]  Theorem
      
      ⊢ ∀s z. exp continuous (at z within s)
   
   [CONVEX_ALT]  Theorem
      
      ⊢ ∀s. convex s ⇔
            ∀x y u. x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ u ≤ 1 ⇒ (1 − u) * x + u * y ∈ s
   
   [CONVEX_BALL]  Theorem
      
      ⊢ ∀x e. convex (ball (x,e))
   
   [CONVEX_CBALL]  Theorem
      
      ⊢ ∀x e. convex (cball (x,e))
   
   [CONVEX_CONNECTED]  Theorem
      
      ⊢ ∀s. convex s ⇒ connected s
   
   [CONVEX_DISTANCE]  Theorem
      
      ⊢ ∀s a. (λx. dist (a,x)) convex_on s
   
   [CONVEX_INDEXED]  Theorem
      
      ⊢ ∀s. convex s ⇔
            ∀k u x.
              (∀i. 1 ≤ i ∧ i ≤ k ⇒ 0 ≤ u i ∧ x i ∈ s) ∧ sum (1 .. k) u = 1 ⇒
              sum (1 .. k) (λi. u i * x i) ∈ s
   
   [CONVEX_INTERVAL]  Theorem
      
      ⊢ ∀a b. convex (interval [(a,b)]) ∧ convex (interval (a,b))
   
   [CONVEX_SUM]  Theorem
      
      ⊢ ∀s k u x.
          FINITE k ∧ convex s ∧ sum k u = 1 ∧
          (∀i. i ∈ k ⇒ 0 ≤ u i ∧ x i ∈ s) ⇒
          sum k (λi. u i * x i) ∈ s
   
   [DIFFERENTIABLE_BOUND]  Theorem
      
      ⊢ ∀f f' s B.
          convex s ∧
          (∀x. x ∈ s ⇒ (f has_derivative f' x) (at x within s)) ∧
          (∀x. x ∈ s ⇒ oabs (f' x) ≤ B) ⇒
          ∀x y. x ∈ s ∧ y ∈ s ⇒ abs (f x − f y) ≤ B * abs (x − y)
   
   [DIFFERENTIABLE_IMP_CONTINUOUS_AT]  Theorem
      
      ⊢ ∀f x. f differentiable at x ⇒ f continuous at x
   
   [DIFFERENTIABLE_IMP_CONTINUOUS_ON]  Theorem
      
      ⊢ ∀f s. f differentiable_on s ⇒ f continuous_on s
   
   [DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]  Theorem
      
      ⊢ ∀f x s.
          f differentiable (at x within s) ⇒ f continuous (at x within s)
   
   [DIFFERENTIABLE_ON_EMPTY]  Theorem
      
      ⊢ ∀f. f differentiable_on ∅
   
   [DIFFERENTIABLE_ON_SUBSET]  Theorem
      
      ⊢ ∀f s t. f differentiable_on t ∧ s ⊆ t ⇒ f differentiable_on s
   
   [DIFFERENTIABLE_WITHIN_SUBSET]  Theorem
      
      ⊢ ∀f s t x.
          f differentiable (at x within t) ∧ s ⊆ t ⇒
          f differentiable (at x within s)
   
   [DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM]  Theorem
      
      ⊢ ∀f f' x s e.
          x ∈ s ∧ convex s ∧ (f has_derivative f') (at x within s) ∧
          0 < e ∧ (∀w. w ∈ s ∩ ball (x,e) ⇒ f w ≤ f x) ⇒
          ∀y. y ∈ s ⇒ f' (y − x) ≤ 0
   
   [DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM]  Theorem
      
      ⊢ ∀f f' x s e.
          x ∈ s ∧ convex s ∧ (f has_derivative f') (at x within s) ∧
          0 < e ∧ (∀w. w ∈ s ∩ ball (x,e) ⇒ f x ≤ f w) ⇒
          ∀y. y ∈ s ⇒ 0 ≤ f' (y − x)
   
   [DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN]  Theorem
      
      ⊢ ∀f f' x s.
          x ∈ s ∧ open s ∧ (f has_derivative f') (at x) ∧
          ((∀w. w ∈ s ⇒ f w ≤ f x) ∨ ∀w. w ∈ s ⇒ f x ≤ f w) ⇒
          ∀h. f' h = 0
   
   [DIFFERENTIAL_ZERO_MAXMIN]  Theorem
      
      ⊢ ∀f f' x s.
          x ∈ s ∧ open s ∧ (f has_derivative f') (at x) ∧
          ((∀y. y ∈ s ⇒ f y ≤ f x) ∨ ∀y. y ∈ s ⇒ f x ≤ f y) ⇒
          f' = (λv. 0)
   
   [DIFF_CHAIN_WITHIN]  Theorem
      
      ⊢ ∀f g f' g' x s.
          (f has_derivative f') (at x within s) ∧
          (g has_derivative g') (at (f x) within IMAGE f s) ⇒
          (g ∘ f has_derivative g' ∘ f') (at x within s)
   
   [EXP_CONVERGES]  Theorem
      
      ⊢ ∀z. ((λn. z pow n / &FACT n) sums exp z) (from 0)
   
   [EXP_CONVERGES_UNIFORMLY]  Theorem
      
      ⊢ ∀R e.
          0 < R ∧ 0 < e ⇒
          ∃N. ∀n z.
            n ≥ N ∧ abs z < R ⇒
            abs (sum (0 .. n) (λi. z pow i / &FACT i) − exp z) ≤ e
   
   [EXP_CONVERGES_UNIFORMLY_CAUCHY]  Theorem
      
      ⊢ ∀R e.
          0 < e ∧ 0 < R ⇒
          ∃N. ∀m n z.
            m ≥ N ∧ abs z ≤ R ⇒
            abs (sum (m .. n) (λi. z pow i / &FACT i)) < e
   
   [EXP_CONVERGES_UNIQUE]  Theorem
      
      ⊢ ∀w z. ((λn. z pow n / &FACT n) sums w) (from 0) ⇔ w = exp z
   
   [FRECHET_DERIVATIVE_WORKS]  Theorem
      
      ⊢ ∀f net.
          f differentiable net ⇔
          (f has_derivative frechet_derivative f net) net
   
   [HAS_DERIVATIVE_ADD]  Theorem
      
      ⊢ ∀f f' g g' net.
          (f has_derivative f') net ∧ (g has_derivative g') net ⇒
          ((λx. f x + g x) has_derivative (λh. f' h + g' h)) net
   
   [HAS_DERIVATIVE_AT]  Theorem
      
      ⊢ ∀f f' x.
          (f has_derivative f') (at x) ⇔
          linear f' ∧
          ∀e. 0 < e ⇒
              ∃d. 0 < d ∧
                  ∀x'.
                    0 < abs (x' − x) ∧ abs (x' − x) < d ⇒
                    abs (f x' − f x − f' (x' − x)) / abs (x' − x) < e
   
   [HAS_DERIVATIVE_AT_ALT]  Theorem
      
      ⊢ ∀f f' x.
          (f has_derivative f') (at x) ⇔
          linear f' ∧
          ∀e. 0 < e ⇒
              ∃d. 0 < d ∧
                  ∀y. abs (y − x) < d ⇒
                      abs (f y − f x − f' (y − x)) ≤ e * abs (y − x)
   
   [HAS_DERIVATIVE_AT_WITHIN]  Theorem
      
      ⊢ ∀f f' x s.
          (f has_derivative f') (at x) ⇒
          (f has_derivative f') (at x within s)
   
   [HAS_DERIVATIVE_BILINEAR_AT]  Theorem
      
      ⊢ ∀h f g f' g' x.
          (f has_derivative f') (at x) ∧ (g has_derivative g') (at x) ∧
          bilinear h ⇒
          ((λx. h (f x) (g x)) has_derivative
           (λd. h (f x) (g' d) + h (f' d) (g x))) (at x)
   
   [HAS_DERIVATIVE_BILINEAR_WITHIN]  Theorem
      
      ⊢ ∀h f g f' g' x s.
          (f has_derivative f') (at x within s) ∧
          (g has_derivative g') (at x within s) ∧ bilinear h ⇒
          ((λx. h (f x) (g x)) has_derivative
           (λd. h (f x) (g' d) + h (f' d) (g x))) (at x within s)
   
   [HAS_DERIVATIVE_CMUL]  Theorem
      
      ⊢ ∀f f' net c.
          (f has_derivative f') net ⇒
          ((λx. c * f x) has_derivative (λh. c * f' h)) net
   
   [HAS_DERIVATIVE_CONST]  Theorem
      
      ⊢ ∀c net. ((λx. c) has_derivative (λh. 0)) net
   
   [HAS_DERIVATIVE_EXP]  Theorem
      
      ⊢ ∀z. (exp has_derivative (λy. exp z * y)) (at z)
   
   [HAS_DERIVATIVE_ID]  Theorem
      
      ⊢ ∀net. ((λx. x) has_derivative (λh. h)) net
   
   [HAS_DERIVATIVE_IMP_CONTINUOUS_AT]  Theorem
      
      ⊢ ∀f f' x. (f has_derivative f') (at x) ⇒ f continuous at x
   
   [HAS_DERIVATIVE_LINEAR]  Theorem
      
      ⊢ ∀f net. linear f ⇒ (f has_derivative f) net
   
   [HAS_DERIVATIVE_MUL_AT]  Theorem
      
      ⊢ ∀f f' g g' a.
          (f has_derivative f') (at a) ∧ (g has_derivative g') (at a) ⇒
          ((λx. f x * g x) has_derivative (λh. f a * g' h + f' h * g a))
            (at a)
   
   [HAS_DERIVATIVE_MUL_WITHIN]  Theorem
      
      ⊢ ∀f f' g g' a s.
          (f has_derivative f') (at a within s) ∧
          (g has_derivative g') (at a within s) ⇒
          ((λx. f x * g x) has_derivative (λh. f a * g' h + f' h * g a))
            (at a within s)
   
   [HAS_DERIVATIVE_NEG]  Theorem
      
      ⊢ ∀f f' net.
          (f has_derivative f') net ⇒
          ((λx. -f x) has_derivative (λh. -f' h)) net
   
   [HAS_DERIVATIVE_POW]  Theorem
      
      ⊢ ∀q0 n.
          ((λq. q pow n) has_derivative
           (λq. sum (1 .. n) (λi. q0 pow (n − i) * q * q0 pow (i − 1))))
            (at q0)
   
   [HAS_DERIVATIVE_SEQUENCE]  Theorem
      
      ⊢ ∀s f f' g'.
          convex s ∧
          (∀n x. x ∈ s ⇒ (f n has_derivative f' n x) (at x within s)) ∧
          (∀e. 0 < e ⇒
               ∃N. ∀n x h.
                 n ≥ N ∧ x ∈ s ⇒ abs (f' n x h − g' x h) ≤ e * abs h) ∧
          (∃x l. x ∈ s ∧ ((λn. f n x) ⟶ l) sequentially) ⇒
          ∃g. ∀x.
            x ∈ s ⇒
            ((λn. f n x) ⟶ g x) sequentially ∧
            (g has_derivative g' x) (at x within s)
   
   [HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ]  Theorem
      
      ⊢ ∀s f f' g'.
          convex s ∧
          (∀n x. x ∈ s ⇒ (f n has_derivative f' n x) (at x within s)) ∧
          (∀e. 0 < e ⇒
               ∃N. ∀n x h.
                 n ≥ N ∧ x ∈ s ⇒ abs (f' n x h − g' x h) ≤ e * abs h) ⇒
          ∀e. 0 < e ⇒
              ∃N. ∀m n x y.
                m ≥ N ∧ n ≥ N ∧ x ∈ s ∧ y ∈ s ⇒
                abs (f m x − f n x − (f m y − f n y)) ≤ e * abs (x − y)
   
   [HAS_DERIVATIVE_SERIES]  Theorem
      
      ⊢ ∀s f f' g' k.
          convex s ∧
          (∀n x. x ∈ s ⇒ (f n has_derivative f' n x) (at x within s)) ∧
          (∀e. 0 < e ⇒
               ∃N. ∀n x h.
                 n ≥ N ∧ x ∈ s ⇒
                 abs
                   (sum (k ∩ {x | 0 ≤ x ∧ x ≤ n}) (λi. f' i x h) − g' x h) ≤
                 e * abs h) ∧ (∃x l. x ∈ s ∧ ((λn. f n x) sums l) k) ⇒
          ∃g. ∀x.
            x ∈ s ⇒
            ((λn. f n x) sums g x) k ∧
            (g has_derivative g' x) (at x within s)
   
   [HAS_DERIVATIVE_SERIES']  Theorem
      
      ⊢ ∀s f f' g' k.
          convex s ∧
          (∀n x.
             x ∈ s ⇒ (f n has_derivative (λy. f' n x * y)) (at x within s)) ∧
          (∀e. 0 < e ⇒
               ∃N. ∀n x.
                 n ≥ N ∧ x ∈ s ⇒
                 abs (sum (k ∩ (0 .. n)) (λi. f' i x) − g' x) ≤ e) ∧
          (∃x l. x ∈ s ∧ ((λn. f n x) sums l) k) ⇒
          ∃g. ∀x.
            x ∈ s ⇒
            ((λn. f n x) sums g x) k ∧
            (g has_derivative (λy. g' x * y)) (at x within s)
   
   [HAS_DERIVATIVE_SUB]  Theorem
      
      ⊢ ∀f f' g g' net.
          (f has_derivative f') net ∧ (g has_derivative g') net ⇒
          ((λx. f x − g x) has_derivative (λh. f' h − g' h)) net
   
   [HAS_DERIVATIVE_SUM]  Theorem
      
      ⊢ ∀f f' net s.
          FINITE s ∧ (∀a. a ∈ s ⇒ (f a has_derivative f' a) net) ⇒
          ((λx. sum s (λa. f a x)) has_derivative (λh. sum s (λa. f' a h)))
            net
   
   [HAS_DERIVATIVE_TRANSFORM_AT]  Theorem
      
      ⊢ ∀f f' g x d.
          0 < d ∧ (∀x'. dist (x',x) < d ⇒ f x' = g x') ∧
          (f has_derivative f') (at x) ⇒
          (g has_derivative f') (at x)
   
   [HAS_DERIVATIVE_TRANSFORM_WITHIN]  Theorem
      
      ⊢ ∀f f' g x s d.
          0 < d ∧ x ∈ s ∧ (∀x'. x' ∈ s ∧ dist (x',x) < d ⇒ f x' = g x') ∧
          (f has_derivative f') (at x within s) ⇒
          (g has_derivative f') (at x within s)
   
   [HAS_DERIVATIVE_WITHIN]  Theorem
      
      ⊢ ∀f f' x s.
          (f has_derivative f') (at x within s) ⇔
          linear f' ∧
          ∀e. 0 < e ⇒
              ∃d. 0 < d ∧
                  ∀x'.
                    x' ∈ s ∧ 0 < abs (x' − x) ∧ abs (x' − x) < d ⇒
                    abs (f x' − f x − f' (x' − x)) / abs (x' − x) < e
   
   [HAS_DERIVATIVE_WITHIN_ALT]  Theorem
      
      ⊢ ∀f f' s x.
          (f has_derivative f') (at x within s) ⇔
          linear f' ∧
          ∀e. 0 < e ⇒
              ∃d. 0 < d ∧
                  ∀y. y ∈ s ∧ abs (y − x) < d ⇒
                      abs (f y − f x − f' (y − x)) ≤ e * abs (y − x)
   
   [HAS_DERIVATIVE_WITHIN_OPEN]  Theorem
      
      ⊢ ∀f f' a s.
          a ∈ s ∧ open s ⇒
          ((f has_derivative f') (at a within s) ⇔
           (f has_derivative f') (at a))
   
   [HAS_DERIVATIVE_WITHIN_SUBSET]  Theorem
      
      ⊢ ∀f f' s t x.
          (f has_derivative f') (at x within s) ∧ t ⊆ s ⇒
          (f has_derivative f') (at x within t)
   
   [HAS_VECTOR_DERIVATIVE_AT_WITHIN]  Theorem
      
      ⊢ ∀f f' x s.
          (f has_vector_derivative f') (at x) ⇒
          (f has_vector_derivative f') (at x within s)
   
   [HAS_VECTOR_DERIVATIVE_BILINEAR_AT]  Theorem
      
      ⊢ ∀h f g f' g' x.
          (f has_vector_derivative f') (at x) ∧
          (g has_vector_derivative g') (at x) ∧ bilinear h ⇒
          ((λx. h (f x) (g x)) has_vector_derivative
           h (f x) g' + h f' (g x)) (at x)
   
   [HAS_VECTOR_DERIVATIVE_BILINEAR_WITHIN]  Theorem
      
      ⊢ ∀h f g f' g' x s.
          (f has_vector_derivative f') (at x within s) ∧
          (g has_vector_derivative g') (at x within s) ∧ bilinear h ⇒
          ((λx. h (f x) (g x)) has_vector_derivative
           h (f x) g' + h f' (g x)) (at x within s)
   
   [HAS_VECTOR_DERIVATIVE_WITHIN_SUBSET]  Theorem
      
      ⊢ ∀f f' s t x.
          (f has_vector_derivative f') (at x within s) ∧ t ⊆ s ⇒
          (f has_vector_derivative f') (at x within t)
   
   [IN_CONVEX_SET]  Theorem
      
      ⊢ ∀s a b u.
          convex s ∧ a ∈ s ∧ b ∈ s ∧ 0 ≤ u ∧ u ≤ 1 ⇒
          (1 − u) * a + u * b ∈ s
   
   [IS_INTERVAL_CONNECTED]  Theorem
      
      ⊢ ∀s. is_interval s ⇒ connected s
   
   [IS_INTERVAL_CONNECTED_1]  Theorem
      
      ⊢ ∀s. is_interval s ⇔ connected s
   
   [IS_INTERVAL_CONVEX]  Theorem
      
      ⊢ ∀s. is_interval s ⇒ convex s
   
   [IS_INTERVAL_CONVEX_1]  Theorem
      
      ⊢ ∀s. is_interval s ⇔ convex s
   
   [LIMPT_APPROACHABLE]  Theorem
      
      ⊢ ∀x s.
          x limit_point_of s ⇔
          ∀e. 0 < e ⇒ ∃x'. x' ∈ s ∧ x' ≠ x ∧ dist (x',x) < e
   
   [LIMPT_OF_CONVEX]  Theorem
      
      ⊢ ∀s x. convex s ∧ x ∈ s ⇒ (x limit_point_of s ⇔ s ≠ {x})
   
   [LIM_MUL_ABS_WITHIN]  Theorem
      
      ⊢ ∀f a s.
          (f ⟶ 0) (at a within s) ⇒
          ((λx. abs (x − a) * f x) ⟶ 0) (at a within s)
   
   [LINEAR_FRECHET_DERIVATIVE]  Theorem
      
      ⊢ ∀f net. f differentiable net ⇒ linear (frechet_derivative f net)
   
   [MVT]  Theorem
      
      ⊢ ∀f f' a b.
          a < b ∧ f continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) ⇒ (f has_derivative f' x) (at x)) ⇒
          ∃x. x ∈ interval (a,b) ∧ f b − f a = f' x (b − a)
   
   [MVT_GENERAL]  Theorem
      
      ⊢ ∀f f' a b.
          a < b ∧ f continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) ⇒ (f has_derivative f' x) (at x)) ⇒
          ∃x. x ∈ interval (a,b) ∧ abs (f b − f a) ≤ abs (f' x (b − a))
   
   [OABS]  Theorem
      
      ⊢ ∀f. linear f ⇒
            (∀x. abs (f x) ≤ oabs f * abs x) ∧
            ∀b. (∀x. abs (f x) ≤ b * abs x) ⇒ oabs f ≤ b
   
   [REAL_CONVEX_BOUND2_LT]  Theorem
      
      ⊢ ∀x y a b u v.
          x < a ∧ y < b ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒
          u * x + v * y < u * a + v * b
   
   [REAL_CONVEX_BOUND_LT]  Theorem
      
      ⊢ ∀x y a u v.
          x < a ∧ y < a ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒ u * x + v * y < a
   
   [REAL_MUL_NZ]  Theorem
      
      ⊢ ∀a b. a ≠ 0 ∧ b ≠ 0 ⇒ a * b ≠ 0
   
   [ROLLE]  Theorem
      
      ⊢ ∀f f' a b.
          a < b ∧ f a = f b ∧ f continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) ⇒ (f has_derivative f' x) (at x)) ⇒
          ∃x. x ∈ interval (a,b) ∧ f' x = (λv. 0)
   
   [TRIVIAL_LIMIT_WITHIN_CONVEX]  Theorem
      
      ⊢ ∀s x. convex s ∧ x ∈ s ⇒ (trivial_limit (at x within s) ⇔ s = {x})
   
   [has_derivative_at]  Theorem
      
      ⊢ ∀f f' x.
          (f has_derivative f') (at x) ⇔
          linear f' ∧
          ((λy. (abs (y − x))⁻¹ * (f y − (f x + f' (y − x)))) ⟶ 0) (at x)
   
   [has_derivative_within]  Theorem
      
      ⊢ ∀f f' x s.
          (f has_derivative f') (at x within s) ⇔
          linear f' ∧
          ((λy. (abs (y − x))⁻¹ * (f y − (f x + f' (y − x)))) ⟶ 0)
            (at x within s)
   
   
*)
end

HOL 4, Kananaskis-14