Resolvent mass from the polynomial Cauchy representation #
The normalized operator-valued Cauchy representation for every polynomial
already contains the raw resolvent mass identity: specialize it to the
constant polynomial 1 and clear the nonzero scalar 2πi.
Main declaration #
contourIntegral_resolvent_eq_two_pi_I_smul_one_of_polynomial_cauchy-- derives the raw resolvent contour identity from polynomial Cauchy data.
theorem
contourIntegral_resolvent_eq_two_pi_I_smul_one_of_polynomial_cauchy
{E : Type u}
[NormedAddCommGroup E]
[InnerProductSpace ℂ E]
(A : E →L[ℂ] E)
(Omega : SmoothJordanDomain)
(hCauchyP :
∀ (p : Polynomial ℂ),
(Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam)
:
A normalized Cauchy representation valid for all polynomials implies the
raw resolvent contour mass identity by taking the constant polynomial 1.