TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Coordinate functionals of a Schauder basis are bounded

Statement

Assume DC. If $(e_{n})_{n \geq 1}$ is a Schauder basis of a Banach space $X$ , then every coordinate functional $e_{n}^{*}$ and every partial-sum projection $P_{N}$ is bounded. Moreover

$K : = \sup_{N \geq 0} ∥ P_{N} ∥ < \infty .$

Facts & Assumptions

[A1]

The Axiom of Dependent Choice holds (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[L1]

The coefficient space $E$ is Banach and its summation map $S : E \to X$ is a bounded linear bijection (The Schauder coefficient space is Banach).

[L2]

Under DC, a bounded linear bijection between Banach spaces has bounded inverse (Bounded inverse theorem).

[L3]

$P_{N} x = \sum_{n \leq N} e_{n}^{*} (x) e_{n}$ and the basis constant is the supremum of their norms (Partial-sum projections and basis constant).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1

Apply [L2] to [L1]. The only choice use is [A1], through that bounded-inverse [given, L2, L1, A1] theorem. Thus $S^{- 1} : X \to E$ is bounded.

A1L1L2

2.1

Truncation $Q_{N} : E \to E$ , $(a_{n}) \mapsto (a_{1}, \dots, a_{N}, 0, \dots)$ , satisfies $∥ Q_{N} a ∥_{E} \leq ∥ a ∥_{E}$ , because every partial sum of $Q_{N} a$ is a partial sum of $a$ . Since $P_{N} = S Q_{N} S^{- 1}$ and $∥ S ∥ \leq 1$ ,

givenL1L3step 1.1

$∥ P_{N} ∥ \leq ∥ S^{- 1} ∥$

for every $N$ , including $N = 0$ . Hence $K < \infty$ . [L1, L3, step 1.1]

3.1

For $n \geq 1$ ,

givenL3step 2.1

$e_{n}^{*} (x) e_{n} = (P_{n} - P_{n - 1}) x .$

Because $e_{n} \neq 0$ , taking norms gives $∣ e_{n}^{*} (x) ∣ \leq (∥ P_{n} ∥ + ∥ P_{n - 1} ∥) ∥ x ∥ / ∥ e_{n} ∥$ . Thus every $e_{n}^{*}$ is bounded. [L3, step 2.1] ∎

Depends on

Used by

Dependency tree · two levels

14 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

Thomas Schlumprecht, Course Notes in Functional Analysis, Math 655 (standard reference, not scraped)