The polynomial auxiliary operator on a centered circle

On the circle |z| = R, conjugating a polynomial turns every positive monomial into a negative Laurent mode. The normalized resolvent integral kills all of those modes, while the constant mode integrates to the identity. Consequently, the Crouzeix--Palencia polynomial auxiliary operator is simply star (p.eval 0) • 1 in the centered-disk model.

Main declaration

• crouzeixPolynomialAuxiliaryOperator_ball_eq_eval_zero_smul_one — the exact centered-circle auxiliary identity used by the sharp product bound.

theorem crouzeixPolynomialAuxiliaryOperator_ball_eq_eval_zero_of_circle_integrals {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {R : ℝ} (hRpos : 0 < R) (hcont : ∀ (q : Polynomial ℂ), CircleIntegrable (fun (z : ℂ) => star (Polynomial.eval z q) • resolvent A z) 0 R) (hmass : (2 * ↑Real.pi * Complex.I)⁻¹ • circleIntegral (resolvent A) 0 R = 1) (hnegative : ∀ (m : ℕ), 0 < m → (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, R), z⁻¹ ^ m • resolvent A z = 0) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball 0 R hRpos) p = star (Polynomial.eval 0 p) • 1

Polynomial induction reduces the conjugate-circle auxiliary value to its constant resolvent mode and vanishing negative Laurent modes. Both norm and spectral circle-enclosure criteria supply these same analytic identities.

theorem crouzeixPolynomialAuxiliaryOperator_ball_eq_eval_zero_smul_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball 0 R ⋯) p = star (Polynomial.eval 0 p) • 1

For ‖A‖ < R, the conjugate-polynomial auxiliary operator on the centered disk is the constant operator star (p.eval 0) • 1.