Algebraic estimates for the numerical radius

The numerical radius is not submultiplicative, but its sharp equivalence with the operator norm gives uniform product estimates. This file records those estimates and their immediate commutator and anticommutator consequences.

theorem numericalRadius_mul_le_norm_mul_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) : numericalRadius (A * B) ≤ ‖A‖ * ‖B‖

The numerical radius of a product is bounded by the product of the operator norms.

theorem numericalRadius_mul_le_two_mul_numericalRadius_mul_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) : numericalRadius (A * B) ≤ 2 * numericalRadius A * ‖B‖

A product estimate using numerical radius in the left factor.

theorem numericalRadius_mul_le_two_mul_norm_mul_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) : numericalRadius (A * B) ≤ 2 * ‖A‖ * numericalRadius B

A product estimate using numerical radius in the right factor.

theorem numericalRadius_mul_le_four_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) : numericalRadius (A * B) ≤ 4 * numericalRadius A * numericalRadius B

Uniform quasi-submultiplicativity of numerical radius.

theorem numericalRadius_pow_le_two_mul_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (n : ℕ) : numericalRadius (A ^ n) ≤ (2 * numericalRadius A) ^ n

Powers are controlled by the power of twice the numerical radius.

theorem numericalRadius_commutator_le_eight_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) : numericalRadius (A * B - B * A) ≤ 8 * numericalRadius A * numericalRadius B

The numerical radius of a commutator has the uniform constant-eight bound coming from quasi-submultiplicativity.

theorem numericalRadius_anticommutator_le_eight_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) : numericalRadius (A * B + B * A) ≤ 8 * numericalRadius A * numericalRadius B

The same uniform constant-eight bound holds for the anticommutator.