Numerical range and numerical radius

DefinitionNumerical radius#✓fully proved

The numerical radius of a bounded linear operator \(T\) on a complex Hilbert space \(H\) is the real number \(w(T) = \sup \{ |\langle T x, x \rangle| : x \in H,\ \|x\| = 1 \}\), the supremum of the moduli of the values \(\langle T x, x \rangle\) over the unit vectors of \(H\) (taken to be \(0\) when \(H = 0\)).

noncomputable def numericalRadius (T : H →L[ℂ] H) : ℝ :=
  ⨆ x : { x : H // ‖x‖ = 1 }, ‖⟪T (x : H), (x : H)⟫_ℂ‖
Used by 12
Used byNumerical radius bounds the normalized imaginary part of the quadratic form · Numerical radius bounds the Rayleigh quotient · Numerical radius bounds the normalized real part of the quadratic form · The numerical radius bounds the quadratic form on unit vectors · Norm of the imaginary part is at most the numerical radius · Norm of the real part is at most the numerical radius · Operator norm at most twice the numerical radius · Numerical radius of the adjoint · Numerical radius of a self-adjoint operator · Bounding the numerical radius from above · Numerical radius at most the operator norm · Nonnegativity of the numerical radius

DefinitionReal Cartesian part of an operator#✓fully proved

For a bounded linear operator \(T\) on a complex Hilbert space with adjoint \(T^*\), the real Cartesian part of \(T\) is the bounded linear operator \((T + T^*)/2\).

noncomputable def cartesianRealPart (T : H →L[ℂ] H) : H →L[ℂ] H :=
  ↑(realPart T)
Used by 5
Used byCartesian decomposition · The real Cartesian part is symmetric · Norm of the real part is at most the numerical radius · Operator norm at most twice the numerical radius · Quadratic form of the real Cartesian part

DefinitionImaginary Cartesian part of an operator#✓fully proved

For a bounded linear operator \(T\) on a complex Hilbert space with adjoint \(T^*\), the imaginary Cartesian part of \(T\) is the bounded linear operator \((T - T^*)/(2i)\).

noncomputable def cartesianImagPart (T : H →L[ℂ] H) : H →L[ℂ] H :=
  ↑(imaginaryPart T)
Used by 5
Used byCartesian decomposition · The imaginary Cartesian part is symmetric · Norm of the imaginary part is at most the numerical radius · Operator norm at most twice the numerical radius · Quadratic form of the imaginary Cartesian part

TheoremThe numerical-radius family is bounded above#✓fully proved

Let \(T\) be a bounded linear operator on a complex inner product space \(H\). The set \(\{|\langle Tx, x\rangle| : x \in H,\ \|x\| = 1\}\) is bounded above.

The proof shows that \(\|T\|\) is an upper bound, by the Cauchy–Schwarz inequality.

theorem bddAbove_numericalRadius (T : H →L[ℂ] H) :
    BddAbove (Set.range fun x : { x : H // ‖x‖ = 1 } => ‖⟪T (x : H), (x : H)⟫_ℂ‖)
Used by 1
Used byThe numerical radius bounds the quadratic form on unit vectors

TheoremNonnegativity of the numerical radius#✓fully proved

For every bounded operator \(T\) on a complex inner product space, the numerical radius \(w(T)\) of \(T\) satisfies \(w(T) \ge 0\).

theorem numericalRadius_nonneg (T : H →L[ℂ] H) : 0 ≤ numericalRadius T
Uses 1 · Used by 6
Statement usesNumerical radius
Used byNumerical radius bounds the normalized imaginary part of the quadratic form · Numerical radius bounds the normalized real part of the quadratic form · Norm of the imaginary part is at most the numerical radius · Norm of the real part is at most the numerical radius · Numerical radius of the adjoint · Numerical radius of a self-adjoint operator

TheoremThe numerical radius bounds the quadratic form on unit vectors#✓fully proved

Let \(T\) be a bounded linear operator on a complex inner product space \(H\), with numerical radius \(w(T)\). For every \(x \in H\) with \(\|x\| = 1\), \(|\langle Tx, x\rangle| \le w(T)\).

theorem le_numericalRadius {T : H →L[ℂ] H} {x : H} (hx : ‖x‖ = 1) :
    ‖⟪T x, x⟫_ℂ‖ ≤ numericalRadius T
Uses 2 · Used by 3
Statement usesNumerical radius
Proof usesThe numerical-radius family is bounded above
Used byNumerical radius bounds the normalized imaginary part of the quadratic form · Numerical radius bounds the normalized real part of the quadratic form · Numerical radius of the adjoint

TheoremBounding the numerical radius from above#✓fully proved

Let \(T\) be a bounded operator on a complex inner product space \(H\) and let \(c \ge 0\) be a real number. If \(|\langle T x, x\rangle| \le c\) for every unit vector \(x \in H\), then the numerical radius of \(T\) satisfies \(w(T) \le c\).

The hypothesis \(c \ge 0\) matters only when \(H = 0\): there are no unit vectors, and \(w(T) = 0\).

theorem numericalRadius_le {T : H →L[ℂ] H} {c : ℝ} (hc : 0 ≤ c)
    (h : ∀ x : H, ‖x‖ = 1 → ‖⟪T x, x⟫_ℂ‖ ≤ c) : numericalRadius T ≤ c
Uses 1 · Used by 2
Statement usesNumerical radius
Used byNumerical radius of the adjoint · Numerical radius at most the operator norm

TheoremNumerical radius at most the operator norm#✓fully proved

For every bounded operator \(T\) on a complex inner product space, the numerical radius \(w(T)\) is at most the operator norm: \(w(T) \le \|T\|\).

The proof is the Cauchy–Schwarz inequality.

theorem numericalRadius_le_norm (T : H →L[ℂ] H) : numericalRadius T ≤ ‖T‖
Uses 2 · Used by 1
Statement usesNumerical radius
Proof usesBounding the numerical radius from above
Used byNumerical radius of a self-adjoint operator

TheoremQuadratic form at the normalized vector#✓fully proved

Let \(T\) be a bounded operator on a complex inner product space \(H\). For every \(x \in H\), \(\langle T(\|x\|^{-1} x), \|x\|^{-1} x \rangle = \|x\|^{-2} \langle T x, x \rangle\), where \(0^{-1}\) is read as \(0\), so that for \(x = 0\) both sides vanish.

theorem quadForm_scale (T : H →L[ℂ] H) {x : H} :
    ⟪T ((RCLike.ofReal (‖x‖⁻¹) : ℂ) • x), ((RCLike.ofReal (‖x‖⁻¹) : ℂ) • x)⟫_ℂ
      = (RCLike.ofReal ((‖x‖ ^ 2)⁻¹) : ℂ) * ⟪T x, x⟫_ℂ
Used by 2
Used byNumerical radius bounds the normalized imaginary part of the quadratic form · Numerical radius bounds the normalized real part of the quadratic form

TheoremNormalizing a nonzero vector gives a unit vector#✓fully proved

Let \(x\) be a nonzero vector in a complex inner product space. Then the vector \(\|x\|^{-1} x\) has norm \(1\).

theorem norm_normalize {x : H} (hx : x ≠ 0) :
    ‖((RCLike.ofReal (‖x‖⁻¹) : ℂ) • x)‖ = 1
Used by 2
Used byNumerical radius bounds the normalized imaginary part of the quadratic form · Numerical radius bounds the normalized real part of the quadratic form

TheoremNumerical radius bounds the normalized real part of the quadratic form#✓fully proved

Let \(T\) be a bounded linear operator on a complex inner product space \(H\), with numerical radius \(w(T)\). For every \(x \in H\), \(|\operatorname{Re} \langle Tx, x\rangle| / \|x\|^2 \le w(T)\), where division by zero is taken to be \(0\), so the case \(x = 0\) is trivial.

theorem abs_re_quadForm_div_le_numericalRadius (T : H →L[ℂ] H) (x : H) :
    |RCLike.re ⟪T x, x⟫_ℂ| / ‖x‖ ^ 2 ≤ numericalRadius T
Uses 5 · Used by 2
Statement usesNumerical radius
Proof usesThe numerical radius bounds the quadratic form on unit vectors · Normalizing a nonzero vector gives a unit vector · Nonnegativity of the numerical radius · Quadratic form at the normalized vector
Used byNumerical radius bounds the Rayleigh quotient · Norm of the real part is at most the numerical radius

TheoremNumerical radius bounds the normalized imaginary part of the quadratic form#✓fully proved

Let \(T\) be a bounded linear operator on a complex inner product space \(H\), with numerical radius \(w(T)\). For every \(x \in H\), \(|\operatorname{Im} \langle Tx, x\rangle| / \|x\|^2 \le w(T)\), where division by zero is taken to be \(0\), so the case \(x = 0\) is trivial.

theorem abs_im_quadForm_div_le_numericalRadius (T : H →L[ℂ] H) (x : H) :
    |RCLike.im ⟪T x, x⟫_ℂ| / ‖x‖ ^ 2 ≤ numericalRadius T
Uses 5 · Used by 1
Statement usesNumerical radius
Proof usesThe numerical radius bounds the quadratic form on unit vectors · Normalizing a nonzero vector gives a unit vector · Nonnegativity of the numerical radius · Quadratic form at the normalized vector
Used byNorm of the imaginary part is at most the numerical radius

TheoremNumerical radius bounds the Rayleigh quotient#✓fully proved

Let \(T\) be a bounded linear operator on a complex inner product space \(H\), with numerical radius \(w(T)\). For every \(x \in H\), the Rayleigh quotient \(R_T(x) = \operatorname{Re} \langle Tx, x\rangle / \|x\|^2\), taken to be \(0\) at \(x = 0\), satisfies \(|R_T(x)| \le w(T)\).

theorem abs_rayleighQuotient_le_numericalRadius (T : H →L[ℂ] H) (x : H) :
    |T.rayleighQuotient x| ≤ numericalRadius T
Uses 2 · Used by 1
Statement usesNumerical radius
Proof usesNumerical radius bounds the normalized real part of the quadratic form
Used byNumerical radius of a self-adjoint operator

TheoremComplex conjugate of one half#✓fully proved

The complex conjugate of \(1/2 \in \mathbb{C}\) is \(1/2\), that is, \(\overline{1/2} = 1/2\).

theorem starRingEnd_half : starRingEnd ℂ (1 / 2 : ℂ) = 1 / 2
Used by 1
Used byQuadratic form of the real Cartesian part

TheoremComplex conjugate of minus half the imaginary unit#✓fully proved

The complex conjugate of \(-i/2 \in \mathbb{C}\) is \(i/2\), that is, \(\overline{-i/2} = i/2\).

theorem starRingEnd_neg_I_div_two :
    starRingEnd ℂ (-(Complex.I / 2) : ℂ) = Complex.I / 2
Used by 1
Used byQuadratic form of the imaginary Cartesian part

TheoremThe real Cartesian part is symmetric#✓fully proved

For every bounded linear operator \(T\) on a complex Hilbert space \(H\) with adjoint \(T^*\), the real Cartesian part \(A = (T + T^*)/2\) is symmetric: \(\langle Ax, y\rangle = \langle x, Ay\rangle\) for all \(x, y \in H\).

theorem isSymmetric_cartesianRealPart (T : H →L[ℂ] H) :
    LinearMap.IsSymmetric (cartesianRealPart T : H →ₗ[ℂ] H)
Uses 1
Statement usesReal Cartesian part of an operator

TheoremThe imaginary Cartesian part is symmetric#✓fully proved

For every bounded linear operator \(T\) on a complex Hilbert space \(H\) with adjoint \(T^*\), the imaginary Cartesian part \(B = (T - T^*)/(2i)\) is symmetric: \(\langle Bx, y\rangle = \langle x, By\rangle\) for all \(x, y \in H\).

theorem isSymmetric_cartesianImagPart (T : H →L[ℂ] H) :
    LinearMap.IsSymmetric (cartesianImagPart T : H →ₗ[ℂ] H)
Uses 1
Statement usesImaginary Cartesian part of an operator

TheoremQuadratic form of the real Cartesian part#✓fully proved

Let \(T\) be a bounded operator on a complex Hilbert space \(H\) and let \(A = (T + T^*)/2\) be the real Cartesian part of \(T\). Then for every \(x \in H\) one has \(\langle A x, x \rangle = \operatorname{Re} \langle T x, x \rangle\).

theorem quadForm_cartesianRealPart (T : H →L[ℂ] H) (x : H) :
    ⟪cartesianRealPart T x, x⟫_ℂ = (RCLike.ofReal (RCLike.re ⟪T x, x⟫_ℂ) : ℂ)
Uses 2 · Used by 1
Statement usesReal Cartesian part of an operator
Proof usesComplex conjugate of one half
Used byNorm of the real part is at most the numerical radius

TheoremQuadratic form of the imaginary Cartesian part#✓fully proved

Let \(T\) be a bounded operator on a complex Hilbert space \(H\), whose inner product \(\langle \cdot, \cdot \rangle\) is conjugate-linear in its first argument, and let \(B = (T - T^*)/(2i)\) be the imaginary Cartesian part of \(T\). Then for every \(x \in H\) one has \(\langle B x, x \rangle = -\operatorname{Im} \langle T x, x \rangle\).

The sign comes from the convention on the inner product: writing \(T = A + iB\) with \(A = (T + T^*)/2\), one has \(\langle T x, x \rangle = \langle A x, x \rangle - i \langle B x, x \rangle\).

theorem quadForm_cartesianImagPart (T : H →L[ℂ] H) (x : H) :
    ⟪cartesianImagPart T x, x⟫_ℂ = (RCLike.ofReal (-(RCLike.im ⟪T x, x⟫_ℂ)) : ℂ)
Uses 2 · Used by 1
Statement usesImaginary Cartesian part of an operator
Proof usesComplex conjugate of minus half the imaginary unit
Used byNorm of the imaginary part is at most the numerical radius

TheoremCartesian decomposition#✓fully proved

Every bounded linear operator \(T\) on a complex Hilbert space satisfies \(T = A + iB\), where \(A = (T + T^*)/2\) and \(B = (T - T^*)/(2i)\) are the real and imaginary Cartesian parts of \(T\) and \(T^*\) is the adjoint of \(T\).

theorem cartesian_decomposition (T : H →L[ℂ] H) :
    T = cartesianRealPart T + Complex.I • cartesianImagPart T
Uses 2 · Used by 1
Statement usesImaginary Cartesian part of an operator · Real Cartesian part of an operator
Used byOperator norm at most twice the numerical radius

TheoremNorm of the real part is at most the numerical radius#✓fully proved

Let \(T\) be a bounded operator on a complex Hilbert space, with adjoint \(T^*\), and let \(A = (T + T^*)/2\) be its real Cartesian part. Then \(\|A\| \le w(T)\), where \(\|A\|\) is the operator norm of \(A\) and \(w(T)\) is the numerical radius of \(T\).

theorem norm_cartesianRealPart_le_numericalRadius (T : H →L[ℂ] H) :
    ‖cartesianRealPart T‖ ≤ numericalRadius T
Uses 5 · Used by 1
Statement usesReal Cartesian part of an operator · Numerical radius
Proof usesNumerical radius bounds the normalized real part of the quadratic form · Nonnegativity of the numerical radius · Quadratic form of the real Cartesian part
Used byOperator norm at most twice the numerical radius

TheoremNorm of the imaginary part is at most the numerical radius#✓fully proved

Let \(T\) be a bounded operator on a complex Hilbert space, with adjoint \(T^*\), and let \(B = (T - T^*)/(2i)\) be its imaginary Cartesian part. Then \(\|B\| \le w(T)\), where \(\|B\|\) is the operator norm of \(B\) and \(w(T)\) is the numerical radius of \(T\).

theorem norm_cartesianImagPart_le_numericalRadius (T : H →L[ℂ] H) :
    ‖cartesianImagPart T‖ ≤ numericalRadius T
Uses 5 · Used by 1
Statement usesImaginary Cartesian part of an operator · Numerical radius
Proof usesNumerical radius bounds the normalized imaginary part of the quadratic form · Nonnegativity of the numerical radius · Quadratic form of the imaginary Cartesian part
Used byOperator norm at most twice the numerical radius

TheoremOperator norm at most twice the numerical radius#✓fully proved

For every bounded operator \(T\) on a complex Hilbert space, \(\|T\| \le 2\,w(T)\), where \(\|T\|\) is the operator norm and \(w(T)\) is the numerical radius of \(T\).

theorem norm_le_two_mul_numericalRadius (T : H →L[ℂ] H) :
    ‖T‖ ≤ 2 * numericalRadius T
Uses 6
Statement usesNumerical radius
Proof usesImaginary Cartesian part of an operator · Real Cartesian part of an operator · Cartesian decomposition · Norm of the imaginary part is at most the numerical radius · Norm of the real part is at most the numerical radius

TheoremNumerical radius of a self-adjoint operator#✓fully proved

If \(T\) is a self-adjoint bounded operator on a complex Hilbert space, then its numerical radius equals its operator norm: \(w(T) = \|T\|\).

theorem numericalRadius_eq_norm_of_isSelfAdjoint {T : H →L[ℂ] H} (hT : IsSelfAdjoint T) :
    numericalRadius T = ‖T‖
Uses 4
Statement usesNumerical radius
Proof usesNumerical radius bounds the Rayleigh quotient · Numerical radius at most the operator norm · Nonnegativity of the numerical radius

TheoremThe quadratic form of the adjoint has the same modulus#✓fully proved

Let \(T\) be a bounded operator on a complex Hilbert space \(H\), with adjoint \(T^*\). For every \(x \in H\), \(|\langle T^* x, x\rangle| = |\langle T x, x\rangle|\), since \(\langle T^* x, x\rangle\) is the complex conjugate of \(\langle T x, x\rangle\).

theorem norm_quadForm_adjoint (T : H →L[ℂ] H) (x : H) :
    ‖⟪ContinuousLinearMap.adjoint T x, x⟫_ℂ‖ = ‖⟪T x, x⟫_ℂ‖
Used by 1
Used byNumerical radius of the adjoint

TheoremNumerical radius of the adjoint#✓fully proved

For every bounded operator \(T\) on a complex Hilbert space, the numerical radius of its adjoint \(T^*\) equals the numerical radius of \(T\): \(w(T^*) = w(T)\).

theorem numericalRadius_adjoint (T : H →L[ℂ] H) :
    numericalRadius (ContinuousLinearMap.adjoint T) = numericalRadius T
Uses 5
Statement usesNumerical radius
Proof usesThe numerical radius bounds the quadratic form on unit vectors · The quadratic form of the adjoint has the same modulus · Bounding the numerical radius from above · Nonnegativity of the numerical radius

DefinitionNumerical range#✓fully proved

For a bounded linear operator \(A\) on a complex inner product space \(E\), the numerical range of \(A\) is the set \(W(A) = \{\langle A x, x \rangle : x \in E,\ \|x\| = 1\} \subseteq \mathbb{C}\), where the inner product \(\langle \cdot, \cdot \rangle\) of \(E\) is conjugate-linear in its first argument and linear in its second.

noncomputable def numericalRange
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (A : E →L[ℂ] E) : Set ℂ :=
  { c : ℂ | ∃ x : E, ‖x‖ = 1 ∧ inner (𝕜 := ℂ) (A x) x = c }
Used by 15
Used byOpen unit disc lies in the backward shift's numerical range · Open unit disc lies in the forward shift's numerical range · Backward shift's numerical range lies in the open unit disc · Forward shift's numerical range lies in the open unit disc · Numerical range of the backward shift is the open unit disc · Numerical range of the unilateral shift is the open unit disc · Conjugates of spectral values lie in the closed numerical range · Conjugates of eigenvalues lie in the numerical range · Unit vectors give points of the numerical range · Conjugate shifts off the closed numerical range are invertible · Membership in the numerical range · The numerical range is bounded by the operator norm · The spectrum lies in the conjugate of the closed numerical range · Toeplitz–Hausdorff theorem · Toeplitz–Hausdorff theorem without completeness

TheoremMembership in the numerical range#✓fully proved

Let \(A\) be a bounded linear operator on a complex inner product space \(E\). A complex number \(c\) lies in the numerical range \(W(A)\) if and only if there is a vector \(x \in E\) with \(\|x\| = 1\) and \(\langle A x, x \rangle = c\).

theorem mem_numericalRange_iff
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (A : E →L[ℂ] E) (c : ℂ) :
    c ∈ numericalRange A ↔ ∃ x : E, ‖x‖ = 1 ∧ inner (𝕜 := ℂ) (A x) x = c
Uses 1 · Used by 2
Statement usesNumerical range
Used byBackward shift's numerical range lies in the open unit disc · Forward shift's numerical range lies in the open unit disc

TheoremUnit vectors give points of the numerical range#✓fully proved

Let \(A\) be a bounded linear operator on a complex inner product space \(E\). For every \(x \in E\) with \(\|x\| = 1\), the number \(\langle A x, x \rangle\) lies in the numerical range \(W(A)\).

theorem inner_mem_numericalRange
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (A : E →L[ℂ] E) {x : E} (hx : ‖x‖ = 1) :
    inner (𝕜 := ℂ) (A x) x ∈ numericalRange A
Uses 1 · Used by 1
Statement usesNumerical range
Used byConjugate shifts off the closed numerical range are invertible

TheoremToeplitz–Hausdorff theorem without completeness#✓fully proved

The numerical range of a bounded linear operator on a complex inner product space is convex. Completeness of the space is not needed.

theorem toeplitz_hausdorff_general
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (A : E →L[ℂ] E) :
    Convex ℝ (numericalRange A)
Uses 1 · Used by 1
Statement usesNumerical range
Used byToeplitz–Hausdorff theorem

TheoremToeplitz–Hausdorff theorem#✓fully proved

The numerical range of a bounded linear operator on a complex Hilbert space is convex.

@[nolint unusedArguments]
theorem toeplitz_hausdorff
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (A : E →L[ℂ] E) :
    Convex ℝ (numericalRange A)
Sources
  • O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejer, Math. Z. 2 (1918), 187-197, DOI 10.1007/BF01212904; F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314-316, DOI 10.1007/BF01292610. It follows from toeplitz_hausdorff_general; the hypothesis CompleteSpace E is unused and keeps the source's shape.
Uses 2
Statement usesNumerical range
Proof usesToeplitz–Hausdorff theorem without completeness

TheoremConjugate shifts off the closed numerical range are invertible#✓fully proved

Let \(A\) be a bounded linear operator on a complex Hilbert space \(E\), whose inner product \(\langle \cdot, \cdot \rangle\) is conjugate-linear in its first argument and linear in its second, let \(W(A) = \{\langle A x, x \rangle : x \in E,\ \|x\| = 1\}\) be the numerical range of \(A\) and let \(\mu \in \mathbb{C}\). If \(\mu\) is not in the closure of \(W(A)\), then \(A - \overline{\mu}\, I\), where \(\overline{\mu}\) is the complex conjugate of \(\mu\) and \(I\) is the identity operator, is invertible in the algebra of bounded linear operators on \(E\).

Both this operator and its adjoint are bounded below, so it is injective with closed range, and its range has trivial orthogonal complement, hence it is surjective.

theorem isUnit_of_notMem_closure_numericalRange [CompleteSpace E] {A : E →L[ℂ] E}
    {μ : ℂ} (hμ : μ ∉ closure (ToeplitzHausdorffWanted.numericalRange A)) :
    IsUnit (A - (starRingEnd ℂ) μ • (1 : E →L[ℂ] E))
Uses 2 · Used by 1
Statement usesNumerical range
Proof usesUnit vectors give points of the numerical range
Used byConjugates of spectral values lie in the closed numerical range

TheoremConjugates of spectral values lie in the closed numerical range#✓fully proved

Let \(A\) be a bounded linear operator on a complex Hilbert space \(E\), whose inner product \(\langle \cdot, \cdot \rangle\) is conjugate-linear in its first argument and linear in its second, and let \(W(A) = \{\langle A x, x \rangle : x \in E,\ \|x\| = 1\}\) be the numerical range of \(A\). If \(z\) is in the spectrum of \(A\), then the complex conjugate \(\overline{z}\) lies in the closure of \(W(A)\).

theorem conj_mem_closure_numericalRange_of_mem_spectrum [CompleteSpace E]
    {A : E →L[ℂ] E} {z : ℂ} (hz : z ∈ spectrum ℂ A) :
    (starRingEnd ℂ) z ∈ closure (ToeplitzHausdorffWanted.numericalRange A)
Uses 2 · Used by 1
Statement usesNumerical range
Proof usesConjugate shifts off the closed numerical range are invertible
Used byThe spectrum lies in the conjugate of the closed numerical range

TheoremThe spectrum lies in the conjugate of the closed numerical range#✓fully proved

Let \(A\) be a bounded linear operator on a complex Hilbert space \(E\), whose inner product \(\langle \cdot, \cdot \rangle\) is conjugate-linear in its first argument and linear in its second, and let \(W(A) = \{\langle A x, x \rangle : x \in E,\ \|x\| = 1\}\) be the numerical range of \(A\). Then every point of the spectrum of \(A\) is the complex conjugate \(\overline{w}\) of some point \(w\) of the closure of \(W(A)\).

theorem spectrum_subset_star_image_closure_numericalRange [CompleteSpace E]
    (A : E →L[ℂ] E) :
    spectrum ℂ A ⊆ (starRingEnd ℂ) '' closure (ToeplitzHausdorffWanted.numericalRange A)
Uses 2
Statement usesNumerical range
Proof usesConjugates of spectral values lie in the closed numerical range

TheoremConjugates of eigenvalues lie in the numerical range#✓fully proved

Let \(A\) be a bounded linear operator on a complex inner product space \(E\), whose inner product \(\langle \cdot, \cdot \rangle\) is conjugate-linear in its first argument and linear in its second, let \(W(A) = \{\langle A x, x \rangle : x \in E,\ \|x\| = 1\}\) be the numerical range of \(A\) and let \(z \in \mathbb{C}\). If there is a vector \(x \in E\) with \(\|x\| = 1\) and \(A x = z x\), then the complex conjugate \(\overline{z}\) lies in \(W(A)\) itself, not just in its closure.

Indeed \(\langle A x, x \rangle = \overline{z}\) for such a unit eigenvector \(x\).

theorem conj_mem_numericalRange_of_exists_unit_eigenvector {A : E →L[ℂ] E} {z : ℂ}
    (h : ∃ x : E, ‖x‖ = 1 ∧ A x = z • x) :
    (starRingEnd ℂ) z ∈ ToeplitzHausdorffWanted.numericalRange A
Uses 1
Statement usesNumerical range

TheoremThe numerical range is bounded by the operator norm#✓fully proved

Let \(A\) be a bounded linear operator on a complex inner product space \(E\). Then every point of the numerical range \(W(A)\) has absolute value at most the operator norm \(\|A\|\): \(W(A)\) lies in the closed disc of radius \(\|A\|\) centred at \(0\).

theorem numericalRange_subset_closedBall_norm (A : E →L[ℂ] E) :
    ToeplitzHausdorffWanted.numericalRange A ⊆ Metric.closedBall 0 ‖A‖
Uses 1
Statement usesNumerical range

TheoremLower bound from the numerical range#●ready to prove

Let \(H\) be a complex Hilbert space with inner product \(\langle \cdot, \cdot \rangle\), conjugate-linear in the first argument and linear in the second, and let \(T : H \to H\) be a bounded linear operator. Let \(N(T) = \{\langle \psi, T\psi \rangle : \psi \in H,\ \|\psi\| = 1\} \subseteq \mathbb{C}\) be the numerical range of \(T\), and for \(z \in \mathbb{C}\) let \(d(z, N(T))\) be the infimum of the distances from \(z\) to the points of \(N(T)\), taken to be \(0\) when \(N(T)\) is empty. Then for every \(\psi \in H\) and every \(z \in \mathbb{C}\), \(\|(T - zI)\psi\| \ge d(z, N(T))\,\|\psi\|\), where \(I\) is the identity operator on \(H\).

public theorem_wanted infDist_numericalRange_mul_norm_le_norm_sub_smul_apply
  (H : Type*)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (T : H →L[ℂ] H)
  (N : Set ℂ)
  (hN : N = {w : ℂ | ∃ ψ : H, ‖ψ‖ = 1 ∧ inner ℂ ψ (T ψ) = w}) :
  ∀ ψ : H, ∀ z : ℂ,
    ‖(T - z • ContinuousLinearMap.id ℂ H) ψ‖ ≥ Metric.infDist z N * ‖ψ‖
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem ma_proofbench_l2_55.
36 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.