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

The terminology and notation used in this paper have been introduced in the following articles [14] [18] [2] [16] [7] [4] [5] [15] [1] [9] [8] [12] [13] [6] [17] [10]

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.

Received November 4, 1999