Monotonicity of polynomial spectral sets

Polynomial spectral-set estimates persist when the constant is increased or when a compact control set is enlarged.

theorem IsKPolynomialSpectralSet.mono_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {K L : ℝ} {X : Set ℂ} (h : IsKPolynomialSpectralSet A K X) (hKL : K ≤ L) : IsKPolynomialSpectralSet A L X

A polynomial spectral-set estimate remains true with a larger constant.

theorem IsKPolynomialSpectralSet.mono_set {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {K : ℝ} {X Y : Set ℂ} (h : IsKPolynomialSpectralSet A K X) (hK : 0 ≤ K) (hXY : X ⊆ Y) (hY : IsCompact Y) : IsKPolynomialSpectralSet A K Y

With a nonnegative constant, enlarging a compact control set preserves a polynomial spectral-set estimate.

theorem IsKPolynomialSpectralSet.mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {K L : ℝ} {X Y : Set ℂ} (h : IsKPolynomialSpectralSet A K X) (hK : 0 ≤ K) (hKL : K ≤ L) (hXY : X ⊆ Y) (hY : IsCompact Y) : IsKPolynomialSpectralSet A L Y

Simultaneously enlarge the constant and a compact control set.

theorem IsPolynomialSpectralSet.mono_set {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {X Y : Set ℂ} (h : IsPolynomialSpectralSet A X) (hXY : X ⊆ Y) (hY : IsCompact Y) : IsPolynomialSpectralSet A Y

A constant-one polynomial spectral set remains one after compact enlargement.

theorem IsKPolynomialSpectralSet.closure_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {K : ℝ} {X : Set ℂ} (h : IsKPolynomialSpectralSet A K X) (hX : Bornology.IsBounded X) : IsKPolynomialSpectralSet A K (closure X)

Passing from a bounded control set to its closure preserves the spectral set constant exactly.

theorem IsKPolynomialSpectralSet.closure_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {K : ℝ} {X : Set ℂ} (h : IsKPolynomialSpectralSet A K X) (hX : IsCompact X) : IsKPolynomialSpectralSet A K (closure X)

Compact control sets can be closed without changing a polynomial spectral-set estimate.