Affine covariance of the numerical range

Affine changes of an operator induce the same affine changes on its numerical range. The general formula in this file simultaneously covers scalar multiplication, translation by a scalar operator, and the centered-rescaled operators used in disk normalization arguments.

theorem numericalRange_smul_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c z₀ : ℂ) : numericalRange (c • (A - z₀ • 1)) = (fun (z : ℂ) => c * (z - z₀)) '' numericalRange A

The numerical range commutes with the affine normalization A ↦ c • (A - z₀ I).

theorem numericalRange_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) : numericalRange (c • A) = (fun (z : ℂ) => c * z) '' numericalRange A

Scalar multiplication of an operator multiplies its numerical range by the same scalar.

theorem numericalRange_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) : numericalRange (A - c • 1) = (fun (z : ℂ) => z - c) '' numericalRange A

Subtracting a scalar operator translates the numerical range.

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

Adding a scalar operator translates the numerical range.

@[simp]

theorem numericalRange_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] : numericalRange 0 = {0}

On a nontrivial space, the numerical range of the zero operator is the singleton {0}.

@[simp]

theorem numericalRange_scalar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (c : ℂ) : numericalRange (c • 1) = {c}

On a nontrivial space, a scalar operator has singleton numerical range.