Crouzeix--Palencia assembly on smooth thickening domains

This file connects the concrete closed-thickening exhaustion to the sharp smooth-boundary symmetrized estimate. It shows that the full Crouzeix--Palencia conclusion follows if the open metric thickenings of the closed numerical range admit compatible smooth Jordan parametrizations with the polynomial Cauchy and support identities, and if the remaining product estimate holds at every stage. It also packages the published companion route: a uniformly sup-norm-contractive sequence of polynomials converging at the operator to the canonical auxiliary operator suffices. The resolvent Cauchy mass identity is the constant-polynomial specialization of the polynomial formula.

The hypotheses deliberately expose the remaining analytic gaps. No smoothness of an arbitrary metric-thickening frontier, general-domain Cauchy theorem, polynomial companion approximation, or product inequality is inferred from the set-theoretic approximation alone.

Main declaration

• crouzeix_palencia_of_convexThickening_cauchy_support_product -- exact Crouzeix--Palencia from compatible smooth thickening data and stagewise positive-degree product bounds.
• crouzeix_palencia_of_convexThickening_cauchy_support_tendsto_polynomial_companions -- exact Crouzeix--Palencia from the same smooth data and convergent polynomial companions.
• crouzeix_palencia_of_convexThickening_cauchy_support_approximate_polynomial_companions -- the natural additive-error polynomial-approximation interface.
• crouzeixPalencia_of_thickening_cauchy_support_contractive_companion_approximation -- the published-route interface in terms of contractive interior scalar companions, uniform polynomial approximation, and calculus identification.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_tendsto_polynomial_companions {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hcompanion : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (q : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (q j) (compactThickeningApprox (closure (numericalRange A)) n) ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n)) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds (crouzeixPolynomialAuxiliaryOperator A (Omega n) p))) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Suppose the open thickenings of the closed numerical range are realized by smooth Jordan domains whose parametrizations satisfy the polynomial Cauchy identity and whose outward normals support the numerical range. If the canonical Crouzeix auxiliary operator at every stage is the operator-norm limit of polynomials uniformly contractive for the corresponding closed-stage sup norm, then the exact Crouzeix--Palencia estimate follows.

The all-polynomial Cauchy formula supplies the finite stagewise calculus bound needed to run the fourth-power best-constant bootstrap.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_approximate_polynomial_companions {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hcompanion : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (r : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (r j) (compactThickeningApprox (closure (numericalRange A)) n) ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n) + 1 / (↑j + 1)) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (r j)) Filter.atTop (nhds (crouzeixPolynomialAuxiliaryOperator A (Omega n) p))) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The smooth-stage companion assembly only needs the natural additive-error form of uniform polynomial approximation. A sequence bounded by supNorm p + 1 / (j + 1) is asymptotically rescaled to an exactly contractive one before applying crouzeix_palencia_of_convexThickening_cauchy_support_tendsto_polynomial_companions.

In the nontrivial Hilbert-space case, every compact thickening is infinite. Thus a zero stage sup norm forces p = 0, and conjugate linearity makes the canonical auxiliary operator zero, discharging the necessary normalization edge case.

theorem crouzeixPalencia_of_thickening_cauchy_support_contractive_companion_approximation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hcompanion : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (g : ℂ → ℂ) (r : ℕ → Polynomial ℂ), (∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖g z‖ ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n)) ∧ (∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - g z‖ ≤ 1 / (↑j + 1)) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (r j)) Filter.atTop (nhds (crouzeixPolynomialAuxiliaryOperator A (Omega n) p))) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The published companion route in scalar analytic form. At every smooth stage, suppose an interior scalar companion g is bounded by the stage sup norm of p, is uniformly approximated there by polynomials r j with error 1 / (j + 1), and those polynomial evaluations converge at A to the canonical contour auxiliary. Then the exact Crouzeix--Palencia estimate follows.

This theorem leaves precisely the analytic companion contraction, polynomial approximation, and functional-calculus identification as explicit inputs; the additive-to-exact normalization and fourth-power bootstrap are internal.

theorem crouzeixPalencia_of_thickening_cauchy_support_continuous_companion_approximation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hcompanion : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (g : ℂ → ℂ) (r : ℕ → Polynomial ℂ), ContinuousOn g ((Omega n).boundaryParam '' Set.Icc 0 (2 * Real.pi)) ∧ (∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖g z‖ ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n)) ∧ (∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - g z‖ ≤ 1 / (↑j + 1)) ∧ crouzeixAuxiliaryOperator A (Omega n) g = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The published scalar-companion route with functional-calculus convergence derived rather than assumed. At every stage, a continuous boundary datum is contractive on the compact control set and uniformly approximated there by polynomials. The single remaining calculus input is the Plemelj identity saying that its normalized resolvent contour integral is the canonical conjugate-polynomial auxiliary.

The quantitative contour convergence theorem turns these data into the operator-limit premise of crouzeixPalencia_of_thickening_cauchy_support_contractive_companion_approximation.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_product {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hprod : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (Omega n) p‖ ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n) ^ 2) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Suppose the open thickenings of the closed numerical range are realized by smooth Jordan domains whose parametrizations satisfy the polynomial Cauchy identity and whose outward normals support the numerical range. If the associated auxiliary operators also satisfy the sharp product bound on the closed thickenings for positive-degree polynomials, then the exact Crouzeix--Palencia polynomial spectral-set estimate follows. Specializing the polynomial identity to C 1 supplies the resolvent mass identity and, through it, the degree-zero product case.