Universal symmetrization forces scalar-circle alignment

The off-center scalar-circle example shows that a sharp symmetrized estimate for one polynomial does not force the corresponding auxiliary product bound. The universal L4.2d family is genuinely stronger. For the scalar operator a • 1, applying it to X - C a forces the circle center to be a: the polynomial vanishes on the numerical range, while its circle auxiliary detects the center displacement. Once aligned, the normal-operator product theorem gives the literal L4.2e bound for every polynomial.

Main declarations

• circle_center_eq_scalar_of_forall_crouzeix_symmetrized_bound proves the alignment forced by universal fixed-control-set symmetrization.
• norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_smul_one_le_of_forall_symmetrized_bound derives the actual auxiliary product bound for every polynomial in this coupled scalar branch.

theorem circle_center_eq_scalar_of_forall_crouzeix_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (a c : ℂ) {R : ℝ} (hA : ‖a • 1 - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval (a • 1)) q + star (crouzeixPolynomialAuxiliaryOperator (a • 1) (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange (a • 1)))) : c = a

If the sharp fixed-control-set symmetrized bound holds for every polynomial at the scalar operator a • 1, an enclosing circle must be centered at a. Testing with X - C a detects any displacement.

theorem norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_smul_one_le_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (a c : ℂ) {R : ℝ} (hA : ‖a • 1 - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval (a • 1)) q + star (crouzeixPolynomialAuxiliaryOperator (a • 1) (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange (a • 1)))) (p : Polynomial ℂ) : ‖(Polynomial.aeval (a • 1)) p * crouzeixPolynomialAuxiliaryOperator (a • 1) (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p (closure (numericalRange (a • 1))) ^ 2

On a scalar operator, the universal sharp symmetrized family forces circle alignment and therefore implies the literal sharp auxiliary product bound for every polynomial.