Constancy of the scalar Cauchy kernel on a convex carrier

For constant boundary data, the scalar Crouzeix companion is the normalized Cauchy winding kernel. Its derivative in the carrier is the contour integral of (sigma - z)⁻², which vanishes because this integrand has the global primitive -(sigma - z)⁻¹ along the boundary. The carrier is open and preconnected by strict convexity, so the zero-derivative theorem makes the kernel constant throughout it.

Consequently, the stagewise winding hypothesis in the scalar-companion route need only be checked at one point of each carrier.

Main declarations

• crouzeixPolynomialScalarCompanionDeriv_C_one_eq_zero_of_mem_carrier -- the constant-data companion has zero derivative in the carrier;
• crouzeixScalarCauchyKernel_eq_of_mem_carrier -- the scalar kernel has the same value at every two carrier points;
• crouzeixScalarCauchyKernel_eq_one_of_basepoint -- one normalized basepoint propagates winding normalization through the carrier.
• contourIntegral_inv_sub_eq_zero_of_not_mem_closure_carrier -- the scalar Cauchy contour vanishes at every exterior point;
• crouzeixScalarCauchyKernel_eq_zero_of_not_mem_closure_carrier -- the corresponding exterior winding normalization.

theorem crouzeixPolynomialScalarCompanionDeriv_C_one_eq_zero_of_mem_carrier (Omega : SmoothJordanDomain) {z : ℂ} (hz : z ∈ Omega.carrier) : crouzeixPolynomialScalarCompanionDeriv Omega (Polynomial.C 1) z = 0

The constant-data scalar companion has zero derivative at every carrier point. Its inverse-square derivative kernel has the explicit primitive -(sigma - z)⁻¹ as a function of the contour variable.

theorem crouzeixScalarCauchyKernel_eq_of_mem_carrier (Omega : SmoothJordanDomain) {z w : ℂ} (hz : z ∈ Omega.carrier) (hw : w ∈ Omega.carrier) : crouzeixScalarCauchyKernel Omega z = crouzeixScalarCauchyKernel Omega w

The normalized scalar Cauchy kernel is constant on the open strictly convex carrier.

theorem crouzeixScalarCauchyKernel_eq_one_of_basepoint (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hkc : crouzeixScalarCauchyKernel Omega c = 1) (z : ℂ) : z ∈ Omega.carrier → crouzeixScalarCauchyKernel Omega z = 1

Winding normalization at one point of the carrier propagates to every carrier point.

theorem contourIntegral_inv_sub_eq_zero_of_not_mem_closure_carrier (Omega : SmoothJordanDomain) {z : ℂ} (hz : z ∉ closure Omega.carrier) : contourIntegral (fun (sigma : ℂ) => (sigma - z)⁻¹) Omega.boundaryParam = 0

The scalar Cauchy contour vanishes at every point outside the closed convex carrier. Strict Hahn--Banach separation puts the entire boundary in one branch of the complex logarithm, which supplies a global primitive for the inverse kernel along the contour.

theorem crouzeixScalarCauchyKernel_eq_zero_of_not_mem_closure_carrier (Omega : SmoothJordanDomain) {z : ℂ} (hz : z ∉ closure Omega.carrier) : crouzeixScalarCauchyKernel Omega z = 0

The normalized scalar Cauchy kernel is zero throughout the exterior of the closed convex carrier.