Symmetrized polynomial auxiliary operator

The L4.2d estimate identifies p(A) + G† with a polynomial-weighted double-layer integral. This file proves that identification from the explicit Cauchy representation of p(A). The remaining analytic input is kept as a named hypothesis, so a circle or general contour Cauchy theorem can supply it without changing the algebraic interface.

Main declaration

• aeval_add_star_crouzeixPolynomialAuxiliaryOperator_eq_doubleLayerIntegral_of_cauchy -- the normalized symmetrized auxiliary operator is the polynomial-weighted integral of the resolvent double-layer kernel.

theorem aeval_add_star_crouzeixPolynomialAuxiliaryOperator_eq_doubleLayerIntegral_of_cauchy {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchy : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) : (Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p) = (2 * Real.pi)⁻¹ • ∫ (t : ℝ) in 0..2 * Real.pi, Polynomial.eval (Omega.boundaryParam t) p • ((-Complex.I * deriv Omega.boundaryParam t) • resolvent A (Omega.boundaryParam t) + ContinuousLinearMap.adjoint ((-Complex.I * deriv Omega.boundaryParam t) • resolvent A (Omega.boundaryParam t)))

Assuming the normalized contour Cauchy representation of p(A), the symmetrized operator p(A) + G† is (2π)⁻¹ times the integral of the boundary values of p against the double-layer resolvent kernel.