Alphabeta Math
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.

Schauder compact adjoint theorem

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let X and Y be Banach spaces over the same scalar field and let T:XY be a bounded linear operator (A bounded linear operator between normed spaces), with transpose T:YX (The transpose of a bounded operator, The dual space X^* of a normed space and its dual norm). Then T is compact (Compact linear operator) if and only if T is compact.

Facts & Assumptions

[A1]

S is compact exactly when S(BX) is compact (Compact linear operator); the transpose is the bounded linear map (Sh)(x)=h(Sx) with S=S (The transpose of a bounded operator, The transpose is bounded with the same norm, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A4]

A compact metric space has a finite subcover of every open cover; the balls centred at points of a nonempty compact set cover it, and choosing one index per member of a finite subcover is choice-free (Open cover, subcover, compact metric space, and compact subset of a metric space, Open ball, closed ball and sphere in a metric space, Every natural-number-indexed list of nonempty sets has a choice function on its family of values). An at most countable union of finite sets is at most countable under ACω (Countable unions of at most countable sets, assuming ACω).

[A6]

The canonical maps JX:XX are linear isometries (The canonical bidual map is an isometry) with SJX=JYS for bounded S (The canonical map is natural); an isometric image of a Banach space is a closed subspace (Closed subspaces of complete metric spaces are complete; the converse under countable choice).

[A7]

If S is compact and C is bounded linear, then CS and SC are compact (Compositions with a compact operator are compact).

Proof

technique · direct

Given: AC, Banach spaces X,Y over one scalar field, a bounded linear S:XY, the transpose S:YX, the closed unit balls BX,BY, and Θ:=S(BX).

1.1

Every bounded sequence in K has a convergent subsequence.

A5
1.2

If S is compact then Θ is compact by [A1], so for every real δ>0 there are finitely many points x0,,xmBX with ΘimB(Sxi,δ): the balls ΘB(Sx,δ), xBX, cover Θ by [A5], compactness gives a finite subcover, and one index per member of that finite subcover may be chosen by [A4].

A1A4A5
1.3

The dual X is Banach by [A2], so the set C:=S(BY)X is a complete metric space by [A2].

A2
1.4

If K is a compact operator and M is a closed subspace of its target containing K(X), then the corestriction K0:XM is compact: for bounded EX the closure of K0(E) in M equals K(E)M, a closed subset of the compact set K(E).

A1
1.5

The space JY(Y) is a closed subspace of Y and the inverse of JY:YJY(Y) is a bounded isometry, by [A6].

A6
2.1

Under the hypothesis of [step 1.2], the union D of the finite (1/(k+1))-nets of Θ obtained from [step 1.2] for kN is at most countable and dense in Θ, the nets being chosen together by ACω and their union counted by [A4]; hence there is a surjection ND listing D as (dj).

step 1.2A3A4
2.2

If (gn) is a sequence in BY and D=(dj) is a countable subset of Y, then there are a strictly increasing index map n:NN and scalars to which gnj(dk) converges for all j,k: for each fixed dk the scalar sequence gn(dk) is bounded by dk and has a convergent subsequence by [step 1.1], and the standard diagonal selection of nested subsequences is licensed by DC.

step 1.1A3
3.1

Assume S compact and let (gn) be a sequence in BY. With D as in [step 2.1], [step 2.2] gives a subsequence (gnj) with gnj(d) convergent for every dD. Given a real ε>0, choose k with 1/(k+1)<ε/4 and let FkBX be the finite net of [step 1.2] for δ=1/(k+1); convergence on the finite set Fk gives J with (gnjgnl)(Sxi)<ε/2 for all j,lJ and all im, and for xBX one has SxSxi<ε/4 for some i, so (SgnjSgnl)(x)(gnjgnl)(Sxi)+gnjgnlSxSxi<ε/2+2ε/4=ε; hence (Sgnj) is Cauchy in X.

step 2.1step 2.2A1A4
4.1

Under the hypothesis of [step 3.1] the Cauchy sequence (Sgnj) converges in the complete space X by [step 1.3], and its limit lies in C because every SgnjS(BY)C and C is closed; so every sequence in S(BY) has a subsequence converging in C.

step 1.3step 3.1
5.1

Under the hypothesis of [step 3.1], every sequence (yn) in C has a subsequence converging in C: choosing gnBY with ynSgn<1/(n+1) for every n is a countable selection licensed by [A3], and applying [step 4.1] to (gn) yields a subsequence with SgnjyC, whence ynjy.

step 4.1A3A5
6.1

Under the hypothesis of [step 3.1] the space C is sequentially compact by [step 5.1], hence compact by [A3], and then S is compact by [A1].

step 5.1A1A3
7.1

Suppose now that T:YX is compact. Both X and Y are Banach by [A2], so [step 6.1] applied to the bounded linear operator T between Banach spaces gives that (T)=T is compact; with [step 1.5] and [A6], TJX=JYT, so TJX is compact by [A7], and T=JY1(TJX) is the composite of the corestriction of TJX to the closed subspace JY(Y) — compact by [step 1.4] — with the bounded operator JY1, hence compact by [A7].

step 1.4step 1.5step 6.1A2A6A7
8.1

Conversely, if T is compact then T is compact by [step 6.1]; and if T is compact then T is compact by [step 7.1]; this is the asserted equivalence.

step 6.1step 7.1

Depends on

Used by

Dependency tree · two levels

111 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