Finite-rank approximation of compact operators

TheoremFinite-rank approximation of compact operators#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\) (\(H\) need not be complete), and let \(T\) be a compact bounded linear operator on \(H\). For every real \(\varepsilon > 0\) there is a bounded linear operator \(F\) on \(H\) with finite-dimensional range such that \(\|T - F\| \le \varepsilon\).

The approximant is the composition of \(T\) with the orthogonal projection onto the span of a finite \(\varepsilon\)-net for the image of the closed unit ball.

theorem exists_finiteRank_approx (T : H →L[𝕜] H)
    (hc : IsCompactOperator (T : H → H)) {ε : ℝ} (hε : 0 < ε) :
    ∃ F : H →L[𝕜] H,
      FiniteDimensional 𝕜 ↥(LinearMap.range (F : H →ₗ[𝕜] H)) ∧ ‖T - F‖ ≤ ε

Used by 1

Used byCompact operators are norm limits of finite-rank operators

TheoremCompact operators are norm limits of finite-rank operators#✓fully proved

Let \(H\) be an inner product space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\) (\(H\) need not be complete), and let \(T\) be a compact bounded linear operator on \(H\). Then there is a sequence \((F_n)_{n \in \mathbb{N}}\) of bounded linear operators on \(H\), each with finite-dimensional range, such that \(\|T - F_n\| \to 0\) as \(n \to \infty\).

theorem exists_tendsto_finiteRank_approx (T : H →L[𝕜] H)
    (hc : IsCompactOperator (T : H → H)) :
    ∃ F : ℕ → H →L[𝕜] H,
      (∀ n, FiniteDimensional 𝕜 ↥(LinearMap.range (F n : H →ₗ[𝕜] H))) ∧
      Tendsto (fun n => ‖T - F n‖) atTop (𝓝 0)

Uses 1

Proof usesFinite-rank approximation of compact operators

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.