General smooth-domain symmetrized auxiliary bound

This file assembles the sharp L4.2d estimate on a smooth boundary once the three genuinely analytic/geometric inputs are available:

• the polynomial and resolvent Cauchy identities for the parametrized curve;
• the outward tangent-normal direction supports the numerical range; and
• the polynomial boundary values are uniformly bounded by M.

The proof derives all remaining facts from the landed infrastructure. The resolvent and polynomial kernels are interval integrable, the supporting half-plane condition makes the double-layer kernel positive, and the resolvent Cauchy identity gives total mass 4 * pi • 1. Positive-kernel contractivity then gives the factor 2.

The hypotheses are intentionally explicit: SmoothJordanDomain does not currently record an orientation/support condition, and no general-domain Cauchy or Plemelj theorem is hidden here.

Main declaration

• SmoothJordanDomain.isCompact_frontier -- the parametrized frontier is compact;
• norm_eval_boundaryParam_le_polynomialSupNorm_frontier -- boundary values are controlled by the polynomial sup norm on the frontier;
• exists_global_polynomial_calculus_bound_frontier_of_cauchy -- an all-polynomial Cauchy representation supplies a finite global calculus constant on the fixed smooth domain;
• norm_aeval_add_star_crouzeixPolynomialAuxiliaryOperator_le_two_mul_of_cauchy_support -- the generic smooth-domain L4.2d bound from Cauchy and support data.
• norm_aeval_add_star_auxiliary_le_two_mul_polynomialNorm_frontier_of_cauchy_support -- the same estimate with the canonical frontier sup norm.
• norm_aeval_add_star_auxiliary_le_two_mul_polynomialNorm_of_frontier_subset_of_cauchy_support -- control by any compact set containing the frontier.
• isPositive_aeval_crouzeixProductRemainderPolynomial_add_adjoint_of_cauchy_support -- the Hermitian product remainder is an integrated positive variance.
• re_inner_aeval_crouzeixProductRemainderPolynomial_nonneg_of_cauchy_support -- the corresponding accretive quadratic-form statement.

theorem SmoothJordanDomain.isCompact_frontier (Omega : SmoothJordanDomain) : IsCompact (frontier Omega.carrier)

The frontier of a smooth Jordan domain is compact: it is the range of a continuous function with nonzero period.

theorem norm_eval_boundaryParam_le_polynomialSupNorm_frontier (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (t : ℝ) : ‖Polynomial.eval (Omega.boundaryParam t) p‖ ≤ polynomialSupNorm p (frontier Omega.carrier)

Every value of a polynomial on the parametrized boundary is bounded by its polynomial sup norm on the domain frontier.

theorem exists_global_polynomial_calculus_bound_frontier_of_cauchy {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchy : ∀ (p : Polynomial ℂ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (p : Polynomial ℂ), ‖(Polynomial.aeval A) p‖ ≤ K * polynomialSupNorm p (frontier Omega.carrier)

An all-polynomial Cauchy representation on a fixed smooth domain gives a finite global polynomial-calculus constant relative to the frontier sup norm. The constant is obtained from the compact parameter-interval bound on the unweighted resolvent kernel, extracted by applying the existing auxiliary integrand bound to the constant polynomial 1.

theorem norm_aeval_add_star_crouzeixPolynomialAuxiliaryOperator_le_two_mul_of_cauchy_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {M : ℝ} (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchyP : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) (hCauchyOne : ∫ (t : ℝ) in 0..2 * Real.pi, deriv Omega.boundaryParam t • resolvent A (Omega.boundaryParam t) = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) (hM : 0 ≤ M) (hp : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ‖Polynomial.eval (Omega.boundaryParam t) p‖ ≤ M) : ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p)‖ ≤ 2 * M

Generic smooth-domain L4.2d bound. If the parametrized boundary satisfies the polynomial and resolvent Cauchy identities, its induced outward normal supports the numerical range pointwise, and ‖p‖ ≤ M on the boundary, then the polynomial auxiliary operator satisfies the sharp symmetrized bound ‖p(A) + G†‖ ≤ 2 * M.

theorem re_inner_crouzeixSquareAuxiliaryOperator_nonneg_of_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) (x : E) : 0 ≤ RCLike.re (inner ℂ x ((crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z p) * Polynomial.eval z p) x))

The scalar-square auxiliary operator has nonnegative quadratic real part whenever the outward normal of the contour supports the numerical range. This is the signed half of double-layer positivity needed by the product-remainder identity; it requires no triangle inequality and no Cauchy mass normalization.

theorem neg_re_inner_aeval_crouzeixProductRemainderPolynomial_le_re_inner_product {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) (x : E) : -RCLike.re (inner ℂ x (((Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)) x)) ≤ RCLike.re (inner ℂ x (((Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p) x))

In the exact product decomposition, double-layer positivity retains the sign of the cancellation: the real part of p(A) G_p is bounded below by minus the real part of the evaluated lower-degree remainder.

theorem isPositive_aeval_crouzeixProductRemainderPolynomial_add_adjoint_of_cauchy_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchyP : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) (hCauchyOne : ∫ (t : ℝ) in 0..2 * Real.pi, deriv Omega.boundaryParam t • resolvent A (Omega.boundaryParam t) = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) : ((Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p) + star ((Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p))).IsPositive

The Hermitian part of the product remainder is positive. More precisely, it is the normalized integral of the positive operator-valued variance (p(z) - p(A))† K(z) (p(z) - p(A)), where K is the double-layer kernel. This identity retains the coupling between the square auxiliary and the product term; it does not estimate either separately.

theorem re_inner_aeval_crouzeixProductRemainderPolynomial_nonneg_of_cauchy_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchyP : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) (hCauchyOne : ∫ (t : ℝ) in 0..2 * Real.pi, deriv Omega.boundaryParam t • resolvent A (Omega.boundaryParam t) = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) (x : E) : 0 ≤ RCLike.re (inner ℂ x (((Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)) x))

The evaluated product remainder is accretive: its quadratic real part is nonnegative on every vector. This is the scalar-form consequence of the positive integrated-variance identity above.

theorem norm_aeval_add_star_auxiliary_le_two_mul_polynomialNorm_frontier_of_cauchy_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchyP : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) (hCauchyOne : ∫ (t : ℝ) in 0..2 * Real.pi, deriv Omega.boundaryParam t • resolvent A (Omega.boundaryParam t) = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) : ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p)‖ ≤ 2 * polynomialSupNorm p (frontier Omega.carrier)

The generic smooth-domain symmetrized estimate with the canonical boundary constant. The Cauchy and outward-support inputs imply ‖p(A) + G†‖ ≤ 2 * sup_{z ∈ frontier Ω} ‖p(z)‖.

theorem norm_aeval_add_star_auxiliary_le_two_mul_polynomialNorm_of_frontier_subset_of_cauchy_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (L : Set ℂ) (hL : IsCompact L) (hfrontier : frontier Omega.carrier ⊆ L) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchyP : (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) Omega.boundaryParam) (hCauchyOne : ∫ (t : ℝ) in 0..2 * Real.pi, deriv Omega.boundaryParam t • resolvent A (Omega.boundaryParam t) = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (w - Omega.boundaryParam t)).re ≤ 0) : ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p)‖ ≤ 2 * polynomialSupNorm p L

If a compact set L contains the smooth frontier, the generic symmetrized estimate is controlled by the polynomial sup norm on L. This is the stagewise form consumed by compact-exhaustion arguments.