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 partial sums on c_0
Example
Let or and with the supremum norm and coordinates indexed by . Define if and otherwise. For put Then is Banach, each is bounded linear, for each , and for every . These assertions are choice-free. Under , the sequential uniform boundedness theorem also supplies a qualitative uniform bound.
Facts & Assumptions
Given: The specified field, space, coordinate vectors, and finite truncations.
consists of bounded null sequences, with coordinatewise operations and the supremum norm (The sequence spaces c_0 and ell-infinity).
Every nonempty bounded-above set of reals has a supremum (The Cauchy-sequence reals have the least-upper-bound property); applying this to negatives also supplies infima of nonempty bounded-below sets.
Complex norms use the modulus; norm-metric completeness has the same meaning over either scalar field (Real and complex scalar conventions for normed spaces). Modulus is definite, multiplicative, and subadditive (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Replacement forms the image of a set under a uniquely specified assignment (The Axiom Schema of Replacement: for each formula , if defines a class function on then its image on is a set).
A normed space is Banach if every norm-Cauchy sequence converges in it (Banach space).
Finite vector sums start at the zero vector and append one summand at each successor (Linear combination of a finite list, and the span as the smallest linear subspace containing ).
A linear map with a bound is bounded (A bounded linear operator between normed spaces).
The norm of a bounded operator is its unit-ball supremum (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).
Under , a pointwise bounded sequence from a Banach space to a normed space has uniformly bounded operator norms (Sequential uniform boundedness under countable choice).
Verification
We first prove scalar completeness from the real supremum property. A real Cauchy sequence is bounded: take with for and successively take the larger of and each of . This finite process produces a bound . Each tail has a unique infimum in , and exists. Given , take with for . For fixed and every , all terms in the -tail are in , so its nonempty tail has infimum in that same interval. For , . Thus . Using proves . If two scalar limits differed by , sufficiently late terms within of both would give by triangle inequality. Hence the limit is unique.
Each is a null sequence of norm one. Computing each coordinate in the finite sum gives for and for : when the sole nonzero contribution is , and otherwise every contribution is zero. This calculation follows directly from appending the summands in the recursive finite sum. Thus is eventually zero and lies in . At each coordinate, , so is linear. Also for all , hence and is bounded.
For , the modulus formula yields : the first inequalities follow from , and the last from , comparing nonnegative squares. Therefore the real and imaginary parts of a complex Cauchy sequence are real Cauchy sequences. Their unique limits from step 1.1 give complex limit , since the modulus of the difference is bounded by the sum of the two coordinate errors. The scalar triangle inequality again proves uniqueness.
The estimate in step 1.2 bounds the unit-ball image by . Since and , this image contains as a norm value. Its supremum is therefore exactly for every , including the one-coordinate projection . Also .
The coordinate formula gives . Given , take with for . For the tail supremum is at most , proving . If already vanishes beyond , the error is exactly zero for .
Let be any norm-Cauchy sequence in . For each fixed , , so the coordinate sequence is scalar Cauchy and has a unique limit . Replacement applied on to the unique pair produces a set of these pairs, the graph of a function . This uses unique existence, not a choice of witnesses from non-singleton sets.
If for , then for fixed and , the scalar triangle inequality gives . Since the last term tends to zero, ; a positive excess would be contradicted by making that term smaller than half the excess. Taking and one such gives for every , so is bounded. All subsequent suprema are legitimate by the real supremum property. Thus for general the uniform coordinate bound implies for . Taking proves norm convergence in the bounded-sequence space.
Given , take one with , and then with for , since . For such , . Hence , and the arbitrary Cauchy sequence converges in . This proves is Banach over both fields. The choices here concern a single given ; no simultaneous selection is used.
Under , apply the sequential theorem with domain and codomain : step 5.1 proves the domain Banach, step 1.2 supplies bounded linear maps and the pointwise bound . Its conclusion is a finite common bound for the . Step 2.2 has already computed that bound as without any choice principle, and step 2.3 proves the promised convergence.
Remarks
This concrete example is library-generated. The local completeness proof develops the coordinate-limit method in MIT 18.102 notes, Theorem 16 and following exercise, printed pp.5–6; those notes leave the case as an exercise. Neither a general basis theorem nor another examples page supplies a premise here.
Depends on
- Sequential uniform boundedness under countable choice
- The sequence spaces c_0 and ell-infinity
- The Cauchy-sequence reals have the least-upper-bound property
- Banach space
- A bounded linear operator between normed spaces
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum
- Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$
- Real and complex scalar conventions for normed spaces
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- The Axiom Schema of Replacement: for each formula $\varphi$, if $\varphi$ defines a class function on $A$ then its image on $A$ is a set
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
47 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
- Lin and Rodriguez, MIT 18.102 Complete Lecture Notes (standard reference, not scraped)