The regularized Plemelj identity on a circle

This file discharges the regularized boundary-value inputs from ScalarCompanionPlemelj in the centered-disk model. If xi lies on the circle and

q = p /ₘ (X - C xi),

then polynomial division and the circle reflection identity turn the cancelled boundary integrand into a constant multiple of the scalar companion of q at zero. The landed circle calculation evaluates that companion exactly.

Main declarations

• crouzeixScalarCauchyKernel_ball_eq_one -- winding normalization inside a centered disk.
• crouzeixPolynomialScalarCompanionRegularized_ball_boundary_eq -- the exact cancelled boundary integral.
• tendsto_crouzeixPolynomialScalarCompanionRegularized_ball -- regularized convergence at every circle point.
• crouzeixPolynomialScalarCompanionBoundaryValue_ball_eq_eval_zero -- the explicit Plemelj value is the conjugate polynomial value at the center.
• crouzeixPolynomialScalarCompanionClosedExtension_ball_eq_eval_zero -- the canonical extension has that constant value on the closed disk.
• The corresponding declarations containing _ball_center_ give all of these results for an arbitrary disk center.
• crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_ball_center_eq -- the canonical scalar companion produces the polynomial auxiliary operator.
• exists_continuous_scalarCompanion_approximation_ball_center -- the full continuous, contractive, polynomially approximable companion data on a disk.
• exists_tendsto_polynomial_companions_ball_center -- an exactly contractive constant polynomial sequence converging to the auxiliary operator.

theorem crouzeixScalarCauchyKernel_ball_eq_one {R : ℝ} (hR : 0 < R) {z : ℂ} (hz : z ∈ Metric.ball 0 R) : crouzeixScalarCauchyKernel (SmoothJordanDomain.ball 0 R hR) z = 1

The normalized scalar Cauchy kernel of a positively oriented centered circle is one throughout its interior.

theorem crouzeixScalarCauchyKernel_ball_center_eq_one (c : ℂ) {R : ℝ} (hR : 0 < R) {z : ℂ} (hz : z ∈ Metric.ball c R) : crouzeixScalarCauchyKernel (SmoothJordanDomain.ball c R hR) z = 1

The normalized scalar Cauchy kernel is one throughout the interior of an arbitrarily centered positively oriented circle.

theorem crouzeixPolynomialScalarCompanionRegularized_ball_center_boundary_eq (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ Metric.sphere c R) : crouzeixPolynomialScalarCompanionRegularized (SmoothJordanDomain.ball c R hR) p xi xi = star (Polynomial.eval c p) - star (Polynomial.eval xi p)

On an arbitrary circle, the cancelled transform at a boundary point is the difference between the conjugate polynomial values at the center and at that boundary point.

theorem crouzeixPolynomialScalarCompanionRegularized_ball_boundary_eq {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ Metric.sphere 0 R) : crouzeixPolynomialScalarCompanionRegularized (SmoothJordanDomain.ball 0 R hR) p xi xi = star (Polynomial.eval 0 p) - star (Polynomial.eval xi p)

On a centered circle, the cancelled transform evaluated at its boundary point is exactly the difference between the conjugate center and boundary values of the polynomial.

theorem tendsto_crouzeixPolynomialScalarCompanionRegularized_ball {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ Metric.sphere 0 R) : Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized (SmoothJordanDomain.ball 0 R hR) p xi) (nhdsWithin xi (Metric.ball 0 R)) (nhds (crouzeixPolynomialScalarCompanionRegularized (SmoothJordanDomain.ball 0 R hR) p xi xi))

On a centered disk, the regularized transform converges at every frontier point to its explicitly evaluated boundary integral.

theorem crouzeixPolynomialScalarCompanionBoundaryValue_ball_eq_eval_zero {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ Metric.sphere 0 R) : crouzeixPolynomialScalarCompanionBoundaryValue (SmoothJordanDomain.ball 0 R hR) p xi = star (Polynomial.eval 0 p)

The explicit regularized Plemelj value on a centered circle is the conjugate polynomial value at the disk center.

theorem continuousOn_crouzeixPolynomialScalarCompanionClosedExtension_ball {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) : ContinuousOn (crouzeixPolynomialScalarCompanionClosedExtension (SmoothJordanDomain.ball 0 R hR) p) (Metric.closedBall 0 R)

The canonical scalar-companion extension is continuous on the closed centered disk, now obtained through the regularized Plemelj interface.

theorem crouzeixPolynomialScalarCompanionClosedExtension_ball_eq_eval_zero {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Metric.closedBall 0 R) : crouzeixPolynomialScalarCompanionClosedExtension (SmoothJordanDomain.ball 0 R hR) p z = star (Polynomial.eval 0 p)

The canonical closed extension of the centered-disk companion is the constant star (p.eval 0) on the entire closed disk.

theorem tendsto_crouzeixPolynomialScalarCompanionRegularized_ball_center (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ Metric.sphere c R) : Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized (SmoothJordanDomain.ball c R hR) p xi) (nhdsWithin xi (Metric.ball c R)) (nhds (crouzeixPolynomialScalarCompanionRegularized (SmoothJordanDomain.ball c R hR) p xi xi))

The regularized transform converges at every boundary point of an arbitrarily centered disk.

theorem crouzeixPolynomialScalarCompanionBoundaryValue_ball_center_eq_eval_center (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ Metric.sphere c R) : crouzeixPolynomialScalarCompanionBoundaryValue (SmoothJordanDomain.ball c R hR) p xi = star (Polynomial.eval c p)

The explicit Plemelj value on an arbitrary circle is the conjugate polynomial value at its center.

theorem continuousOn_crouzeixPolynomialScalarCompanionClosedExtension_ball_center (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) : ContinuousOn (crouzeixPolynomialScalarCompanionClosedExtension (SmoothJordanDomain.ball c R hR) p) (Metric.closedBall c R)

The canonical scalar-companion extension is continuous on every closed disk.

theorem crouzeixPolynomialScalarCompanionClosedExtension_ball_center_eq_eval_center (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ Metric.closedBall c R) : crouzeixPolynomialScalarCompanionClosedExtension (SmoothJordanDomain.ball c R hR) p z = star (Polynomial.eval c p)

The canonical closed extension of the companion on ball c R is the constant star (p.eval c) throughout closedBall c R.

theorem crouzeixAuxiliaryOperator_scalarCompanionClosedExtension_ball_center_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (hA : ‖A - c • 1‖ < R) (p : Polynomial ℂ) : crouzeixAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) (crouzeixPolynomialScalarCompanionClosedExtension (SmoothJordanDomain.ball c R hR) p) = crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) p

On a disk containing the operator in norm, feeding the canonical closed scalar companion to the auxiliary contour gives exactly the usual conjugate-polynomial auxiliary operator.

theorem exists_continuous_scalarCompanion_approximation_ball_center {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (hA : ‖A - c • 1‖ < R) (p : Polynomial ℂ) : ∃ (g : ℂ → ℂ) (r : ℕ → Polynomial ℂ), ContinuousOn g ((SmoothJordanDomain.ball c R hR).boundaryParam '' Set.Icc 0 (2 * Real.pi)) ∧ (∀ z ∈ Metric.closedBall c R, ‖g z‖ ≤ polynomialSupNorm p (Metric.closedBall c R)) ∧ (∀ (j : ℕ), ∀ z ∈ Metric.closedBall c R, ‖Polynomial.eval z (r j) - g z‖ ≤ 1 / (↑j + 1)) ∧ crouzeixAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) g = crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) p

The disk model supplies all scalar-companion inputs used by the published approximation route at once. The canonical closed extension is continuous on the boundary and sharply contractive on the closed disk; the constant polynomial sequence agrees with it exactly, and its auxiliary contour is the conjugate-polynomial auxiliary operator.

theorem aeval_C_star_eval_center_eq_crouzeixPolynomialAuxiliaryOperator_ball_center {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (hA : ‖A - c • 1‖ < R) (p : Polynomial ℂ) : (Polynomial.aeval A) (Polynomial.C (star (Polynomial.eval c p))) = crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) p

The constant polynomial representing the closed disk companion evaluates at A to the conjugate-polynomial auxiliary operator. This is the exact functional-calculus identification behind the disk instance of the published companion route.

theorem exists_tendsto_polynomial_companions_ball_center {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (hA : ‖A - c • 1‖ < R) (p : Polynomial ℂ) : ∃ (q : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (q j) (Metric.closedBall c R) ≤ polynomialSupNorm p (Metric.closedBall c R)) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) p))

On an enclosing disk, the polynomial companions required by the published approximation route can be chosen to be a constant sequence. It is exactly contractive for the closed-disk sup norm and its evaluations at A converge (indeed, are equal) to the canonical auxiliary operator.