Spectrum of rank-one operators

TheoremSquare of the operator \(x \mapsto f(x)\,y\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a normed space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, let \(y \in E\), and let \(T\) be the bounded operator on \(E\) given by \(T x = f(x)\,y\). Then \(T^2 = f(y)\,T\).

theorem smulRight_mul_self (f : E →L[𝕜] 𝕜) (y : E) :
    (f.smulRight y) * (f.smulRight y) = (f y) • (f.smulRight y)

TheoremThe spectrum of \(x \mapsto f(x)\,y\) lies in \(\{0, f(y)\}\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a normed space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, let \(y \in E\), and let \(T\) be the bounded operator on \(E\) given by \(T x = f(x)\,y\). If \(\mu \in \mathbb{K}\) satisfies \(\mu \neq 0\) and \(\mu \neq f(y)\), then \(\mu\) is not in the spectrum of \(T\) in the algebra of bounded operators on \(E\).

Explicitly, the inverse of \(\mu I - T\), where \(I\) is the identity operator, is \(\mu^{-1} I + \mu^{-1} (\mu - f(y))^{-1}\,T\).

theorem not_mem_spectrum_smulRight {f : E →L[𝕜] 𝕜} {y : E} {μ : 𝕜} (hμ0 : μ ≠ 0)
    (hμ : μ ≠ f y) : μ ∉ spectrum 𝕜 (f.smulRight y)

Used by 1

Used bySpectrum of the operator \(x \mapsto f(x)\,y\)

Theorem\(f(y)\) is an eigenvalue of \(x \mapsto f(x)\,y\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a normed space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, and let \(y \in E\) with \(y \neq 0\). Then \(f(y)\) is an eigenvalue of the linear operator \(T x = f(x)\,y\) on \(E\).

An eigenvector is \(y\) itself, since \(T y = f(y)\,y\).

theorem hasEigenvalue_smulRight {f : E →L[𝕜] 𝕜} {y : E} (hy : y ≠ 0) :
    Module.End.HasEigenvalue (f.smulRight y : E →ₗ[𝕜] E) (f y)

Used by 1

Used by\(f(y)\) lies in the spectrum of \(x \mapsto f(x)\,y\)

Theorem\(f(y)\) lies in the spectrum of \(x \mapsto f(x)\,y\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a Banach space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, and let \(y \in E\) with \(y \neq 0\). Then \(f(y)\) lies in the spectrum of the bounded operator \(T x = f(x)\,y\) on \(E\).

theorem mem_spectrum_smulRight {f : E →L[𝕜] 𝕜} {y : E} (hy : y ≠ 0) :
    f y ∈ spectrum 𝕜 (f.smulRight y)

Uses 1 · Used by 1

Proof uses\(f(y)\) is an eigenvalue of \(x \mapsto f(x)\,y\)

Used bySpectrum of the operator \(x \mapsto f(x)\,y\)

Theorem\(0\) is an eigenvalue of \(x \mapsto f(x)\,y\) when \(f\) has a nontrivial kernel#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a normed space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, and let \(y \in E\). If some \(w \in E\) with \(w \neq 0\) satisfies \(f(w) = 0\), then \(0\) is an eigenvalue of the linear operator \(T x = f(x)\,y\) on \(E\).

An eigenvector is \(w\) itself, since \(T w = f(w)\,y = 0\).

theorem hasEigenvalue_zero_smulRight {f : E →L[𝕜] 𝕜} {y : E} {w : E} (hw : w ≠ 0)
    (hfw : f w = 0) :
    Module.End.HasEigenvalue (f.smulRight y : E →ₗ[𝕜] E) 0

Used by 1

Used by\(0\) lies in the spectrum of \(x \mapsto f(x)\,y\) when \(f\) has a nontrivial kernel

Theorem\(0\) lies in the spectrum of \(x \mapsto f(x)\,y\) when \(f\) has a nontrivial kernel#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a Banach space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, and let \(y \in E\). If some \(w \in E\) with \(w \neq 0\) satisfies \(f(w) = 0\), then \(0\) lies in the spectrum of the bounded operator \(T x = f(x)\,y\) on \(E\).

theorem mem_spectrum_smulRight_zero {f : E →L[𝕜] 𝕜} {y : E} {w : E} (hw : w ≠ 0)
    (hfw : f w = 0) : (0 : 𝕜) ∈ spectrum 𝕜 (f.smulRight y)

Uses 1 · Used by 1

Proof uses\(0\) is an eigenvalue of \(x \mapsto f(x)\,y\) when \(f\) has a nontrivial kernel

Used bySpectrum of the operator \(x \mapsto f(x)\,y\)

TheoremSpectrum of the operator \(x \mapsto f(x)\,y\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a Banach space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, and let \(y \in E\) with \(y \neq 0\). If some \(w \in E\) with \(w \neq 0\) satisfies \(f(w) = 0\), then the spectrum of the bounded operator \(T x = f(x)\,y\) on \(E\) is exactly \(\{0, f(y)\}\).

Here \(y\) is an eigenvector for \(f(y)\) and \(w\) is an eigenvector for \(0\); the zero functional is allowed. Without the kernel hypothesis this fails: on a one-dimensional space a nonzero operator of this form is a nonzero multiple of the identity, whose spectrum is a single point.

theorem spectrum_smulRight {f : E →L[𝕜] 𝕜} {y : E} (hy : y ≠ 0) {w : E} (hw : w ≠ 0)
    (hfw : f w = 0) : spectrum 𝕜 (f.smulRight y) = {0, f y}

Uses 3 · Used by 2

Proof uses\(f(y)\) lies in the spectrum of \(x \mapsto f(x)\,y\) · \(0\) lies in the spectrum of \(x \mapsto f(x)\,y\) when \(f\) has a nontrivial kernel · The spectrum of \(x \mapsto f(x)\,y\) lies in \(\{0, f(y)\}\)

Used bySpectrum of the operator \(z \mapsto \langle y, z \rangle\,x\) on a Hilbert space · Spectrum of \(x \mapsto f(x)\,y\) when \(f(y) = 0\)

TheoremSpectrum of \(x \mapsto f(x)\,y\) when \(f(y) = 0\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) be a Banach space over \(\mathbb{K}\), let \(f \colon E \to \mathbb{K}\) be a continuous linear functional, and let \(y \in E\) with \(y \neq 0\) and \(f(y) = 0\). Then the spectrum of the bounded operator \(T x = f(x)\,y\) on \(E\) is \(\{0\}\).

theorem spectrum_smulRight_of_apply_eq_zero {f : E →L[𝕜] 𝕜} {y : E} (hy : y ≠ 0)
    (hfy : f y = 0) : spectrum 𝕜 (f.smulRight y) = {0}

Uses 1

Proof usesSpectrum of the operator \(x \mapsto f(x)\,y\)

TheoremSpectrum of the operator \(z \mapsto \langle y, z \rangle\,x\) on a Hilbert space#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(H\) be a Hilbert space over \(\mathbb{K}\) whose inner product \(\langle \cdot, \cdot \rangle\) is linear in the second argument, let \(x, y \in H\) with \(x \neq 0\), and let \(T\) be the bounded operator on \(H\) given by \(T z = \langle y, z \rangle\,x\). If some \(w \in H\) with \(w \neq 0\) satisfies \(\langle y, w \rangle = 0\), then the spectrum of \(T\) is \(\{0, \langle y, x \rangle\}\).

theorem spectrum_rankOne {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
    [CompleteSpace H] {x y : H} (hx : x ≠ 0) {w : H} (hw : w ≠ 0)
    (hyw : inner 𝕜 y w = 0) :
    spectrum 𝕜 (InnerProductSpace.rankOne 𝕜 x y) = {0, inner 𝕜 y x}

Uses 1

Proof usesSpectrum of the operator \(x \mapsto f(x)\,y\)

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.