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

## 6.4 Sequences and Series

In this section, we discuss infinite sequences over R; we often write them in the following form.

Definition 79 (Sequence Quantor) For every variable i and term T, the phrase
[T]i
is a term with bound variable i whose value is the sequence
 [T]i: N -> R [T]i(i) := T.

Example  [a2+c]a = [0+c, 1+c, 4+c, 9+c, ...].

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

Definition 80 (Monotonicity) Let f be an infinite sequence over R. f is  monotonically increasing (monoton wachsend) if every element of f is less than or equal the next element:
f is monotonically increasing : <=> f: N -> R /\  forall i in N: fi <= fi+1.
f is  strictly monotonically increasing (streng monoton wachsend) if every element of f is less than the next element:
 f is strictly monotonically increasing : <=> f: N -> R /\  forall i in N: fi < fi+1.
f is  monotonically decreasing (monoton wachsend) if every element of f is greater than or equal the next element:
f is monotonically decreasing : <=> f: N -> R /\  forall i in N: fi >= fi+1.
f is  strictly monotonically decreasing (streng monoton wachsend) if every element of f is greater than the next element:
 f is strictly monotonically decreasing : <=> f: N -> R /\  forall i in N: fi > fi+1.

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

Example
• [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.

Definition 81 (Upper and Lower Bounds) Let f be an infinite sequence over R. f has an upper bound (obere Schranke) U if every element of f is less than or equal U:
U is upper bound of f : <=> f: N -> R /\  forall i in N: fi <= U.
f has a lower bound (untere Schranke) L if every element of f is less than or equal L:
L is lower bound of f : <=> f: N -> R /\  forall i in N: fi <= L.
The  supremum (Supremum) of f is the smallest upper bound of f:
 sup(f) := such S: S is upper bound of f /\ (forall S': S' is upper bound of f => S <= S').
The  infimum (Infimum) of f is the greatest lower bound of f:
 inf(f) := such I: I is lower bound of f /\ (forall I': I' is lower bound of f => I >= I').

The notions are visualized below:

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

Proof  We define
 S is supremum of f : <=> S is upper bound of f /\ (forall S': S' is upper bound of f => S <= S')
(i.e., sup(f) = such S: S is supremum of f) and show
 forall f, S0, S1: S0 is supremum of f /\  S1 is supremum of f => S0 = S1.
Take arbitrary f and suprema S0 and S1 of f. Since S0 is a supremum and S1 is an upper bound of f, we have S0 <= S1. Conversely, since S1 is a supremum and S0 is an upper bound of f, we have S1 <= S0. Since S0 <= S1 and S1 <= S0, we have S0 = S1.

Example
• [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.
• [i3]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".

Definition 82 (Convergence and Limit) An infinite sequence s over R  converges (konvergiert) to  limit (Grenzwert, Limes) a, if its members approach a arbitrarily close:
 s converges to a : <=> forall epsilon > 0: exists n in N: forall i >= n: |si - a| < epsilon ; lim(s) := such a: s converges to a.
A non-convergent series is called  divergent (divergent):
 s is divergent : <=> ~exists a: s converges to a.

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 [:

Example  Let s := [(-1)i*1/i+1]i. We show that s converges to 0. Take arbitrary epsilon > 0. We have to find some n in N such that
forall i >= n: |(-1)i*1/i+1 - 0| < epsilon
which can be simplified to
forall i >= n: 1/i < epsilon .
Take n := such n in N: 1/ epsilon < n. Because N is unbounded (i.e., forall r in R: exists n in N: r < n), we know 1/ epsilon < n.

Take arbitrary i >= n. We then have

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

Example  Let s := [(-1)i]i. We show that s is divergent. Assume that s is convergent, i.e., s converges to some limit a in R. We show a contradiction.

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

forall i >= n: |(-1)i - a| < 1/2.
We thus have
 |1 - a| < 1/2 /\  |-1 - a| < 1/2
(substituting for i the values n and n+1 one of which is even and one of which is odd).

We then have (see the absolute value laws)

 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.

Proposition 87 (Unicity of Limits) If s converges to both a0 and a1, then a0 = a1:
 forall s, a0, a1: (s converges to a0 /\  s converges to a1) => a0 = a1.

Proof  Take arbitrary s, a0 and a1 such that s converges to both a0 and a1. Assume a0 != a1. We show a contradiction.

Let epsilon := |a1-a0/2|. We know epsilon > 0, therefore there exist n0 in N and n1 in N such that

 (forall i >= n0: |si - a0| < epsilon ) /\  (forall i >= n1: |si - a1| < epsilon ).
Let n := max(n0, n1). We then know
 |sn - a0| < epsilon /\  |sn - a1| < epsilon .
Consequently, we have (see the absolute value laws)
 |a1-a0| = 2 epsilon = epsilon + epsilon > |sn - a0| + |sn - a0| >= |(sn - a0) - (sn - a1)| = |a1 - a0|

We often write limits in form of a quantor.

Definition 83 (Limit Quantor) For every variable i and term T, the following phrase represents a term with bound variable i:
limi -> oo T
The value of this term is that of the term
 lim([T]i).

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

Proposition 89 (Limit Laws) For all convergent sequences [A]i and [B]i, we have
 limi -> oo (A + B) = (limi -> oo A) + (limi -> oo B), limi -> oo (A - B) = (limi -> oo A) - (limi -> oo B), limi -> oo (A * B) = (limi -> oo A) * (limi -> oo B).
If limi -> oo B != 0, we also have
limi -> oo (A/B) = limi -> oo A/limi -> oo B.
Furthermore, we have for every c in R
 limi -> oo (c * A) = c * limi -> oo A.

Proof  Take arbitrary convergent sequences [A]i and [B]i. We prove
 limi -> oo (A + B) = (limi -> oo A) + (limi -> oo B).
Let a := limi -> oo A and b := limi -> oo B. We have to show
 forall epsilon > 0: exists n in N: forall i > n: |A+B-(a+b)| < epsilon .
Take arbitrary epsilon > 0. We know that there exist n0 in N and n1 in N such that
 forall i >= n0: |A - a| < epsilon /2, forall i >= n1: |B - b| < epsilon /2.
Let n := max(n0, n1). We have to show
 forall i >= n: |A+B-(a+b)| < epsilon .
Take arbitrary i >= n. We know
 |A+B-(a+b)| = |(A-a)+(B-b)| <= |A-a| + |B-b| < epsilon /2 + epsilon /2 = epsilon .

Example
limi -> oo (i+2/i-3) = limi -> oo (1+2/i/1-3/i) = limi -> oo (1+2/i)/limi -> oo (1-3/i)
=limi -> oo (1)+limi -> oo (2/i)/limi -> oo (1)-limi -> oo (3/i) = 1+0/1-0 = 1.

An important mathematical constant is defined as a limit.

Definition 84 (Euler's Number)
e := limi -> 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.

Definition 85 (Series) Let a be an infinite sequence over R. The  series (Reihe) corresponding to a is the sequence where every element sn is the sum of the first n+1 elements of a:
 series: (N -> R) -> (N -> R) series(a)n := (sum0 <= i <= n ai).

If a = [T]i, then series(a) is denoted by the term [(sum0 <= i <= n T)]n.

Example  Let a = [i2]i:
a = [0, 1, 4, 9, 16, 25, ...].
Then series(a) = [(sum0 <= i <= n i2)]n:
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.

Example
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([i*c]i)n = (sum0 <= i <= n i*c) = c*n(n+1)/2.
(which can be proved by induction on 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 [qi]i is called a  geometric sequence (geometrische Folge). Correspondingly, series([qi]i) is called a  geometric series (geometrische Reihe). We have, for every n in N,
series([qi]i)n = (sum0 <= i <= n qi) = qn-1/q-1.
(which can be proved by induction on n).

For instance, for q=2, we have

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

The limit of a series is usually denoted as follows.

Definition 86 (Series Limit Quantor) For every variable i and term T, the following phrase denotes a term with bound variable i:
(sumi=0 oo T)
The value of this term is
limn -> oo (sum0 <= i <= n T).

Please note that the value (sumi=0 oo T) is only well defined if [(sum0 <= i <= n T)]n is convergent.

We then have the following well-known result.

Proposition 91 (Limit of Geometric Series) For every q in R with |q| < 1, the series [(sum0 <= i <= n qi)]n converges to 1/1-q:
 forall q in R: |q| < 1 => (sumi=0 oo qi) = 1/1-q.

Proof  Take arbitrary q in R with |q| < 1. We then have
 (sumi=0 oo qi) = limn -> oo (sum0 <= i <= n T) = limn -> oo qn-1/q-1 = limn -> oo (qn-1)/limn -> oo (q-1) = (limn -> oo qn) - (limn -> oo 1)/q-1 = (*) 0-1/q-1 = 1/1-q.
(*) The fact limn -> oo qn = 0 has to be shown in a separate proof.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999