Circle-model support for the Crouzeix--Palencia product bound

This file supplies the operator-norm assembly for L4.2e on a centered disk. First, affine polynomial transport scales von Neumann's inequality from the unit disk to closedBall 0 R. Second, if the polynomial auxiliary operator on the enclosing circle has been identified with star (p.eval 0) • 1, submultiplicativity gives the sharp product estimate.

The auxiliary identification is deliberately an explicit hypothesis: it is the conjugate-boundary circle Cauchy calculation, separate from the norm assembly proved here.

Main declarations

• norm_aeval_le_polynomialSupNorm_closedBall_of_norm_le -- von Neumann's inequality on a centered disk of positive radius.
• norm_aeval_mul_le_polynomialSupNorm_sq_of_auxiliary_eq_eval_zero_smul_one -- the sharp circle-model product estimate from the scalar auxiliary identification.
• norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_le -- the sharp product estimate for the actual centered-disk auxiliary operator.

theorem norm_aeval_le_polynomialSupNorm_closedBall_of_norm_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : 0 < R) (hA : ‖A‖ ≤ R) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ polynomialSupNorm p (Metric.closedBall 0 R)

Von Neumann's inequality scaled from the unit disk to a centered disk: if ‖A‖ ≤ R and 0 < R, then polynomial evaluation at A is bounded by the polynomial sup norm on closedBall 0 R.

theorem norm_aeval_mul_le_polynomialSupNorm_sq_of_auxiliary_eq_eval_zero_smul_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : 0 < R) (hA : ‖A‖ ≤ R) (p : Polynomial ℂ) (G : E →L[ℂ] E) (hG : G = star (Polynomial.eval 0 p) • 1) : ‖(Polynomial.aeval A) p * G‖ ≤ polynomialSupNorm p (Metric.closedBall 0 R) ^ 2

On a centered disk, the scalar auxiliary identification G = star (p.eval 0) • 1 implies the sharp L4.2e product estimate. The subsingleton branch makes the result valid for the zero Hilbert space, where the continuous-linear-map algebra does not have NormOneClass.

theorem norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball 0 R ⋯) p‖ ≤ polynomialSupNorm p (Metric.closedBall 0 R) ^ 2

Centered-disk L4.2e product bound. For ‖A‖ < R, the actual conjugate-polynomial auxiliary operator on ball 0 R satisfies the sharp product estimate.