The auxiliary product bound for aligned circles and normal polynomial values

The fixed-domain auxiliary product estimate against the closed numerical range is false for arbitrary containing circles: an off-center contour can sample p at a point unrelated to the control set. This file records a correct strengthened branch. If the individual value p(A) is star-normal and the circle center belongs to closure (numericalRange A), spectral calculus controls p(A) by the numerical-range sup norm, while center membership controls the scalar value appearing in the affine-circle auxiliary identity.

Main declarations

• norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_center_le_of_isStarNormal_aeval proves the literal L4.2e product conclusion when the individual value p(A) is star-normal.
• norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_center_le_of_isStarNormal specializes the result to a star-normal operator.

theorem norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_center_le_of_isStarNormal_aeval {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hc : c ∈ closure (numericalRange A)) (p : Polynomial ℂ) [IsStarNormal ((Polynomial.aeval A) p)] : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p (closure (numericalRange A)) ^ 2

If the individual value p(A) is star-normal, an enclosing circle centered at a point of the closed numerical range satisfies the sharp auxiliary product bound with the closed numerical range itself as control set.

theorem norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_center_le_of_isStarNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hc : c ∈ closure (numericalRange A)) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p (closure (numericalRange A)) ^ 2

For a star-normal operator, an enclosing circle centered at a point of the closed numerical range satisfies the sharp auxiliary product bound with the closed numerical range itself as control set.