Algebraic support for the Crouzeix--Palencia product bound

This file proves the polynomial resolvent splitting used in L4.2e. Dividing p by X - z gives

p = C (p.eval z) + (X - C z) * (p /ₘ (X - C z)).

After evaluation at an operator and left multiplication by the resolvent, the second term collapses using R_A(z) (zI - A) = I. The result separates the scalar boundary value from a polynomial term, which is the algebraic input to the product estimate.

Main declaration

• resolvent_mul_aeval_eq_eval_mul_resolvent_sub_aeval_divByMonic -- the resolvent splitting identity.
• aeval_mul_resolvent_eq_eval_mul_resolvent_sub_aeval_divByMonic -- its right-oriented form, matching the product p(A) G in L4.2e.
• aeval_mul_smul_resolvent_eq_smul_eval_mul_resolvent_sub_aeval_divByMonic -- the scalar-boundary-weighted pointwise integrand identity.
• commute_aeval_resolvent -- polynomial evaluation commutes with the resolvent wherever it is defined.
• aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_contourIntegral -- pulls polynomial evaluation through the auxiliary contour integral.
• aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_split -- rewrites that contour integral using the pointwise resolvent splitting.
• commute_aeval_crouzeixPolynomialAuxiliaryOperator -- polynomial evaluation commutes with every polynomial auxiliary contour operator.
• crouzeixPolynomialAuxiliaryOperator_smul -- the auxiliary operator is conjugate-linear in its polynomial argument.
• polynomial_auxiliary_bounds_of_normalized -- transfers both sharp bounds from unit sup norm to every polynomial with positive sup norm.

theorem polynomialSupNorm_smul (a : ℂ) (p : Polynomial ℂ) (X : Set ℂ) : polynomialSupNorm (a • p) X = ‖a‖ * polynomialSupNorm p X

The polynomial sup norm is homogeneous under complex scalar multiplication.

theorem resolvent_mul_aeval_eq_eval_mul_resolvent_sub_aeval_divByMonic {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E →L[ℂ] E) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ resolventSet ℂ A) : resolvent A z * (Polynomial.aeval A) p = Polynomial.eval z p • resolvent A z - (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))

Splitting p by X - z inside the resolvent: for z in the resolvent set, R_A(z) p(A) = p(z) R_A(z) - (p /ₘ (X - z))(A).

theorem aeval_mul_resolvent_eq_eval_mul_resolvent_sub_aeval_divByMonic {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E →L[ℂ] E) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ resolventSet ℂ A) : (Polynomial.aeval A) p * resolvent A z = Polynomial.eval z p • resolvent A z - (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))

The right-oriented resolvent splitting used directly in p(A) G: p(A) R_A(z) = p(z) R_A(z) - (p /ₘ (X - z))(A).

theorem aeval_mul_smul_resolvent_eq_smul_eval_mul_resolvent_sub_aeval_divByMonic {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E →L[ℂ] E) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ resolventSet ℂ A) (h : ℂ) : (Polynomial.aeval A) p * h • resolvent A z = (h * Polynomial.eval z p) • resolvent A z - h • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))

The right-oriented splitting with a scalar boundary weight h, in the pointwise form used before applying contour-integral linearity in L4.2e.

theorem commute_aeval_resolvent {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E →L[ℂ] E) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ resolventSet ℂ A) : Commute ((Polynomial.aeval A) p) (resolvent A z)

Polynomial evaluation at A commutes with the resolvent of A.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_contourIntegral {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (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 : ℂ) => (Polynomial.aeval A) p * star (Polynomial.eval z p) • resolvent A z) Omega.boundaryParam

Polynomial evaluation at A pulls through the normalized auxiliary contour integral.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_eq_split {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (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 - star (Polynomial.eval z p) • (Polynomial.aeval A) (p /ₘ (Polynomial.X - Polynomial.C z))) Omega.boundaryParam

After pulling p(A) through the auxiliary contour integral, the pointwise resolvent splitting separates the squared boundary value from the polynomial divided-difference term.

theorem commute_aeval_crouzeixPolynomialAuxiliaryOperator {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (p q : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : Commute ((Polynomial.aeval A) p) (crouzeixPolynomialAuxiliaryOperator A Omega q)

Polynomial evaluation at A commutes with every polynomial auxiliary contour operator whose boundary lies in the resolvent set of A.

theorem crouzeixPolynomialAuxiliaryOperator_add {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (p q : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : crouzeixPolynomialAuxiliaryOperator A Omega (p + q) = crouzeixPolynomialAuxiliaryOperator A Omega p + crouzeixPolynomialAuxiliaryOperator A Omega q

On a contour contained in the resolvent set, the polynomial auxiliary operator is additive in its polynomial argument. Together with scalar homogeneity below, this records its conjugate-linear dependence on boundary polynomial data.

theorem crouzeixPolynomialAuxiliaryOperator_smul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A Omega (a • p) = star a • crouzeixPolynomialAuxiliaryOperator A Omega p

The polynomial auxiliary contour operator is conjugate-linear in its polynomial argument.

theorem aeval_add_star_crouzeixPolynomialAuxiliaryOperator_smul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : (Polynomial.aeval A) (a • p) + star (crouzeixPolynomialAuxiliaryOperator A Omega (a • p)) = a • ((Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p))

Scaling a polynomial scales the symmetrized auxiliary expression by the same complex scalar.

theorem aeval_mul_crouzeixPolynomialAuxiliaryOperator_smul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : (Polynomial.aeval A) (a • p) * crouzeixPolynomialAuxiliaryOperator A Omega (a • p) = (a * star a) • ((Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p)

Scaling a polynomial scales its product with the auxiliary operator by a * star a.

theorem norm_aeval_add_star_crouzeixPolynomialAuxiliaryOperator_smul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) (a • p) + star (crouzeixPolynomialAuxiliaryOperator A Omega (a • p))‖ = ‖a‖ * ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p)‖

The symmetrized auxiliary expression is homogeneous in norm.

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

The product with the auxiliary operator is homogeneous of degree two in norm.

theorem polynomial_auxiliary_bounds_of_normalized {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (K : Set ℂ) (p : Polynomial ℂ) (hm : 0 < polynomialSupNorm p K) (hnormalized : ∀ (q : Polynomial ℂ), polynomialSupNorm q K = 1 → ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A Omega q)‖ ≤ 2 ∧ ‖(Polynomial.aeval A) q * crouzeixPolynomialAuxiliaryOperator A Omega q‖ ≤ 1) : ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A Omega p)‖ ≤ 2 * polynomialSupNorm p K ∧ ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ polynomialSupNorm p K ^ 2

If both sharp auxiliary estimates hold for every polynomial of unit sup norm on K, then they hold with the correct homogeneous constants for every polynomial of positive sup norm. The zero-sup-norm case is deliberately left separate, since it requires geometric information about K.