A fixed polynomial has one uniform power bound on the whole range x ≥ 1. This extracts an actual degree and constant for scalar cost formulas.

def EulerPolynomialCost.coefficientCost (p : Polynomial ℝ) : ℝ

Coefficient cost, given by 1+∑ n ∈ p.support, |p.coeff n|.

Equations

• EulerPolynomialCost.coefficientCost p = 1 + ∑ n ∈ p.support, |p.coeff n|

theorem EulerPolynomialCost.coefficientCost_pos (p : Polynomial ℝ) : 0 < coefficientCost p

theorem EulerPolynomialCost.eval_bound (p : Polynomial ℝ) (x : ℝ) (hx : 1 ≤ x) : |Polynomial.eval x p| ≤ coefficientCost p * x ^ p.natDegree