Go backward to 6.3 Embedding SetsGo up to 6 More on FunctionsGo forward to 6.5 Special Functions |

[is a term with bound variableT]_{i}

[ T]_{i}:N->R[ T]_{i}(i) :=T.

The sequence elements may be ordered in a way that is compatible with the order of the element domain.

fis monotonically increasing : <=>f:N->R/\foralliinN:f_{i}<=f_{i+1}.

fis strictly monotonically increasing : <=>f:N->R/\foralliinN:f_{i}<f_{i+1}.

fis monotonically decreasing : <=>f:N->R/\foralliinN:f_{i}>=f_{i+1}.

fis strictly monotonically decreasing : <=>f:N->R/\foralliinN:f_{i}>f_{i+1}.

The following figure illustrates a monotonically (not strictly monotonically) decreasing sequence:

- [
`i`]_{i}is strictly monotonically increasing:[

`i`]_{i}= [0, 1, 2, 3, ...] - [1/
`i`+1]_{i}is strictly monotonically decreasing:[1/

`i`+1]_{i}= [1, 1/2, 1/3, 1/4, ...] - [
`i`div 2]_{i}is monotonically increasing:[

`i`div 2]_{i}= [0, 0, 1, 1, 2, 2, ...] - [(-1)
^{i}]_{i}is neither monotonically increasing nor decreasing:[(-1)

^{i}]_{i}= [1, -1, 1, -1, ...]

The elements of an infinite sequence either become arbitrarily large or their size is bounded.

Uis upper bound off: <=>f:N->R/\foralliinN:f_{i}<=U.

TheLis lower bound off: <=>f:N->R/\foralliinN:f_{i}<=L.

The

sup( f) :=suchS:Sis upper bound off/\( forallS':S' is upper bound off=>S<=S').

inf( f) :=suchI:Iis lower bound off/\( forallI':I' is lower bound off=>I>=I').

The notions are visualized below:

While there are infinitely many upper and lower bounds (if any), supremum and infimum are uniquely defined.

(i.e., sup(

Sis supremum off: <=>Sis upper bound off/\( forallS':S' is upper bound off=>S<=S')

Take arbitrary

forallf,S_{0},S_{1}:S_{0}is supremum off/\S_{1}is supremum off=>S_{0}=S_{1}.

- [
`i`]_{i}has infimum 0 but no upper bound. - [1-
`i`]_{i}has supremum 1 but no lower bound. - [1/
`i`+1]_{i}has supremum 1 and infimum 0. - [
`i`^{3}]_{i}has no upper bound and no lower bound.

As above example shows, the infimum and supremum of a sequence need not be among the values of the sequence; in this case the sequence values arbitrarily close approach the bound without ever actually reaching it:

**Logic Evaluator**
We simulate some of the notions introduced above by considering
a finite initial segment of the sequence.

Please note that the predicate `isMonoIncreasing`

(`s`, `n`)
only checks whether the sequence `s` is monotonically increasing in the
first `n` elements and correspondingly for the other predicates. In
general we can describe in the Logic Evaluator infinite notions only by finite
approximations in the style demonstrated above.

Correspondingly, the following definitions determine a pseudo-supremum and
pseudo-infimum among the first `n` values of the given sequence ; please
note that for infinite sequences supremum respectively infimum need *not*
be among the values of the sequence; please compare with the actual
definitions of "sup" and "inf".

A non-convergent series is called

sconverges toa: <=>forallepsilon > 0:existsninN:foralli>=n: |s_{i}-a| < epsilon ;lim( s) :=sucha:sconverges toa.

sis divergent : <=> ~existsa:sconverges toa.

A geometric interpretation of convergence is given by the following picture
that shows that, for every epsilon > 0, all members of a convergent
sequence are eventually in an " epsilon -tunnel" around limit `a`,
i.e., in the interval ]`a`- epsilon , `a`+ epsilon [:

which can be simplified toforalli>=n: |(-1)^{i}*1/i+1 - 0| < epsilon

Takeforalli>=n: 1/i< epsilon .

Take arbitrary `i` >= `n`. We then have

1/i<= 1/n< 1/1/ epsilon = epsilon .

Let epsilon := 1/2. There exists some `n` in **N** such
that

We thus haveforalli>=n: |(-1)^{i}-a| < 1/2.

(substituting for

|1 - a| < 1/2 /\ |-1 -a| < 1/2

We then have (see the absolute value laws)

which represents a contradiction.

1 = 1/2+1/2 > |1 - a| + |-1 -a|= |1 - a| + |1 +a| >= |(1 -a) + (1 +a)| = 2

The limit of a convergent sequence is uniquely defined.

foralls,a_{0},a_{1}: (sconverges toa_{0}/\sconverges toa_{1}) =>a_{0}=a_{1}.

Let epsilon := |`a`_{1}-`a`_{0}/2|.
We know epsilon >
0, therefore there exist `n`_{0} in **N** and `n`_{1} in **N** such that

Let

( foralli>=n_{0}: |s_{i}-a_{0}| < epsilon ) /\ (foralli>=n_{1}: |s_{i}-a_{1}| < epsilon ).

Consequently, we have (see the absolute value laws)

| s_{n}-a_{0}| < epsilon /\ |s_{n}-a_{1}| < epsilon .

which represents a contradiction.

| a_{1}-a_{0}| = 2 epsilon = epsilon + epsilon > |s_{n}-a_{0}| + |s_{n}-a_{0}|>= |( s_{n}-a_{0}) - (s_{n}-a_{1})| = |a_{1}-a_{0}|

We often write limits in form of a quantor.

limThe value of this term is that of the term_{i -> oo }T

lim([ T]_{i}).

We then have the following laws for the manipulation of limit terms.

If lim

lim _{i -> oo }(A+B)= (lim _{i -> oo }A) + (lim_{i -> oo }B),lim _{i -> oo }(A-B)= (lim _{i -> oo }A) - (lim_{i -> oo }B),lim _{i -> oo }(A*B)= (lim _{i -> oo }A) * (lim_{i -> oo }B).

limFurthermore, we have for every_{i -> oo }(A/B) = lim_{i -> oo }A/lim_{i -> oo }B.

lim _{i -> oo }(c*A) =c* lim_{i -> oo }A.

Let

lim _{i -> oo }(A+B) = (lim_{i -> oo }A) + (lim_{i -> oo }B).

Take arbitrary epsilon > 0. We know that there exist

forallepsilon > 0:existsninN:foralli>n: |A+B-(a+b)| < epsilon .

Let

foralli>=n_{0}: |A-a| < epsilon /2,foralli>=n_{1}: |B-b| < epsilon /2.

Take arbitrary

foralli>=n: |A+B-(a+b)| < epsilon .

| A+B-(a+b)|= |( A-a)+(B-b)|<= | A-a| + |B-b|< epsilon /2 + epsilon /2 = epsilon .

lim_{i -> oo }(i+2/i-3) = lim_{i -> oo }(1+2/i/1-3/i) = lim_{i -> oo }(1+2/i)/lim_{i -> oo }(1-3/i)

=lim_{i -> oo }(1)+lim_{i -> oo }(2/i)/lim_{i -> oo }(1)-lim_{i -> oo }(3/i) = 1+0/1-0 = 1.

An important mathematical constant is defined as a limit.

e := lim_{i -> oo }(1+1/i)^{i}.

One can show that the sequence
[(1+1/`i`)^{i}]_{i} is convergent; thus
`e` is indeed well-defined with value is 2.71828....

We now construct a new sequence by summing up the elements of another sequence.

series: ( N->R) -> (N->R)series( a)_{n}:= (sum_{0 <= i <= n}a_{i}).

If `a` = [`T`]_{i}, then series(`a`) is
denoted by the term [(**sum**_{0 <= i <= n} `T`)]_{n}.

Then series(a= [0, 1, 4, 9, 16, 25, ...].

series(a) = [0, 1, 5, 14, 30, 55, ...].

**Logic Evaluator** A series can be simply defined as follows.

The following example illustrates some important classes of series.

**Arithmetic Series**- For every
`c`in**R**, the sequence [`i`*`c`]_{i}is called an*arithmetic sequence (arithmetische Folge)*. Correspondingly, series([`i`*`c`]_{i}) is called an*arithmetic series (arithmetische Reihe)*. We have, for every`n`in**N**,series([

(which can be proved by induction on`i`*`c`]_{i})_{n}= (**sum**_{0 <= i <= n}`i`*`c`) =`c`*`n`(`n`+1)/2.`n`).For instance, for

`c`=1, we have[ `i`]_{i}= [0, 1, 2, 3, 4, 5, ...], series([ `i`]_{i})= [0, 1, 3, 6, 10, 15, ...]. **Geometric Series**- For every
`q`in**R**, the sequence [`q`^{i}]_{i}is called a*geometric sequence (geometrische Folge)*. Correspondingly, series([`q`^{i}]_{i}) is called a*geometric series (geometrische Reihe)*. We have, for every`n`in**N**,series([

`q`^{i}]_{i})_{n}= (**sum**_{0 <= i <= n}`q`^{i}) =`q`^{n}-1/`q`-1.

For instance, for `q`=2, we have

[ 2^{i}]_{i}= [1, 2, 4, 8, 16, ...], series([ 2^{i}]_{i})= [1, 3, 7, 15, 31].

The limit of a series is usually denoted as follows.

(The value of this term issum_{i=0}^{ oo }T)

lim_{n -> oo }(sum_{0 <= i <= n}T).

Please note that the value (**sum**_{i=0}^{ oo } `T`)
is only well defined if [(**sum**_{0 <= i <= n} `T`)]_{n} is convergent.

We then have the following well-known result.

forallqinR: |q| < 1 => (sum_{i=0}^{ oo }q^{i}) = 1/1-q.

(*) The fact lim

( sum_{i=0}^{ oo }q^{i})= lim _{n -> oo }(sum_{0 <= i <= n}T)= lim _{n -> oo }q^{n}-1/q-1= lim _{n -> oo }(q^{n}-1)/lim_{n -> oo }(q-1)= (lim _{n -> oo }q^{n}) - (lim_{n -> oo }1)/q-1= (*) 0-1/ q-1= 1/1- q.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999