Theory: lim

Parents

• seq

Types

Constants

• ->  :(real -> real) -> real -> real -> bool
• diffl  :(real -> real) -> real -> real -> bool
• contl  :(real -> real) -> real -> bool
• differentiable  :(real -> real) -> real -> bool

Definitions

contl

|- !f x. f contl x = ((\h. f (x + h)) -> f x) 0

differentiable

|- !f x. f differentiable x = ?l. (f diffl l) x

diffl

|- !f l x. (f diffl l) x = ((\h. (f (x + h) - f x) / h) -> l) 0

tends_real_real

|- !f l x0. (f -> l) x0 = (f tends l) (mtop mr1,tendsto (mr1,x0))

Theorems

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. inv (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

CONTL_LIM

|- !f x. f contl x = (f -> f x) 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_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 pow 2)) x

DIFF_INV

|- !f l x.
     (f diffl l) x /\ ~(f x = 0) ==>
     ((\x. inv (f x)) diffl ~(l / f x pow 2)) 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 inv 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 inv 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 inv 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_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. inv x) diffl ~(inv x pow 2)) 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

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)

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_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. inv (f x)) -> inv 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