Regularized Plemelj reduction for the scalar companion #
At a prospective boundary point xi, split the scalar Cauchy companion as
C(h)(z) = h(xi) C(1)(z) + C(h - h(xi))(z).
The first term is just the normalized winding kernel. The second has a cancelled numerator and is the regularized transform carrying the genuinely singular boundary analysis. This file proves the split exactly and shows that, once the winding kernel is normalized to one in the carrier, convergence of the regularized transform gives the Plemelj limit, the canonical continuous extension, and the maximum-modulus reduction.
No convergence or sharp boundary estimate for the regularized transform is asserted here; those are the remaining analytic inputs.
Main declarations #
crouzeixScalarCauchyKernel-- the normalized scalar winding kernel.crouzeixPolynomialScalarCompanionRegularized-- the transform with its boundary datum cancelled atxi.crouzeixPolynomialScalarCompanionRegularized_add_C-- cancellation makes the regularized transform invariant under constant polynomial shifts.crouzeixPolynomialScalarCompanionRegularized_smul-- the regularized transform and boundary value are conjugate-homogeneous.contourIntegrable_crouzeixPolynomialScalarCompanionRegularized_self-- cancellation makes the boundary-point kernel genuinely integrable.crouzeixPolynomialScalarCompanion_eq_regularized_add-- the exact split away from the frontier.tendsto_crouzeixPolynomialScalarCompanion_of_regularized-- regularized convergence implies the actual Plemelj boundary limit.crouzeixPolynomialScalarCompanionClosedExtension_add_of_regularized-- the canonical closure construction preserves polynomial addition.norm_crouzeixPolynomialScalarCompanion_le_of_regularized_boundary-- the sharp interior reduction in terms of the explicit regularized values.
The normalized scalar Cauchy kernel of the parametrized frontier. For a
positively oriented Jordan curve it is 1 in the carrier and 0 outside the
closed domain.
Equations
- crouzeixScalarCauchyKernel Omega z = (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (sigma : ℂ) => (sigma - z)⁻¹) Omega.boundaryParam
Instances For
The scalar companion regularized at xi by subtracting the boundary
datum at xi from its numerator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The explicit prospective interior boundary value: the original datum at
xi plus the regularized transform evaluated at xi.
Equations
- crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi = star (Polynomial.eval xi p) + crouzeixPolynomialScalarCompanionRegularized Omega p xi xi
Instances For
Adding a constant polynomial does not change the cancelled regularized transform. Thus all singular boundary analysis may be normalized by subtracting the polynomial value at the selected boundary point.
The cancelled regularized transform is conjugate-homogeneous in the polynomial argument.
The regularized transform of the zero polynomial vanishes.
Regularized boundary convergence is preserved by polynomial scaling.
The canonical boundary-point normalization has zero value at xi.
Regularization is unchanged after replacing p by the canonical
polynomial p - C (p.eval xi) that vanishes at xi.
Regularized boundary convergence is equivalent for p and its
boundary-point normalization.
The Plemelj value splits into the conjugate boundary datum plus the
boundary value of the polynomial normalized to vanish at xi.
The explicit Plemelj boundary value is conjugate-affine under addition of a constant polynomial.
The explicit Plemelj boundary value is conjugate-homogeneous in the polynomial argument.
The explicit Plemelj boundary value for the zero polynomial vanishes.
Cancellation makes the regularized kernel contour-integrable at its own
base point, even when that point lies on the frontier. Polynomial division
factors the numerator by sigma - xi; after conjugation and multiplication
by its inverse, the remaining singular factor has norm one.
At the cancelled base point, the regularized transform is additive in the polynomial argument. The integrability needed for interval-integral additivity is supplied by the preceding cancellation theorem.
Away from the frontier, the regularized transform is additive in its polynomial argument.
Regularized Plemelj convergence is stable under polynomial addition.
The explicit Plemelj boundary value is additive in the polynomial argument.
Away from the frontier, the scalar companion is exactly the sum of its regularized transform and the boundary datum times the normalized winding kernel.
Away from the frontier, the full scalar companion is additive in its polynomial argument.
Away from the frontier, adding a constant polynomial shifts the full companion by the conjugate constant times the normalized winding kernel.
If the scalar winding kernel is normalized to one in the carrier, then
convergence of the cancelled transform at xi implies the actual Plemelj
limit there.
Frontierwise convergence of the regularized transforms makes the canonical closed companion extension continuous.
Under the regularized convergence hypotheses, the canonical extension takes the explicit regularized Plemelj value on the frontier.
Under winding normalization and regularized Plemelj convergence for two polynomials, the canonical closed companion extension preserves their sum on the whole closure.
Under winding normalization and regularized Plemelj convergence, the canonical closed companion extension is conjugate-homogeneous on the whole closure.
If the explicit regularized Plemelj values have norm at most C on the
frontier, the scalar companion has the same bound throughout the carrier.