Polynomial bounds on natural-number functions

PolyBound f says f is dominated pointwise (at every argument, not merely eventually) by the evaluation of a natural polynomial. Resource bookkeeping assembles time and space bounds by addition, multiplication, and monotonicity, so an everywhere-bound closed under those operations is easier to carry through a construction than a big-O statement; PolyBound.bigO converts to the big-O form the complexity classes are stated in.

Main results

• PolyBound — pointwise domination by a natural polynomial
• PolyBound.const, .id, .add, .mul, .pow, .mono, .max, .eval — the closure API
• PolyBound.bigO — a polynomial bound is a big-O power bound
• PolyBound.exists_mul_pow_bound — a polynomial bound is an A * (n + 1) ^ B bound

def Complexity.PolyBound (f : ℕ → ℕ) : Prop

Pointwise domination by the evaluation of a natural polynomial.

Equations

• Complexity.PolyBound f = ∃ (p : Polynomial ℕ), ∀ (inputLength : ℕ), f inputLength ≤ Polynomial.eval inputLength p

theorem Complexity.PolyBound.const (value : ℕ) : PolyBound fun (x : ℕ) => value

theorem Complexity.PolyBound.id : PolyBound fun (inputLength : ℕ) => inputLength

theorem Complexity.PolyBound.add {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) : PolyBound fun (inputLength : ℕ) => f inputLength + g inputLength

theorem Complexity.PolyBound.mul {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) : PolyBound fun (inputLength : ℕ) => f inputLength * g inputLength

theorem Complexity.PolyBound.mono {f g : ℕ → ℕ} (hg : PolyBound g) (hle : ∀ (inputLength : ℕ), f inputLength ≤ g inputLength) : PolyBound f

theorem Complexity.PolyBound.max {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) : PolyBound fun (inputLength : ℕ) => Max.max (f inputLength) (g inputLength)

theorem Complexity.PolyBound.eval (p : Polynomial ℕ) : PolyBound fun (inputLength : ℕ) => Polynomial.eval inputLength p

theorem Complexity.PolyBound.pow {f : ℕ → ℕ} (hf : PolyBound f) (exponent : ℕ) : PolyBound fun (inputLength : ℕ) => f inputLength ^ exponent

theorem Complexity.PolyBound.bigO {f : ℕ → ℕ} (hf : PolyBound f) : ∃ (d : ℕ), BigO f fun (x : ℕ) => x ^ d

A polynomial bound is a big-O bound by the polynomial's degree.

theorem Complexity.PolyBound.exists_mul_pow_bound {f : ℕ → ℕ} (hf : PolyBound f) : ∃ (A : ℕ) (B : ℕ), ∀ (n : ℕ), f n ≤ A * (n + 1) ^ B

A polynomial bound is a bound of the form A * (n + 1) ^ B: take A to be the sum of the coefficients and B the degree.