OpenMath Content Dictionary: cauchypv

Canonical URL:

http://www.openmath.org/cd/cauchypv.ocd

CD File:

cauchypv.ocd

CD as XML Encoded OpenMath:

cauchypv.omcd

Defines:

defint

Date:

2001-09-23

Version:

1

Review Date:

2002-09-01

Status:

experimental

Uses CD:

alg1, arith1, expint, fns1, interval1, list1, nums1, transc1, relation1, quant1, logic1

This CD extends calculus1 (compatible with the calculus operations in Content MathML) with a Cauchy principal value definite integral.

defint

Description:

This symbol is used to represent definite (Cauchy principal value) integration of unary functions. It takes two arguments; the first being the range (e.g. a set) of integration, and the second the function.

Commented Mathematical property (CMP):

for all a,b | integral from a to b = -integral from b to a

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="a"/>
      <OMV name="b"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="cauchypv" name="defint"/>
	<OMA>
	  <OMS cd="interval1" name="interval"/>
	  <OMV name="a"/>
	  <OMV name="b"/>
	</OMA>
	<OMBIND>
	  <OMS cd="fns1" name="lambda"/>
	  <OMBVAR>
	    <OMV name="x"/>
	  </OMBVAR>
	  <OMA>
	    <OMV name="f"/>
	    <OMV name="x"/>
	  </OMA>
	</OMBIND>
      </OMA>
      <OMA>
        <OMS cd="arith1" name="unary_minus"/>
        <OMA>
          <OMS cd="cauchypv" name="defint"/>
	  <OMA>
	    <OMS cd="interval1" name="interval"/>
	    <OMV name="b"/>
	    <OMV name="a"/>
	  </OMA>
	  <OMBIND>
	    <OMS cd="fns1" name="lambda"/>
	    <OMBVAR>
	      <OMV name="x"/>
	    </OMBVAR>
	    <OMA>
	      <OMV name="f"/>
	      <OMV name="x"/>
	    </OMA>
	  </OMBIND>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ a b ] . (eq (defint (interval ( a, b) , lambda [ x ] . ( f ( x) ) ) , unary_minus (defint (interval ( b, a) , lambda [ x ] . ( f ( x) ) ) ) ) )

$$\forall \hspace{0.17em}a,b.\mathrm{defint}((a,b),\lambda \hspace{0.17em}x.f\left(x\right))=-\mathrm{defint}((b,a),\lambda \hspace{0.17em}x.f\left(x\right))$$

Example:

An example: the definition of the exponential integral. $$Ei(x)=\int_{-\infty}^x\frac{e^t}t dt\qquad(x>0)$$

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
      <OMA>
        <OMS name="implies" cd="logic1"/>
        <OMA>
          <OMS name="gt" cd="relation1"/>
          <OMV name="x"/>
          <OMS name="zero" cd="alg1"/>
        </OMA>
        <OMA>
          <OMS name="eq" cd="relation1"/>
          <OMA>
            <OMS name="Ei" cd="expint"/>
            <OMV name="x"/>
          </OMA>
          <OMA>
            <OMS name="defint" cd="cauchypv"/>
            <OMA>
              <OMS name="interval" cd="interval1"/>
              <OMA>
                <OMS name="unary_minus" cd="arith1"/>
                <OMS name="infinity" cd="nums1"/>
              </OMA>
              <OMV name="x"/>
            </OMA>
            <OMBIND>
              <OMBVAR>
                <OMV name="t"/>
              </OMBVAR>
              <OMA>
                <OMS name="divide" cd="arith1"/>
                <OMA>
                  <OMS name="exp" cd="transc1"/>
                  <OMV name="t"/>
                </OMA>
                <OMV name="t"/>
              </OMA>
            </OMBIND>
          </OMA>
        </OMA>
      </OMA>
    </OMOBJ>

implies (gt ( x, zero) , eq (Ei ( x) , defint (interval (unary_minus (infinity) , x) , t [divide (exp ( t) , t) ] . () ) ) )

$$x>0\Rightarrow \mathrm{Ei}\left(x\right)=\mathrm{defint}((-\infty ,x),t\hspace{0.17em}.)$$

Signatures:

sts