Affine-disk Crouzeix--Palencia inequality

This file transports the centered unit-disk Crouzeix--Palencia estimate to an arbitrary enclosing disk by the usual affine normalization.

Main declaration

• norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_closedBall_of_norm_sub_smul_one_lt -- the unconditional polynomial bound on an arbitrary open operator-norm disk.

theorem norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_closedBall_of_norm_sub_smul_one_lt {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‖ ≤ (1 + √2) * polynomialSupNorm p (Metric.closedBall c R)

Affine-disk Crouzeix--Palencia inequality. If A - cI has norm strictly less than R, polynomial evaluation at A is bounded by (1 + √2) times the polynomial sup-norm on closedBall c R.