Constant-polynomial base case for the auxiliary product bound

The recursive product decomposition in ProductContour.lean lowers the degree of its polynomial remainder. This file supplies the corresponding degree-zero base case on an arbitrary smooth contour satisfying the raw resolvent Cauchy identity.

For p = C a, the conjugate-polynomial auxiliary operator is star a • 1. Hence p(A) G has norm ‖a‖², which is exactly the square of the polynomial sup norm on every nonempty set.

Main declarations

• polynomialSupNorm_C_of_nonempty -- the sup norm of a constant polynomial.
• normalized_contourIntegral_resolvent_eq_one_of_cauchy -- normalization of the raw resolvent Cauchy mass identity.
• crouzeixPolynomialAuxiliaryOperator_C_eq_star_smul_one -- the auxiliary operator for a constant polynomial.
• norm_aeval_mul_auxiliary_le_polynomialNorm_sq_of_natDegree_eq_zero -- the sharp L4.2e base case.

theorem polynomialSupNorm_C_of_nonempty (a : ℂ) {K : Set ℂ} (hK : K.Nonempty) : polynomialSupNorm (Polynomial.C a) K = ‖a‖

The polynomial sup norm of C a on a nonempty set is ‖a‖.

theorem normalized_contourIntegral_resolvent_eq_one_of_cauchy {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hCauchy : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) : (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (resolvent A) Omega.boundaryParam = 1

A raw smooth-contour resolvent Cauchy identity becomes the identity operator after multiplication by (2πi)⁻¹.

theorem crouzeixPolynomialAuxiliaryOperator_C_eq_star_smul_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a : ℂ) (hCauchy : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) : crouzeixPolynomialAuxiliaryOperator A Omega (Polynomial.C a) = star a • 1

On a contour satisfying the resolvent Cauchy identity, the auxiliary operator for C a is star a • 1.

theorem crouzeixPolynomialAuxiliaryOperator_add_C {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (a : ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchy : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) : crouzeixPolynomialAuxiliaryOperator A Omega (p + Polynomial.C a) = crouzeixPolynomialAuxiliaryOperator A Omega p + star a • 1

Adding a constant to a polynomial adds the conjugate scalar identity to its auxiliary operator. This is the operator counterpart of the exact constant-shift invariance of the product remainder.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_add_C {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (a : ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchy : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) : (Polynomial.aeval A) (p + Polynomial.C a) * crouzeixPolynomialAuxiliaryOperator A Omega (p + Polynomial.C a) = (Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p + star a • (Polynomial.aeval A) p + a • crouzeixPolynomialAuxiliaryOperator A Omega p + (a * star a) • 1

Exact constant-shift expansion of the auxiliary product. All four terms are retained, so a later quadratic-form argument may choose the centering scalar without discarding cancellation.

theorem norm_aeval_mul_auxiliary_le_polynomialNorm_sq_of_natDegree_eq_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {K : Set ℂ} (hK : K.Nonempty) (hp : p.natDegree = 0) (hCauchy : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ polynomialSupNorm p K ^ 2

Sharp L4.2e base case. A degree-zero polynomial satisfies the auxiliary product bound on every nonempty control set, provided the smooth contour has the resolvent Cauchy mass identity.