Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 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.

Riesz Schauder ascent and descent stabilize

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain). Let X be a Banach space over R or C, let K:X→X be a compact operator (Compact linear operator) and put A:=I−K. Then there is m0∈N such that for every n≥m0

ker⁡An=ker⁡Am0,ran⁡An=ran⁡Am0,

and for every such m the following hold:

  1. X=ker⁡Am⊕ran⁡Am as a direct sum of linear subspaces;
  2. ker⁡Am is finite dimensional (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) and ran⁡Am is closed in X;
  3. A maps ran⁡Am bijectively onto itself, and the restricted map ran⁡Am→ran⁡Am, y↦Ay, is a bounded linear isomorphism with bounded inverse (Bounded inverse theorem).

Facts & Assumptions

[A1]

For every n≥1 there is a compact Kn with An=I−Kn: A=I−K, and if An=I−Kn with Kn compact then An+1=(I−Kn)A=I−Kn−K+KnK, where Kn+K−KnK is compact by the ideal and linear-subspace properties (Compositions with a compact operator are compact, Linear combinations of compact operators are compact, Compact linear operator, A bounded linear operator between normed spaces).

[A2]

For compact C the kernel ker⁡(I−C) is finite dimensional (Kernel of identity minus compact is finite dimensional) and ran⁡(I−C) is closed, with dist⁡(x,ker⁡(I−C))≤C0∥(I−C)x∥ for some real C0>0 (Range of identity minus compact is closed, The quotient seminorm ∥x+M∥X/M=inf⁡m∈M∥x+m∥=dist⁡(x,M)).

[A3]

Riesz lemma: for a proper closed subspace M of a normed space and 0<α<1 there is x with ∥x∥=1 and dist⁡(x,M)>α (Riesz lemma, The quotient seminorm ∥x+M∥X/M=inf⁡m∈M∥x+m∥=dist⁡(x,M), A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[A4]

Under DC, Countable Choice is available, and a compact operator sends bounded sequences to sequences with convergent subsequences (Dependent choice implies countable choice, Sequential characterization of compact operators, Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R); a subsequence of a bounded sequence is bounded.

[A5]

A closed linear subspace of a Banach space is a Banach space (A closed subspace of a Banach space is Banach), and a bounded bijection between Banach spaces has a bounded inverse (Bounded inverse theorem, Banach space).

Proof

technique · direct

Given: DC, a Banach space X over R or C, a compact K:X→X, and A=I−K.

1.1A1

For every n≥1 the operator An equals I−Kn with Kn compact.

2.1step 1.1A2

For every n≥1 the kernel ker⁡An is finite dimensional with ker⁡An⊆ker⁡An+1, and the range ran⁡An is closed with ran⁡An+1⊆ran⁡An.

3.1step 2.1A3

For every n with ker⁡An≠ker⁡An+1, the finite-dimensional subspace ker⁡An is closed in the normed space ker⁡An+1, so Riesz's lemma gives x∈ker⁡An+1 with ∥x∥=1 and dist⁡(x,ker⁡An)>1/2 (A finite-dimensional normed subspace is closed).

3.2step 2.1A3

For every n with ran⁡An≠ran⁡An+1 there is x∈ran⁡An with ∥x∥=1 and dist⁡(x,ran⁡An+1)>1/2, the distance being computed in X.

4.1step 3.1A4

The chain ker⁡An stabilizes: if ker⁡An≠ker⁡An+1 for every n, Countable Choice in [A4] applied to [step 3.1] gives unit vectors xn∈ker⁡An+1 with dist⁡(xn,ker⁡An)>1/2; for m<n one has xm∈ker⁡An, Axm∈ker⁡An and Axn∈ker⁡An, so Kxn−Kxm=xn−(xm+Axn−Axm) is at distance >1/2 from 0, and the bounded sequence (Kxn) has no convergent subsequence, contradicting [A4].

4.2step 3.2A4

The chain ran⁡An stabilizes: if ran⁡An≠ran⁡An+1 for every n, Countable Choice in [A4] applied to [step 3.2] gives unit vectors xn∈ran⁡An with dist⁡(xn,ran⁡An+1)>1/2; for m>n one has xm∈ran⁡An+1, Axn∈ran⁡An+1 and Axm∈ran⁡An+1, so Kxn−Kxm=xn−(xm+Axn−Axm) has norm >1/2, and the bounded sequence (Kxn) has no convergent subsequence, contradicting [A4].

5.1step 4.1step 4.2

Choose m so that both chains are constant from m onward by [step 4.1] and [step 4.2], and put N:=ker⁡Am, Y:=ran⁡Am. Then X=N+Y: for x∈X the element Amx lies in Y=ran⁡A2m, so Amx=A2my for some y∈X, and x−Amy∈N.

6.1step 5.1

Under the choice of [step 5.1] one has N∩Y={0}: if x∈N∩Y, say x=Amy with Amx=0, then A2my=0, so y∈ker⁡A2m=ker⁡Am by [step 4.1] and x=Amy=0.

6.2step 5.1

Under the choice of [step 5.1], A(Y)=Y: A(Y)=A(AmX)=Am+1X=Y by the stabilization of [step 4.2].

7.1step 5.1step 6.1step 2.1

Under the choice of [step 5.1], X=N⊕Y, and N is finite dimensional and Y is closed by [step 2.1].

8.1step 7.1

Under the choice of [step 5.1], the restriction A∣Y is injective: if Ay=0 with y=Amz∈Y, then Am+1z=0, so z∈ker⁡Am+1=ker⁡Am by [step 4.1] and y=Amz=0.

9.1step 7.1step 6.2step 8.1A5

Under the choice of [step 5.1], A∣Y:Y→Y is a bounded bijection by [step 6.2] and [step 8.1], and Y is a Banach space by [step 7.1] and [A5], so the inverse (A∣Y)−1 is bounded by [A5].

10.1step 5.1step 7.1step 6.2step 9.1∎

Taking m0:=m from [step 5.1] gives the stabilization, and [step 7.1], [step 6.2] and [step 9.1] give the decomposition, the finite-dimensional kernel, the closed range and the bounded isomorphism on that range; every larger m works as well because the chains are constant from m0 onward.

Depends on

Used by

Dependency tree · two levels

95 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