Affine disk normalization

This file transports the unit-disk form of von Neumann's inequality to an arbitrary closed disk. The operator is normalized to R⁻¹ • (A - c • 1), while the polynomial is precomposed with z ↦ R * z + c.

Main declarations

• polynomialSupNorm_affineComposition_closedBall — affine transport of the sup-norm;
• closure_numericalRange_subset_closedBall_of_norm_sub_smul_one_le — the centered operator-norm bound encloses the numerical range;
• norm_aeval_le_polynomialSupNorm_closedBall_of_norm_sub_smul_one_le — von Neumann's inequality on an arbitrary disk;
• isPolynomialSpectralSet_closedBall_of_norm_sub_smul_one_le — the corresponding spectral-set package.

theorem polynomialSupNorm_affineComposition_closedBall (p : Polynomial ℂ) (c : ℂ) {R : ℝ} (hR : 0 ≤ R) : polynomialSupNorm (p.affineComposition (↑R) c) (Metric.closedBall 0 1) = polynomialSupNorm p (Metric.closedBall c R)

Precomposing with z ↦ R * z + c transports the polynomial sup-norm from the unit closed disk to closedBall c R.

theorem closure_numericalRange_subset_closedBall_of_norm_sub_smul_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ ≤ R) : closure (numericalRange A) ⊆ Metric.closedBall c R

If A - cI has norm at most R, then the closure of the numerical range of A lies in the closed disk with center c and radius R.

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

Von Neumann's inequality on a closed disk: if ‖A - cI‖ ≤ R and R > 0, then evaluation at A is bounded by the polynomial sup-norm on closedBall c R.

theorem isPolynomialSpectralSet_closedBall_of_norm_sub_smul_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (hA : ‖A - c • 1‖ ≤ R) : IsPolynomialSpectralSet A (Metric.closedBall c R)

A disk containing A in the centered operator-norm sense is a polynomial spectral set for A, with sharp constant 1.