The Crouzeix--Palencia auxiliary operator (L4.2c)

This file supplies the kernel-checked contour-integral part of the auxiliary operator construction. If a smooth Jordan domain Omega strictly contains closure (numericalRange A), every point of its boundary lies in the resolvent set of A. Consequently, any continuous scalar boundary datum h gives an integrable operator-valued kernel z ↦ h z • resolvent A z and hence the bounded operator

G = (2 * pi * i)⁻¹ • contourIntegral (h • resolvent A) Omega.boundaryParam.

The sharp L4.2d/e estimates are intentionally not asserted here: they require identifying the resulting contour expressions through boundary Cauchy-transform identities. Mathlib has no located Plemelj boundary-value theorem from which those identities follow directly.

Main declarations

• SmoothJordanDomain.boundaryParam_mem_resolventSet -- the boundary of a domain containing closure (numericalRange A) lies in the resolvent set.
• exists_smoothJordanDomain_for_numericalRange -- such a containing smooth Jordan domain exists for every bounded operator.
• crouzeixAuxiliaryIntegrand_contourIntegrable -- continuity of the scalar boundary datum implies integrability of the operator-valued kernel.
• crouzeixAuxiliaryOperator -- the normalized contour-integral operator.
• crouzeixPolynomialAuxiliaryIntegrand_contourIntegrable -- integrability for conjugate polynomial boundary values.
• crouzeixPolynomialAuxiliaryOperator -- its specialization to the conjugate boundary values of a polynomial.
• exists_bound_crouzeixPolynomialAuxiliaryIntegrand -- the polynomial resolvent kernel is uniformly bounded along the compact parameter interval.
• norm_crouzeixAuxiliaryOperator_le -- its explicit contour-length bound.
• exists_smoothJordanDomain_norm_bound_crouzeixPolynomialAuxiliaryOperator -- the packaged bounded auxiliary-operator construction.

theorem exists_smoothJordanDomain_for_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : ∃ (Omega : SmoothJordanDomain), closure (numericalRange A) ⊆ Omega.carrier

The closure of the numerical range of every bounded operator is contained in a smooth strictly convex Jordan domain.

theorem SmoothJordanDomain.boundaryParam_mem_resolventSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (Omega : SmoothJordanDomain) (A : E →L[ℂ] E) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (t : ℝ) : Omega.boundaryParam t ∈ resolventSet ℂ A

Every boundary point of a smooth Jordan domain that contains closure (numericalRange A) belongs to the resolvent set of A.

theorem crouzeixAuxiliaryIntegrand_contourIntegrable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (h : ℂ → ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hh : ContinuousOn h (Omega.boundaryParam '' Set.Icc 0 (2 * Real.pi))) : ContourIntegrable (fun (z : ℂ) => h z • resolvent A z) Omega.boundaryParam

A continuous scalar boundary datum gives a contour-integrable operator-valued resolvent kernel.

noncomputable def crouzeixAuxiliaryOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (h : ℂ → ℂ) : E →L[ℂ] E

The normalized Crouzeix--Palencia auxiliary operator associated to a scalar boundary datum h on a smooth Jordan domain.

Equations

• crouzeixAuxiliaryOperator A Omega h = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => h z • resolvent A z) Omega.boundaryParam

theorem crouzeixPolynomialAuxiliaryIntegrand_contourIntegrable {E : Type u_1} [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) • resolvent A z) Omega.boundaryParam

The conjugate polynomial boundary datum produces an integrable operator-valued resolvent kernel. This is the specialization used in the Crouzeix--Palencia symmetrized and product estimates.

theorem exists_bound_crouzeixPolynomialAuxiliaryIntegrand {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t • star (Polynomial.eval (Omega.boundaryParam t) p) • resolvent A (Omega.boundaryParam t)‖ ≤ C

The parameterized conjugate-polynomial resolvent kernel is uniformly bounded on [0, 2 * pi].

noncomputable def crouzeixPolynomialAuxiliaryOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : E →L[ℂ] E

The normalized auxiliary operator associated to the conjugate boundary values of a polynomial p.

Equations

• crouzeixPolynomialAuxiliaryOperator A Omega p = crouzeixAuxiliaryOperator A Omega fun (z : ℂ) => star (Polynomial.eval z p)

theorem norm_crouzeixAuxiliaryOperator_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (h : ℂ → ℂ) {C : ℝ} (hbound : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t • h (Omega.boundaryParam t) • resolvent A (Omega.boundaryParam t)‖ ≤ C) : ‖crouzeixAuxiliaryOperator A Omega h‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * C)

A pointwise bound C on the parameterized resolvent kernel gives the corresponding explicit operator-norm bound for the normalized auxiliary operator.

theorem norm_crouzeixPolynomialAuxiliaryOperator_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {C : ℝ} (hbound : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t • star (Polynomial.eval (Omega.boundaryParam t) p) • resolvent A (Omega.boundaryParam t)‖ ≤ C) : ‖crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * C)

The explicit contour-length bound specialized to the conjugate boundary values of a polynomial.

theorem exists_norm_bound_crouzeixPolynomialAuxiliaryOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : ∃ (C : ℝ), ‖crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * C)

For every containing smooth Jordan domain, the polynomial auxiliary operator admits a finite explicit contour-length bound.

theorem exists_smoothJordanDomain_norm_bound_crouzeixPolynomialAuxiliaryOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (p : Polynomial ℂ) : ∃ (Omega : SmoothJordanDomain) (C : ℝ), closure (numericalRange A) ⊆ Omega.carrier ∧ ‖crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * C)

Every polynomial admits a normalized auxiliary operator on some smooth Jordan domain containing closure (numericalRange A), together with a finite contour-length norm bound.