Cartesian-part bounds from numerical radius

The selfadjoint and skew-adjoint numerators of an operator are each bounded in norm by twice its numerical radius.

theorem norm_add_adjoint_le_two_mul_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : ‖A + ContinuousLinearMap.adjoint A‖ ≤ 2 * numericalRadius A

The selfadjoint numerator A + A† has norm at most 2w(A).

theorem norm_sub_adjoint_le_two_mul_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : ‖A - ContinuousLinearMap.adjoint A‖ ≤ 2 * numericalRadius A

The skew-adjoint numerator A - A† has norm at most 2w(A).

theorem norm_inv_two_smul_add_adjoint_le_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : ‖2⁻¹ • (A + ContinuousLinearMap.adjoint A)‖ ≤ numericalRadius A

The selfadjoint Cartesian part has norm at most the numerical radius.

theorem norm_inv_two_smul_sub_adjoint_le_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : ‖2⁻¹ • (A - ContinuousLinearMap.adjoint A)‖ ≤ numericalRadius A

The skew-adjoint Cartesian part has norm at most the numerical radius.