Theory: lim

Theorems

CONTL_LIM

⊢ ∀f x. f contl x ⇔ (f -> f x) x

CONT_ADD

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x + g x) contl x

CONT_ATTAINS

⊢ ∀f a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ (f x = M)

CONT_ATTAINS2

⊢ ∀f a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ M ≤ f x) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ (f x = M)

CONT_ATTAINS_ALL

⊢ ∀f a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃L M.
      L ≤ M ∧ (∀y. L ≤ y ∧ y ≤ M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)) ∧
      ∀x. a ≤ x ∧ x ≤ b ⇒ L ≤ f x ∧ f x ≤ M

CONT_BOUNDED

⊢ ∀f a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃M. ∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M

CONT_COMPOSE

⊢ ∀f g x. f contl x ∧ g contl f x ⇒ (λx. g (f x)) contl x

CONT_CONST

⊢ ∀k x. (λx. k) contl x

CONT_DIV

⊢ ∀f g x. f contl x ∧ g contl x ∧ g x ≠ 0 ⇒ (λx. f x / g x) contl x

CONT_HASSUP

⊢ ∀f a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧
        ∀N. N < M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ N < f x

CONT_INJ_LEMMA

⊢ ∀f g x d.
    0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
    (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
    ¬∀z. abs (z − x) ≤ d ⇒ f z ≤ f x

CONT_INJ_LEMMA2

⊢ ∀f g x d.
    0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
    (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
    ¬∀z. abs (z − x) ≤ d ⇒ f x ≤ f z

CONT_INJ_RANGE

⊢ ∀f g x d.
    0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
    (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
    ∃e. 0 < e ∧ ∀y. abs (y − f x) ≤ e ⇒ ∃z. abs (z − x) ≤ d ∧ (f z = y)

CONT_INV

⊢ ∀f x. f contl x ∧ f x ≠ 0 ⇒ (λx. (f x)⁻¹) contl x

CONT_INVERSE

⊢ ∀f g x d.
    0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
    (∀z. abs (z − x) ≤ d ⇒ f contl z) ⇒
    g contl f x

CONT_MUL

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x * g x) contl x

CONT_NEG

⊢ ∀f x. f contl x ⇒ (λx. -f x) contl x

CONT_SUB

⊢ ∀f g x. f contl x ∧ g contl x ⇒ (λx. f x − g x) contl x

DIFF_ADD

⊢ ∀f g l m x.
    (f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x + g x) diffl (l + m)) x

DIFF_CARAT

⊢ ∀f l x.
    (f diffl l) x ⇔
    ∃g. (∀z. f z − f x = g z * (z − x)) ∧ g contl x ∧ (g x = l)

DIFF_CHAIN

⊢ ∀f g l m x.
    (f diffl l) (g x) ∧ (g diffl m) x ⇒ ((λx. f (g x)) diffl (l * m)) x

DIFF_CMUL

⊢ ∀f c l x. (f diffl l) x ⇒ ((λx. c * f x) diffl (c * l)) x

DIFF_CONG

⊢ ∀f g l m x y.
    (∃a b. a < y ∧ y < b ∧ ∀z. a < z ∧ z < b ⇒ (f z = g z)) ∧ (l = m) ∧
    (x = y) ⇒
    ((f diffl l) x ⇔ (g diffl m) y)

DIFF_CONG_IMP

⊢ ∀f g y x. (∀x. f x = g x) ∧ (g diffl y) x ⇒ (f diffl y) x

DIFF_CONST

⊢ ∀k x. ((λx. k) diffl 0) x

DIFF_CONT

⊢ ∀f l x. (f diffl l) x ⇒ f contl x

DIFF_DIV

⊢ ∀f g l m x.
    (f diffl l) x ∧ (g diffl m) x ∧ g x ≠ 0 ⇒
    ((λx. f x / g x) diffl ((l * g x − m * f x) / (g x)²)) x

DIFF_EQ_FUN_EQ

⊢ ∀f g s.
    is_interval s ∧ (∀z. z ∈ s ⇒ f contl z) ∧ (∀z. z ∈ s ⇒ g contl z) ∧
    (∀z. z ∈ interior s ⇒ ∃l. (f diffl l) z ∧ (g diffl l) z) ⇒
    ∃c. ∀x. x ∈ s ⇒ (f x = g x + c)

DIFF_INV

⊢ ∀f l x. (f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. (f x)⁻¹) diffl -(l / (f x)²)) x

DIFF_INVERSE

⊢ ∀f g l x d.
    0 < d ∧ (∀z. abs (z − x) ≤ d ⇒ (g (f z) = z)) ∧
    (∀z. abs (z − x) ≤ d ⇒ f contl z) ∧ (f diffl l) x ∧ l ≠ 0 ⇒
    (g diffl l⁻¹) (f x)

DIFF_INVERSE_LT

⊢ ∀f g l x d.
    0 < d ∧ (∀z. abs (z − x) < d ⇒ (g (f z) = z)) ∧
    (∀z. abs (z − x) < d ⇒ f contl z) ∧ (f diffl l) x ∧ l ≠ 0 ⇒
    (g diffl l⁻¹) (f x)

DIFF_INVERSE_OPEN

⊢ ∀f g l a x b.
    a < x ∧ x < b ∧ (∀z. a < z ∧ z < b ⇒ (g (f z) = z) ∧ f contl z) ∧
    (f diffl l) x ∧ l ≠ 0 ⇒
    (g diffl l⁻¹) (f x)

DIFF_ISCONST

⊢ ∀f a b.
    a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
    (∀x. a < x ∧ x < b ⇒ (f diffl 0) x) ⇒
    ∀x. a ≤ x ∧ x ≤ b ⇒ (f x = f a)

DIFF_ISCONST_ALL

⊢ ∀f. (∀x. (f diffl 0) x) ⇒ ∀x y. f x = f y

DIFF_ISCONST_END

⊢ ∀f a b.
    a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
    (∀x. a < x ∧ x < b ⇒ (f diffl 0) x) ⇒
    (f b = f a)

DIFF_LCONST

⊢ ∀f x l.
    (f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ (f y = f x)) ⇒
    (l = 0)

DIFF_LDEC

⊢ ∀f x l.
    (f diffl l) x ∧ l < 0 ⇒ ∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x − h)

DIFF_LINC

⊢ ∀f x l.
    (f diffl l) x ∧ 0 < l ⇒ ∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x + h)

DIFF_LMAX

⊢ ∀f x l.
    (f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f y ≤ f x) ⇒ (l = 0)

DIFF_LMIN

⊢ ∀f x l.
    (f diffl l) x ∧ (∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ f x ≤ f y) ⇒ (l = 0)

DIFF_MUL

⊢ ∀f g l m x.
    (f diffl l) x ∧ (g diffl m) x ⇒
    ((λx. f x * g x) diffl (l * g x + m * f x)) x

DIFF_NEG

⊢ ∀f l x. (f diffl l) x ⇒ ((λx. -f x) diffl -l) x

DIFF_NEG_ANTIMONO_LT_CC

⊢ ∀f a b.
    f contl a ∧ f contl b ∧ (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. a ≤ x ∧ y ≤ b ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_CO

⊢ ∀f a b.
    f contl a ∧ (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. a ≤ x ∧ y < b ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_CU

⊢ ∀f a.
    f contl a ∧ (∀z. a < z ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. a ≤ x ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_INTERVAL

⊢ ∀f s.
    is_interval s ∧ (∀z. z ∈ s ⇒ f contl z) ∧
    (∀z. z ∈ interior s ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_OC

⊢ ∀f a b.
    f contl b ∧ (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. a < x ∧ y ≤ b ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_OO

⊢ ∀f a b.
    (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. a < x ∧ y < b ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_OU

⊢ ∀f a.
    (∀z. a < z ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. a < x ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_UC

⊢ ∀f b.
    f contl b ∧ (∀z. z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. y ≤ b ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_UO

⊢ ∀f b.
    (∀z. z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
    ∀x y. y < b ∧ x < y ⇒ f y < f x

DIFF_NEG_ANTIMONO_LT_UU

⊢ ∀f. (∀z. ∃l. l < 0 ∧ (f diffl l) z) ⇒ ∀x y. x < y ⇒ f y < f x

DIFF_POS_MONO_LT_CC

⊢ ∀f a b.
    f contl a ∧ f contl b ∧ (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. a ≤ x ∧ y ≤ b ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_CO

⊢ ∀f a b.
    f contl a ∧ (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. a ≤ x ∧ y < b ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_CU

⊢ ∀f a.
    f contl a ∧ (∀z. a < z ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. a ≤ x ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_INTERVAL

⊢ ∀f s.
    is_interval s ∧ (∀z. z ∈ s ⇒ f contl z) ∧
    (∀z. z ∈ interior s ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_OC

⊢ ∀f a b.
    f contl b ∧ (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. a < x ∧ y ≤ b ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_OO

⊢ ∀f a b.
    (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. a < x ∧ y < b ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_OU

⊢ ∀f a.
    (∀z. a < z ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. a < x ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_UC

⊢ ∀f b.
    f contl b ∧ (∀z. z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. y ≤ b ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_UO

⊢ ∀f b.
    (∀z. z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
    ∀x y. y < b ∧ x < y ⇒ f x < f y

DIFF_POS_MONO_LT_UU

⊢ ∀f. (∀z. ∃l. 0 < l ∧ (f diffl l) z) ⇒ ∀x y. x < y ⇒ f x < f y

DIFF_POW

⊢ ∀n x. ((λx. x pow n) diffl (&n * x pow (n − 1))) x

DIFF_SUB

⊢ ∀f g l m x.
    (f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x − g x) diffl (l − m)) x

DIFF_SUM

⊢ ∀f f' m n x.
    (∀r. m ≤ r ∧ r < m + n ⇒ ((λx. f r x) diffl f' r x) x) ⇒
    ((λx. sum (m,n) (λn. f n x)) diffl sum (m,n) (λr. f' r x)) x

DIFF_UNIQ

⊢ ∀f l m x. (f diffl l) x ∧ (f diffl m) x ⇒ (l = m)

DIFF_X

⊢ ∀x. ((λx. x) diffl 1) x

DIFF_XM1

⊢ ∀x. x ≠ 0 ⇒ ((λx. x⁻¹) diffl -x⁻¹ ²) x

HAS_DERIVATIVE_POW'

⊢ ∀n x. ((λx. x pow n) has_derivative (λy. &n * x pow (n − 1) * y)) (at x)

HAS_VECTOR_DERIVATIVE_ALT

⊢ ∀f l x.
    (f has_vector_derivative l) (at x) ⇔
    ((λh. (f (x + h) − f x) / h) ⟶ l) (at 0)

HAS_VECTOR_DERIVATIVE_POW

⊢ ∀n x. ((λx. x pow n) has_vector_derivative &n * x pow (n − 1)) (at x)

INTERVAL_ABS

⊢ ∀x z d. x − d ≤ z ∧ z ≤ x + d ⇔ abs (z − x) ≤ d

INTERVAL_CLEMMA

⊢ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (y − x) ≤ d ⇒ a < y ∧ y < b

INTERVAL_LEMMA

⊢ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ a ≤ y ∧ y ≤ b

INTERVAL_LEMMA_LT

⊢ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (x − y) < d ⇒ a < y ∧ y < b

IVT

⊢ ∀f a b y.
    a ≤ b ∧ (f a ≤ y ∧ y ≤ f b) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)

IVT2

⊢ ∀f a b y.
    a ≤ b ∧ (f b ≤ y ∧ y ≤ f a) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ⇒
    ∃x. a ≤ x ∧ x ≤ b ∧ (f x = y)

IVT_DERIVATIVE_0

⊢ ∀f f' a b.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ f' a > 0 ∧ f' b < 0 ⇒
    ∃z. a < z ∧ z < b ∧ (f' z = 0)

IVT_DERIVATIVE_NEG

⊢ ∀f f' a b y.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ f' a < y ∧ f' b > y ⇒
    ∃z. a < z ∧ z < b ∧ (f' z = y)

IVT_DERIVATIVE_POS

⊢ ∀f f' a b y.
    a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ∧ f' a > y ∧ f' b < y ⇒
    ∃z. a < z ∧ z < b ∧ (f' z = y)

LIM

⊢ ∀f y0 x0.
    (f -> y0) x0 ⇔
    ∀e. 0 < e ⇒
        ∃d. 0 < d ∧
            ∀x. 0 < abs (x − x0) ∧ abs (x − x0) < d ⇒ abs (f x − y0) < e

LIM_ADD

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x + g x) -> l + m) x

LIM_AT_LIM

⊢ ∀f l a. (f ⟶ l) (at a) ⇔ (f -> l) a

LIM_CONST

⊢ ∀k x. ((λx. k) -> k) x

LIM_DIV

⊢ ∀f g l m x.
    (f -> l) x ∧ (g -> m) x ∧ m ≠ 0 ⇒ ((λx. f x / g x) -> l / m) x

LIM_EQUAL

⊢ ∀f g l x0. (∀x. x ≠ x0 ⇒ (f x = g x)) ⇒ ((f -> l) x0 ⇔ (g -> l) x0)

LIM_INV

⊢ ∀f l x. (f -> l) x ∧ l ≠ 0 ⇒ ((λx. (f x)⁻¹) -> l⁻¹) x

LIM_MUL

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x * g x) -> l * m) x

LIM_NEG

⊢ ∀f l x. (f -> l) x ⇔ ((λx. -f x) -> -l) x

LIM_NULL

⊢ ∀f l x. (f -> l) x ⇔ ((λx. f x − l) -> 0) x

LIM_SUB

⊢ ∀f g l m x. (f -> l) x ∧ (g -> m) x ⇒ ((λx. f x − g x) -> l − m) x

LIM_TRANSFORM

⊢ ∀f g x0 l. ((λx. f x − g x) -> 0) x0 ∧ (g -> l) x0 ⇒ (f -> l) x0

LIM_UNIQ

⊢ ∀f l m x. (f -> l) x ∧ (f -> m) x ⇒ (l = m)

LIM_X

⊢ ∀x0. ((λx. x) -> x0) x0

MVT

⊢ ∀f a b.
    a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
    (∀x. a < x ∧ x < b ⇒ f differentiable x) ⇒
    ∃l z. a < z ∧ z < b ∧ (f diffl l) z ∧ (f b − f a = (b − a) * l)

MVT_LEMMA

⊢ ∀f a b.
    (λx. f x − (f b − f a) / (b − a) * x) a =
    (λx. f x − (f b − f a) / (b − a) * x) b

ROLLE

⊢ ∀f a b.
    a < b ∧ (f a = f b) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f contl x) ∧
    (∀x. a < x ∧ x < b ⇒ f differentiable x) ⇒
    ∃z. a < z ∧ z < b ∧ (f diffl 0) z

contl_eq_continuous_at

⊢ ∀f x. f contl x ⇔ f continuous at x

diff1_I

⊢ diff1 (λx. x) = (λx. 1)

diff1_add

⊢ ∀f g x.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λt. f t + g t) x = diff1 f x + diff1 g x)

diff1_alt

⊢ ∀f x. diff1 f x = @y. (f has_vector_derivative y) (at x)

diff1_cmul

⊢ ∀f c x.
    (∀x. higher_differentiable 1 f x) ⇒
    (diff1 (λx. c * f x) x = c * diff1 f x)

diff1_def

⊢ ∀f x. diff1 f x = @y. (f diffl y) x

diff1_imp_diffl

⊢ ∀f x y. higher_differentiable 1 f x ∧ (diff1 f x = y) ⇒ (f diffl y) x

diff1_mul

⊢ ∀f g x.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λt. f t * g t) x = diff1 f x * g x + f x * diff1 g x)

diff1_sub

⊢ ∀f g x.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λt. f t − g t) x = diff1 f x − diff1 g x)

differentiable_alt

⊢ ∀f x. f differentiable x ⇔ derivative$differentiable f (at x)

differentiable_has_vector_derivative

⊢ ∀f x. f differentiable x ⇔ ∃l. (f has_vector_derivative l) (at x)

diffl_has_derivative

⊢ ∀f l x. (f diffl l) x ⇔ (f has_derivative (λx. x * l)) (at x)

diffl_has_derivative'

⊢ ∀f l x. (f diffl l) x ⇔ (f has_derivative $* l) (at x)

diffl_has_vector_derivative

⊢ ∀f l x. (f diffl l) x ⇔ (f has_vector_derivative l) (at x)

diffl_imp_diff1

⊢ ∀f x y. (f diffl y) x ⇒ (diff1 f x = y)

diffl_imp_diffn

⊢ ∀m f x y. (diffn m f diffl y) x ⇒ (diffn (SUC m) f x = y)

diffn_0

⊢ diffn 0 f = f

diffn_1

⊢ ∀f x. diff1 f x = @y. (f diffl y) x

diffn_ADD

⊢ ∀m n f.
    (∀x. higher_differentiable (m + n) f x) ⇒
    (diffn m (diffn n f) = diffn (m + n) f)

diffn_SUC

⊢ ∀m f.
    (∀x. higher_differentiable (SUC m) f x) ⇒
    (diffn m (diff1 f) = diffn (SUC m) f)

diffn_SUC'

⊢ ∀m f.
    (∀x. higher_differentiable (SUC m) f x) ⇒
    (diff1 (diffn m f) = diffn (SUC m) f)

diffn_add

⊢ ∀f g.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λx. f x + g x) = (λx. diff1 f x + diff1 g x))

diffn_chain

⊢ ∀f g.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λx. f (g x)) = (λx. diff1 f (g x) * diff1 g x))

diffn_cmul

⊢ ∀f c.
    (∀x. higher_differentiable 1 f x) ⇒
    (diff1 (λx. c * f x) = (λx. c * diff1 f x))

diffn_cmul_general

⊢ ∀c f n.
    (∀x. higher_differentiable n f x) ⇒
    ∀x. diffn n (λt. c * f t) x = c * diffn n f x

diffn_compute

⊢ (∀f x. diffn 0 f x = f x) ∧
  (∀m f x.
     diffn (NUMERAL (BIT1 m)) f x =
     @y. (diffn (NUMERAL (BIT1 m) − 1) f diffl y) x) ∧
  ∀m f x.
    diffn (NUMERAL (BIT2 m)) f x =
    @y. (diffn (NUMERAL (BIT1 m)) f diffl y) x

diffn_cong

⊢ ∀n f g x. (∀x. f x = g x) ⇒ (diffn n f x = diffn n g x)

diffn_const

⊢ ∀k. diff1 (λx. k) = (λx. 0)

diffn_const_0

⊢ ∀n x. (diffn n (λx. 0) diffl 0) x

diffn_imp_diffl

⊢ ∀f x y n.
    higher_differentiable (SUC n) f x ∧ (diffn (SUC n) f x = y) ⇒
    (diffn n f diffl y) x

diffn_linear

⊢ ∀a b. diff1 (λx. a * x + b) = (λx. a)

diffn_linear'

⊢ ∀a b n.
    2 ≤ n ∧ (∀t. higher_differentiable n (λx. a * x + b) t) ⇒
    (diffn n (λx. a * x + b) = (λx. 0))

diffn_linear_general

⊢ ∀a b f n.
    (∀x. higher_differentiable n f x) ⇒
    (diffn n (λx. f (a * x + b)) = (λx. a pow n * diffn n f (a * x + b)))

diffn_mul

⊢ ∀f g.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λx. f x * g x) = (λx. diff1 f x * g x + diff1 g x * f x))

diffn_neg_sub

⊢ ∀n f a.
    (∀x. higher_differentiable n f x) ⇒
    (diffn n (λx. f (a − x)) = (λx. -1 pow n * diffn n f (a − x)))

diffn_sub

⊢ ∀f g.
    (∀t. higher_differentiable 1 f t) ∧ (∀t. higher_differentiable 1 g t) ⇒
    (diff1 (λx. f x − g x) = (λx. diff1 f x − diff1 g x))

diffn_thm

⊢ ∀f. (∀m t. ∃x. (diffn m f diffl x) t) ⇒
      (diffn 0 f = f) ∧ ∀m t. (diffn m f diffl diffn (SUC m) f t) t

has_vector_derivative_imp_diff1

⊢ ∀f x y. (f has_vector_derivative y) (at x) ⇒ (diff1 f x = y)

higher_differentiable_0

⊢ ∀n x. higher_differentiable n (λx. 0) x

higher_differentiable_1

⊢ ∀f x. higher_differentiable 1 f x ⇔ ∃y. (f diffl y) x

higher_differentiable_1_eq_differentiable

⊢ ∀f x. higher_differentiable 1 f x ⇔ derivative$differentiable f (at x)

higher_differentiable_1_eq_differentiable_on

⊢ ∀f. (∀x. higher_differentiable 1 f x) ⇔ f differentiable_on 𝕌(:real)

higher_differentiable_1_eq_differentiable_on'

⊢ ∀f s.
    open s ⇒
    ((∀x. x ∈ s ⇒ higher_differentiable 1 f x) ⇔ f differentiable_on s)

higher_differentiable_I

⊢ ∀k x. higher_differentiable k (λx. x) x

higher_differentiable_add

⊢ ∀f g n.
    (∀x. higher_differentiable n f x) ∧ (∀x. higher_differentiable n g x) ⇒
    ∀x. higher_differentiable n (λx. f x + g x) x

higher_differentiable_affine

⊢ ∀a b n f.
    (∀x. higher_differentiable n f x) ⇒
    ∀x. higher_differentiable n (λx. f (a * x + b)) x

higher_differentiable_ainv

⊢ ∀k x. higher_differentiable k (λx. -x) x

higher_differentiable_chain

⊢ ∀n f g.
    (∀x. higher_differentiable n f x) ∧ (∀x. higher_differentiable n g x) ⇒
    ∀x. higher_differentiable n (λx. f (g x)) x

higher_differentiable_cmul

⊢ ∀f c n.
    (∀x. higher_differentiable n f x) ⇒
    ∀x. higher_differentiable n (λx. c * f x) x

higher_differentiable_cmul_eq

⊢ ∀f c n.
    c ≠ 0 ⇒
    ((∀x. higher_differentiable n (λx. c * f x) x) ⇔
     ∀x. higher_differentiable n f x)

higher_differentiable_compose

⊢ ∀n f g.
    (∀x. higher_differentiable n f x) ∧ (∀x. higher_differentiable n g x) ⇒
    ∀x. higher_differentiable n (f ∘ g) x

higher_differentiable_compute

⊢ (∀f x. higher_differentiable 0 f x ⇔ T) ∧
  (∀m f x.
     higher_differentiable (NUMERAL (BIT1 m)) f x ⇔
     (∃y. (diffn (NUMERAL (BIT1 m) − 1) f diffl y) x) ∧
     higher_differentiable (NUMERAL (BIT1 m) − 1) f x) ∧
  ∀m f x.
    higher_differentiable (NUMERAL (BIT2 m)) f x ⇔
    (∃y. (diffn (NUMERAL (BIT1 m)) f diffl y) x) ∧
    higher_differentiable (NUMERAL (BIT1 m)) f x

higher_differentiable_const

⊢ ∀n k x. higher_differentiable n (λx. k) x

higher_differentiable_continuous_on

⊢ ∀m n f.
    (∀x. higher_differentiable n f x) ∧ m < n ∧ 0 < n ⇒
    diffn m f continuous_on 𝕌(:real)

higher_differentiable_imp_11

⊢ ∀n f x.
    1 < n ∧ higher_differentiable n f x ⇒
    higher_differentiable 1 (diff1 f) x

higher_differentiable_imp_1n

⊢ ∀n f.
    (∀x. higher_differentiable (SUC n) f x) ⇒
    ∀x. higher_differentiable 1 (diffn n f) x

higher_differentiable_imp_continuous

⊢ ∀f x. higher_differentiable 1 f x ⇒ f continuous at x

higher_differentiable_imp_continuous'

⊢ ∀n f x. higher_differentiable n f x ∧ 1 ≤ n ⇒ f continuous at x

higher_differentiable_imp_mn

⊢ ∀m n f.
    (∀x. higher_differentiable (m + n) f x) ⇒
    ∀x. higher_differentiable m (diffn n f) x

higher_differentiable_imp_n1

⊢ ∀n f.
    (∀x. higher_differentiable (SUC n) f x) ⇒
    ∀x. higher_differentiable n (diff1 f) x

higher_differentiable_linear

⊢ ∀a b n x. higher_differentiable n (λx. a * x + b) x

higher_differentiable_mono

⊢ ∀f n m t.
    m ≤ n ∧ higher_differentiable n f t ⇒ higher_differentiable m f t

higher_differentiable_mul

⊢ ∀f g n.
    (∀x. higher_differentiable n f x) ∧ (∀x. higher_differentiable n g x) ⇒
    ∀x. higher_differentiable n (λx. f x * g x) x

higher_differentiable_neg

⊢ ∀n f.
    (∀x. higher_differentiable n f x) ⇒
    ∀x. higher_differentiable n (λx. -f x) x

higher_differentiable_neg'

⊢ ∀n f.
    (∀x. higher_differentiable n f x) ⇒
    ∀x. higher_differentiable n (λx. f (-x)) x

higher_differentiable_neg_sub

⊢ ∀a n f.
    (∀x. higher_differentiable n f x) ⇒
    ∀x. higher_differentiable n (λx. f (a − x)) x

higher_differentiable_sub

⊢ ∀f g n.
    (∀x. higher_differentiable n f x) ∧ (∀x. higher_differentiable n g x) ⇒
    ∀x. higher_differentiable n (λx. f x − g x) x

higher_differentiable_sub_linear

⊢ ∀a k x. higher_differentiable k (λx. a − x) x

higher_differentiable_thm

⊢ ∀f. (diffn 0 f = f) ∧
      ∀m t.
        higher_differentiable (SUC m) f t ⇒
        (diffn m f diffl diffn (SUC m) f t) t

Theory lim

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems