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
[ http://en.wikipedia.org/wiki/ ]
(for example).
We can approach the calculus in two ways:
- Formal Operations - See Math.44 Formal Calculus
- Topologically - Here
- Calculus::=Net{Differential_Calculus, Integral_Calculus, Ordinary_differential_equations, Partial_differential_equations,... }.
- 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.
[click here if you can fill this hole]
- (above)|-D (_^n) = n * (_^(n-1)).
- (-1)|-D(map[x](x^n)) = map[x](n*(x^(n-1))).
- (above)|-D sin = cos, D cos = -sin, D tan = sec^2, ... .
- (above)|-D ln = (1/_).
- (above)|-D (e^_) = (e^_).
- (above)|-D( f(g)) = D(f)(g) * D g.
- (above)|-D(u+v) = D u + D v.
- (above)|-D(u-v) = D u - D v.
- (above)|-D(c*u) = c*D(u), where c is a Real constant.
- (above)|-D(u*v) = u * (D v) + (D u) * v.
- (above)|-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.
[click here D (_)^(_) = ?. if you can fill this hole]
- 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
- (above)|-D(e^_)=e^_.
- However this is not the only solution because for constant a
- (above)|-D(a*e^_) = a*e^_.
There is a rich, complex and elegant theory of these equations.
These links
[ ordinaryDiffEq.html ]
[ ODE_resources.htm ]
seem to be useful starting points.
[click here if you can fill this hole]
}=::
Ordinary_differential_equations.
For h: Real E^h::(C->C)=(map[f](map[x](f(x+h))).
[click here if you can fill this hole]
- develop theory of expressions that treat E and D as an algebra: Operator_algebra(Real, {D,E}).
- (above)|- (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))).
[click here if you can fill this hole]
}=::
Classical_derivative.
- Frechet_deriative::=
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.
- ∂ y / ∂ x.
The MATHS symbol for the curly d of classical mathematics is the
same as in Τ_{Ε}Χ:
\partial y / \partial x
It means that y equals an expression and all the variables in it are
assumed to be constants except x.
[click here if you can fill this hole]
}=::
Differential_Calculus.
- Integral_Calculus::=
Net{
Here are two excellent resources:
[ Integral ]
to get you started. This page
[ 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):
- (above)|-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.
- ∫::=/D.
- integral_sign::=∫.
\int
- (above)|-∫(2*_) = (_)^2 + Const.
[click here if you can fill this hole]
}=::
Indefinite_integral.
- Definite_integral::=
Net{
A definite integral is given a integrable function
and a closed set to integrate over,
returns a number.
- ∫::Integrable_function->(Closed_set(Number)->Number).
- Integrable_function::@(Number->Number).
[click here if you can fill this hole]
- (above)|-∫(2*_)[a..b] = b^2 - a^2.
[click here if you can fill this hole]
}=::
Definite_integral.
}=::
Integral_Calculus.
- Partial_differential_equations::=
. . . . . . . . . ( end of section The Differential and Integral Calculi) <<Contents | End>>
Special characters are defined in
[ intro_characters.html ]
that also outlines the syntax of expressions and a document.
Proofs follow a natural deduction style that start with
assumptions ("Let") and continue to a consequence ("Close Let")
and then discard the assumptions and deduce a conclusion. Look
here
[ Block Structure in logic_25_Proofs ]
for more on the structure and rules.
The notation also allows you to create a new network of variables
and constraints. A "Net" has a number of variables (including none) and
a number of properties (including none) that connect variables.
You can give them a name and then reuse them. The schema, formal system,
or an elementary piece of documentation starts with "Net" and finishes "End of Net".
For more, see
[ notn_13_Docn_Syntax.html ]
for these ways of defining and reusing pieces of logic and algebra
in your documents. A quick example: a circle
might be described by
Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see
[ home.html ]
The notation used here is a formal language with syntax
and a semantics described using traditional formal logic
[ logic_0_Intro.html ]
plus sets, functions, relations, and other mathematical extensions.
For a more rigorous description of the standard notations
see
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
- above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements.
The previous and previous but one statments are shown as (-1) and (-2).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.