ExampleConstruction: Literature-sourcedVerification: 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.

Standard Schauder bases of c0 and ell-p

Example

For $c_{0}$ and for $ℓ^{p}$ , $1 \leq p < \infty$ , let $(e_{n})_{n \geq 1}$ be the standard unit vectors indexed so that $e_{n}$ is $1$ in coordinate $n - 1$ and $0$ elsewhere. They form a Schauder basis. Their coordinate truncations are contractions, so the basis constant is exactly one in every nonzero case.

Facts & Assumptions

[L1]

Finite truncations converge in $c_{0}$ and $ℓ^{1}$ (Finite truncations approximate null and summable sequences).

[L2]

$ℓ^{p}$ is $L^{p}$ of counting measure, with its usual series norm ( $ℓ^{p}$ is the $L^{p}$ space of counting measure).

[L3]

The basis constant is the supremum of coordinate-truncation norms (Partial-sum projections and basis constant).

Verification

technique · direct

Given: The objects and hypotheses in the Statement.

1.1

For $N \geq 1$ , $P_{N}$ retains coordinates $0, \dots, N - 1$ , and $P_{0} = 0$ . [given, L1, L2] Thus in $c_{0}$ , [L1] (with its truncation index $N - 1$ ) gives $P_{N} x \to x$ in supremum norm. In $ℓ^{p}$ , [L2] gives $∥ x - P_{N} x ∥_{p}^{p} = \sum_{m \geq N} ∣ x_{m} ∣^{p} \to 0$ ; for $p = 1$ this is also [L1]. The coefficients are necessarily the coordinates, so the expansions are unique.

L1L2

2.1

Deleting coordinates cannot increase either the supremum norm or the [given, L3, step 1.1] $p$ -norm, hence $∥ P_{N} ∥ \leq 1$ . In a nonzero space $P_{N} e_{1} = e_{1}$ for $N \geq 1$ , so $∥ P_{N} ∥ = 1$ and [L3] gives basis constant one.

L3coordinate calculation∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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)