Go backward to 6.3 Embedding Sets Go up to 6 More on Functions Go forward to 6.5 Special Functions |
[T]iis a term with bound variable i whose value is the sequence
[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.
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 monotonically decreasing (monoton wachsend) if every element of f is greater than or equal the next element:
f is strictly monotonically increasing : <=> f: N -> R /\ forall i in N: fi < fi+1.
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:
[i]i = [0, 1, 2, 3, ...]
[1/i+1]i = [1, 1/2, 1/3, 1/4, ...]
[i div 2]i = [0, 0, 1, 1, 2, 2, ...]
[(-1)i]i = [1, -1, 1, -1, ...]
The elements of an infinite sequence either become arbitrarily large or their size is bounded.
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:
The infimum (Infimum) of f is the greatest lower bound of f:
sup(f) := such S: S is upper bound of f /\ (forall S': S' is upper bound of f => S <= S').
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.
(i.e., sup(f) = such S: S is supremum of f) and show
S is supremum of f : <=> S is upper bound of f /\ (forall S': S' is upper bound of f => S <= S')
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.
forall f, S0, S1: S0 is supremum of f /\ S1 is supremum of f => S0 = S1.
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 divergent (divergent):
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.
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 [:
forall i >= n: |(-1)i*1/i+1 - 0| < epsilonwhich 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 .
Let epsilon := 1/2. There exists some n in N such that
forall i >= n: |(-1)i - a| < 1/2.We thus have
(substituting for i the values n and n+1 one of which is even and one of which is odd).
|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.
forall s, a0, a1: (s converges to a0 /\ s converges to a1) => a0 = a1.
Let epsilon := |a1-a0/2|. We know epsilon > 0, therefore there exist n0 in N and n1 in N such that
Let n := max(n0, n1). We then know
(forall i >= n0: |si - a0| < epsilon ) /\ (forall i >= n1: |si - a1| < epsilon ).
Consequently, we have (see the absolute value laws)
|sn - a0| < epsilon /\ |sn - a1| < epsilon .
which represents a contradiction.
|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.
limi -> oo TThe value of this term is that of the term
lim([T]i).
We then have the following laws for the manipulation of limit terms.
If limi -> oo B != 0, we also 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).
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.
Let a := limi -> oo A and b := limi -> oo B. We have to show
limi -> oo (A + B) = (limi -> oo A) + (limi -> oo B).
Take arbitrary epsilon > 0. We know that there exist n0 in N and n1 in N such that
forall epsilon > 0: exists n in N: forall i > n: |A+B-(a+b)| < epsilon .
Let n := max(n0, n1). We have to show
forall i >= n0: |A - a| < epsilon /2, forall i >= n1: |B - b| < epsilon /2.
Take arbitrary i >= n. We know
forall i >= n: |A+B-(a+b)| < epsilon .
|A+B-(a+b)| = |(A-a)+(B-b)| <= |A-a| + |B-b| < epsilon /2 + epsilon /2 = epsilon .
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.
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.
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.
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.
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, ...].
series([qi]i)n = (sum0 <= i <= n qi) = qn-1/q-1.
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.
(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.
forall q in R: |q| < 1 => (sumi=0 oo qi) = 1/1-q.
(*) The fact limn -> oo qn = 0 has to be shown in a separate proof.
(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.