noncomputable def HexRootsMathlib.graeffeEvenPart (p : Polynomial ℂ) : Polynomial ℂ

Coefficients of even powers, with exponents divided by two.

Equations

• HexRootsMathlib.graeffeEvenPart p = Polynomial.contract 2 p

noncomputable def HexRootsMathlib.graeffeOddPart (p : Polynomial ℂ) : Polynomial ℂ

Coefficients of odd powers, with one X removed and exponents divided by two.

Equations

• HexRootsMathlib.graeffeOddPart p = Polynomial.contract 2 p.divX

noncomputable def HexRootsMathlib.graeffePoly (p : Polynomial ℂ) : Polynomial ℂ

One exact Graeffe transform.

Equations

• HexRootsMathlib.graeffePoly p = HexRootsMathlib.graeffeEvenPart p ^ 2 - Polynomial.X * HexRootsMathlib.graeffeOddPart p ^ 2

@[simp]

theorem HexRootsMathlib.graeffePoly_zero : graeffePoly 0 = 0

The Graeffe transform fixes the zero polynomial.

theorem HexRootsMathlib.expand_graeffe_parts (p : Polynomial ℂ) : (Polynomial.expand ℂ 2) (graeffeEvenPart p) + Polynomial.X * (Polynomial.expand ℂ 2) (graeffeOddPart p) = p

Recombining the contracted even and odd parts recovers the polynomial.

theorem HexRootsMathlib.expand_graeffePoly (p : Polynomial ℂ) : (Polynomial.expand ℂ 2) (graeffePoly p) = p * p.comp (-Polynomial.X)

Defining identity for one Graeffe step: G(p)(X²) = p(X) p(-X).

theorem HexRootsMathlib.roots_graeffePoly {p : Polynomial ℂ} (hp : p ≠ 0) : (graeffePoly p).roots = Multiset.map (fun (z : ℂ) => z ^ 2) p.roots

One Graeffe step squares every complex root, preserving multiplicity.

theorem HexRootsMathlib.graeffePoly_ne_zero {p : Polynomial ℂ} (hp : p ≠ 0) : graeffePoly p ≠ 0

A Graeffe step of a nonzero polynomial is nonzero.

theorem HexRootsMathlib.rootsInDisc_graeffePoly {p : Polynomial ℂ} (hp : p ≠ 0) (r : ℝ) (hr : 0 ≤ r) : rootsInDisc (graeffePoly p) 0 (r ^ 2) = rootsInDisc p 0 r

Squaring all roots and the radius preserves the number of roots in the open disc.

def HexRootsMathlib.CoeffBall.Encloses (b : Hex.CoeffBall) (z : ℂ) : Prop

A coefficient ball encloses z when the coordinate L¹ distance from its stored centre is at most its real-valued radius.

Equations

• HexRootsMathlib.CoeffBall.Encloses b z = (HexRootsMathlib.complexL1✝ (z - HexRootsMathlib.GaussDyadic.toComplex b.center) ≤ HexRootsMathlib.Dyadic.toReal b.radius)

theorem HexRootsMathlib.CoeffBall.point_encloses (bits : ℕ) (z : Hex.GaussDyadic) : Encloses (Hex.CoeffBall.point bits z) (GaussDyadic.toComplex z)

A rounded point ball encloses its exact Gaussian-dyadic input.

theorem HexRootsMathlib.CoeffBall.add_encloses {x y : Hex.CoeffBall} {z w : ℂ} (hz : Encloses x z) (hw : Encloses y w) (bits : ℕ) : Encloses (Hex.CoeffBall.add bits x y) (z + w)

Outward-rounded ball addition is sound.

theorem HexRootsMathlib.CoeffBall.sub_encloses {x y : Hex.CoeffBall} {z w : ℂ} (hz : Encloses x z) (hw : Encloses y w) (bits : ℕ) : Encloses (Hex.CoeffBall.sub bits x y) (z - w)

Outward-rounded ball subtraction is sound.

theorem HexRootsMathlib.CoeffBall.mul_encloses {x y : Hex.CoeffBall} {z w : ℂ} (hz : Encloses x z) (hw : Encloses y w) (bits : ℕ) : Encloses (Hex.CoeffBall.mul bits x y) (z * w)

Outward-rounded ball multiplication is sound.

theorem HexRootsMathlib.CoeffBall.lo_le_norm {b : Hex.CoeffBall} {z : ℂ} (h : Encloses b z) : Dyadic.toReal b.lo ≤ ‖z‖

The executable lower endpoint of an enclosing coefficient ball is below the exact complex modulus.

theorem HexRootsMathlib.CoeffBall.norm_le_hi {b : Hex.CoeffBall} {z : ℂ} (h : Encloses b z) : ‖z‖ ≤ Dyadic.toReal b.hi

The exact complex modulus is below the executable upper endpoint of an enclosing coefficient ball.

theorem HexRootsMathlib.CoeffBall.softTaylorCoeff_encloses (p : Hex.ZPoly) (c : Hex.GaussDyadic) (h : Dyadic) (bits k : ℕ) : Encloses (Hex.softTaylorCoeff p c h bits k) (GaussDyadic.toComplex (Hex.taylorCoeff p c k) * ↑(Dyadic.toReal h) ^ k)

The soft Taylor coefficient encloses the corresponding coefficient of the exact Taylor shift, scaled by h^k.

noncomputable def HexRootsMathlib.localPoly (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Polynomial ℂ

The exact polynomial in square-local coordinates. Its unit square has the original square's half-width.

Equations

• One or more equations did not get rendered due to their size.

theorem HexRootsMathlib.taylorBalls_enclose (p : Hex.ZPoly) (s : Hex.DyadicSquare) (bits k : ℕ) : CoeffBall.Encloses ((Hex.taylorBalls p s bits).getD k Hex.CoeffBall.zero) ((localPoly p s).coeff k)

Every initial coefficient ball encloses the matching coefficient of the exact local polynomial.

theorem HexRootsMathlib.exactTaylorBalls_enclose (p : Hex.ZPoly) (s : Hex.DyadicSquare) (bits k : ℕ) : CoeffBall.Encloses ((Hex.exactTaylorBalls p s bits).getD k Hex.CoeffBall.zero) ((localPoly p s).coeff k)

The exact-shift ball constructor encloses the same local polynomial coefficients.

def HexRootsMathlib.BallsEnclose (cs : Array Hex.CoeffBall) (q : Polynomial ℂ) : Prop

A coefficient array encloses a polynomial through its stored degree.

Equations

• HexRootsMathlib.BallsEnclose cs q = (q.natDegree < cs.size ∧ ∀ k < cs.size, HexRootsMathlib.CoeffBall.Encloses (cs.getD k Hex.CoeffBall.zero) (q.coeff k))

theorem HexRootsMathlib.BallsEnclose.degree_lt {cs : Array Hex.CoeffBall} {q : Polynomial ℂ} (h : BallsEnclose cs q) : q.natDegree < cs.size

The degree bound carried by a complete coefficient-ball enclosure.

theorem HexRootsMathlib.taylorBalls_enclosePoly (p : Hex.ZPoly) (s : Hex.DyadicSquare) (bits : ℕ) (hp : 0 < Hex.DensePoly.size p) : BallsEnclose (Hex.taylorBalls p s bits) (localPoly p s)

The initial soft Taylor array encloses the complete local polynomial.

theorem HexRootsMathlib.exactTaylorBalls_enclosePoly (p : Hex.ZPoly) (s : Hex.DyadicSquare) (bits : ℕ) (hp : 0 < Hex.DensePoly.size p) : BallsEnclose (Hex.exactTaylorBalls p s bits) (localPoly p s)

The exact-shift array is also a complete coefficient-ball enclosure.

theorem HexRootsMathlib.natDegree_graeffePoly {q : Polynomial ℂ} (hq : q ≠ 0) : (graeffePoly q).natDegree = q.natDegree

A Graeffe step preserves natural degree for nonzero complex polynomials.

theorem HexRootsMathlib.graeffe_enclosePoly {cs : Array Hex.CoeffBall} {q : Polynomial ℂ} (h : BallsEnclose cs q) (bits : ℕ) : BallsEnclose (Hex.graeffe bits cs) (graeffePoly q)

One executable coefficient-ball Graeffe step encloses the exact transform.

theorem HexRootsMathlib.sum_erase_range {M : Type u_1} [AddCommMonoid M] (f : ℕ → M) (n k : ℕ) : ∑ i ∈ (Finset.range n).erase k, f i = ∑ i ∈ Finset.range n, if i = k then 0 else f i

Writing an omitted summand as an erased range or as an if gives the same finite sum. Shared by the Pellet-style dominance arguments downstream (RootFree, Pellet, Completeness.PelletDyadic).

theorem HexRootsMathlib.softPelletAt_size {cs : Array Hex.CoeffBall} {k : ℕ} {rlo rhi : Dyadic} (h : Hex.softPelletAt cs k rlo rhi = true) : k < cs.size

A successful soft comparison names a stored coefficient.

theorem HexRootsMathlib.softPelletThree_size {cs : Array Hex.CoeffBall} {k : ℕ} {rs : Hex.SoftRadii} (h : Hex.softPelletThree cs k rs = true) : k < cs.size

A successful three-radius comparison names a stored coefficient.

theorem HexRootsMathlib.softGraeffeLoop_size {cs : Array Hex.CoeffBall} {bits k rounds : ℕ} {rs : Hex.SoftRadii} (h : Hex.softGraeffeLoop bits k rounds cs rs = true) : k < cs.size

Array size is invariant through Graeffe, so any successful loop result still names a coefficient in the initial array.

theorem HexRootsMathlib.softPelletAt_bound {cs : Array Hex.CoeffBall} {k : ℕ} {rlo rhi : Dyadic} (h : Hex.softPelletAt cs k rlo rhi = true) : ∑ i ∈ (Finset.range cs.size).erase k, Dyadic.toReal (cs.getD i Hex.CoeffBall.zero).hi * Dyadic.toReal rhi ^ i < Dyadic.toReal (cs.getD k Hex.CoeffBall.zero).lo * Dyadic.toReal rlo ^ k

A successful soft comparison exposes its strict real endpoint inequality.

theorem HexRootsMathlib.softPelletAt_dominates {cs : Array Hex.CoeffBall} {q : Polynomial ℂ} {k : ℕ} {rlo rhi : Dyadic} {r : ℝ} (henclose : BallsEnclose cs q) (h : Hex.softPelletAt cs k rlo rhi = true) (hrlo : 0 ≤ Dyadic.toReal rlo) (hlo : Dyadic.toReal rlo ≤ r) (hhi : r ≤ Dyadic.toReal rhi) : ∑ i ∈ (Finset.range cs.size).erase k, ‖q.coeff i‖ * r ^ i < ‖q.coeff k‖ * r ^ k

Endpoint bounds plus coefficient-ball enclosure imply the exact coefficient dominance required by Pellet's theorem at every real radius in the supplied interval.