Riesz–Schauder theory

TheoremRiesz–Schauder theorem, kernel part#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{R}\) or \(\mathbb{C}\), let \(T : E \to E\) be a compact bounded linear operator, let \(\mu \neq 0\) be a scalar and let \(I\) be the identity of \(E\). Then the kernel of \(\mu I - T\) is finite-dimensional.

The proof is the standard restriction trick: \(T\) maps the kernel of \(\mu I - T\) into itself and agrees with \(\mu I\) there, so the identity of the kernel is a compact operator.

theorem finiteDimensional_ker (hT : IsCompactOperator T) (hμ : μ ≠ 0) :
    FiniteDimensional 𝕜 (LinearMap.ker ((μ • 1 - T : E →L[𝕜] E).toLinearMap))

Used by 2

Used byFredholm alternative, Riesz–Schauder form · Riesz–Schauder theorem, range part

TheoremContinuous projection onto a finite-dimensional subspace#✓fully proved

Let \(E\) be a normed space over \(\mathbb{R}\) or \(\mathbb{C}\) and let \(K\) be a finite-dimensional subspace of \(E\). Then there is a continuous linear map \(P : E \to E\) such that \(P x = x\) for every \(x \in K\) and \(P x \in K\) for every \(x \in E\).

The projection is built from a basis of \(K\), with the coordinate functionals extended to all of \(E\) by Hahn–Banach.

theorem exists_continuous_projection (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 K] :
    ∃ P : E →L[𝕜] E, (∀ x ∈ K, P x = x) ∧ ∀ x, P x ∈ K

Used by 1

Used byRiesz–Schauder theorem, range part

TheoremRiesz–Schauder theorem, range part#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{R}\) or \(\mathbb{C}\), let \(T : E \to E\) be a compact bounded linear operator, let \(\mu \neq 0\) be a scalar and let \(I\) be the identity of \(E\). Then the range of \(\mu I - T\) is closed in \(E\).

The proof restricts \(\mu I - T\) to a closed complement of its kernel, where a sequence argument using compactness of \(T\) shows that it is bounded below, hence has closed range.

theorem isClosed_range_smul_one_sub (hT : IsCompactOperator T) (hμ : μ ≠ 0) :
    IsClosed (LinearMap.range ((μ • 1 - T : E →L[𝕜] E).toLinearMap) : Set E)

Uses 2 · Used by 2

Proof usesContinuous projection onto a finite-dimensional subspace · Riesz–Schauder theorem, kernel part

Used byFredholm alternative, Riesz–Schauder form · Riesz–Schauder theorem on a Hilbert space

TheoremFredholm alternative, Riesz–Schauder form#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{R}\) or \(\mathbb{C}\), let \(T : E \to E\) be a compact bounded linear operator, let \(\mu \neq 0\) be a scalar and let \(I\) be the identity of \(E\). Then either \(\mu I - T\) is bijective, or the kernel of \(\mu I - T\) is nonzero and finite-dimensional and the range of \(\mu I - T\) is closed.

theorem fredholm_alternative (hT : IsCompactOperator T) (hμ : μ ≠ 0) :
    Function.Bijective (μ • 1 - T : E →L[𝕜] E) ∨
      (LinearMap.ker ((μ • 1 - T : E →L[𝕜] E).toLinearMap) ≠ ⊥ ∧
        FiniteDimensional 𝕜 (LinearMap.ker ((μ • 1 - T : E →L[𝕜] E).toLinearMap)) ∧
        IsClosed (LinearMap.range ((μ • 1 - T : E →L[𝕜] E).toLinearMap) : Set E))

Uses 2

Proof usesRiesz–Schauder theorem, kernel part · Riesz–Schauder theorem, range part

TheoremRiesz–Schauder theorem on a Hilbert space#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a compact operator on \(E\), let \(\mu \in \mathbb{K}\) with \(\mu \ne 0\), and let \(I\) be the identity operator on \(E\). Then the range of \(\mu I - T\) is the orthogonal complement of the kernel of its adjoint: \(\operatorname{ran}(\mu I - T) = \ker\big((\mu I - T)^*\big)^\perp\).

For self-adjoint \(T\) this gives \(\operatorname{ran}(\mu I - T) = \ker(\mu I - T)^\perp\).

theorem range_eq_orthogonal_ker_adjoint (hT : IsCompactOperator T) (hμ : μ ≠ 0) :
    LinearMap.range ((μ • 1 - T : E →L[𝕜] E).toLinearMap)
      = (LinearMap.ker ((μ • 1 - T : E →L[𝕜] E)†.toLinearMap))ᗮ

Uses 1 · Used by 1

Proof usesRiesz–Schauder theorem, range part

Used byRiesz–Schauder theorem on a Hilbert space, adjoint form

TheoremAdjoint of a shifted operator#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a bounded linear operator on \(E\) with adjoint \(T^*\), let \(\mu \in \mathbb{K}\) and let \(I\) be the identity operator on \(E\). Then \((\mu I - T)^* = \overline{\mu} I - T^*\), where \(\overline{\mu}\) is the complex conjugate of \(\mu\) (so \(\overline{\mu} = \mu\) when \(\mathbb{K} = \mathbb{R}\)).

theorem adjoint_smul_one_sub :
    (μ • 1 - T : E →L[𝕜] E)† = star μ • 1 - T†

Used by 1

Used byRiesz–Schauder theorem on a Hilbert space, adjoint form

TheoremRiesz–Schauder theorem on a Hilbert space, adjoint form#✓fully proved

Let \(E\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a compact operator on \(E\) with adjoint \(T^*\), let \(\mu \in \mathbb{K}\) with \(\mu \ne 0\), and let \(I\) be the identity operator on \(E\). Then the range of \(\mu I - T\) is the orthogonal complement of the kernel of \(\overline{\mu} I - T^*\), where \(\overline{\mu}\) is the complex conjugate of \(\mu\): \(\operatorname{ran}(\mu I - T) = \ker(\overline{\mu} I - T^*)^\perp\).

theorem range_eq_orthogonal_ker_smul_one_sub_adjoint (hT : IsCompactOperator T)
    (hμ : μ ≠ 0) :
    LinearMap.range ((μ • 1 - T : E →L[𝕜] E).toLinearMap)
      = (LinearMap.ker ((star μ • 1 - T† : E →L[𝕜] E).toLinearMap))ᗮ

Uses 2

Proof usesAdjoint of a shifted operator · Riesz–Schauder theorem on a Hilbert space

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.