noncomputable def HexRootsMathlib.isolateComplexRoots (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) : Array (Hex.DyadicRootIsolation p)

Isolate all complex roots of a nonzero squarefree integer polynomial.

Unlike Hex.ZPoly.isolateComplexRoots?, this proof-facing wrapper cannot return none: its required hypotheses discharge the driver's completeness conditions. The result is characterized by isolateComplexRoots_eq as the successful executable output, with the same atom strategy and requested-precision parameters.

Equations

• HexRootsMathlib.isolateComplexRoots p h hp atomPrec strategy = ⋯.choose

theorem HexRootsMathlib.isolateComplexRoots_eq (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) : p.isolateComplexRoots? h atomPrec strategy = some (isolateComplexRoots p h hp atomPrec strategy)

The total wrapper is exactly the successful result of Hex.ZPoly.isolateComplexRoots?.

theorem HexRootsMathlib.isolateComplexRoots_count (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) : (isolateComplexRoots p h hp atomPrec strategy).size = (toPolyℂ p).natDegree

The total wrapper returns one atom for each complex root, counted with multiplicity.

theorem HexRootsMathlib.isolateComplexRoots_roots (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) : (List.map DyadicRootIsolation.root (isolateComplexRoots p h hp atomPrec strategy).toList).toFinset = (toPolyℂ p).roots.toFinset

The semantic roots selected by the returned atoms are exactly the roots of the input polynomial.

theorem HexRootsMathlib.isolateComplexRoots_prec (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) (iso : Hex.DyadicRootIsolation p) : iso ∈ (isolateComplexRoots p h hp atomPrec strategy).toList → atomPrec ≤ iso.square.prec

Every returned atom meets the requested precision.

theorem HexRootsMathlib.isolateComplexRoots_disjoint (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) {i j : ℕ} (hi : i < (isolateComplexRoots p h hp atomPrec strategy).size) (hj : j < (isolateComplexRoots p h hp atomPrec strategy).size) (hij : i ≠ j) : Disjoint (DyadicSquare.closedDisc (isolateComplexRoots p h hp atomPrec strategy)[i].square) (DyadicSquare.closedDisc (isolateComplexRoots p h hp atomPrec strategy)[j].square)

Distinct atoms returned by the total wrapper have disjoint closed circumscribed discs.