noncomputable def HexRootsMathlib.NKData.exactCoeffNorm (p : Polynomial ℂ) (k : ℕ) (x : NewtonKantorovich.ComplexSup) : ℝ

Exact-centre inverse applied to one Taylor coefficient, measured in the sup operator norm.

Equations

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

theorem HexRootsMathlib.NKData.continuousAt_exactCoeffNorm {p : Polynomial ℂ} {x : NewtonKantorovich.ComplexSup} (hx : Polynomial.eval (NewtonKantorovich.ComplexSup.equiv.symm x) (Polynomial.derivative p) ≠ 0) (k : ℕ) : ContinuousAt (exactCoeffNorm p k) x

The exact-coefficient norm varies continuously wherever the polynomial derivative is nonzero.

noncomputable def HexRootsMathlib.NKData.tailMajorant (p : Hex.ZPoly) (x : NewtonKantorovich.ComplexSup) : ℝ

The exact majorant for the executable radial Taylor sum with every radius power replaced by one.

Equations

• HexRootsMathlib.NKData.tailMajorant p x = 2 * ∑ k ∈ Finset.range (Hex.DensePoly.size p), if 2 ≤ k then ↑k * HexRootsMathlib.NKData.exactCoeffNorm (HexRootsMathlib.toPolyℂ p) k x else 0

theorem HexRootsMathlib.NKData.continuousAt_tailMajorant {p : Hex.ZPoly} {x : NewtonKantorovich.ComplexSup} (hx : Polynomial.eval (NewtonKantorovich.ComplexSup.equiv.symm x) (Polynomial.derivative (toPolyℂ p)) ≠ 0) : ContinuousAt (tailMajorant p) x

The tail majorant is continuous wherever the derivative does not vanish.

theorem HexRootsMathlib.NKData.tailMajorant_nonneg (p : Hex.ZPoly) (x : NewtonKantorovich.ComplexSup) : 0 ≤ tailMajorant p x

The tail majorant is nonnegative.

theorem HexRootsMathlib.NKData.exists_tail_bound {p : Hex.ZPoly} {z : ℂ} (hsimple : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0) : ∃ (R : NNReal), 0 < R ∧ ∃ (B : ℝ), 0 < B ∧ ∀ x ∈ Metric.closedBall (NewtonKantorovich.ComplexSup.equiv z) ↑R, tailMajorant p x ≤ B

The exact radial majorant is uniformly bounded on some nontrivial closed neighbourhood of a simple root.

theorem HexRootsMathlib.NKData.invFloor_defect {x : Dyadic} (hx : 0 < x) : have q := 8 + max 0 (Hex.Dyadic.ceilLog2 x); have u := Hex.Dyadic.invFloor x q; 0 ≤ Dyadic.toReal (1 - u * x) ∧ Dyadic.toReal (1 - u * x) < 2 ^ (-8)

The pinned reciprocal precision makes the relative floor error strictly less than 2⁻⁸, independently of the magnitude of the positive dyadic input.

theorem HexRootsMathlib.NKData.z1_lt (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hnorm : 0 < normSq p s) : Dyadic.toReal (z1 p s) < 2 ^ (-8)

The executable first-order defect inherits the uniform 2⁻⁸ bound from the pinned reciprocal floor.

theorem NewtonKantorovich.ComplexSup.deriv_ne_zero_of_defect {p : Polynomial ℂ} {z : ℂ} (x : ComplexSup) (hdefect : ‖newtonDeriv p z x‖ < 1) : Polynomial.eval (equiv.symm x) (Polynomial.derivative p) ≠ 0

A Newton defect strictly below one forces the derivative at the nearby centre to remain nonzero.

theorem NewtonKantorovich.ComplexSup.inverseAt_eval_le {p : Polynomial ℂ} {z : ℂ} (hsimple : Polynomial.eval z (Polynomial.derivative p) ≠ 0) (x : ComplexSup) (hdefect : ‖newtonDeriv p z x‖ ≤ 1 / 8) : ‖(inverseAt p (equiv.symm x)) (eval p x)‖ ≤ 8 / 7 * ‖(inverseAt p z) (eval p x)‖

If the frozen exact-root Newton derivative has norm at most 1/8 at a nearby centre, inversion at that centre amplifies the exact-root correction by at most 8/7.

theorem HexRootsMathlib.NKData.approxInverse_factor (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hnorm : 0 < normSq p s) : ∃ (θ : ℝ), 0 ≤ θ ∧ θ ≤ 1 ∧ approxInverse p s = θ • NewtonKantorovich.ComplexSup.inverseAt (toPolyℂ p) (DyadicSquare.center s)

The executable approximate inverse is a scalar in [0,1] times the exact inverse at the executable centre.

theorem HexRootsMathlib.NKData.norm_approxInverse_le (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hnorm : 0 < normSq p s) (v₀ : NewtonKantorovich.ComplexSup) : ‖(approxInverse p s) v₀‖ ≤ ‖(NewtonKantorovich.ComplexSup.inverseAt (toPolyℂ p) (DyadicSquare.center s)) v₀‖

Flooring the reciprocal can only decrease the sup norm of the exact Newton correction based at the executable centre.

theorem HexRootsMathlib.NKData.norm_exactCoeff (p : Hex.ZPoly) (s : Hex.DyadicSquare) (k : ℕ) : ‖NewtonKantorovich.ComplexSup.inverseAt (toPolyℂ p) (DyadicSquare.center s) ∘SL NewtonKantorovich.ComplexSup.mul (GaussDyadic.toComplex ((coeffs p s).getD k (0, 0)))‖ = exactCoeffNorm (toPolyℂ p) k (centerSup s)

The operator norm of the scaled executable Taylor-coefficient multiplier is the exact coefficient norm at the square's centre.

theorem HexRootsMathlib.NKData.hi_residual_le (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hnorm : 0 < normSq p s) (k : ℕ) : Dyadic.toReal (residual p s k).hi ≤ exactCoeffNorm (toPolyℂ p) k (centerSup s)

Each executable residual-coefficient row norm is bounded by its exact centre-inverse counterpart.

theorem HexRootsMathlib.NKData.z2_le_tailMajorant (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hnorm : 0 < normSq p s) (hradius : Dyadic.toReal s.radiusHi ≤ 1) : Dyadic.toReal (z2 p s) ≤ tailMajorant p (centerSup s)

Once the executable radial upper bound is at most one, z2 is bounded by the continuous exact-centre majorant.

theorem HexRootsMathlib.NKData.normSq_pos (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hderiv : Polynomial.eval (DyadicSquare.center s) (Polynomial.derivative (toPolyℂ p)) ≠ 0) : 0 < normSq p s

A nonzero derivative at the executable centre gives a positive exact dyadic squared norm.

theorem HexRootsMathlib.NKData.witness_of_estimates (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hsize : 2 ≤ (coeffs p s).size) (hnorm : 0 < normSq p s) (hy : Dyadic.toReal (y p s) ≤ 9 / 14 * DyadicSquare.halfWidth s) (hz2 : Dyadic.toReal (z2 p s) * DyadicSquare.halfWidth s < 1 / 8) : Hex.nkWitness p s

The concrete margins used to close the executable witness inequalities. The first-order defect is supplied automatically by the pinned reciprocal; the caller supplies the local residual and shrinking z2 * r estimates.

theorem HexRootsMathlib.NKData.exists_witness_of_z2 {p : Hex.ZPoly} {z : ℂ} (hroot : Polynomial.eval z (toPolyℂ p) = 0) (hsimple : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0) (hsize : 2 ≤ Hex.DensePoly.size p) : ∃ (R : NNReal), 0 < R ∧ ∀ (s : Hex.DyadicSquare), centerSup s ∈ Metric.closedBall (NewtonKantorovich.ComplexSup.equiv z) ↑R → dist (centerSup s) (NewtonKantorovich.ComplexSup.equiv z) ≤ DyadicSquare.halfWidth s / 2 → Dyadic.toReal (z2 p s) * DyadicSquare.halfWidth s < 1 / 8 → Hex.nkWitness p s

On the local Newton neighbourhood, a square whose root has the doubled enclosing-square margin certifies as soon as its radial z2 * r term is small.

theorem HexRootsMathlib.NKData.exists_nkWitness_radius {p : Hex.ZPoly} {z : ℂ} (hroot : Polynomial.eval z (toPolyℂ p) = 0) (hsimple : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0) (hsize : 2 ≤ Hex.DensePoly.size p) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (s : Hex.DyadicSquare), dist (centerSup s) (NewtonKantorovich.ComplexSup.equiv z) ≤ DyadicSquare.halfWidth s / 2 → DyadicSquare.halfWidth s < ε → Hex.nkWitness p s

Every sufficiently small doubled square whose centre is within half a half-width of a simple root passes the actual executable NK witness.

theorem HexRootsMathlib.NKData.exists_nkWitness_prec {p : Hex.ZPoly} {z : ℂ} (hroot : Polynomial.eval z (toPolyℂ p) = 0) (hsimple : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0) (hsize : 2 ≤ Hex.DensePoly.size p) : ∃ (N : ℕ), ∀ (s : Hex.DyadicSquare), ↑N ≤ s.prec → dist (centerSup s) (NewtonKantorovich.ComplexSup.equiv z) ≤ DyadicSquare.halfWidth s / 2 → Hex.nkWitness p s

Precision-threshold form of eventual executable NK recertification. The half-radius centre hypothesis is exactly the margin obtained by testing the square concentric with an enclosing square one level coarser.