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 [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.

MML Identifier: ASYMPT_0

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

[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.