Fredholm alternative

TheoremThe kernel of a scalar minus an operator is an eigenspace#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a bounded linear operator on \(H\), let \(I\) be the identity of \(H\), and let \(\mu \in \mathbb{K}\). Then the kernel of \(\mu I - T\) equals the eigenspace \(\{x \in H : T x = \mu x\}\) of \(T\) for \(\mu\).

theorem ker_smul_id_sub_eq_eigenspace (T : H →L[𝕜] H) (μ : 𝕜) :
    LinearMap.ker (μ • (ContinuousLinearMap.id 𝕜 H) - T).toLinearMap =
      Module.End.eigenspace (T.toLinearMap) μ

Used by 1

Used byFredholm alternative for compact self-adjoint operators

TheoremFredholm alternative for compact self-adjoint operators#✓fully proved

Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a compact self-adjoint bounded operator on \(H\), let \(I\) be the identity of \(H\), and let \(\mu \in \mathbb{K}\) with \(\mu \neq 0\). Then the range of \(\mu I - T\) equals the orthogonal complement \((\ker(\mu I - T))^\perp\) of its kernel, and either \(\mu I - T\) is bijective, or its kernel is nonzero and finite-dimensional.

theorem fredholm_alternative_of_isCompactOperator_isSelfAdjoint
    {T : H →L[𝕜] H} (hT : IsCompactOperator (T : H → H)) (hsa : IsSelfAdjoint T)
    {μ : 𝕜} (hμ : μ ≠ 0) :
    LinearMap.range (μ • (ContinuousLinearMap.id 𝕜 H) - T).toLinearMap =
      (LinearMap.ker (μ • (ContinuousLinearMap.id 𝕜 H) - T).toLinearMap).orthogonal ∧
    (Function.Bijective (μ • (ContinuousLinearMap.id 𝕜 H) - T) ∨
      (LinearMap.ker (μ • (ContinuousLinearMap.id 𝕜 H) - T).toLinearMap ≠ ⊥ ∧
       FiniteDimensional 𝕜
         (LinearMap.ker (μ • (ContinuousLinearMap.id 𝕜 H) - T).toLinearMap)))

Uses 1 · Used by 2

Proof usesThe kernel of a scalar minus an operator is an eigenspace

Used byFredholm alternative for compact self-adjoint operators, operator-minus-scalar form · Closed range for compact self-adjoint perturbations of nonzero scalars

TheoremClosed range for compact self-adjoint perturbations of nonzero scalars#✓fully proved

Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a compact self-adjoint bounded operator on \(H\), let \(I\) be the identity of \(H\), and let \(\mu \in \mathbb{K}\) with \(\mu \neq 0\). Then the range of \(\mu I - T\) is a closed subset of \(H\).

theorem isClosed_range_smul_id_sub_of_isCompactOperator_isSelfAdjoint
    {T : H →L[𝕜] H} (hT : IsCompactOperator (T : H → H)) (hsa : IsSelfAdjoint T)
    {μ : 𝕜} (hμ : μ ≠ 0) :
    IsClosed (LinearMap.range (μ • (ContinuousLinearMap.id 𝕜 H) - T).toLinearMap : Set H)

Uses 1

Proof usesFredholm alternative for compact self-adjoint operators

TheoremFredholm alternative for compact self-adjoint operators, operator-minus-scalar form#✓fully proved

Let \(H\) be a Hilbert space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a compact self-adjoint bounded operator on \(H\), let \(I\) be the identity of \(H\), and let \(\mu \in \mathbb{K}\) with \(\mu \neq 0\). Then the range of \(T - \mu I\) equals the orthogonal complement \((\ker(T - \mu I))^\perp\) of its kernel, and either \(T - \mu I\) is bijective, or its kernel is nonzero and finite-dimensional.

This differs from the \(\mu I - T\) form of the Fredholm alternative only by a sign.

theorem fredholm_alternative_sub_of_isCompactOperator_isSelfAdjoint
    {T : H →L[𝕜] H} (hT : IsCompactOperator (T : H → H)) (hsa : IsSelfAdjoint T)
    {μ : 𝕜} (hμ : μ ≠ 0) :
    LinearMap.range (T - μ • (ContinuousLinearMap.id 𝕜 H)).toLinearMap =
      (LinearMap.ker (T - μ • (ContinuousLinearMap.id 𝕜 H)).toLinearMap).orthogonal ∧
    (Function.Bijective (T - μ • (ContinuousLinearMap.id 𝕜 H)) ∨
      (LinearMap.ker (T - μ • (ContinuousLinearMap.id 𝕜 H)).toLinearMap ≠ ⊥ ∧
       FiniteDimensional 𝕜
         (LinearMap.ker (T - μ • (ContinuousLinearMap.id 𝕜 H)).toLinearMap)))

Uses 1

Proof usesFredholm alternative for compact self-adjoint operators

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.