The exterior resolvent Cauchy kernel

The scalar Cauchy kernel vanishes outside a closed convex carrier. Combining that fact with the two-parameter resolvent identity evaluates the nested operator kernel

(2 * pi * I)⁻¹ ∮ (sigma - z)⁻¹ R_A(z) dz = R_A(sigma).

This is the inner-contour calculation needed to identify the scalar companion functional calculus with the original conjugate-polynomial auxiliary contour.

theorem inv_sub_smul_resolvent_eq_resolvent_mul_resolvent_add {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {z sigma : ℂ} (hz : z ∈ resolventSet ℂ A) (hsigma : sigma ∈ resolventSet ℂ A) (hne : z ≠ sigma) : (sigma - z)⁻¹ • resolvent A z = resolvent A z * resolvent A sigma + (sigma - z)⁻¹ • resolvent A sigma

The two-parameter resolvent identity in the form adapted to the nested Cauchy kernel.

theorem contourIntegral_smul_const {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (f : ℂ → ℂ) (b : F) (gamma : ℝ → ℂ) : contourIntegral (fun (z : ℂ) => f z • b) gamma = contourIntegral f gamma • b

A fixed vector can be moved through a scalar-weighted contour integral.

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

Integrating the nested exterior Cauchy kernel against a resolvent contour returns the resolvent at the exterior point, with the unnormalized contour mass factor.

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

Normalized operator-valued Cauchy reproduction for an exterior resolvent point of a smooth convex carrier.

theorem contourIntegral_contourIntegral_swap {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → ℂ → F) (gamma delta : ℝ → ℂ) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => deriv gamma x.1 • deriv delta x.2 • f (gamma x.1) (delta x.2)) (Set.uIoc 0 (2 * Real.pi) ×ˢ Set.uIoc 0 (2 * Real.pi)) MeasureTheory.volume) : contourIntegral (fun (z : ℂ) => contourIntegral (f z) delta) gamma = contourIntegral (fun (w : ℂ) => contourIntegral (fun (z : ℂ) => f z w) gamma) delta

Fubini's theorem for two contour integrals, with the exact product integrability hypothesis on the derivative-weighted kernel.

theorem integrableOn_nested_scalarCompanion_resolvent_kernel {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega Psi : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hnest : closure Omega.carrier ⊆ Psi.carrier) : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => deriv Omega.boundaryParam x.1 • deriv Psi.boundaryParam x.2 • star (Polynomial.eval (Psi.boundaryParam x.2) p) • (2 * ↑Real.pi * Complex.I)⁻¹ • (Psi.boundaryParam x.2 - Omega.boundaryParam x.1)⁻¹ • resolvent A (Omega.boundaryParam x.1)) (Set.uIoc 0 (2 * Real.pi) ×ˢ Set.uIoc 0 (2 * Real.pi)) MeasureTheory.volume

For two nested smooth Jordan domains, the derivative-weighted scalar-companion/resolvent kernel is integrable on the parameter square.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_of_nested {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega Psi : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hmass : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) (hnest : closure Omega.carrier ⊆ Psi.carrier) : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Psi p) = crouzeixPolynomialAuxiliaryOperator A Psi p

If one smooth Jordan domain compactly contains another, applying the inner auxiliary calculus to the outer scalar companion reproduces the outer conjugate-polynomial auxiliary contour.