Numerical range of the adjoint (L2.3)

For a continuous linear operator on a complex Hilbert space, the numerical range of its adjoint is the pointwise complex conjugate of its numerical range.

Main declaration

• numericalRange_adjoint — W(A†) = conj '' W(A).

theorem numericalRange_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : numericalRange (ContinuousLinearMap.adjoint A) = ⇑(starRingEnd ℂ) '' numericalRange A

The numerical range of the adjoint is the pointwise complex conjugate of the numerical range.