Crouzeix--Palencia assembly over smooth Jordan exhaustions #
The analytic argument only needs an antitone compact exhaustion whose stages contain smooth Jordan frontiers; it does not need those carriers to equal a particular metric thickening. This module isolates that invariant interface, derives contour mass and winding from oriented numerical-range support, and packages scalar-companion approximation into the sharp exhaustion limit.
A uniformly convergent polynomial sequence has a subsequence with the
explicit error schedule 1, 1/2, 1/3, .... This converts the standard output
of a polynomial approximation theorem into the quantitative interface used by
the exhaustion assembly.
A strictly nested smooth Jordan exhaustion of a compact planar target. The closed stages are the compact control sets used by the Palencia limit; adjacent closure containment gives their antitonicity automatically.
Constructing this bundle for an arbitrary compact convex planar set is the remaining geometric smooth-approximation input to the terminal assembly.
- domain : ℕ → SmoothJordanDomain
The nested smooth Jordan domain at each stage of the exhaustion.
Instances For
Smooth realizations of the explicit open metric thickenings automatically form a strict nested smooth Jordan exhaustion. All closed-stage data comes from the corresponding compact thickenings; even target nonemptiness follows from nonemptiness of the represented smooth carrier.
Equations
- StrictNestedSmoothJordanExhaustion.ofConvexThickening K hcompact Omega hcarrier = { domain := Omega, target_subset := ⋯, isCompact_closure := ⋯, closure_succ_subset := ⋯, iInter_closure := ⋯ }
Instances For
Closed disks provide an unconditional model of the strict nested smooth
Jordan exhaustion: enlarge the radius by 1 / (n + 1) and use the standard
circle parametrization.
Equations
Instances For
The open carrier of a closed-disk exhaustion stage is its concentric radius-enlarged disk.
The boundary trace of a closed-disk exhaustion stage is its standard circle parametrization.
The derivative of a closed-disk exhaustion contour is the usual tangent to its standard circle parametrization.
The compact control set of a closed-disk exhaustion stage is its concentric radius-enlarged closed disk.
The frontier of a closed-disk exhaustion stage is its concentric metric sphere.
Multiplication of the disk-contour tangent by -I yields the radial
outward normal.
Every canonical closed scalar companion on a bundled smooth stage has the regularity required by complex polynomial approximation: it is continuous on the compact closure and complex differentiable in the carrier. Canonical orientation supplies winding one, while compactness supplies boundedness.
The complex polynomial approximation property needed at a smooth Jordan stage: every function continuous on the closure and complex differentiable in the carrier is a compact-uniform limit of complex polynomials. This is the Mergelyan conclusion specialized to the represented domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sharp Crouzeix--Palencia bound over an arbitrary antitone compact exhaustion, assuming the polynomial Cauchy formula and approximability of the stagewise auxiliary operators.
An oriented point in every smooth Jordan carrier supplies the resolvent mass, hence the polynomial Cauchy formula needed by the exhaustion theorem.
A point of the numerical range supplies the same oriented carrier point at every stage whose boundary normals support the numerical range.
The oriented support point determines the same resolvent mass on each carrier; the choice of point is irrelevant to the integral identity.
Supporting boundary normals give the polynomial Cauchy formula on every smooth carrier containing the closed numerical range.
Numerical-range support automatically supplies the oriented carrier point at every stage of a smooth Jordan exhaustion.
Full scalar-companion assembly over a realistic smooth Jordan exhaustion:
uniform polynomial approximation on each compact stage and the Plemelj
identification imply the sharp 1 + sqrt 2 spectral-set bound.
Constant-shift and scaling invariance reduce the scalar-companion inputs over a smooth Jordan exhaustion to positive-degree polynomials that vanish at zero; contour reproduction need only be checked after frontier normalization.
On a strictly nested smooth exhaustion, polynomial approximation of the closed scalar companions is enough: integration on the next inner contour automatically reproduces the polynomial auxiliary on the current contour.
Constant shifts reduce the approximation input in the strictly nested assembly to positive-degree polynomials vanishing at zero.
The canonical metric-thickening specialization of the strictly nested scalar-companion assembly. Identifying the smooth carriers with the explicit open thickenings automatically supplies their adjacent closure nesting, while the corresponding closed thickenings supply the compact antitone exhaustion.
Consequently no separate Plemelj identity, contour-mass identity, winding normalization, or exhaustion data is required. The remaining analytic input is uniform polynomial approximation of positive-degree closed companions that vanish at zero.
A one-point orientation specialization of the canonical thickening capstone. At each stage it is enough to exhibit one point of the smooth carrier whose canonical normal has the supporting sign at parameter zero. Strict convexity and continuity propagate that single sign to the whole trace and then to every point of the numerical range.
The canonical-orientation specialization removes the final geometric support premise from the metric-thickening capstone. Any supplied smooth realization is reoriented automatically; uniform approximation is required only for the resulting canonically oriented closed scalar companions.
Canonical orientation removes the numerical-range support premise from the general strictly nested smooth-exhaustion assembly as well. This version does not require the carriers to be particular metric thickenings: compact exhaustion, numerical-range containment, strict adjacent nesting, and uniform approximation of the canonically oriented closed companions suffice.
Standard compact-uniform polynomial convergence is sufficient for the canonically oriented nested-exhaustion capstone. A subsequence realizes the quantitative error schedule required by the preceding theorem.
Terminal bundled form of the verified Crouzeix--Palencia assembly. A
strictly nested smooth Jordan exhaustion of the closed numerical range and
compact-uniform polynomial approximation of its canonically oriented closed
scalar companions imply the exact 1 + sqrt 2 spectral-set bound.
Textbook terminal criterion: a strictly nested smooth exhaustion whose canonically oriented stages satisfy the Mergelyan polynomial approximation property yields the exact Crouzeix--Palencia bound. The regularity theorem above applies that property automatically to every closed scalar companion.
Textbook explicit-thickening criterion: if the explicit metric thickenings of the closed numerical range admit smooth Jordan realizations with the Mergelyan polynomial approximation property, then the exact Crouzeix--Palencia bound follows.