Quantitative decay of the scalar companion

The scalar Crouzeix--Palencia companion is a Cauchy transform supported on the compact Jordan frontier. This file records the elementary quantitative part of its exterior normalization: the numerator is uniformly bounded on the parameter interval, so the transform is bounded by the reciprocal of the distance to the frontier and therefore tends to zero at infinity.

These facts are useful inputs to a future Plemelj jump argument. They do not assert boundary continuity or the sharp companion contraction.

Main declarations

• exists_nonneg_bound_crouzeixPolynomialScalarCompanionNumerator -- a uniform parameter-interval numerator bound.
• exists_nonneg_bound_boundaryParam_deriv -- a domain-only bound for the boundary speed.
• norm_crouzeixPolynomialScalarCompanion_le_of_boundary_separation -- the explicit inverse-separation estimate.
• norm_crouzeixPolynomialScalarCompanion_le_infDist -- its canonical distance-to-frontier form.
• exists_uniform_norm_crouzeixPolynomialScalarCompanion_le_infDist -- one domain constant controls all polynomials by their frontier sup norm.
• tendsto_crouzeixPolynomialScalarCompanion_cocompact -- the exterior companion tends to zero at infinity.

theorem exists_nonneg_bound_boundaryParam_deriv (Omega : SmoothJordanDomain) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t‖ ≤ D

The speed of a smooth Jordan parametrization is uniformly bounded on the compact parameter interval.

theorem exists_nonneg_bound_crouzeixPolynomialScalarCompanionNumerator (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t * star (Polynomial.eval (Omega.boundaryParam t) p)‖ ≤ C

The numerator of the parameterized scalar Cauchy companion is uniformly bounded on the compact interval [0, 2 * pi].

theorem norm_crouzeixPolynomialScalarCompanion_le_of_boundary_separation (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} {delta C : ℝ} (hdelta : 0 < delta) (hC_nonneg : 0 ≤ C) (hC : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t * star (Polynomial.eval (Omega.boundaryParam t) p)‖ ≤ C) (hsep : ∀ t ∈ Set.Icc 0 (2 * Real.pi), delta ≤ ‖Omega.boundaryParam t - z‖) : ‖crouzeixPolynomialScalarCompanion Omega p z‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (C * delta⁻¹))

If every point on the parametrized frontier is at least delta away from z, a numerator bound C gives the expected C / delta estimate for the normalized scalar Cauchy companion.

theorem norm_crouzeixPolynomialScalarCompanion_le_infDist (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} {C : ℝ} (hC_nonneg : 0 ≤ C) (hC : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t * star (Polynomial.eval (Omega.boundaryParam t) p)‖ ≤ C) (hz : z ∉ frontier Omega.carrier) : ‖crouzeixPolynomialScalarCompanion Omega p z‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (C * (Metric.infDist z (frontier Omega.carrier))⁻¹))

Away from the frontier, the preceding estimate specializes to the minimal distance from z to that frontier.

theorem norm_crouzeixPolynomialScalarCompanion_le_infDist_mul_polynomialSupNorm (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {z : ℂ} {D : ℝ} (hD_nonneg : 0 ≤ D) (hD : ∀ t ∈ Set.Icc 0 (2 * Real.pi), ‖deriv Omega.boundaryParam t‖ ≤ D) (hz : z ∉ frontier Omega.carrier) : ‖crouzeixPolynomialScalarCompanion Omega p z‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm p (frontier Omega.carrier) * (Metric.infDist z (frontier Omega.carrier))⁻¹))

A domain-only boundary-speed bound and the canonical frontier polynomial sup norm give a fully uniform inverse-distance estimate.

theorem exists_uniform_norm_crouzeixPolynomialScalarCompanion_le_infDist (Omega : SmoothJordanDomain) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (p : Polynomial ℂ), ∀ z ∉ frontier Omega.carrier, ‖crouzeixPolynomialScalarCompanion Omega p z‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * (D * polynomialSupNorm p (frontier Omega.carrier) * (Metric.infDist z (frontier Omega.carrier))⁻¹))

One nonnegative constant depending only on the smooth Jordan domain controls the scalar companions of every polynomial away from the frontier.

theorem tendsto_infDist_frontier_cocompact_atTop (Omega : SmoothJordanDomain) : Filter.Tendsto (fun (z : ℂ) => Metric.infDist z (frontier Omega.carrier)) (Filter.cocompact ℂ) Filter.atTop

The distance from a point to a compact Jordan frontier tends to infinity as the point tends to infinity.

theorem tendsto_crouzeixPolynomialScalarCompanion_cocompact (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : Filter.Tendsto (crouzeixPolynomialScalarCompanion Omega p) (Filter.cocompact ℂ) (nhds 0)

The exterior scalar companion has the canonical Cauchy-transform normalization: it tends to zero at infinity.