Theory: seq

Parents

• nets

Types

Constants

• lim  :(num -> real) -> real
• subseq  :(num -> num) -> bool
• summable  :(num -> real) -> bool
• -->  :(num -> real) -> real -> bool
• suminf  :(num -> real) -> real
• mono  :(num -> real) -> bool
• convergent  :(num -> real) -> bool
• sums  :(num -> real) -> real -> bool
• cauchy  :(num -> real) -> bool

Definitions

cauchy

|- !f.
     cauchy f =
     !e. 0 < e ==> ?N. !m n. m >= N /\ n >= N ==> abs (f m - f n) < e

convergent

|- !f. convergent f = ?l. f --> l

lim

|- !f. lim f = @l. f --> l

mono

|- !f. mono f = (!m n. m <= n ==> f m <= f n) \/ !m n. m <= n ==> f m >= f n

subseq

|- !f. subseq f = !m n. m < n ==> f m < f n

suminf

|- !f. suminf f = @s. f sums s

summable

|- !f. summable f = ?s. f sums s

sums

|- !f s. f sums s = (\n. sum (0,n) f) --> s

tends_num_real

|- !x x0. x --> x0 = (x tends x0) (mtop mr1,$>=)

Theorems

ABS_NEG_LEMMA

|- !c. c <= 0 ==> !x y. abs x <= c * abs y ==> (x = 0)

BOLZANO_LEMMA

|- !P.
     (!a b c. a <= b /\ b <= c /\ P (a,b) /\ P (b,c) ==> P (a,c)) /\
     (!x. ?d. 0 < d /\ !a b. a <= x /\ x <= b /\ b - a < d ==> P (a,b)) ==>
     !a b. a <= b ==> P (a,b)

GP

|- !x. abs x < 1 ==> (\n. x pow n) sums inv (1 - x)

GP_FINITE

|- !x. ~(x = 1) ==> !n. sum (0,n) (\n. x pow n) = (x pow n - 1) / (x - 1)

MAX_LEMMA

|- !s N. ?k. !n. n < N ==> abs (s n) < k

MONO_SUC

|- !f. mono f = (!n. f (SUC n) >= f n) \/ !n. f (SUC n) <= f n

NEST_LEMMA

|- !f g.
     (!n. f (SUC n) >= f n) /\ (!n. g (SUC n) <= g n) /\ (!n. f n <= g n) ==>
     ?l m. l <= m /\ ((!n. f n <= l) /\ f --> l) /\ (!n. m <= g n) /\ g --> m

NEST_LEMMA_UNIQ

|- !f g.
     (!n. f (SUC n) >= f n) /\ (!n. g (SUC n) <= g n) /\ (!n. f n <= g n) /\
     (\n. f n - g n) --> 0 ==>
     ?l. ((!n. f n <= l) /\ f --> l) /\ (!n. l <= g n) /\ g --> l

SEQ

|- !x x0. x --> x0 = !e. 0 < e ==> ?N. !n. n >= N ==> abs (x n - x0) < e

SEQ_ABS

|- !f. (\n. abs (f n)) --> 0 = f --> 0

SEQ_ABS_IMP

|- !f l. f --> l ==> (\n. abs (f n)) --> abs l

SEQ_ADD

|- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x n + y n) --> (x0 + y0)

SEQ_BCONV

|- !f. bounded (mr1,$>=) f /\ mono f ==> convergent f

SEQ_BOUNDED

|- !s. bounded (mr1,$>=) s = ?k. !n. abs (s n) < k

SEQ_BOUNDED_2

|- !f k k'. (!n. k <= f n /\ f n <= k') ==> bounded (mr1,$>=) f

SEQ_CAUCHY

|- !f. cauchy f = convergent f

SEQ_CBOUNDED

|- !f. cauchy f ==> bounded (mr1,$>=) f

SEQ_CONST

|- !k. (\x. k) --> k

SEQ_DIRECT

|- !f. subseq f ==> !N1 N2. ?n. n >= N1 /\ f n >= N2

SEQ_DIV

|- !x x0 y y0.
     x --> x0 /\ y --> y0 /\ ~(y0 = 0) ==> (\n. x n / y n) --> (x0 / y0)

SEQ_ICONV

|- !f. bounded (mr1,$>=) f /\ (!m n. m >= n ==> f m >= f n) ==> convergent f

SEQ_INV

|- !x x0. x --> x0 /\ ~(x0 = 0) ==> (\n. inv (x n)) --> inv x0

SEQ_INV0

|- !f. (!y. ?N. !n. n >= N ==> f n > y) ==> (\n. inv (f n)) --> 0

SEQ_LE

|- !f g l m. f --> l /\ g --> m /\ (?N. !n. n >= N ==> f n <= g n) ==> l <= m

SEQ_LIM

|- !f. convergent f = f --> lim f

SEQ_MONOSUB

|- !s. ?f. subseq f /\ mono (\n. s (f n))

SEQ_MUL

|- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x n * y n) --> (x0 * y0)

SEQ_NEG

|- !x x0. x --> x0 = (\n. ~x n) --> ~x0

SEQ_NEG_BOUNDED

|- !f. bounded (mr1,$>=) (\n. ~f n) = bounded (mr1,$>=) f

SEQ_NEG_CONV

|- !f. convergent f = convergent (\n. ~f n)

SEQ_POWER

|- !c. abs c < 1 ==> (\n. c pow n) --> 0

SEQ_POWER_ABS

|- !c. abs c < 1 ==> (\n. abs c pow n) --> 0

SEQ_SBOUNDED

|- !s f. bounded (mr1,$>=) s ==> bounded (mr1,$>=) (\n. s (f n))

SEQ_SUB

|- !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x n - y n) --> (x0 - y0)

SEQ_SUBLE

|- !f. subseq f ==> !n. n <= f n

SEQ_SUC

|- !f l. f --> l = (\n. f (SUC n)) --> l

SEQ_UNIQ

|- !x x1 x2. x --> x1 /\ x --> x2 ==> (x1 = x2)

SER_0

|- !f n. (!m. n <= m ==> (f m = 0)) ==> f sums sum (0,n) f

SER_ABS

|- !f. summable (\n. abs (f n)) ==> abs (suminf f) <= suminf (\n. abs (f n))

SER_ACONV

|- !f. summable (\n. abs (f n)) ==> summable f

SER_ADD

|- !x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. x n + y n) sums (x0 + y0)

SER_CAUCHY

|- !f. summable f = !e. 0 < e ==> ?N. !m n. m >= N ==> abs (sum (m,n) f) < e

SER_CDIV

|- !x x0 c. x sums x0 ==> (\n. x n / c) sums (x0 / c)

SER_CMUL

|- !x x0 c. x sums x0 ==> (\n. c * x n) sums (c * x0)

SER_COMPAR

|- !f g. (?N. !n. n >= N ==> abs (f n) <= g n) /\ summable g ==> summable f

SER_COMPARA

|- !f g.
     (?N. !n. n >= N ==> abs (f n) <= g n) /\ summable g ==>
     summable (\k. abs (f k))

SER_GROUP

|- !f k. summable f /\ 0 < k ==> (\n. sum (n * k,k) f) sums suminf f

SER_LE

|- !f g. (!n. f n <= g n) /\ summable f /\ summable g ==> suminf f <= suminf g

SER_LE2

|- !f g.
     (!n. abs (f n) <= g n) /\ summable g ==>
     summable f /\ suminf f <= suminf g

SER_NEG

|- !x x0. x sums x0 ==> (\n. ~x n) sums ~x0

SER_OFFSET

|- !f. summable f ==> !k. (\n. f (n + k)) sums (suminf f - sum (0,k) f)

SER_PAIR

|- !f. summable f ==> (\n. sum (2 * n,2) f) sums suminf f

SER_POS_LE

|- !f n. summable f /\ (!m. n <= m ==> 0 <= f m) ==> sum (0,n) f <= suminf f

SER_POS_LT

|- !f n. summable f /\ (!m. n <= m ==> 0 < f m) ==> sum (0,n) f < suminf f

SER_POS_LT_PAIR

|- !f n.
     summable f /\ (!d. 0 < f (n + 2 * d) + f (n + (2 * d + 1))) ==>
     sum (0,n) f < suminf f

SER_RATIO

|- !f c N.
     c < 1 /\ (!n. n >= N ==> abs (f (SUC n)) <= c * abs (f n)) ==> summable f

SER_SUB

|- !x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. x n - y n) sums (x0 - y0)

SER_ZERO

|- !f. summable f ==> f --> 0

SUBSEQ_SUC

|- !f. subseq f = !n. f n < f (SUC n)

SUM_SUMMABLE

|- !f l. f sums l ==> summable f

SUM_UNIQ

|- !f x. f sums x ==> (x = suminf f)

SUMMABLE_SUM

|- !f. summable f ==> f sums suminf f