TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Compact operator sends weakly convergent sequences to norm convergent sequences

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ and $Y$ be Banach spaces over the same scalar field, let $T : X \to Y$ be a compact operator (Compact linear operator) and let $(x_{n})$ be a sequence in $X$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with $x_{n} ⇀ x$ weakly (Weak convergence of nets and sequences). Then $∥ T x_{n} - T x ∥ \to 0$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

Facts & Assumptions

[A1]

Under the Axiom of Dependent Choice, a family of bounded linear operators on a Banach space that is pointwise bounded is norm bounded (Uniform boundedness principle, Banach space); the continuous dual $X^{*}$ is Banach even when $X$ is incomplete (The continuous dual, its completeness, and evaluation), and the canonical map $J_{X} : X \to X^{* *}$ is a linear isometry (The canonical bidual map is an isometry).

[A2]

$x_{n} ⇀ x$ means $f (x_{n}) \to f (x)$ for every $f \in X^{*}$ ; the transpose satisfies $(T^{*} g) (x) = g (T x)$ and $T^{*} g \in X^{*}$ for $g \in Y^{*}$ (Weak convergence of nets and sequences, The transpose of a bounded operator, A bounded linear operator between normed spaces).

[A3]

Assume $D C$ : if a sequence fails to converge to a point then there are a real $ε > 0$ and a strictly increasing index map $j$ with $∥ T x_{n_{j}} - T x ∥ \geq ε$ for all $j$ (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , A strictly increasing index map satisfies $n_{k} \geq k$ , The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[A4]

Under $D C$ , a compact operator sends bounded sequences to sequences with convergent subsequences (Sequential characterization of compact operators, Compact linear operator).

[A5]

The dual separates points: $u \neq v$ in a normed space gives $g$ with $g (u) \neq g (v)$ (The dual space separates points of a normed space); and $A C$ implies $D C$ (AC supplies the countable and dependent choices used in Banach integration, The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

Proof

technique · direct

Given: $A C$ , Banach spaces $X, Y$ over one scalar field, a compact operator $T : X \to Y$ , a sequence $(x_{n})$ in $X$ with $x_{n} ⇀ x$ .

1.1

The sequence $(x_{n})$ is norm bounded: the operators $J_{X} x_{n} : X^{*} \to K$ are pointwise bounded because $f (x_{n}) \to f (x)$ makes $(f (x_{n}))_{n}$ a bounded scalar sequence for each $f \in X^{*}$ , so [A1] and the isometry property give $\sup_{n} ∥ x_{n} ∥ = \sup_{n} ∥ J_{X} x_{n} ∥ < \infty$ .

A1A2A5

1.2

The sequence $(T x_{n})$ converges to $T x$ weakly: for $g \in Y^{*}$ one has $g (T x_{n}) = (T^{*} g) (x_{n}) \to (T^{*} g) (x) = g (T x)$ by [A2].

1.3

If $∥ T x_{n} - T x ∥ \to̸ 0$ , then by [A3] there are $ε > 0$ and a strictly increasing $j$ with $∥ T x_{n_{j}} - T x ∥ \geq ε$ for every $j$ .

2.1

Assume $∥ T x_{n} - T x ∥ \to̸ 0$ and take $ε$ and $(x_{n_{j}})$ as in [step 1.3]. The subsequence $(x_{n_{j}})$ is bounded by [step 1.1], so [A4] gives a further subsequence $(x_{n_{j_{k}}})$ with $T x_{n_{j_{k}}} \to y$ for some $y \in Y$ .

step 1.1step 1.3A4

3.1

For every $g \in Y^{*}$ the scalar sequence $g (T x_{n_{j_{k}}})$ converges to $g (y)$ because $g$ is bounded hence continuous, and to $g (T x)$ by [step 1.2]; hence $g (y) = g (T x)$ for every $g$ , and [A5] gives $y = T x$ .

step 1.2step 2.1A2A5

4.1

But $∥ T x_{n_{j_{k}}} - T x ∥ \geq ε$ for every $k$ by [step 1.3], contradicting $T x_{n_{j_{k}}} \to T x = y$ from [step 3.1].

step 1.3step 3.1

5.1

Hence the assumption $∥ T x_{n} - T x ∥ \to̸ 0$ is false, that is, $∥ T x_{n} - T x ∥ \to 0$ .

step 4.1∎

Depends on

Used by

Relative compactness with respect to an operator Definition
Weyl's theorem: invariance of the essential spectrum Theorem

Dependency tree · two levels

63 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Theo Bühler and Dietmar Salamon, Functional Analysis — §4.2 pp.183–184, Lemma 4.21 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §6.5, weak convergence and compact operators (standard reference, not scraped)