Polynomial composition bounds

This module packages natural-polynomial composition as power-form big-O bounds. The second theorem records the coarse time expression used when two deterministic function computations are connected sequentially.

Main results

• BigO.polynomial_eval_comp — nested polynomial evaluation is polynomially bounded
• BigO.polynomial_composition_time — the coarse sequential runtime is polynomially bounded

theorem Complexity.BigO.polynomial_eval_comp (p q : Polynomial ℕ) : BigO (fun (n : ℕ) => Polynomial.eval (Polynomial.eval n p) q) fun (x : ℕ) => x ^ (q.comp p).natDegree

Composing evaluations of natural-coefficient polynomials gives a function bounded by a power whose exponent is the degree of the composed polynomial.

theorem Complexity.BigO.polynomial_composition_time (p q : Polynomial ℕ) : BigO (fun (n : ℕ) => 4 * Polynomial.eval n p + 11 + Polynomial.eval (Polynomial.eval n p) q) fun (x : ℕ) => x ^ (Polynomial.C 4 * p + Polynomial.C 11 + q.comp p).natDegree

The coarse runtime for sequentially composing computations with polynomial bounds p and q is itself bounded by a power.