Polynomial spectral sets — definitions (L2.1)

Defines polynomialSupNorm, IsKPolynomialSpectralSet, and IsPolynomialSpectralSet. These are polynomial spectral sets (norm bound on Polynomial.aeval).

noncomputable def polynomialSupNorm (p : Polynomial ℂ) (X : Set ℂ) : ℝ

The supremum of the norm of a polynomial over a complex set.

Equations

• polynomialSupNorm p X = ⨆ z ∈ X, ‖Polynomial.eval z p‖

def IsKPolynomialSpectralSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (K : ℝ) (X : Set ℂ) : Prop

Spectrum containment and a polynomial-calculus bound with constant K.

Equations

• IsKPolynomialSpectralSet A K X = (spectrum ℂ A ⊆ X ∧ ∀ (p : Polynomial ℂ), ‖(Polynomial.aeval A) p‖ ≤ K * polynomialSupNorm p X)

def IsPolynomialSpectralSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (X : Set ℂ) : Prop

A polynomial spectral set with multiplicative constant one.

Equations

• IsPolynomialSpectralSet A X = IsKPolynomialSpectralSet A 1 X