@[reducible, inline]

abbrev NewtonKantorovich.ComplexSup : Type

Complex numbers represented as two real coordinates with the sup norm.

Equations

• NewtonKantorovich.ComplexSup = (Fin 2 → ℝ)

noncomputable def NewtonKantorovich.ComplexSup.equiv : ℂ ≃L[ℝ] ComplexSup

The natural continuous real-linear equivalence between ℂ and its two-coordinate sup-norm model.

Equations

• NewtonKantorovich.ComplexSup.equiv = Complex.equivRealProdCLM.trans (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm

@[simp]

theorem NewtonKantorovich.ComplexSup.equiv_apply_zero (z : ℂ) : equiv z 0 = z.re

@[simp]

theorem NewtonKantorovich.ComplexSup.equiv_apply_one (z : ℂ) : equiv z 1 = z.im

@[simp]

theorem NewtonKantorovich.ComplexSup.equiv_symm_re (x : ComplexSup) : (equiv.symm x).re = x 0

@[simp]

theorem NewtonKantorovich.ComplexSup.equiv_symm_im (x : ComplexSup) : (equiv.symm x).im = x 1

theorem NewtonKantorovich.ComplexSup.norm_equiv (z : ℂ) : ‖equiv z‖ = max |z.re| |z.im|

The transported norm is the maximum absolute coordinate.

def NewtonKantorovich.ComplexSup.mulMatrix (z : ℂ) : Matrix (Fin 2) (Fin 2) ℝ

The real matrix of multiplication by a complex scalar.

Equations

• NewtonKantorovich.ComplexSup.mulMatrix z = !![z.re, -z.im; z.im, z.re]

noncomputable def NewtonKantorovich.ComplexSup.mul (z : ℂ) : ComplexSup →L[ℝ] ComplexSup

Multiplication by a complex scalar as a continuous real-linear operator on the sup-norm model.

Equations

• NewtonKantorovich.ComplexSup.mul z = { toLinearMap := (NewtonKantorovich.ComplexSup.mulMatrix z).mulVecLin, cont := ⋯ }

@[simp]

theorem NewtonKantorovich.ComplexSup.mul_apply_zero (z : ℂ) (x : ComplexSup) : (mul z) x 0 = z.re * x 0 - z.im * x 1

@[simp]

theorem NewtonKantorovich.ComplexSup.mul_apply_one (z : ℂ) (x : ComplexSup) : (mul z) x 1 = z.im * x 0 + z.re * x 1

theorem NewtonKantorovich.ComplexSup.equiv_symm_mul (z : ℂ) (x : ComplexSup) : equiv.symm ((mul z) x) = z * equiv.symm x

Transporting the sup-norm multiplication operator back to ℂ gives ordinary complex multiplication.

theorem NewtonKantorovich.ComplexSup.mul_eq_transport (z : ℂ) : mul z = ↑equiv ∘SL ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ z) ∘SL ↑equiv.symm

Complex multiplication is conjugation of scalar multiplication by the coordinate equivalence.

theorem NewtonKantorovich.ComplexSup.norm_mul (z : ℂ) : ‖mul z‖ = |z.re| + |z.im|

Exact sup-operator norm of complex multiplication.

theorem NewtonKantorovich.ComplexSup.continuous_mul : Continuous mul

Complex multiplication varies continuously in the operator norm.

@[simp]

theorem NewtonKantorovich.ComplexSup.mul_one : mul 1 = 1

theorem NewtonKantorovich.ComplexSup.mul_sub (z w : ℂ) : mul (z - w) = mul z - mul w

theorem NewtonKantorovich.ComplexSup.mul_add (z w : ℂ) : mul (z + w) = mul z + mul w

@[simp]

theorem NewtonKantorovich.ComplexSup.mul_zero : mul 0 = 0

theorem NewtonKantorovich.ComplexSup.mul_sum {ι : Type u_1} (S : Finset ι) (f : ι → ℂ) : mul (∑ i ∈ S, f i) = ∑ i ∈ S, mul (f i)

theorem NewtonKantorovich.ComplexSup.mul_comp (z w : ℂ) : mul z ∘SL mul w = mul (z * w)

theorem NewtonKantorovich.ComplexSup.norm_one_sub_mul (z : ℂ) : ‖1 - mul z‖ = |1 - z.re| + |z.im|

Exact first-order defect: there is no Euclidean-to-sup norm loss.

theorem NewtonKantorovich.ComplexSup.norm_mul_le_sqrt_two (z : ℂ) : ‖mul z‖ ≤ √2 * ‖z‖

Comparison of the sup operator norm with the Euclidean complex norm.

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

Evaluation of a complex polynomial, transported to the sup-norm model.

Equations

• NewtonKantorovich.ComplexSup.eval p x = NewtonKantorovich.ComplexSup.equiv (Polynomial.eval (NewtonKantorovich.ComplexSup.equiv.symm x) p)

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

The real Fréchet derivative of transported polynomial evaluation.

Equations

• NewtonKantorovich.ComplexSup.evalDeriv p x = NewtonKantorovich.ComplexSup.mul (Polynomial.eval (NewtonKantorovich.ComplexSup.equiv.symm x) (Polynomial.derivative p))

theorem NewtonKantorovich.ComplexSup.hasFDerivAt_eval (p : Polynomial ℂ) (x : ComplexSup) : HasFDerivAt (eval p) (evalDeriv p x) x

Transported polynomial evaluation has the expected real Fréchet derivative. The norm-inherited parent structures are explicit because Pi also has definitionally distinct direct parent instances; the generic Newton--Kantorovich theorem consumes the norm-inherited ones.

theorem NewtonKantorovich.ComplexSup.continuous_evalDeriv (p : Polynomial ℂ) : Continuous (evalDeriv p)

The derivative of transported polynomial evaluation varies continuously.

theorem NewtonKantorovich.ComplexSup.existsUnique_root {p : Polynomial ℂ} {A : ComplexSup →L[ℝ] ComplexSup} {R : ENNReal} {x₀ : ComplexSup} {y z₁ z₂ r : NNReal} (hy : ‖A (eval p x₀)‖₊ ≤ y) (hz₁ : ‖1 - A ∘SL evalDeriv p x₀‖₊ ≤ z₁) (hz₂ : ∀ x ∈ Metric.closedEBall x₀ R, ‖A ∘SL (evalDeriv p x - evalDeriv p x₀)‖₊ ≤ z₂ * ‖x - x₀‖₊) (hrR : ↑r ≤ R) (hyr : y + z₁ * r + z₂ * r ^ 2 / 2 ≤ r) (hzr : z₁ + z₂ * r < 1) : ∃! x : ComplexSup, Polynomial.eval (equiv.symm x) p = 0 ∧ ‖x - x₀‖₊ ≤ r

Newton--Kantorovich specialized to a complex polynomial in sup-norm coordinates. The witness-specific estimates enter only through the three exact bounds hy, hz₁, and hz₂.