The separated Crouzeix--Palencia product contour

The pointwise polynomial resolvent splitting in PalenciaSupport.lean writes the integrand for p(A) G as the difference of two terms. To estimate those terms separately, one first has to know that the divided-difference term depends continuously on the boundary point. This file proves that continuity directly from Mathlib's coefficient formula

coeff (p /ₘ (X - C z)) n = ∑ i, z ^ (i - n - 1) * coeff p i,

then proves contour integrability of both terms and separates the contour integral. The resulting identity is exact, but its two terms are not independently sharp: applying the triangle inequality loses the cancellation needed for the m² product constant. The separated form is therefore an algebraic diagnostic and a possible input to a stronger coupled invariant, not by itself a reduction to two attainable norm estimates.

Main declarations

• continuous_aeval_divByMonic_X_sub_C -- continuity of the evaluated polynomial divided difference in its boundary point.
• crouzeixProductMainIntegrand_contourIntegrable and crouzeixProductRemainderIntegrand_contourIntegrable -- integrability of the two separated product-contour terms.
• crouzeixProductRemainderPolynomial and normalized_crouzeixProductRemainderContour_eq_aeval -- the remainder contour is polynomial functional calculus of degree strictly below that of a nonconstant input polynomial.
• crouzeixProductRemainderPolynomial_smul -- degree-two homogeneity of the remainder, its evaluated norm, and its polynomial sup norm under scaling.
• crouzeixSquareAuxiliaryOperator_smul -- matching degree-two homogeneity of the scalar-square main auxiliary operator.
• aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_main_sub_remainder -- the exact separated contour identity for p(A) G.
• aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_main_sub_aeval_remainderPolynomial -- the same identity with the lower-degree remainder written as polynomial functional calculus.
• aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_squareAux_sub_aeval_remainderPolynomial -- the recursive form: a scalar-square auxiliary operator minus the lower-degree polynomial functional calculus.
• norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_le_main_add_remainder -- the corresponding two-term norm reduction.

theorem continuous_aeval_divByMonic_X_sub_C {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (p : Polynomial ℂ) : Continuous fun (z : ℂ) => (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))

The operator evaluation of the divided difference p /ₘ (X - C z) depends continuously on z.

This is not an immediate application of continuity of polynomial evaluation, because the polynomial itself varies with z. Expanding every coefficient of the quotient as a finite polynomial sum in z makes continuity explicit.

theorem continuous_coeff_divByMonic_X_sub_C (p : Polynomial ℂ) (n : ℕ) : Continuous fun (z : ℂ) => (p /ₘ (Polynomial.X - Polynomial.C z)).coeff n

Every coefficient of the polynomial divided difference depends continuously on its boundary point.

theorem contourIntegral_pow_eq_zero (Omega : SmoothJordanDomain) (n : ℕ) : contourIntegral (fun (z : ℂ) => z ^ n) Omega.boundaryParam = 0

Monomials have zero integral around a smooth closed boundary.

theorem contourIntegral_finset_sum_pow_mul_eq_zero (Omega : SmoothJordanDomain) (s : Finset ℕ) (k : ℕ → ℕ) (c : ℕ → ℂ) : contourIntegral (fun (z : ℂ) => ∑ j ∈ s, z ^ k j * c j) Omega.boundaryParam = 0

Finite linear combinations of monomials have zero closed-boundary integral.

theorem crouzeixProductMainIntegrand_contourIntegrable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : ContourIntegrable (fun (z : ℂ) => (star (Polynomial.eval z p) * Polynomial.eval z p) • resolvent A z) Omega.boundaryParam

The scalar-square resolvent term in the Crouzeix--Palencia product splitting is contour integrable on every smooth boundary containing the closed numerical range.

theorem crouzeixProductRemainderIntegrand_contourIntegrable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : ContourIntegrable (fun (z : ℂ) => star (Polynomial.eval z p) • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam

The polynomial divided-difference remainder in the Crouzeix--Palencia product splitting is contour integrable on every smooth boundary.

theorem contourIntegral_crouzeixProductRemainder_eq_sum {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : contourIntegral (fun (z : ℂ) => star (Polynomial.eval z p) • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam = ∑ i ∈ Finset.range p.natDegree, contourIntegral (fun (z : ℂ) => star (Polynomial.eval z p) * (p /ₘ (Polynomial.X - Polynomial.C z)).coeff i) Omega.boundaryParam • A ^ i

The divided-difference remainder contour is a finite sum of scalar contour coefficients multiplying powers of A.

noncomputable def crouzeixProductRemainderPolynomial (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : Polynomial ℂ

The polynomial whose functional calculus is the normalized divided-difference remainder contour.

Equations

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

theorem crouzeixProductRemainderPolynomial_add_C (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (a : ℂ) : crouzeixProductRemainderPolynomial Omega (p + Polynomial.C a) = crouzeixProductRemainderPolynomial Omega p

Adding a constant to p leaves its product-remainder polynomial unchanged. The divided difference does not see the constant, while the new cross term is the contour integral of a scalar polynomial and hence vanishes on the closed boundary.

theorem crouzeixProductRemainderPolynomial_smul (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : crouzeixProductRemainderPolynomial Omega (a • p) = (star a * a) • crouzeixProductRemainderPolynomial Omega p

Scaling p by a scales its product-remainder polynomial by star a * a.

theorem norm_aeval_crouzeixProductRemainderPolynomial_smul {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega (a • p))‖ = ‖a‖ ^ 2 * ‖(Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)‖

After evaluation at A, the remainder polynomial is homogeneous of degree two in norm.

theorem polynomialSupNorm_crouzeixProductRemainderPolynomial_smul (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) (K : Set ℂ) : polynomialSupNorm (crouzeixProductRemainderPolynomial Omega (a • p)) K = ‖a‖ ^ 2 * polynomialSupNorm (crouzeixProductRemainderPolynomial Omega p) K

The product-remainder polynomial has degree-two homogeneity in polynomial sup norm on every control set.

theorem natDegree_crouzeixProductRemainderPolynomial_smul (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) (ha : a ≠ 0) : (crouzeixProductRemainderPolynomial Omega (a • p)).natDegree = (crouzeixProductRemainderPolynomial Omega p).natDegree

Scaling by a nonzero scalar preserves the natural degree of the product-remainder polynomial.

theorem crouzeixAuxiliaryOperator_smul {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a : ℂ) (h : ℂ → ℂ) : (crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => a • h z) = a • crouzeixAuxiliaryOperator A Omega h

The auxiliary operator is complex-linear in its scalar boundary datum.

theorem crouzeixSquareAuxiliaryOperator_smul {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : (crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z (a • p)) * Polynomial.eval z (a • p)) = (star a * a) • crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z p) * Polynomial.eval z p

The scalar-square main auxiliary operator is homogeneous of degree two under polynomial scaling.

theorem norm_crouzeixSquareAuxiliaryOperator_smul {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : ‖crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z (a • p)) * Polynomial.eval z (a • p)‖ = ‖a‖ ^ 2 * ‖crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z p) * Polynomial.eval z p‖

The scalar-square main auxiliary operator has the corresponding degree-two norm homogeneity.

theorem natDegree_crouzeixProductRemainderPolynomial_lt (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hp : 0 < p.natDegree) : (crouzeixProductRemainderPolynomial Omega p).natDegree < p.natDegree

For a nonconstant p, its product-remainder polynomial has strictly smaller degree.

theorem crouzeixProductRemainderPolynomial_eq_zero_of_natDegree_eq_zero (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hp : p.natDegree = 0) : crouzeixProductRemainderPolynomial Omega p = 0

A constant polynomial has zero product-remainder polynomial.

theorem normalized_crouzeixProductRemainderContour_eq_aeval {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => star (Polynomial.eval z p) • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam = (Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)

The normalized divided-difference remainder contour is exactly the evaluation at A of crouzeixProductRemainderPolynomial.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_main_sub_remainder {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : (Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => (star (Polynomial.eval z p) * Polynomial.eval z p) • resolvent A z) Omega.boundaryParam - (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => star (Polynomial.eval z p) • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam

The product p(A) G is the normalized scalar-square resolvent contour minus the normalized polynomial divided-difference remainder contour.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_main_sub_aeval_remainderPolynomial {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : (Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => (star (Polynomial.eval z p) * Polynomial.eval z p) • resolvent A z) Omega.boundaryParam - (Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)

The product p(A) G is the scalar-square resolvent contour minus functional calculus of the explicitly constructed lower-degree remainder polynomial.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_squareAux_sub_aeval_remainderPolynomial {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : (Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p = (crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z p) * Polynomial.eval z p) - (Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)

The induction-ready product decomposition: p(A) G is the auxiliary operator associated to the scalar boundary datum |p|², minus functional calculus of a strictly lower-degree polynomial.

theorem norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_le_squareAux_add_remainder {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ ‖crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z p) * Polynomial.eval z p‖ + ‖(Polynomial.aeval A) (crouzeixProductRemainderPolynomial Omega p)‖

The recursive product decomposition reduces its norm to the norm of the scalar-square auxiliary operator plus the lower-degree functional calculus term.

theorem norm_aeval_mul_crouzeixPolynomialAuxiliaryOperator_le_main_add_remainder {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => (star (Polynomial.eval z p) * Polynomial.eval z p) • resolvent A z) Omega.boundaryParam‖ + ‖(2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => star (Polynomial.eval z p) • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam‖

The triangle-inequality consequence of the exact separated contour identity. This estimate is valid, but it does not retain the cancellation needed for the sharp m² product bound.