The zero case for polynomial sup norms on infinite compact sets

Normalization arguments for the Crouzeix--Palencia auxiliary estimates divide by the polynomial sup norm. This file isolates the complementary zero case: a polynomial whose sup norm on an infinite compact subset of the complex plane is zero must itself be zero. Positive-radius closed disks are recorded as the principal geometric specialization.

Main declarations

• polynomial_eq_zero_of_polynomialSupNorm_eq_zero -- vanishing of the sup norm on an infinite compact set forces the polynomial to vanish.
• polynomial_eq_zero_of_polynomialSupNorm_closedBall_eq_zero -- the closed disk specialization.
• polynomial_auxiliary_bounds_of_normalized_of_isCompact_infinite -- normalized sharp auxiliary bounds extend to every polynomial on an infinite compact set.
• polynomial_auxiliary_bounds_of_normalized_closedBall -- normalized sharp auxiliary bounds imply the corresponding bounds for every polynomial on a nondegenerate closed disk, including the zero sup-norm case.

theorem polynomial_eq_zero_of_polynomialSupNorm_eq_zero (p : Polynomial ℂ) {K : Set ℂ} (hK : IsCompact K) (hKinf : K.Infinite) (hzero : polynomialSupNorm p K = 0) : p = 0

A complex polynomial with zero sup norm on an infinite compact set is the zero polynomial.

theorem polynomial_eq_zero_of_polynomialSupNorm_closedBall_eq_zero (p : Polynomial ℂ) (c : ℂ) {R : ℝ} (hR : 0 < R) (hzero : polynomialSupNorm p (Metric.closedBall c R) = 0) : p = 0

A complex polynomial with zero sup norm on a closed disk of positive radius is the zero polynomial.

theorem polynomial_auxiliary_bounds_of_normalized_of_isCompact_infinite {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (K : Set ℂ) (hK : IsCompact K) (hKinf : K.Infinite) (p : Polynomial ℂ) (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

On an infinite compact set, sharp auxiliary bounds for all polynomials of sup norm one imply the correctly scaled bounds for every polynomial. This complements polynomial_auxiliary_bounds_of_normalized, whose division argument assumes that the sup norm is positive.

theorem polynomial_auxiliary_bounds_of_normalized_closedBall {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (Omega : SmoothJordanDomain) (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) (hnormalized : ∀ (q : Polynomial ℂ), polynomialSupNorm q (Metric.closedBall c R) = 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 (Metric.closedBall c R) ∧ ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ polynomialSupNorm p (Metric.closedBall c R) ^ 2

On a closed disk of positive radius, normalized sharp auxiliary bounds imply the correctly scaled bounds for every polynomial.