Normalize approximate polynomial companions

Uniform polynomial approximation naturally gives a scalar sup-norm bound with an arbitrarily small additive error. The fourth-power Crouzeix--Palencia bootstrap instead consumes an exactly contractive sequence. This file bridges those interfaces by shrinking the j-th approximant by m / (m + 1 / (j + 1)). The shrinkage factors tend to one, so the operator limit is unchanged.

The zero case necessarily needs separate information: exact contractivity at m = 0 forces every normalized polynomial to vanish, and hence can converge only to zero. This condition is explicit in the generic statement; for the canonical Crouzeix auxiliary operator it follows from vanishing of the source polynomial on an infinite compact control set.

Main declaration

• exists_tendsto_polynomial_companions_of_add_one_div_bounds -- convert additive 1 / (j + 1) sup-norm errors into an exactly contractive sequence without changing the operator-norm limit.
• polynomialSupNorm_le_add_of_uniform_approximation -- a contractive scalar target and a uniform polynomial approximation give the required additive sup-norm bound.
• exists_tendsto_polynomial_companions_of_uniform_approximation -- combine uniform approximation of a contractive scalar companion with exact normalization.

theorem exists_tendsto_polynomial_companions_of_add_one_div_bounds {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E →L[ℂ] E) (S : Set ℂ) (m : ℝ) (hm : 0 ≤ m) (G : E →L[ℂ] E) (hGzero : m = 0 → G = 0) (r : ℕ → Polynomial ℂ) (hr : ∀ (j : ℕ), polynomialSupNorm (r j) S ≤ m + 1 / (↑j + 1)) (hrlim : Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (r j)) Filter.atTop (nhds G)) : ∃ (q : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (q j) S ≤ m) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds G)

Additive 1 / (j + 1) errors in polynomial sup norm can be removed by rescaling without changing the operator-norm limit. The explicit zero-case hypothesis is necessary: a sequence with exact bound zero consists of zero polynomials, so its operator limit must be zero.

theorem polynomialSupNorm_le_add_of_uniform_approximation (r : Polynomial ℂ) (S : Set ℂ) (g : ℂ → ℂ) (m ε : ℝ) (hm : 0 ≤ m) (hε : 0 ≤ ε) (hg : ∀ z ∈ S, ‖g z‖ ≤ m) (happrox : ∀ z ∈ S, ‖Polynomial.eval z r - g z‖ ≤ ε) : polynomialSupNorm r S ≤ m + ε

If a scalar function is bounded by m on S and a polynomial uniformly approximates it within ε, the polynomial sup norm on S is at most m + ε. No compactness assumption is needed because the pointwise upper bound directly controls the conditionally complete supremum.

theorem exists_tendsto_polynomial_companions_of_uniform_approximation {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : E →L[ℂ] E) (S : Set ℂ) (m : ℝ) (hm : 0 ≤ m) (g : ℂ → ℂ) (hg : ∀ z ∈ S, ‖g z‖ ≤ m) (G : E →L[ℂ] E) (hGzero : m = 0 → G = 0) (r : ℕ → Polynomial ℂ) (happrox : ∀ (j : ℕ), ∀ z ∈ S, ‖Polynomial.eval z (r j) - g z‖ ≤ 1 / (↑j + 1)) (hrlim : Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (r j)) Filter.atTop (nhds G)) : ∃ (q : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (q j) S ≤ m) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds G)

Uniform polynomial approximation of a scalar companion bounded by m produces an exactly sup-norm-contractive polynomial sequence, provided the polynomial evaluations already converge to the identified operator companion. The latter identification is deliberately separate: analytically it comes from the holomorphic functional calculus for the scalar Cauchy companion.