Boundary approximation implies polynomial-companion convergence

For any continuous scalar boundary datum, if polynomials approximate that datum uniformly and satisfy the polynomial Cauchy representation, their evaluations at the operator converge in norm to the associated normalized resolvent contour integral. The canonical Crouzeix auxiliary operator is the specialization to the conjugate boundary values of a polynomial.

This file makes the passage quantitative. Compactness of the parameter interval bounds deriv γ(t) • resolvent A (γ(t)) by a fixed constant, so a boundary error of 1 / (j + 1) gives an operator error bounded by a fixed multiple of the same null sequence.

Main declaration

• tendsto_aeval_to_crouzeixAuxiliaryOperator_of_boundary_approximation -- the generic continuous-boundary-datum convergence theorem.
• tendsto_aeval_to_crouzeixPolynomialAuxiliaryOperator_of_boundary_approximation -- its conjugate-polynomial specialization.

theorem tendsto_aeval_to_crouzeixAuxiliaryOperator_of_boundary_approximation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (g : ℂ → ℂ) (q : ℕ → Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hg : ContinuousOn g (Omega.boundaryParam '' Set.Icc 0 (2 * Real.pi))) (hCauchy : ∀ (j : ℕ), (Polynomial.aeval A) (q j) = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z (q j) • resolvent A z) Omega.boundaryParam) (happrox : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖Polynomial.eval (Omega.boundaryParam t) (q j) - g (Omega.boundaryParam t)‖ ≤ 1 / (↑j + 1)) : Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds (crouzeixAuxiliaryOperator A Omega g))

Uniform approximation of a continuous scalar boundary datum at rate 1 / (j + 1) implies operator-norm convergence of the polynomial evaluations to its normalized resolvent contour integral.

theorem tendsto_aeval_to_crouzeixPolynomialAuxiliaryOperator_of_boundary_approximation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (q : ℕ → Polynomial ℂ) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (hCauchy : ∀ (j : ℕ), (Polynomial.aeval A) (q j) = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z (q j) • resolvent A z) Omega.boundaryParam) (happrox : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖Polynomial.eval (Omega.boundaryParam t) (q j) - star (Polynomial.eval (Omega.boundaryParam t) p)‖ ≤ 1 / (↑j + 1)) : Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds (crouzeixPolynomialAuxiliaryOperator A Omega p))

Uniform approximation of the conjugate polynomial boundary datum at rate 1 / (j + 1) implies operator-norm convergence of the polynomial evaluations to the canonical Crouzeix auxiliary operator.