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

Asymptotic Notation. Part II: Examples and Problems


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 [4] 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. This article is a follow-up to [13] in which we introduced the basic notions and general theory. This article presents a Mizar formalization of examples and solutions to problems from Chapter 3 of [4] (some of the examples and solved problems are also in [13]). Not all problems have been solved as some required solutions not amenable for formalization.

This work has been supported by NSERC Grant OGP9207.

MML Identifier: ASYMPT_1

The terminology and notation used in this paper have been introduced in the following articles [19] [25] [2] [21] [8] [5] [6] [20] [23] [1] [11] [9] [26] [14] [16] [17] [12] [15] [22] [10] [18] [3] [7] [24] [13]

Contents (PDF format)

  1. Examples from the Text
  2. Problem 3.1
  3. Problem 3.5
  4. Problem 3.6
  5. Problem 3.7
  6. Problem 3.8
  7. Problem 3.11
  8. Problem 3.19
  9. Problem 3.21
  10. Problem 3.22
  11. Problem 3.23
  12. Problem 3.24
  13. Problem 3.26
  14. Problem 3.28
  15. Problem 3.30
  16. Problem 3.31
  17. Problem 3.34
  18. Problem 3.35
  19. Addition
  20. Potentatially Useful

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] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[4] Gilles Brassard and Paul Bratley. \em Fundamentals of Algorithmics. Prentice Hall, 1996.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[8] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[9] Jaroslaw Kotowicz. Convergent sequences and the limit of sequences. Journal of Formalized Mathematics, 1, 1989.
[10] Jaroslaw Kotowicz. Monotone real sequences. Subsequences. Journal of Formalized Mathematics, 1, 1989.
[11] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.
[12] Elzbieta Kraszewska and Jan Popiolek. Series in Banach and Hilbert spaces. Journal of Formalized Mathematics, 4, 1992.
[13] Richard Krueger, Piotr Rudnicki, and Paul Shelley. Asymptotic notation. Part I: Theory. Journal of Formalized Mathematics, 11, 1999.
[14] Rafal Kwiatek. Factorial and Newton coefficients. Journal of Formalized Mathematics, 2, 1990.
[15] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.
[16] Konrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Journal of Formalized Mathematics, 2, 1990.
[17] Konrad Raczkowski and Andrzej Nedzusiak. Series. Journal of Formalized Mathematics, 3, 1991.
[18] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[19] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[20] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.
[21] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[22] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.
[23] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[24] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.
[25] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[26] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received November 4, 1999

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