Polynomial bounds on natural-valued functions

PolynomiallyBounded f means that f n ≤ n ^ d eventually, for some fixed degree d. This is equivalent to a real-valued IsBigO bound and to a bound c * (n + 1) ^ d at every input. It is a growth condition and does not assert computability.

def Cslib.PolynomiallyBounded (f : ℕ → ℕ) : Prop

A function is polynomially bounded if a fixed power eventually bounds its values.

theorem Cslib.polynomiallyBounded_iff_isBigO {f : ℕ → ℕ} : PolynomiallyBounded f ↔ ∃ (d : ℕ), (fun (n : ℕ) => ↑(f n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ d

Polynomial growth is equivalent to a big-O bound after casting to the reals.

theorem Cslib.polynomiallyBounded_iff_le {f : ℕ → ℕ} : PolynomiallyBounded f ↔ ∃ (c : ℕ) (d : ℕ), ∀ (n : ℕ), f n ≤ c * (n + 1) ^ d

A polynomial bound can absorb every finite prefix into its constant factor.