.Open The Differential and Integral Calculi
There is a lot of work to be done here. However classical mathematics
has a 200 year history of developments that are already well documented on the
world wide web
.See http://en.wikipedia.org/wiki/
(for example).
We can approach the calculus in two ways:
.List
Formal Operations - See Math.44 Formal Calculus
Topologically - Here
.Close.List
Calculus::=Net{$Differential_Calculus, $Integral_Calculus, $Ordinary_differential_equations, $Partial_differential_equations,... }.
. Differential Calculus
Differential_Calculus::=Net{
Classical_derivative::=Net{
C::=(continuous)Real->Real,
D::C<>->C, only some functions can be differentiated.
differentiable::@C=cor(D),
|-for f:C, D f= map[x:Real]lim[h+>0]((f(x+h)-f(x))/h).
Differentiable functions are functions where the limit above exists and is
unique. A more complicated version would allow the `D` operator to
produce partial functions when applied to functions where the limit
only exists for certain values of x.
.Hole
()|- D (_^n) = n * (_^(n-1)).
(-1)|- D(map[x](x^n)) = map[x](n*(x^(n-1))).
()|- D sin = cos, D cos = -sin, D tan = sec^2, ... .
()|- D ln = (1/_).
()|- D (e^_) = (e^_).
()|- D( f(g)) = D(f)(g) * D g.
()|- D(u+v) = D u + D v.
()|- D(u-v) = D u - D v.
()|- D(c*u) = c*D(u), where c is a Real constant.
()|- D(u*v) = u * (D v) + (D u) * v.
()|- D(u/v) = ( (D u) * v - u*(D v) )/(v^2).
Notice that we can apply the above rules to any elementary expression, top-down
to calculate the 'D' of the expression with respect to any one variable.
.Hole D (_)^(_) = ?.
For f,g:differentiable, d f/ d g ::=D(f)/D(g).
The classic Liebnitz notation: dy/dx stands (roughly) for
(D map[x]y)(x).
Ordinary_differential_equations::=Net{
Ordinary differential equations are a collection of
equations that include several variables and their classical derivatives.
They have proved a powerful tool for modeling life, death and the universe.
For example the equation
(ode1): D f = f.
has a solution because
()|- D(e^_)=e^_.
However this is not the only solution because for constant `a`
()|- D(a*e^_) = a*e^_.
There is a rich, complex and elegant theory of these equations.
These links
.See http://archives.math.utk.edu/topics/ordinaryDiffEq.html
.See http://www.math.tamu.edu/~Don.Allen/ODE_resources.htm
seem to be useful starting points.
.Hole
}=::Ordinary_differential_equations.
For h: Real E^h::(C->C)=(map[f](map[x](f(x+h))).
.Hole
`develop theory of expressions that treat E and D as an algebra: Operator_algebra(Real, {D,E}).`
()|-(Taylor): E^h = e^(h*D).
We can easily extend the definition of the derivative `D` to functions mapping
real numbers into n-tuples of reals by treating them as `n` differentiable functions:
For n:Nat, C(n)::=(continuous)Real->(Real^n),
For f:C(n), define a vector of `n` functions f[i]:Real->Real,
f(t) = (f1(t), f2(t),... f[n](t)),
D::C(n)<>->C(n)= map[f:C(n)]map[t:Real](map[i:1..n](D(f[i](t))).
.Hole
}=::Classical_derivative.
Frechet_deriative::=Net{
.Hole
}=::Frechet_derivative.
. Partial Differentials
In a formula like
d ( y^2 + x^2 )/d x
in classical mathematics some of the variables represent functions
of a dependent variable and other symbols are constants. Typically,
`x` is the independent variable and `y`, `z`, `w`, `u`, `v`, ... are
assumed to be functions of `x` -- normally.
However it is useful to be able to make all but one of the variables constants. The so-called
partial differentials. There are several theorems that express a normal differential as
the sum of terms where each term is made of a differential and a partial differential, for example.
On the applied side many physical laws can be expressed as partial differential equation.
This a partial differential.
\partial y / \partial x.
The MATHS symbol for the curly `d` of classical mathematics is the
same as in \TeX:
.As_is \partial y / \partial x
It means that `y` equals an expression and all the variables in it are
assumed to be constants except `x`.
.Hole
}=::Differential_Calculus.
. Integral Calculus
Integral_Calculus::=Net{
Here are two excellent resources:
.See http://en.wikipedia.org/wiki/Integral
to get you started. This page
.See http://en.wikipedia.org/wiki/Lists_of_integrals
has more integrals than I've seen in some books.
Integrals are, in
general, harder to calculate than differentials:-(
There is no efficient algorithm, like that for differentiation, for integrating a function.
Indefinite_integral::= Net{
An indefinite integral is `indefinite` because `D` is not (1)-(1):
()|- for all f:differentiable, c:Real, D(f+c) = D(f).
Const::= { f:C || for some c:Real ( f=map[x:Real](c)), the set of const functions.
\int::=/D.
integral_sign::=\int.
.As_is \int
()|- \int(2*_) = (_)^2 + Const.
.Hole
}=::Indefinite_integral.
Definite_integral::= Net{
A definite integral is given a integrable function
and a closed set to integrate over,
returns a number.
\int::Integrable_function->(Closed_set(Number)->Number).
Integrable_function::@(Number->Number).
.Hole
()|- \int(2*_)[a..b] = b^2 - a^2.
.Hole
}=::Definite_integral.
}=::Integral_Calculus.
Partial_differential_equations::=Net{
.Hole
}=::Partial_differential_equations.
.Close The Differential and Integral Calculi