Complete continuity of compact operators

TheoremComplete continuity of compact operators#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) and \(F\) be normed spaces over \(\mathbb{K}\), and let \(T : E \to F\) be a compact continuous linear operator. If a sequence \((u_n)\) in \(E\) converges weakly to \(x \in E\), that is, \(f(u_n) \to f(x)\) for every continuous linear functional \(f : E \to \mathbb{K}\), then \(T u_n \to T x\) in norm.

The proof is the standard subsequence argument: if \(T u_n\) did not converge in norm to \(T x\), some subsequence would stay \(\varepsilon\)-away from \(T x\); the sequence \((u_n)\) is norm-bounded by uniform boundedness, so compactness gives a further subsequence of \((T u_n)\) converging in norm to some \(a\); but \(T\) preserves weak convergence, so \(a = T x\) by uniqueness of scalar limits and the fact that the dual separates points, contradicting the \(\varepsilon\)-separation.

theorem tendsto_apply_of_isCompactOperator_of_forall_tendsto {T : E →L[𝕜] F}
    (hT : IsCompactOperator (T : E → F)) {u : ℕ → E} {x : E}
    (h : ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 (f x))) :
    Tendsto (fun n => T (u n)) atTop (𝓝 (T x))

Uses 2 · Used by 2

Proof usesWeakly convergent sequences are norm-bounded · Bounded operators preserve weak convergence

Used byCompact operators send weakly null sequences to norm null sequences · Complete continuity of compact operators, weak-topology form

TheoremCompact operators send weakly null sequences to norm null sequences#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) and \(F\) be normed spaces over \(\mathbb{K}\), and let \(T : E \to F\) be a compact continuous linear operator. If a sequence \((u_n)\) in \(E\) converges weakly to \(0\), that is, \(f(u_n) \to 0\) for every continuous linear functional \(f : E \to \mathbb{K}\), then \(T u_n \to 0\) in norm.

theorem tendsto_apply_of_isCompactOperator_of_tendsto_zero {T : E →L[𝕜] F}
    (hT : IsCompactOperator (T : E → F)) {u : ℕ → E}
    (h : ∀ f : StrongDual 𝕜 E, Tendsto (fun n => f (u n)) atTop (𝓝 0)) :
    Tendsto (fun n => T (u n)) atTop (𝓝 0)

Uses 1

Proof usesComplete continuity of compact operators

TheoremComplete continuity of compact operators, weak-topology form#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(E\) and \(F\) be normed spaces over \(\mathbb{K}\), and let \(T : E \to F\) be a compact continuous linear operator. If a sequence \((u_n)\) in \(E\) converges to \(x \in E\) in the weak topology of \(E\), then \(T u_n \to T x\) in norm.

theorem tendsto_apply_of_isCompactOperator_of_tendsto_weakSpace
    {T : E →L[𝕜] F} (hT : IsCompactOperator (T : E → F)) {u : ℕ → E} {x : E}
    (h : Tendsto (fun n => toWeakSpace 𝕜 E (u n)) atTop (𝓝 (toWeakSpace 𝕜 E x))) :
    Tendsto (fun n => T (u n)) atTop (𝓝 (T x))

Uses 2

Proof usesWeak convergence gives convergence under every functional · Complete continuity of compact operators

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.