Closure properties of polynomial bounds

PolynomiallyBounded is closed under the operations that arise when accounting for sizes and running times: addition, multiplication, fixed powers, composition, truncated subtraction, max/min, division and remainder, logarithms and conditionals. Every closure lemma is registered with fun_prop, so a goal such as

example (hf : PolynomiallyBounded f) : PolynomiallyBounded (fun n => 2 * f n ^ 3 + n - 5) := by
  fun_prop

is discharged automatically from the local hypothesis hf. This is the arithmetic engine behind the complexity calculus: time and size polynomials of composite constructions are stated as expressions in the component bounds and collapsed by fun_prop.

Main results

• Nat.mul_add_one_pow_le_two_pow: an explicit bound c * (n + 1) ^ d is at most c * 2 ^ d * n ^ d + c.
• Cslib.PolynomiallyBounded.mono: a function eventually below a polynomially bounded one is polynomially bounded.
• Cslib.PolynomiallyBounded.add, mul, pow, comp: the closure rules proper.
• Cslib.PolynomiallyBounded.polynomial_eval: evaluation of a polynomial.
• Cslib.PolynomiallyBounded.tsub, max, min, div, mod, log, ite: operations that never exceed one of their arguments.

theorem Nat.mul_add_one_pow_le_two_pow (c d n : ℕ) : c * (n + 1) ^ d ≤ c * 2 ^ d * n ^ d + c

An explicit polynomial bound c * (n + 1) ^ d is a bound O(n ^ d).

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

Produce a polynomial bound from a bound c * (n + 1) ^ d valid at every input.

theorem Cslib.PolynomiallyBounded.mono {f g : ℕ → ℕ} (hg : PolynomiallyBounded g) (h : f ≤ᶠ[Filter.atTop] g) : PolynomiallyBounded f

A function eventually dominated by a polynomially bounded function is polynomially bounded.

theorem Cslib.PolynomiallyBounded.mono_of_le {f g : ℕ → ℕ} (hg : PolynomiallyBounded g) (h : f ≤ g) : PolynomiallyBounded f

A function dominated pointwise by a polynomially bounded function is polynomially bounded.

theorem Cslib.PolynomiallyBounded.const (c : ℕ) : PolynomiallyBounded fun (x : ℕ) => c

Constants are polynomially bounded.

theorem Cslib.PolynomiallyBounded.id : PolynomiallyBounded fun (n : ℕ) => n

The identity is polynomially bounded.

theorem Cslib.PolynomiallyBounded.add {f g : ℕ → ℕ} (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) : PolynomiallyBounded fun (n : ℕ) => f n + g n

Sums of polynomially bounded functions are polynomially bounded.

theorem Cslib.PolynomiallyBounded.mul {f g : ℕ → ℕ} (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) : PolynomiallyBounded fun (n : ℕ) => f n * g n

Products of polynomially bounded functions are polynomially bounded.

theorem Cslib.PolynomiallyBounded.pow {f : ℕ → ℕ} (hf : PolynomiallyBounded f) (d : ℕ) : PolynomiallyBounded fun (n : ℕ) => f n ^ d

Fixed powers of a polynomially bounded function are polynomially bounded.

theorem Cslib.PolynomiallyBounded.comp {f g : ℕ → ℕ} (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) : PolynomiallyBounded fun (n : ℕ) => f (g n)

Compositions of polynomially bounded functions are polynomially bounded.

theorem Cslib.PolynomiallyBounded.polynomial_eval (p : Polynomial ℕ) : PolynomiallyBounded fun (n : ℕ) => Polynomial.eval n p

Evaluating a polynomial with natural coefficients is polynomially bounded. This is how the certificate lengths of NP, given by polynomials, enter bound computations.

theorem Cslib.PolynomiallyBounded.tsub {f : ℕ → ℕ} (hf : PolynomiallyBounded f) (g : ℕ → ℕ) : PolynomiallyBounded fun (n : ℕ) => f n - g n

Truncated subtraction does not exceed its first argument.

theorem Cslib.PolynomiallyBounded.max {f g : ℕ → ℕ} (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) : PolynomiallyBounded fun (n : ℕ) => max (f n) (g n)

The maximum of two polynomially bounded functions is polynomially bounded.

theorem Cslib.PolynomiallyBounded.min {f : ℕ → ℕ} (hf : PolynomiallyBounded f) (g : ℕ → ℕ) : PolynomiallyBounded fun (n : ℕ) => min (f n) (g n)

The minimum does not exceed its first argument.

theorem Cslib.PolynomiallyBounded.div {f : ℕ → ℕ} (hf : PolynomiallyBounded f) (g : ℕ → ℕ) : PolynomiallyBounded fun (n : ℕ) => f n / g n

Division does not exceed the dividend.

theorem Cslib.PolynomiallyBounded.mod {f : ℕ → ℕ} (hf : PolynomiallyBounded f) (g : ℕ → ℕ) : PolynomiallyBounded fun (n : ℕ) => f n % g n

A remainder does not exceed the dividend.

theorem Cslib.PolynomiallyBounded.log {f : ℕ → ℕ} (b : ℕ) (hf : PolynomiallyBounded f) : PolynomiallyBounded fun (n : ℕ) => Nat.log b (f n)

A logarithm does not exceed its argument.

theorem Cslib.PolynomiallyBounded.ite {f g : ℕ → ℕ} (p : ℕ → Prop) [DecidablePred p] (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) : PolynomiallyBounded fun (n : ℕ) => if p n then f n else g n

A case distinction between polynomially bounded functions is polynomially bounded.