The scalar Crouzeix--Palencia companion

For a polynomial p and a smooth Jordan domain Omega, the published Crouzeix--Palencia proof uses the scalar Cauchy companion

g(z) = (2πi)⁻¹ ∮∂Ω conj(p(σ)) / (σ - z) dσ.

This file defines that function using the project's parameterized contour integral and proves it is holomorphic throughout Omega.carrier. The proof differentiates under the interval integral. Around each interior point, an open ball remains disjoint from the compact parametrized frontier; this gives the uniform inverse-square bound required by the dominated derivative theorem.

The remaining sharp analytic input is not hidden here: extending the companion continuously to the boundary and proving its sup-norm contraction require a Plemelj boundary-value argument.

Main declarations

• crouzeixPolynomialScalarCompanion -- the scalar Cauchy companion.
• crouzeixPolynomialScalarCompanionDeriv -- its inverse-square derivative integral.
• crouzeixPolynomialScalarCompanion_smul -- the companion and its derivative are conjugate-homogeneous in the polynomial.
• crouzeixPolynomialScalarCompanion_eq_auxiliaryOperator_apply_one -- the companion is the scalarization of the one-dimensional auxiliary operator.
• norm_crouzeixPolynomialScalarCompanion_eq_norm_auxiliaryOperator -- this scalarization preserves the operator norm exactly.
• hasDerivAt_crouzeixPolynomialScalarCompanion_of_not_mem_frontier -- the exact derivative formula away from the boundary.
• analyticOn_crouzeixPolynomialScalarCompanion_frontier_compl -- the interior and exterior holomorphic branches.
• hasDerivAt_crouzeixPolynomialScalarCompanion and analyticOn_crouzeixPolynomialScalarCompanion -- their interior forms.

noncomputable def crouzeixPolynomialScalarCompanion (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (z : ℂ) : ℂ

The scalar Cauchy companion of p on a smooth Jordan domain.

Equations

• crouzeixPolynomialScalarCompanion Omega p z = (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (σ : ℂ) => star (Polynomial.eval σ p) * (σ - z)⁻¹) Omega.boundaryParam

noncomputable def crouzeixPolynomialScalarCompanionDeriv (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (z : ℂ) : ℂ

The scalar integral obtained by differentiating the Cauchy companion kernel with respect to its interior argument.

Equations

• One or more equations did not get rendered due to their size.

theorem crouzeixPolynomialScalarCompanion_smul (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) (z : ℂ) : crouzeixPolynomialScalarCompanion Omega (a • p) z = star a * crouzeixPolynomialScalarCompanion Omega p z

The scalar companion is conjugate-homogeneous in its polynomial argument.

@[simp]

theorem crouzeixPolynomialScalarCompanion_zero (Omega : SmoothJordanDomain) (z : ℂ) : crouzeixPolynomialScalarCompanion Omega 0 z = 0

The scalar companion of the zero polynomial vanishes identically.

theorem crouzeixPolynomialScalarCompanionDeriv_smul (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) (z : ℂ) : crouzeixPolynomialScalarCompanionDeriv Omega (a • p) z = star a * crouzeixPolynomialScalarCompanionDeriv Omega p z

The derivative integral of the scalar companion is likewise conjugate-homogeneous in the polynomial.

@[simp]

theorem crouzeixPolynomialScalarCompanionDeriv_zero (Omega : SmoothJordanDomain) (z : ℂ) : crouzeixPolynomialScalarCompanionDeriv Omega 0 z = 0

The derivative integral for the zero polynomial vanishes identically.

theorem crouzeixPolynomialScalarCompanion_eq_auxiliaryOperator_apply_one (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Omega.carrier) : crouzeixPolynomialScalarCompanion Omega p z = (crouzeixPolynomialAuxiliaryOperator (ContinuousLinearMap.toSpanSingleton ℂ z) Omega p) 1

At any interior point, the scalar Crouzeix companion is the value at 1 of the polynomial auxiliary operator for one-dimensional multiplication by that point. Thus the scalar analytic construction is exactly the one-dimensional scalarization of the operator contour construction, for an arbitrary smooth Jordan domain.

theorem norm_crouzeixPolynomialScalarCompanion_eq_norm_auxiliaryOperator (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Omega.carrier) : ‖crouzeixPolynomialScalarCompanion Omega p z‖ = ‖crouzeixPolynomialAuxiliaryOperator (ContinuousLinearMap.toSpanSingleton ℂ z) Omega p‖

Scalarization is isometric: the norm of the scalar companion at an interior point equals the operator norm of the corresponding one-dimensional polynomial auxiliary operator. Hence an auxiliary-operator estimate in the scalar model transfers to the analytic companion with no loss.

theorem hasDerivAt_crouzeixPolynomialScalarCompanion_of_not_mem_frontier (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} (hz : z ∉ frontier Omega.carrier) : HasDerivAt (crouzeixPolynomialScalarCompanion Omega p) (crouzeixPolynomialScalarCompanionDeriv Omega p z) z

At every point away from the smooth Jordan frontier, the scalar companion has the expected inverse-square Cauchy-kernel derivative. This simultaneously constructs its interior and exterior holomorphic branches.

theorem hasDerivAt_crouzeixPolynomialScalarCompanion (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Omega.carrier) : HasDerivAt (crouzeixPolynomialScalarCompanion Omega p) (crouzeixPolynomialScalarCompanionDeriv Omega p z) z

At every point in the smooth Jordan carrier, the scalar companion has the expected inverse-square Cauchy-kernel derivative.

theorem analyticOn_crouzeixPolynomialScalarCompanion_frontier_compl (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : AnalyticOn ℂ (crouzeixPolynomialScalarCompanion Omega p) (frontier Omega.carrier)ᶜ

The scalar companion is holomorphic on the complement of the smooth Jordan frontier, giving both its interior and exterior branches.

theorem analyticOn_crouzeixPolynomialScalarCompanion (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : AnalyticOn ℂ (crouzeixPolynomialScalarCompanion Omega p) Omega.carrier

The scalar Crouzeix--Palencia companion is holomorphic throughout the smooth Jordan carrier.