The scalar Crouzeix companion on a disk

On a circle, conjugating a polynomial turns every positive centered monomial into a negative Laurent mode. Consequently, the scalar Cauchy companion is constant throughout the disk: only the conjugate value at the center survives.

Rather than duplicate the Laurent-series calculation, this file realizes an interior scalar z as the one-dimensional multiplication operator on ℂ. The exact operator circle-auxiliary identity then gives the scalar result after passing the contour integral through evaluation at 1. A small resolvent lemma identifies that evaluated operator kernel with (sigma - z)⁻¹.

This supplies an unconditional model of the companion construction, continuous extension, and sharp contraction. The corresponding assertions for a general smooth convex boundary still require the Plemelj argument.

Main declarations

• crouzeixPolynomialScalarCompanion_ball_center_eq_eval_center -- the exact constant value of the companion in an arbitrary disk.
• crouzeixPolynomialScalarCompanion_ball_eq_eval_zero -- its centered form.
• norm_crouzeixPolynomialScalarCompanion_ball_center_le_polynomialSupNorm_closedBall -- sharp contraction on an arbitrary closed disk.
• norm_crouzeixPolynomialScalarCompanion_ball_le_polynomialSupNorm_closedBall -- the centered contraction.

theorem crouzeixPolynomialScalarCompanion_ball_center_eq_eval_center (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Metric.ball c R) : crouzeixPolynomialScalarCompanion (SmoothJordanDomain.ball c R hR) p z = star (Polynomial.eval c p)

For every interior point of a disk, the scalar Crouzeix companion is the constant star (p.eval c), where c is the center.

theorem crouzeixPolynomialScalarCompanion_ball_eq_eval_zero {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Metric.ball 0 R) : crouzeixPolynomialScalarCompanion (SmoothJordanDomain.ball 0 R hR) p z = star (Polynomial.eval 0 p)

For every interior point of a centered disk, the scalar Crouzeix companion is the constant star (p.eval 0).

theorem norm_crouzeixPolynomialScalarCompanion_ball_center_le_polynomialSupNorm_closedBall (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Metric.ball c R) : ‖crouzeixPolynomialScalarCompanion (SmoothJordanDomain.ball c R hR) p z‖ ≤ polynomialSupNorm p (Metric.closedBall c R)

The scalar companion on an arbitrary disk is contractive for the polynomial sup norm on the corresponding closed disk.

theorem norm_crouzeixPolynomialScalarCompanion_ball_le_polynomialSupNorm_closedBall {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Metric.ball 0 R) : ‖crouzeixPolynomialScalarCompanion (SmoothJordanDomain.ball 0 R hR) p z‖ ≤ polynomialSupNorm p (Metric.closedBall 0 R)

The scalar companion on a centered disk is contractive for the polynomial sup norm on the closed disk.