Theory "seq"

Parents nets

Signature

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

Definitions

tends_num_real

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

convergent

|- ∀f. convergent f ⇔ ∃l. f --> l

cauchy

|- ∀f. cauchy f ⇔ ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ∧ n ≥ N ⇒ abs (f m − f n) < e

lim

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

subseq

|- ∀f. subseq f ⇔ ∀m n. m < n ⇒ f m < f n

mono

|- ∀f. mono f ⇔ (∀m n. m ≤ n ⇒ f m ≤ f n) ∨ ∀m n. m ≤ n ⇒ f m ≥ f n

sums

|- ∀f s. f sums s ⇔ (λn. sum (0,n) f) --> s

summable

|- ∀f. summable f ⇔ ∃s. f sums s

suminf

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

Theorems

SEQ

|- ∀x x0. x --> x0 ⇔ ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ abs (x n − x0) < e

SEQ_CONST

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

SEQ_ADD

|- ∀x x0 y y0. x --> x0 ∧ y --> y0 ⇒ (λn. x n + y n) --> (x0 + y0)

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_INV

|- ∀x x0. x --> x0 ∧ x0 ≠ 0 ⇒ (λn. inv (x n)) --> inv x0

SEQ_SUB

|- ∀x x0 y y0. x --> x0 ∧ y --> y0 ⇒ (λn. x n − y n) --> (x0 − y0)

SEQ_DIV

|- ∀x x0 y y0. x --> x0 ∧ y --> y0 ∧ y0 ≠ 0 ⇒ (λn. x n / y n) --> (x0 / y0)

SEQ_UNIQ

|- ∀x x1 x2. x --> x1 ∧ x --> x2 ⇒ (x1 = x2)

SEQ_LIM

|- ∀f. convergent f ⇔ f --> lim f

SUBSEQ_SUC

|- ∀f. subseq f ⇔ ∀n. f n < f (SUC n)

MONO_SUC

|- ∀f. mono f ⇔ (∀n. f (SUC n) ≥ f n) ∨ ∀n. f (SUC n) ≤ f n

MAX_LEMMA

|- ∀s N. ∃k. ∀n. n < N ⇒ abs (s n) < k

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_CBOUNDED

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

SEQ_ICONV

|- ∀f. bounded (mr1,$>=) f ∧ (∀m n. m ≥ n ⇒ f m ≥ f n) ⇒ convergent f

SEQ_NEG_CONV

|- ∀f. convergent f ⇔ convergent (λn. -f n)

SEQ_NEG_BOUNDED

|- ∀f. bounded (mr1,$>=) (λn. -f n) ⇔ bounded (mr1,$>=) f

SEQ_BCONV

|- ∀f. bounded (mr1,$>=) f ∧ mono f ⇒ convergent f

SEQ_MONOSUB

|- ∀s. ∃f. subseq f ∧ mono (λn. s (f n))

SEQ_SBOUNDED

|- ∀s f. bounded (mr1,$>=) s ⇒ bounded (mr1,$>=) (λn. s (f n))

SEQ_SUBLE

|- ∀f. subseq f ⇒ ∀n. n ≤ f n

SEQ_DIRECT

|- ∀f. subseq f ⇒ ∀N1 N2. ∃n. n ≥ N1 ∧ f n ≥ N2

SEQ_CAUCHY

|- ∀f. cauchy f ⇔ convergent f

SEQ_LE

|- ∀f g l m. f --> l ∧ g --> m ∧ (∃N. ∀n. n ≥ N ⇒ f n ≤ g n) ⇒ l ≤ m

SEQ_SUC

|- ∀f l. f --> l ⇔ (λn. f (SUC n)) --> l

SEQ_ABS

|- ∀f. (λn. abs (f n)) --> 0 ⇔ f --> 0

SEQ_ABS_IMP

|- ∀f l. f --> l ⇒ (λn. abs (f n)) --> abs l

SEQ_INV0

|- ∀f. (∀y. ∃N. ∀n. n ≥ N ⇒ f n > y) ⇒ (λn. inv (f n)) --> 0

SEQ_POWER_ABS

|- ∀c. abs c < 1 ⇒ (λn. abs c pow n) --> 0

SEQ_POWER

|- ∀c. abs c < 1 ⇒ (λn. c pow n) --> 0

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

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)

SUM_SUMMABLE

|- ∀f l. f sums l ⇒ summable f

SUMMABLE_SUM

|- ∀f. summable f ⇒ f sums suminf f

SUM_UNIQ

|- ∀f x. f sums x ⇒ (x = suminf f)

SER_0

|- ∀f n. (∀m. n ≤ m ⇒ (f m = 0)) ⇒ f sums sum (0,n) 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_GROUP

|- ∀f k. summable f ∧ 0 < k ⇒ (λn. sum (n * k,k) f) sums suminf f

SER_PAIR

|- ∀f. summable f ⇒ (λn. sum (2 * n,2) f) sums suminf f

SER_OFFSET

|- ∀f. summable f ⇒ ∀k. (λn. f (n + k)) sums (suminf f − sum (0,k) 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_ADD

|- ∀x x0 y y0. x sums x0 ∧ y sums y0 ⇒ (λn. x n + y n) sums (x0 + y0)

SER_CMUL

|- ∀x x0 c. x sums x0 ⇒ (λn. c * x n) sums (c * x0)

SER_NEG

|- ∀x x0. x sums x0 ⇒ (λn. -x n) sums -x0

SER_SUB

|- ∀x x0 y y0. x sums x0 ∧ y sums y0 ⇒ (λn. x n − y n) sums (x0 − y0)

SER_CDIV

|- ∀x x0 c. x sums x0 ⇒ (λn. x n / c) sums (x0 / c)

SER_CAUCHY

|- ∀f. summable f ⇔ ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ⇒ abs (sum (m,n) f) < e

SER_ZERO

|- ∀f. summable f ⇒ f --> 0

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_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_ACONV

|- ∀f. summable (λn. abs (f n)) ⇒ summable f

SER_ABS

|- ∀f. summable (λn. abs (f n)) ⇒ abs (suminf f) ≤ suminf (λn. abs (f n))

GP_FINITE

|- ∀x. x ≠ 1 ⇒ ∀n. sum (0,n) (λn. x pow n) = (x pow n − 1) / (x − 1)

GP

|- ∀x. abs x < 1 ⇒ (λn. x pow n) sums inv (1 − x)

ABS_NEG_LEMMA

|- ∀c. c ≤ 0 ⇒ ∀x y. abs x ≤ c * abs y ⇒ (x = 0)

SER_RATIO

|- ∀f c N. c < 1 ∧ (∀n. n ≥ N ⇒ abs (f (SUC n)) ≤ c * abs (f n)) ⇒ summable f

LE_SEQ_IMP_LE_LIM

|- ∀x y f. (∀n. x ≤ f n) ∧ f --> y ⇒ x ≤ y

SEQ_LE_IMP_LIM_LE

|- ∀x y f. (∀n. f n ≤ x) ∧ f --> y ⇒ y ≤ x

SEQ_MONO_LE

|- ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ f --> x ⇒ f n ≤ x

SEQ_LE_MONO

|- ∀f x n. (∀n. f (n + 1) ≤ f n) ∧ f --> x ⇒ x ≤ f n