| author | wenzelm |
| Mon, 18 Jun 2007 23:30:46 +0200 | |
| changeset 23414 | 927203ad4b3a |
| parent 17749 | 4fb42f4d61df |
| permissions | -rw-r--r-- |
| 15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
||
| 15582 | 3 |
<!-- $Id$ --> |
4 |
||
5 |
<HTML> |
|
6 |
||
7 |
<HEAD> |
|
8 |
<meta http-equiv="content-type" content="text/html;charset=iso-8859-1"> |
|
9 |
<TITLE>HOL/Complex/README</TITLE> |
|
10 |
</HEAD> |
|
11 |
||
12 |
<BODY> |
|
| 14005 | 13 |
|
| 14631 | 14 |
<H1>Complex: The Complex Numbers</H1> |
15 |
<P>This directory defines the type <KBD>complex</KBD> of the complex numbers, |
|
| 14005 | 16 |
with numeric constants and some complex analysis. The development includes |
17 |
nonstandard analysis for the complex numbers. Note that the image |
|
| 14020 | 18 |
<KBD>HOL-Complex</KBD> includes theories from the directories |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
19 |
<KBD><a href="#Anchor-Real">HOL/Real</a></KBD> and <KBD><a href="#Anchor-Hyperreal">HOL/Hyperreal</a></KBD>. They define other types including <kbd>real</kbd> (the real numbers) and <kbd>hypreal</kbd> (the hyperreal or non-standard reals). |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
20 |
|
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
21 |
<ul> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
22 |
<li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
23 |
<li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
24 |
<li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
25 |
<li><a href="Complex.html">Complex</a> The complex numbers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
26 |
<li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
27 |
<li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
28 |
</ul> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
29 |
|
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
30 |
<h2><a name="Anchor-Real" id="Anchor-Real"></a>Real: Dedekind Cut Construction of the Real Line</h2> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
31 |
|
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
32 |
<ul> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
33 |
<li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs. |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
34 |
<li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
35 |
<li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
36 |
<li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property. |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
37 |
<li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
38 |
<li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
39 |
</ul> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
40 |
<h2><a name="Anchor-Hyperreal" id="Anchor-Hyperreal"></a>Hyperreal: Ultrafilter Construction of the Non-Standard Reals</h2> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
41 |
See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
42 |
<ul> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
43 |
<li><a href="Filter.html">Filter</a> Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma. |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
44 |
<li><a href="HLog.html">HLog</a> Non-standard logarithms |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
45 |
<li><a href="HSeries.html">HSeries</a> Non-standard theory of finite summation and infinite series |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
46 |
<li><a href="HTranscendental.html">HTranscendental</a> Non-standard extensions of transcendental functions |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
47 |
<li><a href="HyperDef.html">HyperDef</a> Ultrapower construction of the hyperreals |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
48 |
<li><a href="HyperNat.html">HyperNat</a> Ultrapower construction of the hypernaturals |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
49 |
<li><a href="HyperPow.html">HyperPow</a> Powers theory for the hyperreals |
| 17749 | 50 |
<!-- <li><a href="IntFloor.html">IntFloor</a> Floor and Ceiling functions relating the reals and integers --> |
|
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
51 |
<li><a href="Integration.html">Integration</a> Gage integrals |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
52 |
<li><a href="Lim.html">Lim</a> Theory of limits, continuous functions, and derivatives |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
53 |
<li><a href="Log.html">Log</a> Logarithms for the reals |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
54 |
<li><a href="MacLaurin.html">MacLaurin</a> MacLaurin series |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
55 |
<li><a href="NatStar.html">NatStar</a> Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
56 |
<li><a href="NthRoot.html">NthRoot</a> Existence of n-th roots of real numbers |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
57 |
<li><a href="NSA.html">NSA</a> Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties. |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
58 |
<li><a href="Poly.html">Poly</a> Univariate real polynomials |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
59 |
<li><a href="SEQ.html">SEQ</a> Convergence of sequences and series using standard and nonstandard analysis |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
60 |
<li><a href="Series.html">Series</a> Finite summation and infinite series for the reals |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
61 |
<li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
62 |
<li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
63 |
</ul> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
64 |
<HR> |
|
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14634
diff
changeset
|
65 |
<P>Last modified $Date$ |
| 15582 | 66 |
</BODY> |
| 14005 | 67 |
</HTML> |