Schauder's theorem on compact adjoints

TheoremThe adjoint of a finite-rank operator is compact#✓fully proved

Let \(E\) and \(F\) be Hilbert spaces over \(\mathbb{R}\) or \(\mathbb{C}\). If a bounded linear operator \(T : E \to F\) has finite-dimensional range, then its adjoint \(T^* : F \to E\) is a compact operator.

The proof factors \(T\) through its range \(R\) as \(T = i \circ \pi\), where \(\pi : E \to R\) is \(T\) with its codomain restricted to \(R\) and \(i : R \to F\) is the inclusion. Then \(T^* = \pi^* \circ i^*\), and \(\pi^*\) is compact because its domain \(R\) is finite-dimensional, hence locally compact.

theorem isCompactOperator_adjoint_of_finiteRank {T : E →L[𝕜] F}
    (hT : FiniteDimensional 𝕜 ↥(LinearMap.range (T : E →ₗ[𝕜] F))) :
    IsCompactOperator (ContinuousLinearMap.adjoint T : F → E)

Used by 1

Used bySchauder's theorem

TheoremSchauder's theorem#✓fully proved

The adjoint of a compact operator between Hilbert spaces is compact.

theorem isCompactOperator_adjoint {T : E →L[𝕜] F}
    (hT : IsCompactOperator (T : E → F)) :
    IsCompactOperator (ContinuousLinearMap.adjoint T : F → E)

Uses 1 · Used by 1

Proof usesThe adjoint of a finite-rank operator is compact

Used bySchauder's theorem, iff form

TheoremSchauder's theorem, iff form#✓fully proved

A bounded operator between Hilbert spaces is compact if and only if its adjoint is compact.

theorem isCompactOperator_adjoint_iff {T : E →L[𝕜] F} :
    IsCompactOperator (ContinuousLinearMap.adjoint T : F → E) ↔
      IsCompactOperator (T : E → F)

Uses 1

Proof usesSchauder's theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.