Affine covariance of polynomial spectral sets

An invertible affine change of an operator transports its spectrum and any polynomial spectral-set estimate by the same affine map, without changing the spectral-set constant.

theorem spectrum_smul_add_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {a : ℂ} (ha : a ≠ 0) (b : ℂ) : spectrum ℂ (a • A + b • 1) = (fun (z : ℂ) => a * z + b) '' spectrum ℂ A

The spectrum commutes with an invertible affine change of an operator.

theorem IsKPolynomialSpectralSet.affine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {K : ℝ} {X : Set ℂ} (h : IsKPolynomialSpectralSet A K X) {a : ℂ} (ha : a ≠ 0) (b : ℂ) : IsKPolynomialSpectralSet (a • A + b • 1) K ((fun (z : ℂ) => a * z + b) '' X)

A polynomial spectral-set estimate is transported by an invertible affine change of variables, with the same constant.

theorem isKPolynomialSpectralSet_affine_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (K : ℝ) (X : Set ℂ) {a : ℂ} (ha : a ≠ 0) (b : ℂ) : IsKPolynomialSpectralSet (a • A + b • 1) K ((fun (z : ℂ) => a * z + b) '' X) ↔ IsKPolynomialSpectralSet A K X

Affine transport is an equivalence for nonzero linear coefficient.

theorem IsPolynomialSpectralSet.affine {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →L[ℂ] E} {X : Set ℂ} (h : IsPolynomialSpectralSet A X) {a : ℂ} (ha : a ≠ 0) (b : ℂ) : IsPolynomialSpectralSet (a • A + b • 1) ((fun (z : ℂ) => a * z + b) '' X)

Invertible affine changes preserve the constant-one polynomial spectral-set property.

theorem isPolynomialSpectralSet_affine_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (X : Set ℂ) {a : ℂ} (ha : a ≠ 0) (b : ℂ) : IsPolynomialSpectralSet (a • A + b • 1) ((fun (z : ℂ) => a * z + b) '' X) ↔ IsPolynomialSpectralSet A X

Constant-one polynomial spectral sets are invariant under invertible affine changes.