The centered-circle auxiliary operator under spectral enclosure

The circle Cauchy formulas in SpectralCauchy.lean require only that the spectrum lie strictly inside the circle. This file applies their resolvent and negative-Laurent identities to the conjugate boundary values of a polynomial. As in the operator-norm model, every positive monomial vanishes and only the constant coefficient remains.

This identity does not supply the product norm estimate in the general Crouzeix--Palencia argument: that estimate still needs the divided-difference boundary transform rather than a disk von Neumann inequality.

Main declaration

• crouzeixPolynomialAuxiliaryOperator_ball_eq_eval_zero_smul_one_of_spectrum_subset_ball -- the exact auxiliary value when the centered circle encloses the spectrum.
• norm_aeval_add_eval_zero_smul_one_le_two_mul_polynomialSupNorm_closedBall -- the resulting scalar form of the symmetrized estimate when the circle encloses the numerical range.

theorem crouzeixPolynomialAuxiliaryOperator_ball_eq_eval_zero_smul_one_of_spectrum_subset_ball {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 < r) (hσ : spectrum ℂ A ⊆ Metric.ball 0 r) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball 0 r hr) p = star (Polynomial.eval 0 p) • 1

If spectrum ℂ A lies in the centered open disk of radius r, the conjugate-polynomial auxiliary operator on its boundary circle is the constant operator star (p.eval 0) • 1.

theorem norm_aeval_add_eval_zero_smul_one_le_two_mul_polynomialSupNorm_closedBall {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 < r) (hW : closure (numericalRange A) ⊆ Metric.ball 0 r) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p + Polynomial.eval 0 p • 1‖ ≤ 2 * polynomialSupNorm p (Metric.closedBall 0 r)

If the closure of the numerical range lies inside a centered open disk, the symmetrized Crouzeix--Palencia estimate can be written without an auxiliary-operator symbol: its adjoint is simply p.eval 0 • 1.