Horner's method

DefinitionHorner evaluation with operation count#✓fully proved

Let \(R\) be a commutative semiring, let \(x \in R\), and let \(a_0, \dots, a_{n-1} \in R\) be coefficients listed in ascending order of degree. Horner evaluation starts with the accumulator \(v = 0\) and, for \(i = n-1, \dots, 0\) in turn, replaces \(v\) by \(a_i + x v\), charging two operations (one multiplication and one addition) for each step. It returns the final accumulator together with the total number of operations charged, a natural number.

def hornerEval {n : Nat} (x : R) (coefficients : Fin n → R) : TimeM Nat R :=
  (List.ofFn coefficients).foldrM (fun coefficient value => do
    ✓[2]
    pure (coefficient + x * value)) 0

Used by 6

Used byHorner evaluation of the empty coefficient list · Horner evaluation is polynomial evaluation · Horner evaluation computes the coefficient sum · Horner evaluation of a constant polynomial · Horner evaluation uses \(2n\) operations · Horner evaluation at zero

TheoremHorner evaluation uses \(2n\) operations#✓fully proved

For every commutative semiring \(R\), every \(x \in R\) and all coefficients \(a_0, \dots, a_{n-1} \in R\), Horner evaluation of \(a_0, \dots, a_{n-1}\) at \(x\) charges exactly \(2n\) operations, one multiplication and one addition per coefficient.

@[simp]
theorem hornerEval_time {n : Nat} (x : R) (coefficients : Fin n → R) :
    (hornerEval x coefficients).time = 2 * n

Uses 1 · Used by 2

Statement usesHorner evaluation with operation count

Used byHorner evaluation of the empty coefficient list · Horner evaluation of a constant polynomial

TheoremHorner evaluation computes the coefficient sum#✓fully proved

For every commutative semiring \(R\), every \(x \in R\) and all coefficients \(a_0, \dots, a_{n-1} \in R\), the value returned by Horner evaluation of \(a_0, \dots, a_{n-1}\) at \(x\) is \(\sum_{i=0}^{n-1} a_i x^i\).

theorem hornerEval_ret_eq_sum {n : Nat} (x : R) (coefficients : Fin n → R) :
    (hornerEval x coefficients).ret = ∑ i : Fin n, coefficients i * x ^ i.val

Uses 1 · Used by 4

Statement usesHorner evaluation with operation count

Used byHorner evaluation of the empty coefficient list · Horner evaluation is polynomial evaluation · Horner evaluation of a constant polynomial · Horner evaluation at zero

TheoremHorner evaluation is polynomial evaluation#✓fully proved

For every commutative semiring \(R\), every \(x \in R\) and all coefficients \(a_0, \dots, a_{n-1} \in R\), the value returned by Horner evaluation of \(a_0, \dots, a_{n-1}\) at \(x\) equals \(p(x)\), where \(p = a_0 + a_1 X + \dots + a_{n-1} X^{n-1} \in R[X]\) is the polynomial with these coefficients.

theorem hornerEval_ret_eq_eval [DecidableEq R] {n : Nat} (x : R)
    (coefficients : Fin n → R) :
    (hornerEval x coefficients).ret = (Polynomial.ofFn n coefficients).eval x

Uses 2

Statement usesHorner evaluation with operation count

Proof usesHorner evaluation computes the coefficient sum

TheoremHorner evaluation of the empty coefficient list#✓fully proved

For every commutative semiring \(R\) and every \(x \in R\), Horner evaluation at \(x\) with no coefficients (\(n = 0\)) returns \(0\) and charges \(0\) operations.

@[simp]
theorem hornerEval_empty (x : R) (coefficients : Fin 0 → R) :
    hornerEval x coefficients = ⟨0, 0⟩

Uses 3

Statement usesHorner evaluation with operation count

Proof usesHorner evaluation computes the coefficient sum · Horner evaluation uses \(2n\) operations

TheoremHorner evaluation of a constant polynomial#✓fully proved

For every commutative semiring \(R\), every \(x \in R\) and every single coefficient \(a_0 \in R\) (\(n = 1\)), Horner evaluation of \(a_0\) at \(x\) returns \(a_0\) and charges \(2\) operations.

The two operations are the multiplication \(x \cdot 0\) and the addition \(a_0 + x \cdot 0\), which are executed because the accumulator starts at zero.

@[simp]
theorem hornerEval_singleton (x : R) (coefficients : Fin 1 → R) :
    hornerEval x coefficients = ⟨coefficients 0, 2⟩

Uses 3

Statement usesHorner evaluation with operation count

Proof usesHorner evaluation computes the coefficient sum · Horner evaluation uses \(2n\) operations

TheoremHorner evaluation at zero#✓fully proved

For every commutative semiring \(R\) and all coefficients \(a_0, \dots, a_n \in R\) (at least one coefficient), the value returned by Horner evaluation of \(a_0, \dots, a_n\) at \(x = 0\) is \(a_0\).

@[simp]
theorem hornerEval_zero {n : Nat} (coefficients : Fin (n + 1) → R) :
    (hornerEval 0 coefficients).ret = coefficients 0

Uses 2

Statement usesHorner evaluation with operation count

Proof usesHorner evaluation computes the coefficient sum

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.