Documentation

LeanPool.OperatorTheory.Operator.NumericalRange.Radius

The numerical radius #

This file proves the classical sharp comparison between the numerical radius and the operator norm:

numericalRadius A ≤ ‖A‖ ≤ 2 * numericalRadius A.

The reverse estimate is independent of completeness. Its proof first homogenizes the unit-vector definition of the numerical range, then applies the complex polarization identity to the quadratic form x ↦ ⟪x, A x⟫_ℂ.

source
theorem norm_inner_apply_self_le_numericalRadius_mul_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (x : E) :
‖inner ℂ x (A x)‖ ≤ numericalRadius A * ‖x‖ ^ 2

The quadratic form of an operator at an arbitrary vector is bounded by the numerical radius times the squared norm.

source
theorem norm_inner_apply_le_numericalRadius_mul_add_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (x y : E) :
‖inner ℂ y (A x)‖ ≤ numericalRadius A * (‖x‖ ^ 2 + ‖y‖ ^ 2)

Polarization upgrades the diagonal numerical-radius estimate to every matrix coefficient.

source
theorem norm_apply_le_two_mul_numericalRadius_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {x : E} (hx : ‖x‖ = 1) :
‖A x‖ ≤ 2 * numericalRadius A

On a unit vector, the operator is bounded by twice its numerical radius.

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

Pointwise sharp comparison of the operator norm and numerical radius.

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

The operator norm is at most twice the numerical radius. Together with numericalRadius_le_norm, this is the classical sharp norm equivalence.

source
theorem numericalRadius_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) :
numericalRadius A = 0 ↔ A = 0

The numerical radius vanishes exactly for the zero operator.

source
theorem numericalRadius_pos_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) :
0 < numericalRadius A ↔ A ≠ 0

The numerical radius is positive exactly for nonzero operators.

source
@[simp]
theorem numericalRadius_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] :
numericalRadius 0 = 0
source
theorem numericalRadius_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) :
numericalRadius (A + B) ≤ numericalRadius A + numericalRadius B

Numerical radius is subadditive.

source
theorem numericalRadius_smul_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (c : ℂ) (A : E →L[ℂ] E) :
numericalRadius (c • A) ≤ ‖c‖ * numericalRadius A

One half of absolute homogeneity of the numerical radius.

source
theorem numericalRadius_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (c : ℂ) (A : E →L[ℂ] E) :
numericalRadius (c • A) = ‖c‖ * numericalRadius A

Numerical radius is absolutely homogeneous.

source
@[simp]
theorem numericalRadius_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) :
numericalRadius (-A) = numericalRadius A
source
theorem numericalRadius_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) :
numericalRadius (A - B) ≤ numericalRadius A + numericalRadius B

Numerical radius satisfies the triangle inequality for subtraction.

source
noncomputable def numericalRadiusSeminorm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] :
Seminorm ℂ (E →L[ℂ] E)

The numerical radius bundled as a complex seminorm on bounded operators. Definiteness is supplied separately by numericalRadius_eq_zero_iff.

Equations
Instances For
    source
    @[simp]
    theorem numericalRadiusSeminorm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) :
    numericalRadiusSeminorm A = numericalRadius A
    source
    theorem abs_numericalRadius_sub_le_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A B : E →L[ℂ] E) :
    |numericalRadius A - numericalRadius B| ≤ ‖A - B‖

    Numerical radius changes by at most the operator-norm distance.

    source
    theorem lipschitzWith_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] :
    LipschitzWith 1 numericalRadius

    Numerical radius is 1-Lipschitz with respect to the operator norm.

    source
    theorem continuous_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] :
    Continuous numericalRadius

    Numerical radius is continuous in the operator norm.