Chapter 3. Growth of Functions

CLRS introduces asymptotic notation — O, Ω, Θ, o, ω — as the language for describing how running times grow with input size. This chapter bridges the textbook definitions to mathlib's filter-based asymptotics library.

3.1 Asymptotic Notation

Defines O, Ω, Θ, o, ω as CLRS-style wrappers around mathlib's =O[atTop] / =o[atTop]. Proves equivalence between the CLRS discrete definition (∃ c n₀) and the filter-based one. Collects algebraic properties: reflexivity, transitivity, sum and product rules.

3.2 Standard Functions

Proves concrete growth comparisons that matter for algorithm analysis:

• polynomial n^a vs exponential c^n for every c > 1

• logarithm powers (log n)^a vs polynomial n^ε

• exponential base comparisons a^n = o(b^n) for 0 ≤ a < b

• harmonic numbers H_n ~ log n and H_n = Θ(log n)

• factorial upper/lower bounds, exponential-vs-factorial comparison, and n! = o(n^n)

• floor / ceiling Θ-behavior, including half-scale floor and ceiling

Notation: we use |·| (absolute value) rather than ‖·‖ for readability.