noncomputable def NewtonKantorovich.ComplexSup.inverseAt (p : Polynomial ℂ) (z : ℂ) : ComplexSup →L[ℝ] ComplexSup

Multiplication by the exact inverse derivative at z.

Equations

• NewtonKantorovich.ComplexSup.inverseAt p z = NewtonKantorovich.ComplexSup.mul (Polynomial.eval z (Polynomial.derivative p))⁻¹

theorem NewtonKantorovich.ComplexSup.inverseAt_comp_deriv {p : Polynomial ℂ} {z : ℂ} (hz : Polynomial.eval z (Polynomial.derivative p) ≠ 0) : inverseAt p z ∘SL evalDeriv p (equiv z) = 1

The exact inverse derivative is a left inverse to multiplication by the derivative at a simple root.

theorem NewtonKantorovich.ComplexSup.mul_injective {z : ℂ} (hz : z ≠ 0) : Function.Injective ⇑(mul z)

Multiplication by a nonzero complex scalar is injective in sup coordinates.

theorem NewtonKantorovich.ComplexSup.inverseAt_injective {p : Polynomial ℂ} {z : ℂ} (hz : Polynomial.eval z (Polynomial.derivative p) ≠ 0) : Function.Injective ⇑(inverseAt p z)

The exact inverse derivative operator is injective.

noncomputable def NewtonKantorovich.ComplexSup.newtonAt (p : Polynomial ℂ) (z : ℂ) (x : ComplexSup) : ComplexSup

The frozen-inverse Newton map based at z.

Equations

• NewtonKantorovich.ComplexSup.newtonAt p z x = x - (NewtonKantorovich.ComplexSup.inverseAt p z) (NewtonKantorovich.ComplexSup.eval p x)

noncomputable def NewtonKantorovich.ComplexSup.newtonDeriv (p : Polynomial ℂ) (z : ℂ) (x : ComplexSup) : ComplexSup →L[ℝ] ComplexSup

The real Fréchet derivative of the frozen-inverse Newton map.

Equations

• NewtonKantorovich.ComplexSup.newtonDeriv p z x = 1 - NewtonKantorovich.ComplexSup.inverseAt p z ∘SL NewtonKantorovich.ComplexSup.evalDeriv p x

theorem NewtonKantorovich.ComplexSup.hasFDerivAt_newtonAt (p : Polynomial ℂ) (z : ℂ) (x : ComplexSup) : HasFDerivAt (newtonAt p z) (newtonDeriv p z x) x

The frozen-inverse Newton map has the expected derivative.

theorem NewtonKantorovich.ComplexSup.continuous_newtonDeriv (p : Polynomial ℂ) (z : ℂ) : Continuous (newtonDeriv p z)

The derivative of the frozen-inverse Newton map is continuous.

theorem NewtonKantorovich.ComplexSup.newtonDeriv_at_root {p : Polynomial ℂ} {z : ℂ} (hz : Polynomial.eval z (Polynomial.derivative p) ≠ 0) : newtonDeriv p z (equiv z) = 0

At a simple root, the Newton-map derivative vanishes exactly.

theorem NewtonKantorovich.ComplexSup.newtonAt_fixed {p : Polynomial ℂ} {z : ℂ} (hz : Polynomial.eval z p = 0) : newtonAt p z (equiv z) = equiv z

A root is a fixed point of its frozen-inverse Newton map.

theorem NewtonKantorovich.ComplexSup.newtonAt_fixed_iff {p : Polynomial ℂ} {z : ℂ} (hz : Polynomial.eval z (Polynomial.derivative p) ≠ 0) (x : ComplexSup) : newtonAt p z x = x ↔ Polynomial.eval (equiv.symm x) p = 0

With a nonzero derivative, the fixed points of the frozen Newton map are exactly the polynomial roots.

theorem NewtonKantorovich.ComplexSup.inverseAt_eval_eq_sub (p : Polynomial ℂ) (z : ℂ) (x : ComplexSup) : (inverseAt p z) (eval p x) = x - newtonAt p z x

The Newton correction is exactly the displacement from the frozen Newton image.

theorem NewtonKantorovich.ComplexSup.exists_residual_bounds {p : Polynomial ℂ} {z : ℂ} (hroot : Polynomial.eval z p = 0) (hsimple : Polynomial.eval z (Polynomial.derivative p) ≠ 0) {K : NNReal} (hK : 0 < K) : ∃ (r : NNReal), 0 < r ∧ ∀ x ∈ Metric.closedBall (equiv z) ↑r, ‖newtonDeriv p z x‖ ≤ ↑K ∧ ‖(inverseAt p z) (eval p x)‖ ≤ (1 + ↑K) * dist x (equiv z)

Near a simple root, both the derivative defect and the Newton residual have uniform quantitative bounds for any chosen positive defect target. Item 29 chooses the target against the executable square's centre margin and combines these bounds with the executable reciprocal and Taylor bounds.

theorem NewtonKantorovich.ComplexSup.exists_contraction {p : Polynomial ℂ} {z : ℂ} (hroot : Polynomial.eval z p = 0) (hsimple : Polynomial.eval z (Polynomial.derivative p) ≠ 0) : ∃ (r : NNReal), 0 < r ∧ ∃ (hmap : Set.MapsTo (newtonAt p z) (Metric.closedBall (equiv z) ↑r) (Metric.closedBall (equiv z) ↑r)), ContractingWith (1 / 2) (Set.MapsTo.restrict (newtonAt p z) (Metric.closedBall (equiv z) ↑r) (Metric.closedBall (equiv z) ↑r) hmap) ∧ ∀ x ∈ Metric.closedBall (equiv z) ↑r, newtonAt p z x = x → x = equiv z

Around every simple root, the frozen-inverse Newton map contracts by 1/2 on some nontrivial closed sup ball, preserves that ball, and has the given root as its unique fixed point there.