OpenMath Content Dictionary: complex1

Canonical URL:
http://www.openmath.org/cd/complex1.ocd
CD File:
complex1.ocd
CD as XML Encoded OpenMath:
complex1.omcd
Defines:
argument, complex_cartesian, complex_polar, conjugate, imaginary, real
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
quant1, relation1, arith1, nums1, transc1, logic1, set1, setname1, alg1

This CD is intended to be `compatible' with the MathML view of operations on and constructors for complex numbers.


complex_cartesian

This symbol represents a constructor function for complex numbers specified as the Cartesian coordinates of the relevant point on the complex plane. It takes two arguments, the first is a number x to denote the real part and the second a number y to denote the imaginary part of the complex number x + i y. (Where i is the square root of -1.)

Commented Mathematical property (CMP):
for all x,y | complex_cartesian(x,y) = x + iy
Formal Mathematical property (FMP):
<OMOBJ>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
        <OMV name="y"/>
      </OMBVAR>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="complex1" name="complex_cartesian"/>
          <OMV name="x"/>
          <OMV name="y"/>
        </OMA>
        <OMA>
          <OMS cd="arith1" name="plus"/>
          <OMV name="x"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMS cd="nums1" name="i"/>
            <OMV name="y"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMOBJ>

forall [ x y ] . (eq (complex_cartesian ( x, y) , plus ( x, times (i, y) ) ) )

Signatures:
sts


[Next: real] [Last: conjugate] [Top]

real

This represents the real part of a complex number

Commented Mathematical property (CMP):
for all x,y | x = real(x+iy)
Formal Mathematical property (FMP):
<OMOBJ>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
        <OMV name="y"/>
      </OMBVAR>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMV name="x"/>
        <OMA>
          <OMS name="real" cd="complex1"/>
          <OMA>
            <OMS name="complex_cartesian" cd="complex1"/>
            <OMV name="x"/>
            <OMV name="y"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMOBJ>

forall [ x y ] . (eq ( x, real (complex_cartesian ( x, y) ) ) )

Signatures:
sts


[Next: imaginary] [Previous: complex_cartesian] [Top]

imaginary

This represents the imaginary part of a complex number

Commented Mathematical property (CMP):
for all x,y | y = imaginary(x+iy)
Formal Mathematical property (FMP):
<OMOBJ>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
        <OMV name="y"/>
      </OMBVAR>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMV name="y"/>
        <OMA>
          <OMS name="imaginary" cd="complex1"/>
          <OMA>
            <OMS name="complex_cartesian" cd="complex1"/>
            <OMV name="x"/>
            <OMV name="y"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMOBJ>

forall [ x y ] . (eq ( y, imaginary (complex_cartesian ( x, y) ) ) )

Signatures:
sts


[Next: complex_polar] [Previous: real] [Top]

complex_polar

This symbol represents a constructor function for complex numbers specified as the polar coordinates of the relevant point on the complex plane. It takes two arguments, the first is a nonnegative number r to denote the magnitude and the second a number theta (given in radians) to denote the argument of the complex number r e^(i theta). (i and e are defined as in this CD).

Commented Mathematical property (CMP):
for all r,a | complex_polar(r,a) = r*e^(a*i)
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="r"/>
      <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="complex1" name="complex_polar"/>
        <OMV name="r"/>
        <OMV name="a"/>
      </OMA>
      <OMA>
        <OMS cd="arith1" name="times"/>
	<OMV name="r"/>
	<OMA>
	  <OMS cd="transc1" name="exp"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="a"/>
	    <OMS cd="nums1" name="i"/>
	  </OMA>
	</OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ r a ] . (eq (complex_polar ( r, a) , times ( r, exp (times ( a, i) ) ) ) )

Commented Mathematical property (CMP):
for all x,y,r,a | (r sin a = y and r cos a = x) implies (complex_polar(r,a) = complex_cartesian(x,y)
Formal Mathematical property (FMP):
<OMOBJ>
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="x"/>
    <OMV name="y"/>
    <OMV name="r"/>
    <OMV name="a"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="arith1" name="times"/>
	  <OMV name="r"/>
	  <OMA>
	    <OMS cd="transc1" name="sin"/>
	    <OMV name="a"/>
	  </OMA>
        </OMA>
	<OMV name="y"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="arith1" name="times"/>
	  <OMV name="r"/>
	  <OMA>
	    <OMS cd="transc1" name="cos"/>
	    <OMV name="a"/>
	  </OMA>
        </OMA>
	<OMV name="x"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="complex1" name="complex_polar"/>
        <OMV name="r"/>
        <OMV name="a"/>
      </OMA>
      <OMA>
        <OMS cd="complex1" name="complex_cartesian"/>
        <OMV name="x"/>
        <OMV name="y"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ x y r a ] . (implies (and (eq (times ( r, sin ( a) ) , y) , eq (times ( r, cos ( a) ) , x) ) , eq (complex_polar ( r, a) , complex_cartesian ( x, y) ) ) )

Commented Mathematical property (CMP):
for all x | if a is a real number and k is an integer then complex_polar(x,a) = complex_polar(x,a+2*pi*k)
Formal Mathematical property (FMP):
<OMOBJ>
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="x"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="set1" name="in"/>
	<OMV name="a"/>
	<OMS cd="setname1" name="R"/>
      </OMA>
      <OMA>
        <OMS cd="set1" name="in"/>
	<OMV name="k"/>
	<OMS cd="setname1" name="Z"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="complex1" name="complex_polar"/>
	<OMV name="x"/>
	<OMV name="a"/>
      </OMA>
      <OMA>
        <OMS cd="complex1" name="complex_polar"/>
	<OMV name="x"/>
	<OMA>
	  <OMS cd="arith1" name="plus"/>
	  <OMV name="a"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMI> 2 </OMI>
	    <OMS cd="nums1" name="pi"/>
	    <OMV name="k"/>
	  </OMA>
	</OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ x ] . (implies (and (in ( a, R) , in ( k, Z) ) , eq (complex_polar ( x, a) , complex_polar ( x, plus ( a, times ( 2 , pi, k) ) ) ) ) )

Example:
i = complex_polar(1,pi/2)
<OMOBJ><OMA>
  <OMS cd="relation1" name="eq"/>
  <OMS cd="nums1" name="i"/>
  <OMA>
    <OMS cd="complex1" name="complex_polar"/>
    <OMS cd="alg1" name="one"/>
    <OMA>
      <OMS cd="arith1" name="divide"/>
      <OMS cd="nums1" name="pi"/>
      <OMI> 2 </OMI>
    </OMA>
  </OMA>
</OMA></OMOBJ>

eq (i, complex_polar (one, divide (pi, 2 ) ) )

Signatures:
sts


[Next: argument] [Previous: imaginary] [Top]

argument

This symbol represents the unary function which returns the argument of a complex number, viz. the angle which a straight line drawn from the number to zero makes with the Real line (measured anti-clockwise). The argument to the symbol is the complex number whos argument is being taken.

Commented Mathematical property (CMP):
for all r,a | argument(complex_polar(r,a)=a)
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="r"/>
      <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="complex1" name="argument"/>
        <OMA>
          <OMS cd="complex1" name="complex_polar"/>
          <OMV name="r"/>
          <OMV name="a"/>
        </OMA>
      </OMA>
      <OMV name="a"/>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ r a ] . (eq (argument (complex_polar ( r, a) ) , a) )

Commented Mathematical property (CMP):
the argument of x+i*y = tan(y/x)
Formal Mathematical property (FMP):
<OMOBJ>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="complex1" name="argument"/>
      <OMA>
        <OMS cd="complex1" name="complex_cartesian"/>
        <OMV name="x"/>
        <OMV name="y"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="transc1" name="tan"/>
      <OMA>
        <OMS cd="arith1" name="divide"/>
	<OMV name="y"/>
	<OMV name="x"/>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

eq (argument (complex_cartesian ( x, y) ) , tan (divide ( y, x) ) )

Signatures:
sts


[Next: conjugate] [Previous: complex_polar] [Top]

conjugate

A unary operator representing the complex conjugate of its argument.

Commented Mathematical property (CMP):
if a is a complex number then (conjugate(a) + a) is a real number
Formal Mathematical property (FMP):
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="a"/>
      <OMS cd="setname1" name="C"/>
    </OMA>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMA>
        <OMS cd="arith1" name="plus"/>
        <OMA>
          <OMS cd="complex1" name="conjugate"/>
          <OMV name="a"/>
        </OMA>
        <OMV name="a"/>
      </OMA>
      <OMS cd="setname1" name="R"/>
    </OMA>
  </OMA>
</OMOBJ>

implies (in ( a, C) , in (plus (conjugate ( a) , a) , R) )

Signatures:
sts


[First: complex_cartesian] [Previous: argument] [Top]