Numerical ranges of isometric compressions

If V : F → E is an isometry, the compression V† A V has numerical range contained in that of A. Numerical radius is therefore monotone under isometric compression.

theorem numericalRange_compression_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (A : E →L[ℂ] E) (V : F →L[ℂ] E) (hV : Isometry ⇑V) : numericalRange ((ContinuousLinearMap.adjoint V ∘SL A) ∘SL V) ⊆ numericalRange A

The numerical range of an isometric compression is contained in the original numerical range.

theorem numericalRadius_adjoint_comp_comp_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (A : E →L[ℂ] E) (V : F →L[ℂ] E) : numericalRadius ((ContinuousLinearMap.adjoint V ∘SL A) ∘SL V) ≤ ‖V‖ ^ 2 * numericalRadius A

General congruence estimate for numerical radius.

theorem numericalRadius_compression_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (A : E →L[ℂ] E) (V : F →L[ℂ] E) (hV : Isometry ⇑V) : numericalRadius ((ContinuousLinearMap.adjoint V ∘SL A) ∘SL V) ≤ numericalRadius A

Numerical radius cannot increase under isometric compression.