Approximate point spectrum

DefinitionApproximate eigenvalue of an operator#✓fully proved

μ is an approximate eigenvalue of T if there is a sequence of unit vectors xₙ with (μ • 1 - T) xₙ → 0.

def IsApproximateEigenvalue (T : E →L[𝕜] E) (μ : 𝕜) : Prop :=
  ∃ x : ℕ → E, (∀ n, ‖x n‖ = 1) ∧
    Tendsto (fun n => (μ • (1 : E →L[𝕜] E) - T) (x n)) atTop (𝓝 0)

Used by 6

Used byEpsilon characterization of approximate eigenvalues · Eigenvalues are approximate eigenvalues · Spectral values of a normal operator are approximate eigenvalues · Spectrum of a normal operator equals its approximate point spectrum · Weyl's criterion for self-adjoint operators · Approximate eigenvalues lie in the spectrum

TheoremEpsilon characterization of approximate eigenvalues#✓fully proved

The ∀ ε > 0 characterization of approximate eigenvalues.

theorem isApproximateEigenvalue_iff_forall_eps (T : E →L[𝕜] E) (μ : 𝕜) :
    IsApproximateEigenvalue T μ ↔
      ∀ ε : ℝ, 0 < ε → ∃ x : E, ‖x‖ = 1 ∧
        ‖(μ • (1 : E →L[𝕜] E) - T) x‖ < ε

Uses 1 · Used by 1

Statement usesApproximate eigenvalue of an operator

Used bySpectral values of a normal operator are approximate eigenvalues

TheoremScalar shifts of a normal operator are normal#✓fully proved

Shifting by a scalar preserves normality.

theorem isStarNormal_smul_one_sub (T : E →L[𝕜] E) (hT : IsStarNormal T) (μ : 𝕜) :
    IsStarNormal (μ • (1 : E →L[𝕜] E) - T)

Used by 1

Used bySpectral values of a normal operator are approximate eigenvalues

TheoremSpectral values of a normal operator are approximate eigenvalues#✓fully proved

Every spectral value of a normal operator is an approximate eigenvalue.

theorem isApproximateEigenvalue_of_mem_spectrum {T : E →L[𝕜] E} (hT : IsStarNormal T)
    {μ : 𝕜} (hμ : μ ∈ spectrum 𝕜 T) : IsApproximateEigenvalue T μ

Uses 3 · Used by 1

Statement usesApproximate eigenvalue of an operator

Proof usesEpsilon characterization of approximate eigenvalues · Scalar shifts of a normal operator are normal

Used bySpectrum of a normal operator equals its approximate point spectrum

TheoremApproximate eigenvalues lie in the spectrum#✓fully proved

Every approximate eigenvalue is a spectral value (no normality needed).

theorem mem_spectrum_of_isApproximateEigenvalue {T : E →L[𝕜] E} {μ : 𝕜}
    (h : IsApproximateEigenvalue T μ) : μ ∈ spectrum 𝕜 T

Uses 1 · Used by 1

Statement usesApproximate eigenvalue of an operator

Used bySpectrum of a normal operator equals its approximate point spectrum

TheoremSpectrum of a normal operator equals its approximate point spectrum#✓fully proved

For a normal operator, the spectrum is exactly the approximate point spectrum.

theorem mem_spectrum_iff_isApproximateEigenvalue {T : E →L[𝕜] E} (hT : IsStarNormal T)
    {μ : 𝕜} : μ ∈ spectrum 𝕜 T ↔ IsApproximateEigenvalue T μ

Uses 3 · Used by 1

Statement usesApproximate eigenvalue of an operator

Proof usesSpectral values of a normal operator are approximate eigenvalues · Approximate eigenvalues lie in the spectrum

Used byWeyl's criterion for self-adjoint operators

TheoremWeyl's criterion for self-adjoint operators#✓fully proved

Weyl's criterion: for a self-adjoint operator, the spectrum is exactly the approximate point spectrum.

theorem mem_spectrum_iff_isApproximateEigenvalue_of_isSelfAdjoint {T : E →L[𝕜] E}
    (hT : IsSelfAdjoint T) {μ : 𝕜} :
    μ ∈ spectrum 𝕜 T ↔ IsApproximateEigenvalue T μ

Uses 2

Statement usesApproximate eigenvalue of an operator

Proof usesSpectrum of a normal operator equals its approximate point spectrum

TheoremEigenvalues are approximate eigenvalues#✓fully proved

Exact eigenvalues are approximate eigenvalues.

theorem isApproximateEigenvalue_of_hasEigenvalue {T : E →L[𝕜] E} {μ : 𝕜}
    (h : Module.End.HasEigenvalue (T.toLinearMap) μ) : IsApproximateEigenvalue T μ

Uses 1

Statement usesApproximate eigenvalue of an operator

TheoremNormal operator with trivial kernel has dense range#✓fully proved

A normal operator with trivial kernel has dense range: the residual spectrum of a normal operator is empty.

theorem denseRange_of_isStarNormal_of_ker_eq_bot {T : E →L[𝕜] E} (hT : IsStarNormal T)
    (hker : T.ker = ⊥) : DenseRange (T : E → E)

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.