Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

## Asymptotic Notation. Part I: Theory

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

### Summary.

The widely used textbook by Brassard and Bratley  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  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 . 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.

#### MML Identifier: ASYMPT_0

The terminology and notation used in this paper have been introduced in the following articles                

#### Contents (PDF format)

1. Preliminaries
2. A Notation for the order of"
3. Other Asymptotic Notation
4. Conditional Asymptotic Notation
5. Operations on Asymptotic Notation

#### Bibliography

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