TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

James space is complete and separable

Statement

The real James space $J$ is a separable Banach space. Its standard unit vectors $(e_{n})_{n \geq 1}$ form a Schauder basis, and the coordinate truncations $Π_{N} x = (x_{1}, \dots, x_{N}, 0, \dots)$ satisfy

$∥ Π_{N} x ∥_{J} \leq ∥ x ∥_{J}, ∥ x - Π_{N} x ∥_{J} \leq ∥ x ∥_{J}, ∥ x - Π_{N} x ∥_{J} ⟶ 0.$

Facts & Assumptions

[L0]

James coordinate $n \geq 1$ is the underlying $c_{0}$ coordinate $n - 1$ , and $e_{n}$ is supported at that coordinate (James space).

[L1]

The James formula is a norm, dominates the supremum norm, and satisfies $∥ x ∥_{J} \leq \sqrt{2} ∥ x ∥_{2}$ on $ℓ^{2}$ (The James formula defines a norm).

[L2]

Real $c_{0}$ is complete for the supremum norm (Real and complex $c_{0}$ are Banach).

[L3]

A Schauder basis requires existence and uniqueness of the norm-convergent coordinate expansion (Schauder basis and coordinate functionals).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1L1L2algebra

Let $(x^{(m)})$ be Cauchy in $J$ . By [L1] it is Cauchy in $c_{0}$ , so [L2] [given, L1, L2] gives $x^{(m)} \to x \in c_{0}$ uniformly. For each fixed tuple $p$ , $q_{p} (x) = \lim_{m} q_{p} (x^{(m)})$ , whence $\sup_{p} q_{p} (x) < \infty$ . Letting $m \to \infty$ in $q_{p} (x^{(n)} - x^{(m)}) < ε$ uniformly in $p$ yields $∥ x^{(n)} - x ∥_{J} \leq ε$ . Thus $J$ is complete.

2.1givenL0L1step 1.1

For $p = (p_{1} < \dots < p_{k})$ in the positive labeling of [L0], define the auxiliary endpoint variation

$r_{p} (x)^{2} = \frac{1}{2} (∣ x_{p_{1}} ∣^{2} + \sum_{j < k} ∣ x_{p_{j}} - x_{p_{j + 1}} ∣^{2} + ∣ x_{p_{k}} ∣^{2})$

(with $r_{(p_{1})} (x) = ∣ x_{p_{1}} ∣$ ), and $R (x) = \sup_{p} r_{p} (x)$ . Direct expansion gives $∥ x ∥_{J} \leq \sqrt{2} R (x)$ . Appending an index $m \to \infty$ to $p$ and using $x_{m} \to 0$ gives $r_{p} (x) \leq ∥ x ∥_{J}$ . Hence $2^{- 1 / 2} ∥ x ∥_{J} \leq R (x) \leq ∥ x ∥_{J}$ . [L1, endpoint expansion]

3.1givenstep 2.1

Finite-support sequences are dense. Indeed, for nonzero $x$ and $ε > 0$ , choose $δ > 0$ with $4 δ R (x) < ε^{2}$ . Choose a tuple $p$ with $r_{p} (x) > R (x) - δ$ , append a sufficiently remote final index $N = p_{k}$ so this remains true, and ensure $\sup_{i \geq N} ∣ x_{i} ∣ < δ$ . Put $ξ = Π_{N} x$ . For any tuple $q$ meeting the tail, delete its indices at most $N$ and call the remaining tuple $q^{'}$ . Concatenating $p$ and $q^{'}$ in the definition of $R (x)$ gives

$R (x)^{2} > (R (x) - δ)^{2} - δ^{2} + r_{q^{'}} (x)^{2}, r_{q^{'}} (x)^{2} < 2 δ R (x) .$

Thus $R (x - ξ)^{2} < 2 δ R (x)$ , and step 2.1 gives $∥ x - ξ ∥_{J}^{2} < 4 δ R (x) < ε^{2}$ . The zero vector is already finite support. [step 2.1, finite concatenation, $x \in c_{0}$ ]

4.1step 2.1algebra

Fix a tuple $q$ . If it lies wholly before or after $N$ , the two [given, step 2.1, step 3.1] contractive estimates for $Π_{N} x$ and $x - Π_{N} x$ are immediate. If it crosses $N$ , delete respectively the tail or the head. Expanding the one new jump to zero shows that the resulting $q$ -variation equals an auxiliary endpoint variation $r_{q^{'}} (x)$ , hence is at most $R (x) \leq ∥ x ∥_{J}$ by step 2.1. Taking suprema proves both contractive inequalities.

5.1L0L3step 3.14.1

Given $x$ and $ε > 0$ , step 3.1 gives finite-support $u$ with [given, L0, L3, step 3.1, step 4.1] $∥ x - u ∥_{J} < ε$ . For $N$ beyond its support, step 4.1 gives $∥ x - Π_{N} x ∥_{J} = ∥ (I - Π_{N}) (x - u) ∥_{J} \leq ∥ x - u ∥_{J} < ε$ . Coordinatewise uniqueness in the labeling of [L0] is immediate, so [L3] makes $(e_{n})$ a Schauder basis.

6.1step 3.1algebra∎

Finite-support sequences with rational coordinates form a countable set. [given, step 3.1, step 5.1] They are dense by step 3.1 and finite-dimensional rational approximation, so $J$ is separable.

Depends on

Used by

Dual and bidual models for James space Lemma

Dependency tree · two levels

10 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 (standard reference, not scraped)