Normalize the Crouzeix product estimate #
On an infinite compact control set, a positive-degree polynomial has positive sup norm. Exact degree-two homogeneity therefore reduces the remaining Crouzeix--Palencia product estimate to polynomials of unit sup norm.
Main declaration #
norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_le_of_normalized-- transfers the unit-sup-norm product estimate to every positive-degree polynomial.
theorem
norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_le_of_normalized
{E : Type u}
[NormedAddCommGroup E]
[InnerProductSpace ℂ E]
(A : E →L[ℂ] E)
(Omega : SmoothJordanDomain)
(K : Set ℂ)
(hK : IsCompact K)
(hKinf : K.Infinite)
(p : Polynomial ℂ)
(hp : 0 < p.natDegree)
(hnormalized :
∀ (q : Polynomial ℂ),
0 < q.natDegree →
polynomialSupNorm q K = 1 → ‖(Polynomial.aeval A) q * crouzeixPolynomialAuxiliaryOperator A Omega q‖ ≤ 1)
:
‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ polynomialSupNorm p K ^ 2
On an infinite compact set, it suffices to prove the sharp product bound for positive-degree polynomials of unit sup norm.