Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

**Richard Krueger**- University of Alberta, Edmonton
**Piotr Rudnicki**- University of Alberta, Edmonton
**Paul Shelley**- University of Alberta, Edmonton

- The widely used textbook by Brassard and Bratley [3] includes a chapter devoted to asymptotic notation (Chapter 3, pp. 79-97). We have attempted to test how suitable the current version of Mizar is for recording this type of material in its entirety. A more detailed report on this experiment will be available separately. This article presents the development of notions and a follow-up article [11] includes examples and solutions to problems. The preliminaries introduce a number of properties of real sequences, some operations on real sequences, and a characterization of convergence. The remaining sections in this article correspond to sections of Chapter 3 of [3]. Section 2 defines the $O$ notation and proves the threshold, maximum, and limit rules. Section 3 introduces the $\Omega$ and $\Theta$ notations and their analogous rules. Conditional asymptotic notation is defined in Section 4 where smooth functions are also discussed. Section 5 defines some operations on asymptotic notation (we have decided not to introduce the asymptotic notation for functions of several variables as it is a straightforward generalization of notions for unary functions).

This work has been supported by NSERC Grant OGP9207.

- Preliminaries
- A Notation for ``the order of"
- Other Asymptotic Notation
- Conditional Asymptotic Notation
- Operations on Asymptotic Notation

- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
The ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [3] Gilles Brassard and Paul Bratley. \em Fundamentals of Algorithmics. Prentice Hall, 1996.
- [4]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Jaroslaw Kotowicz.
Convergent sequences and the limit of sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [9]
Jaroslaw Kotowicz.
Real sequences and basic operations on them.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Jaroslaw Kotowicz.
The limit of a real function at infinity.
*Journal of Formalized Mathematics*, 2, 1990. - [11]
Richard Krueger, Piotr Rudnicki, and Paul Shelley.
Asymptotic notation. Part II: Examples and problems.
*Journal of Formalized Mathematics*, 11, 1999. - [12]
Rafal Kwiatek.
Factorial and Newton coefficients.
*Journal of Formalized Mathematics*, 2, 1990. - [13]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
*Journal of Formalized Mathematics*, 2, 1990. - [14]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [15]
Andrzej Trybulec.
Function domains and Fr\aenkel operator.
*Journal of Formalized Mathematics*, 2, 1990. - [16]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [17]
Andrzej Trybulec and Czeslaw Bylinski.
Some properties of real numbers operations: min, max, square, and square root.
*Journal of Formalized Mathematics*, 1, 1989. - [18]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]