Adjoint and unitary invariance of the numerical radius

The numerical range of the adjoint is obtained by complex conjugation, so its radius is unchanged. Likewise, unitary changes of orthonormal coordinates preserve the entire numerical range and hence the numerical radius.

theorem numericalRadius_adjoint_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : numericalRadius (ContinuousLinearMap.adjoint A) ≤ numericalRadius A

Taking the adjoint cannot increase the numerical radius.

@[simp]

theorem numericalRadius_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : numericalRadius (ContinuousLinearMap.adjoint A) = numericalRadius A

Numerical radius is invariant under adjoint.

theorem numericalRange_unitary_conjugate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : numericalRange (ContinuousLinearMap.adjoint U * A * U) = numericalRange A

Conjugating an operator by a unitary preserves its numerical range.

theorem numericalRange_unitary_conjugate' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : numericalRange (U * A * ContinuousLinearMap.adjoint U) = numericalRange A

The alternate orientation of unitary conjugation also preserves the numerical range.

theorem numericalRadius_unitary_conjugate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : numericalRadius (ContinuousLinearMap.adjoint U * A * U) = numericalRadius A

Numerical radius is invariant under unitary conjugation.

theorem numericalRadius_unitary_conjugate' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : numericalRadius (U * A * ContinuousLinearMap.adjoint U) = numericalRadius A

Numerical radius is invariant under the alternate orientation of unitary conjugation.