Deflation: $P(w) = (w-z)Q(w) + P(z)$ with Horner's coefficients

Proved

MetodosNumericos.horner_deflation

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

numerical-analysispolynomials

With $b_0, \\dots, b_n$ the Horner coefficients of $P$ at $z$ , the polynomial $Q(w) = \\sum_{i=0}^{n-1} b_i w^{\\,n-1-i}$ satisfies $P(w) = (w-z)Q(w) + b_n$ for every $w$ . In particular, when $z$ is a root, $Q$ is the deflated polynomial whose zeros are the remaining zeros of $P$ .

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_polinomiosDefs

Formal statement

namespace MetodosNumericos

theorem horner_deflation (a : ℕ → ℝ) (n : ℕ) (hn : 1 ≤ n) (z w : ℝ) :
    polyVal a n w =
      (w - z) * (∑ i ∈ Finset.range n, hornerSeq a z i * w ^ (n - 1 - i)) + hornerSeq a z n := by
  sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 4, §4.7 Deflação de um Polinômio, pp. 81–82.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

For an arbitrary $a : \\mathbb{N} \\to \\mathbb{R}$ , a natural number $n$ with $n \\ge 1$ , and arbitrary reals $z$ and $w$ , the statement asserts

\\sum_{i=0}^{n} a_i\\, w^{\\,n-i} \\;=\\; (w - z)\\left(\\sum_{i=0}^{n-1} b_i\\, w^{\\,n-1-i}\\right) + b_n,

where $b_0 = a_0$ and $b_{i+1} = a_{i+1} + z\\,b_i$ . The second sum runs over $i = 0, \\dots, n-1$ and its exponents use truncated natural-number subtraction. No hypothesis says that $z$ is a root of the polynomial; the identity is asserted for all $z$ and $w$ , with $b_n$ playing the role of the remainder.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Deflation: P(w)=(w−z)Q(w)+P(z)P(w) = (w-z)Q(w) + P(z)P(w)=(w−z)Q(w)+P(z) with Horner's coefficients

Deflation: $P(w) = (w-z)Q(w) + P(z)$ with Horner's coefficients