Theory "derivative"

Signature

Definitions

convex

⊢ ∀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

⊢ ∀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

⊢ ∀f net. f differentiable net ⇔ ∃f'. (f has_derivative f') net

differentiable_on

⊢ ∀f s. f differentiable_on s ⇔ ∀x. x ∈ s ⇒ f differentiable (at x within s)

frechet_derivative

⊢ ∀f net. frechet_derivative f net = @f'. (f has_derivative f') net

has_derivative

⊢ ∀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

⊢ ∀f f' net.
    (f has_vector_derivative f') net ⇔ (f has_derivative (λx. x * f')) net

oabs

⊢ ∀f. oabs f = sup {abs (f x) | abs x = 1}

vector_derivative

⊢ ∀f net. vector_derivative f net = @f'. (f has_vector_derivative f') net

Theorems

ABS_BOUND_GENERALIZE

⊢ ∀f b.
    linear f ⇒ ((∀x. (abs x = 1) ⇒ abs (f x) ≤ b) ⇔ ∀x. abs (f x) ≤ b * abs x)

CONNECTED_COMPACT_INTERVAL_1

⊢ ∀s. connected s ∧ compact s ⇔ ∃a b. s = interval [(a,b)]

CONTINUOUS_AT_EXP

⊢ ∀z. exp continuous at z

CONTINUOUS_ON_EXP

⊢ ∀s. exp continuous_on s

CONTINUOUS_WITHIN_EXP

⊢ ∀s z. exp continuous (at z within s)

CONVEX_ALT

⊢ ∀s. convex s ⇔
      ∀x y u. x ∈ s ∧ y ∈ s ∧ 0 ≤ u ∧ u ≤ 1 ⇒ (1 − u) * x + u * y ∈ s

CONVEX_BALL

⊢ ∀x e. convex (ball (x,e))

CONVEX_CBALL

⊢ ∀x e. convex (cball (x,e))

CONVEX_CONNECTED

⊢ ∀s. convex s ⇒ connected s

CONVEX_DISTANCE

⊢ ∀s a. (λx. dist (a,x)) convex_on s

CONVEX_INDEXED

⊢ ∀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

⊢ ∀a b. convex (interval [(a,b)]) ∧ convex (interval (a,b))

CONVEX_SUM

⊢ ∀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

⊢ ∀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

⊢ ∀f x. f differentiable at x ⇒ f continuous at x

DIFFERENTIABLE_IMP_CONTINUOUS_ON

⊢ ∀f s. f differentiable_on s ⇒ f continuous_on s

DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN

⊢ ∀f x s. f differentiable (at x within s) ⇒ f continuous (at x within s)

DIFFERENTIABLE_ON_EMPTY

⊢ ∀f. f differentiable_on ∅

DIFFERENTIABLE_ON_SUBSET

⊢ ∀f s t. f differentiable_on t ∧ s ⊆ t ⇒ f differentiable_on s

DIFFERENTIABLE_WITHIN_SUBSET

⊢ ∀f s t x.
    f differentiable (at x within t) ∧ s ⊆ t ⇒
    f differentiable (at x within s)

DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀z. ((λn. z pow n / &FACT n) sums exp z) (from 0)

EXP_CONVERGES_UNIFORMLY

⊢ ∀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

⊢ ∀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

⊢ ∀w z. ((λn. z pow n / &FACT n) sums w) (from 0) ⇔ (w = exp z)

FRECHET_DERIVATIVE_WORKS

⊢ ∀f net.
    f differentiable net ⇔ (f has_derivative frechet_derivative f net) net

HAS_DERIVATIVE_ADD

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀f f' x s.
    (f has_derivative f') (at x) ⇒ (f has_derivative f') (at x within s)

HAS_DERIVATIVE_BILINEAR_AT

⊢ ∀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

⊢ ∀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

⊢ ∀f f' net c.
    (f has_derivative f') net ⇒
    ((λx. c * f x) has_derivative (λh. c * f' h)) net

HAS_DERIVATIVE_CONST

⊢ ∀c net. ((λx. c) has_derivative (λh. 0)) net

HAS_DERIVATIVE_EXP

⊢ ∀z. (exp has_derivative (λy. exp z * y)) (at z)

HAS_DERIVATIVE_ID

⊢ ∀net. ((λx. x) has_derivative (λh. h)) net

HAS_DERIVATIVE_IMP_CONTINUOUS_AT

⊢ ∀f f' x. (f has_derivative f') (at x) ⇒ f continuous at x

HAS_DERIVATIVE_LINEAR

⊢ ∀f net. linear f ⇒ (f has_derivative f) net

HAS_DERIVATIVE_MUL_AT

⊢ ∀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

⊢ ∀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

⊢ ∀f f' net.
    (f has_derivative f') net ⇒ ((λx. -f x) has_derivative (λh. -f' h)) net

HAS_DERIVATIVE_POW

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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'

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀s a b u. convex s ∧ a ∈ s ∧ b ∈ s ∧ 0 ≤ u ∧ u ≤ 1 ⇒ (1 − u) * a + u * b ∈ s

IS_INTERVAL_CONNECTED

⊢ ∀s. is_interval s ⇒ connected s

IS_INTERVAL_CONNECTED_1

⊢ ∀s. is_interval s ⇔ connected s

IS_INTERVAL_CONVEX

⊢ ∀s. is_interval s ⇒ convex s

IS_INTERVAL_CONVEX_1

⊢ ∀s. is_interval s ⇔ convex s

LIMPT_APPROACHABLE

⊢ ∀x s.
    x limit_point_of s ⇔ ∀e. 0 < e ⇒ ∃x'. x' ∈ s ∧ x' ≠ x ∧ dist (x',x) < e

LIMPT_OF_CONVEX

⊢ ∀s x. convex s ∧ x ∈ s ⇒ (x limit_point_of s ⇔ s ≠ {x})

LIM_MUL_ABS_WITHIN

⊢ ∀f a s.
    (f ⟶ 0) (at a within s) ⇒ ((λx. abs (x − a) * f x) ⟶ 0) (at a within s)

LINEAR_FRECHET_DERIVATIVE

⊢ ∀f net. f differentiable net ⇒ linear (frechet_derivative f net)

MVT

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀x y a u v. x < a ∧ y < a ∧ 0 ≤ u ∧ 0 ≤ v ∧ (u + v = 1) ⇒ u * x + v * y < a

REAL_MUL_NZ

⊢ ∀a b. a ≠ 0 ∧ b ≠ 0 ⇒ a * b ≠ 0

ROLLE

⊢ ∀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

⊢ ∀s x. convex s ∧ x ∈ s ⇒ (trivial_limit (at x within s) ⇔ (s = {x}))

has_derivative_at

⊢ ∀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

⊢ ∀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)