Affine-disk support for the Crouzeix--Palencia product bound

Once the polynomial auxiliary operator on a circle centered at c is the scalar operator star (p(c)) • 1, the sharp L4.2e product estimate follows from von Neumann's inequality on that disk and the scalar sup-norm bound at its center.

Main declaration

• norm_aeval_mul_auxiliary_ball_le_of_auxiliary_eq_eval_center_smul_one -- the sharp product estimate on an arbitrary positive-radius disk from the explicit scalar auxiliary identity.
• norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_ball_center_le -- the unconditional arbitrary-center disk estimate under strict operator-norm enclosure.

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

On a disk centered at c, the scalar auxiliary identity G = star (p(c)) • 1 implies the sharp L4.2e product estimate.

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

Affine-disk L4.2e product bound. If ‖A - cI‖ < R, the actual polynomial auxiliary operator on ball c R satisfies the sharp squared sup-norm estimate.