Documentation

LeanPool.OperatorTheory.Operator.NumericalRange.AffineClosure

Affine covariance of the closed numerical range #

The raw numerical-range covariance extends to the standard affine form A ↦ aA + bI. When a is nonzero this affine map is a homeomorphism, so it also commutes exactly with closure.

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

The numerical range commutes with the usual affine action A ↦ aA + bI.

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

A nondegenerate affine change of an operator transports the closure of its numerical range by the same affine map.