Quantitative bounds for the regularized Plemelj value

Polynomial division by X - C xi factors the cancelled boundary numerator. Consequently, the apparent singular phase in the regularized self-value has unit norm, and a bound on the speed of the boundary parametrization gives an explicit estimate in terms of the frontier sup norm of the divided-difference polynomial.

This is not the final sharp companion contraction: it isolates the additional divided-difference term that a sharp boundary argument must control.

Main declarations

• norm_crouzeixPolynomialScalarCompanionRegularized_self_le -- the explicit bound for a chosen boundary-speed constant.
• crouzeixPolynomialScalarCompanionRegularized_self_eq_divByMonic -- the exact lower-degree phase-weighted contour representation.
• crouzeixPolynomialBoundaryPhaseTransform -- the named lower-degree phase contour carrying the remaining sharp frontier estimate.
• crouzeixPolynomialBoundaryPhaseTransform_add and _smul -- its conjugate-linear polynomial API.
• norm_crouzeixPolynomialBoundaryPhaseTransform_le -- its explicit domain-speed norm bound.
• exists_uniform_norm_crouzeixPolynomialScalarCompanionRegularized_self_le -- one domain-only constant works for all polynomials and base points.
• norm_crouzeixPolynomialScalarCompanionBoundaryValue_le -- the resulting quantitative bound for the explicit Plemelj boundary value.

noncomputable def crouzeixPolynomialBoundaryPhaseTransform (Omega : SmoothJordanDomain) (xi : ℂ) (q : Polynomial ℂ) : ℂ

The phase-weighted conjugate Cauchy contour at a prospective boundary point. In the Plemelj recursion its polynomial argument is the strictly lower-degree quotient p /ₘ (X - C xi).

Equations

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

theorem natDegree_divByMonic_X_sub_C_eq_sub_one (p : Polynomial ℂ) (xi : ℂ) : (p /ₘ (Polynomial.X - Polynomial.C xi)).natDegree = p.natDegree - 1

The polynomial divided difference used at xi has degree exactly one less, truncated at zero.

theorem natDegree_divByMonic_X_sub_C_lt (p : Polynomial ℂ) (xi : ℂ) (hp : 0 < p.natDegree) : (p /ₘ (Polynomial.X - Polynomial.C xi)).natDegree < p.natDegree

For a positive-degree polynomial, the divided difference has strictly smaller natural degree.

theorem crouzeixPolynomialScalarCompanionRegularized_self_eq_divByMonic (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (xi : ℂ) : crouzeixPolynomialScalarCompanionRegularized Omega p xi xi = (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (sigma : ℂ) => star (sigma - xi) * star (Polynomial.eval sigma (p /ₘ (Polynomial.X - Polynomial.C xi))) * (sigma - xi)⁻¹) Omega.boundaryParam

The regularized self-value is exactly a phase-weighted contour of the strictly lower-degree divided difference. The factor star (sigma - xi) * (sigma - xi)⁻¹ has norm one away from its removable zero.

theorem crouzeixPolynomialScalarCompanionBoundaryValue_eq_divByMonic (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (xi : ℂ) : crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi = star (Polynomial.eval xi p) + (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (sigma : ℂ) => star (sigma - xi) * star (Polynomial.eval sigma (p /ₘ (Polynomial.X - Polynomial.C xi))) * (sigma - xi)⁻¹) Omega.boundaryParam

The explicit Plemelj boundary value consists of the conjugate boundary datum and the phase-weighted contour of a lower-degree polynomial.

theorem crouzeixPolynomialScalarCompanionRegularized_self_eq_boundaryPhaseTransform (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (xi : ℂ) : crouzeixPolynomialScalarCompanionRegularized Omega p xi xi = crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))

The regularized self-value is the named boundary phase transform of the divided difference.

theorem crouzeixPolynomialScalarCompanionBoundaryValue_eq_boundaryPhaseTransform (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (xi : ℂ) : crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi = star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))

The explicit Plemelj boundary value is the conjugate point value plus the lower-degree boundary phase transform.

theorem crouzeixPolynomialBoundaryPhaseTransform_eq_regularized_mul (Omega : SmoothJordanDomain) (xi : ℂ) (q : Polynomial ℂ) : crouzeixPolynomialBoundaryPhaseTransform Omega xi q = crouzeixPolynomialScalarCompanionRegularized Omega ((Polynomial.X - Polynomial.C xi) * q) xi xi

The phase transform of q is itself the regularized self-value of the polynomial (X - C xi) * q. This realizes the lower-degree contour as the same cancelled Cauchy construction already used by the Plemelj split.

theorem contourIntegrable_crouzeixPolynomialBoundaryPhaseTransform (Omega : SmoothJordanDomain) (xi : ℂ) (q : Polynomial ℂ) : ContourIntegrable (fun (sigma : ℂ) => star (sigma - xi) * star (Polynomial.eval sigma q) * (sigma - xi)⁻¹) Omega.boundaryParam

The phase-weighted contour is genuinely integrable, including at its base point on the trace.

theorem crouzeixPolynomialBoundaryPhaseTransform_add (Omega : SmoothJordanDomain) (xi : ℂ) (p q : Polynomial ℂ) : crouzeixPolynomialBoundaryPhaseTransform Omega xi (p + q) = crouzeixPolynomialBoundaryPhaseTransform Omega xi p + crouzeixPolynomialBoundaryPhaseTransform Omega xi q

The boundary phase transform is additive in its polynomial argument.

theorem crouzeixPolynomialBoundaryPhaseTransform_smul (Omega : SmoothJordanDomain) (xi a : ℂ) (q : Polynomial ℂ) : crouzeixPolynomialBoundaryPhaseTransform Omega xi (a • q) = star a * crouzeixPolynomialBoundaryPhaseTransform Omega xi q

The boundary phase transform is conjugate-homogeneous in its polynomial argument.

@[simp]

theorem crouzeixPolynomialBoundaryPhaseTransform_zero (Omega : SmoothJordanDomain) (xi : ℂ) : crouzeixPolynomialBoundaryPhaseTransform Omega xi 0 = 0

The boundary phase transform of the zero polynomial vanishes.

theorem norm_eval_add_crouzeixPolynomialBoundaryPhaseTransform_le_of_natDegree_eq_zero (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hp : p.natDegree = 0) (xi : ℂ) : ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier Omega.carrier)

Degree-zero polynomials satisfy the sharp boundary-phase inequality automatically: their divided difference and hence their phase transform vanish. This is the base case for any induction through the lower-degree phase contour.

theorem norm_crouzeixPolynomialScalarCompanion_le_of_boundaryPhaseTransform (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hbounded : Bornology.IsBounded Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) (hreg : ∀ xi ∈ frontier Omega.carrier, Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized Omega p xi) (nhdsWithin xi Omega.carrier) (nhds (crouzeixPolynomialScalarCompanionRegularized Omega p xi xi))) (hphase : ∀ xi ∈ frontier Omega.carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier Omega.carrier)) {z : ℂ} (hz : z ∈ Omega.carrier) : ‖crouzeixPolynomialScalarCompanion Omega p z‖ ≤ polynomialSupNorm p (frontier Omega.carrier)

The exact remaining sharp frontier inequality for the lower-degree phase transform implies the sharp scalar-companion contraction in the carrier.

theorem norm_crouzeixPolynomialScalarCompanionClosedExtension_le_of_boundaryPhaseTransform (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hbounded : Bornology.IsBounded Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) (hreg : ∀ xi ∈ frontier Omega.carrier, Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized Omega p xi) (nhdsWithin xi Omega.carrier) (nhds (crouzeixPolynomialScalarCompanionRegularized Omega p xi xi))) (hphase : ∀ xi ∈ frontier Omega.carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier Omega.carrier)) {z : ℂ} (hz : z ∈ closure Omega.carrier) : ‖crouzeixPolynomialScalarCompanionClosedExtension Omega p z‖ ≤ polynomialSupNorm p (frontier Omega.carrier)

Under the same sharp phase inequality, the canonical Plemelj extension is contractive on the entire closed domain.

theorem norm_crouzeixPolynomialScalarCompanionRegularized_self_le (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (xi : ℂ) {D : ℝ} (hD_nonneg : 0 ≤ D) (hD : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t‖ ≤ D) : ‖crouzeixPolynomialScalarCompanionRegularized Omega p xi xi‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm (p /ₘ (Polynomial.X - Polynomial.C xi)) (frontier Omega.carrier)))

A boundary-speed bound controls the regularized self-value by the frontier sup norm of the divided-difference polynomial.

theorem norm_crouzeixPolynomialBoundaryPhaseTransform_le (Omega : SmoothJordanDomain) (xi : ℂ) (q : Polynomial ℂ) {D : ℝ} (hD_nonneg : 0 ≤ D) (hD : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t‖ ≤ D) : ‖crouzeixPolynomialBoundaryPhaseTransform Omega xi q‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm q (frontier Omega.carrier)))

A boundary-speed bound controls the named phase transform directly by the frontier sup norm of its polynomial argument.

theorem exists_uniform_norm_crouzeixPolynomialScalarCompanionRegularized_self_le (Omega : SmoothJordanDomain) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (p : Polynomial ℂ) (xi : ℂ), ‖crouzeixPolynomialScalarCompanionRegularized Omega p xi xi‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm (p /ₘ (Polynomial.X - Polynomial.C xi)) (frontier Omega.carrier)))

One nonnegative constant depending only on the smooth Jordan domain controls every regularized self-value.

theorem exists_uniform_norm_crouzeixPolynomialBoundaryPhaseTransform_le (Omega : SmoothJordanDomain) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (xi : ℂ) (q : Polynomial ℂ), ‖crouzeixPolynomialBoundaryPhaseTransform Omega xi q‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm q (frontier Omega.carrier)))

One nonnegative domain-only speed constant controls every boundary phase transform, uniformly in its base point and polynomial argument.

theorem norm_crouzeixPolynomialScalarCompanionBoundaryValue_le (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ frontier Omega.carrier) {D : ℝ} (hD_nonneg : 0 ≤ D) (hD : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t‖ ≤ D) : ‖crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi‖ ≤ polynomialSupNorm p (frontier Omega.carrier) + ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm (p /ₘ (Polynomial.X - Polynomial.C xi)) (frontier Omega.carrier)))

At a frontier point, the explicit Plemelj value is bounded by the polynomial frontier sup norm plus the divided-difference remainder bound.

theorem exists_uniform_norm_crouzeixPolynomialScalarCompanionBoundaryValue_le (Omega : SmoothJordanDomain) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (p : Polynomial ℂ), ∀ xi ∈ frontier Omega.carrier, ‖crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi‖ ≤ polynomialSupNorm p (frontier Omega.carrier) + ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm (p /ₘ (Polynomial.X - Polynomial.C xi)) (frontier Omega.carrier)))

A single domain-only speed constant gives the preceding boundary-value bound for every polynomial and every frontier point.