Theory "seq"

Signature

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

mono_decreasing_def

⊢ ∀f. mono_decreasing f ⇔ ∀m n. m ≤ n ⇒ f n ≤ f m

mono_increasing_def

⊢ ∀f. mono_increasing f ⇔ ∀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 (1 − x)⁻¹

GP_FINITE

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

HALF_CANCEL

⊢ 2 * (1 / 2) = 1

HALF_LT_1

⊢ 1 / 2 < 1

HALF_POS

⊢ 0 < 1 / 2

INCREASING_SEQ

⊢ ∀f l.
    (∀n. f n ≤ f (SUC n)) ∧ (∀n. f n ≤ l) ∧ (∀e. 0 < e ⇒ ∃n. l < f n + e) ⇒
    f ⟶ l

K_PARTIAL

⊢ ∀x. K x = (λz. x)

LE_SEQ_IMP_LE_LIM

⊢ ∀x y f. (∀n. x ≤ f n) ∧ f ⟶ y ⇒ x ≤ y

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

NUM_2D_BIJ_BIG_SQUARE

⊢ ∀f N.
    BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    ∃k. IMAGE f (count N) ⊆ count k × count k

NUM_2D_BIJ_SMALL_SQUARE

⊢ ∀f k.
    BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    ∃N. count k × count k ⊆ IMAGE f (count N)

ONE_MINUS_HALF

⊢ 1 − 1 / 2 = 1 / 2

POS_SUMMABLE

⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃x. ∀n. sum (0,n) f ≤ x) ⇒ summable f

POW_HALF_SER

⊢ (λn. (1 / 2) pow (n + 1)) sums 1

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. (x n)⁻¹) ⟶ x0⁻¹

SEQ_INV0

⊢ ∀f. (∀y. ∃N. ∀n. n ≥ N ⇒ f n > y) ⇒ (λn. (f n)⁻¹) ⟶ 0

SEQ_LE

⊢ ∀f g l m. f ⟶ l ∧ g ⟶ m ∧ (∃N. ∀n. n ≥ N ⇒ f n ≤ g n) ⇒ l ≤ m

SEQ_LE_IMP_LIM_LE

⊢ ∀x y f. (∀n. f n ≤ x) ∧ f ⟶ y ⇒ y ≤ x

SEQ_LE_MONO

⊢ ∀f x n. (∀n. f (n + 1) ≤ f n) ∧ f ⟶ x ⇒ x ≤ f n

SEQ_LIM

⊢ ∀f. convergent f ⇔ f ⟶ lim f

SEQ_MONOSUB

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

SEQ_MONO_LE

⊢ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ f ⟶ x ⇒ f n ≤ x

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_SANDWICH

⊢ ∀f g h l. f ⟶ l ∧ h ⟶ l ∧ (∀n. f n ≤ g n ∧ g n ≤ h n) ⇒ g ⟶ l

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

⊢ ∀f. summable f ∧ (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f

SER_POS_COMPARE

⊢ ∀f g.
    (∀n. 0 ≤ f n) ∧ summable g ∧ (∀n. f n ≤ g n) ⇒
    summable f ∧ suminf f ≤ suminf g

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_POS_MONO

⊢ ∀f. (∀n. 0 ≤ f n) ⇒ mono (λn. sum (0,n) 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)

SUMINF_2D

⊢ ∀f g h.
    (∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
    BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    fᴾ ∘ h sums suminf g

SUMINF_ADD

⊢ ∀f g.
    summable f ∧ summable g ⇒
    summable (λn. f n + g n) ∧ (suminf f + suminf g = suminf (λn. f n + g n))

SUMINF_POS

⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ 0 ≤ suminf f

SUMMABLE_LE

⊢ ∀f x. summable f ∧ (∀n. sum (0,n) f ≤ x) ⇒ suminf f ≤ x

SUMMABLE_SUM

⊢ ∀f. summable f ⇒ f sums suminf f

SUMS_EQ

⊢ ∀f x. f sums x ⇔ summable f ∧ (suminf f = x)

SUMS_ZERO

⊢ K 0 sums 0

SUM_CONST_R

⊢ ∀n r. sum (0,n) (K r) = &n * r

SUM_LT

⊢ ∀f g m n.
    (∀r. m ≤ r ∧ r < n + m ⇒ f r < g r) ∧ 0 < n ⇒ sum (m,n) f < sum (m,n) g

SUM_PICK

⊢ ∀n k x. sum (0,n) (λm. if m = k then x else 0) = if k < n then x else 0

SUM_SUMMABLE

⊢ ∀f l. f sums l ⇒ summable f

SUM_UNIQ

⊢ ∀f x. f sums x ⇒ (x = suminf f)

TRANSFORM_2D_NUM

⊢ ∀P. (∀m n. P m n ⇒ P n m) ∧ (∀m n. P m (m + n)) ⇒ ∀m n. P m n

TRIANGLE_2D_NUM

⊢ ∀P. (∀d n. P n (d + n)) ⇒ ∀m n. m ≤ n ⇒ P m n

X_HALF_HALF

⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x

mono_decreasing_suc

⊢ ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n

mono_increasing_converges_to_sup

⊢ ∀f r. mono_increasing f ∧ f ⟶ r ⇒ (r = sup (IMAGE f 𝕌(:num)))

mono_increasing_suc

⊢ ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)