Go backward to 4.4 The Real Numbers
Go up to 4 Numbers
Go forward to 4.6 Relationships between Number Domains
|
Go backward to 4.4 The Real Numbers Go up to 4 Numbers Go forward to 4.6 Relationships between Number Domains |
|
x*x = -1.
We introduce a domain in which all equations of this kind can be solved.
C:= R x R.We define a corresponding constructor
Let c in C and take x and y such that c=<x,y>. We call x the real part (Realteil) of c and y its imaginary part (Imaginärteil):
_+_i: R x R -> C x+yi := <x, y>.
real(c) := such x: exists y: c in C /\ c = <x, y>; imaginary(c) := such y: exists x: c in C /\ c = <x, y>.
So the question what a complex number x+yi is, can be easily answered: it is the tuple <x, y>.
Logic Evaluator
The corresponding executable definitions (on the basis of rationals instead of
reals) are given in Appendix complex.txt.
The usual operations on complex numbers are then defined as follows:
The imaginary constant (imaginäre Konstante):
0 := 0R+0Ri; 1 := 1R+0Ri; 2 := 2R+0Ri;
i := 0R+1Ri.
x + y := (x0 +R y0) + (x1 +R y1)i; x - y := (x0 -R y0) + (x1 -R y1)i; -x := (-Rx0)+(-Rx1)i; x * y := ((x0 *R y0) -R (x1 *R y1)) + ((x0 * R y1) + (x1 *R y0))i; x / y := (((x0 *R y0) +R (x1 *R y1)) /R d) + (((x1 *R y0) -R (x0 * R y1)) /R d)i where d = (y0 *R y0) +R (y1 *R y1); x-1 := 1 / x.
The complex conjugate (konjugiert komplexe Zahl):
x := x0 + (-R x1)i.
The absolute value (Absolutbetrag):
|x| := sqrt((x0 *R x0) +R (x1 *R x1)).
Please note that an application x+yi of the constructor function denotes the tuple <x, y> while the imaginary constant i denotes (0R+1Ri), i.e., <0R, 1R>. This imaginary constant is the "missing value" that solves the equation stated at the begin of this section.
i * i = (definition of i) (0R + 1Ri) *R (0R + 1Ri) = (definition of *)
((0R *R 0R) -R (1R *R 1R)) + ((0R *R 1R)+R (1R *R 0R))i = (arithmetic in R) (-R 1R) + (-R 0R)i = (definition of -) -(1R + 0Ri) = (definition of 1) -1.
Logic Evaluator Function conj
computes the complex conjugate and ||^2 returns the square of the
absolute value:
The following proposition tells us that our quest for a closed number domain has reached its goal.
a0*x0 + ...+ an-1*xn-1 = 0.
We now introduce the complex root function analogously to the corresponding operation on the reals.
sqrtn(x) := such y: xn = y
As a consequence of Proposition Fundamental Theorem, we then have
forall a in C, n in N>0: (sqrtn(a))n = a.
For the special case of the square root function, we give a definition that immediately allows us to "compute" the square of a complex number.
sqrt(.): C -> C sqrt(x) := if x1 >= R 0R then u+vi else u+(-Rv)i where u = sqrt((x0 +R sqrt(x02 +R x12)) /R 2R) v = sqrt((-Rx0 +R sqrt(x02 +R x12)) /R 2R).
The equation x*x=a has in general two solutions, the one denoted by the definition above and the one we get by multiplying the value with (-1). In other words, the following holds:
forall x in C : let r = sqrt(x): x=r*r /\ x=(-r)*(-r).
Absolute Value Out definition of the absolute value implies, for every x in R, |x+0i| = sqrt(x*Rx), i.e.,
|x+0i| = if x <= R 0R then -Rx else xwhich corresponds to the usual definition of | | on R. The absolute value satisfies the following equations and inequalities.
|x| >= R 0R, |-x| = |x|, |x| = 0R <=> x = 0, |x+y| <= R |x| +R |y|, |x-y| <= R |x| +R |y|, ||x| -R |y|| <= R |x + y|, ||x| -R |y|| <= R |x - y|, |x*y| = |x| *R |y|, y != 0 => |x/y| = |x| /R |y|.
Likewise we have the following laws for the complex conjugate.
x = x, x+y = x + y, x*y = x * y, y != 0 => x/y = x / y, x1 = 0R <=> x = x, x = ((x+x)/2) + ((x-x)/2)i, |x| = sqrt(z*z)
The set C "embeds" R in the sense that will be discussed in Section Embedding Sets.