Polynomial Cauchy representation from resolvent mass

The all-polynomial operator Cauchy formula on a smooth contour follows algebraically from its constant-polynomial case. The resolvent splitting

p(A) R_A(z) = p(z) R_A(z) - (p / (X - z))(A)

leaves a divided-difference remainder which is polynomial in z. Its integral around any closed smooth parametrized boundary vanishes term by term. Thus a single normalized resolvent-mass identity supplies the full polynomial representation required by the Crouzeix--Palencia assembly.

Main declarations

• contourIntegral_aeval_divByMonic_X_sub_C_eq_zero -- the evaluated divided-difference remainder has zero closed-contour integral;
• polynomial_aeval_eq_normalized_contourIntegral_of_resolvent_mass -- resolvent mass implies the normalized polynomial operator Cauchy formula.

theorem contourIntegral_aeval_divByMonic_X_sub_C_eq_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : contourIntegral (fun (z : ℂ) => (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam = 0

The operator-valued divided difference z ↦ (p /ₘ (X - C z))(A) has zero integral around every smooth closed boundary. Coefficient expansion makes it a finite sum of nonnegative powers of z, each of which has a global polynomial primitive.

theorem polynomial_aeval_eq_normalized_contourIntegral_of_resolvent_mass {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hmass : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) (p : Polynomial ℂ) : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam

A single resolvent-mass identity implies the normalized operator Cauchy formula for every polynomial. No general-domain Cauchy theorem is needed for the polynomial remainder: it vanishes by an explicit primitive computation.