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 convex-block norm-attainment criterion
Statement
Assume the Axiom of Dependent Choice (DC) and the relative Hahn–Banach principle HB. Let be a real Banach space, let , and let be a sequence in . For every bounded sequence in put
Suppose
where is the finite convex hull. If is any sequence of positive reals with , then there are and a sequence in such that, for every ,
and, for every ,
In addition, assume the ultrafilter lemma. If is nonreflexive, then some does not attain its norm on .
Facts & Assumptions
Given: DC, HB, a real Banach space , , a dual-ball sequence satisfying the displayed separation, and positive weights of sum one. The ultrafilter lemma is assumed only for the final nonreflexive consequence.
For a bounded real sequence, limsup and liminf are finite real numbers; limsup is subadditive, reflection exchanges limsup and liminf, and liminf is realized by a subsequence (Limit superior and limit inferior of a real sequence as and in , The tail suprema of any real sequence are nonincreasing in , so the limit superior exists for every sequence, whenever the right-hand side is defined in , and dually for , , with the reflection of exchanging , The limit inferior is the least subsequential limit in ).
Under HB, a real linear functional dominated by a sublinear functional extends to the whole real vector space (Dominated extension conditional on the relative principle, The real dominated-extension principle as an additional hypothesis over ZF).
Nonempty real sets bounded below have infima, and bounded monotone real sequences converge to the corresponding supremum or infimum (Every nonempty set bounded below has an infimum, A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).
The dual norm is the supremum of absolute values on the closed unit ball. Since the scalar field is complete, is Banach, and every absolutely convergent series in it converges (The dual space X^* of a normed space and its dual norm, If (Y) is Banach then (\mathcal B(X,Y)) is Banach, Series criterion for Banach spaces, Series and absolute convergence in a normed space).
DC supplies an infinite chain through any entire relation on a nonempty set (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain).
A strictly increasing subsequence index map satisfies , and the real geometric-series formula holds for every ratio of absolute value less than one (A strictly increasing index map satisfies , For , , and for the series diverges).
Under the ultrafilter lemma, DC and HB, every nonreflexive real Banach space has the annihilator-separated pointwise-null dual-ball sequence of James nonreflexivity sequence separated from an annihilator. Its ultrafilter-lemma input is the compact-Hausdorff Tychonoff theorem (Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact).
Proof
We first record two elementary properties of . For a bounded sequence , say , the function is finite, positively homogeneous, and subadditive: homogeneity follows directly from tail suprema and subadditivity from [F1]. Apply [F2] to the zero functional on dominated by . The extension satisfies , while applying this inequality at and using [F1] gives . Hence , so and . Thus is nonempty and, when , lies in .
Let be the set of sequences for which at every . It is nonempty because . For each , every such convex combination satisfies , so the receding-tail definition gives and therefore . Flattening two finite convex combinations proves when . A subsequence of also belongs to : its th index is at least by [F6].
Reindex the weights by positive integers, for . Extend the corresponding reindexing of the dual sequence to a genuine zero-based library sequence by setting and for . The duplicate initial term does not change any scalar limsup, so , and . Put , so , , every , and . Choose explicitly . Then and [F6] gives \sum_{m=1}^\infty\frac{b_m\varepsilon_m}{T_mT_{m+1}}\le(1-\theta)\sum_{m=1}^\infty2^{-m-1}=\frac{1-\theta}{2}<1-\theta.\tag{1}
Now additionally assume the ultrafilter lemma and that is nonreflexive. Apply [F7] with the same to obtain and , pointwise null on , with its convex hull at distance at least from . If , then for the defining inequality at and gives and . Hence , and the separation hypothesis of the technical criterion holds.
Set . Suppose that and the sequences have been constructed. For and , define and let be the infimum, over all such , of . Step 1.1 makes every nonempty. All displayed functionals have norm at most two, because all the convex blocks and all members of lie in the dual unit ball; hence and [F3] makes the infimum legitimate.
For , any admissible is in the convex hull of the original sequence and by steps 1.2–1.3. The separation hypothesis therefore gives for every admissible , so .
Suppose . The induction will arrange that is a subsequence of some . Consequently by step 1.2. For an admissible at stage , both and lie in , and so does Also by flattening. Since every stage- candidate supplies a stage- candidate of the same supremum. Hence . Together with step 3.1, for all .
The definition of the positive number supplies and such that \alpha_m\le\sup S_m(y_m^*,z^{(m)})<\alpha_m(1+\varepsilon_m).\tag{2} Because , choose for which the norm inside (2) is greater than . By [F4] and the balance of , there is on which the same functional, without absolute-value signs, has value greater than that number. The bounded scalar sequence has a subsequence converging to its liminf by [F1]; denote the corresponding dual sequence by .
These choices depend on the whole finite history. Let the state set consist of all finite histories satisfying step 5.1, beginning with the empty history and , and relate a history to each valid one-stage extension. Step 5.1 proves that every state has a successor. Applying DC once produces all with (2) and the strict lower inequality. No simultaneous selection outside this DC application is being hidden.
The induction has produced the positive-indexed family . Make it a genuine sequence by putting and for . For fixed and every , repeated flattening of the relations in steps 4.1–5.1 gives . Ignoring the single duplicated initial term in , the tail argument of step 1.2 therefore yields L(\widetilde y)\subseteq\bigcap_{n\ge0}L(x^{(n)})\subseteq\bigcap_{n\ge1}L(z^{(n)}).\tag{3} For the second inclusion, is a subsequence of .
Fix . Since by (3) and the -evaluations of converge to the liminf of those of , The last inequality follows by applying the definition at and using limsup reflection. Replacing by therefore preserves the strict lower evaluation chosen in step 5.1. The upper estimate follows from and (2). Thus \alpha_m(1-\varepsilon_m)<\|\sum_{j<m}b_jy_j^*+T_my_m^*-w^*\|<\alpha_m(1+\varepsilon_m).\tag{4}
By steps 2.1 and 4.1, is nondecreasing and bounded above by , so [F3] gives a limit . The series is absolutely convergent and hence convergent in the Banach space by [F4]. If and the functional inside (4) is , then . Since , (4) gives . Because , this is .
It remains to prove the strict prefix estimate. Put , , and . The upper half of (4) and give . The exact identity and induction yield Since , . Using and (1) therefore gives \|P_n\|<\alpha(1-T_{n+1})+\alpha(1-\theta)T_{n+1}=\alpha(1-\theta T_{n+1}).\tag{5} The calculation includes , where .
Define the asserted zero-based sequence by . It and differ only by a one-place shift and a duplicated first term, so their scalar limsups agree and . Step 9.1 is therefore the asserted infinite-series equality for every , while (5) with replaced by is exactly Relabeling as proves the technical criterion, including the first term and every positive weight sequence.
Put and , and take the positive zero-based weights . By [F6] they sum to one; their tails satisfy . Apply the technical criterion to obtain , , and choose one , which is possible by step 1.1. The absolutely convergent series has .
Fix . Step 1.1 gives and . Since , there is an arbitrarily late , and in particular one with , such that . Split before , at , and after . The prefix estimate at , the displayed scalar inequality, and give because . Applying the same argument to gives . Therefore for every : is nonzero but attains its norm nowhere on the closed unit ball.
The first part uses DC only in step 6.1 and HB only in step 1.1. The ultrafilter lemma is absent there and enters solely through [F7] in the final nonreflexive consequence. The empty space cannot meet either separation or nonreflexivity; singleton convex combinations and the first prefix occur in steps 3.1 and 11.1; all tail denominators are positive because every weight is positive; and both strict endpoints are used in (1) and step 13.1.
Source notes
Megginson's Lemma 1.13.12 proves nonemptiness of . Lemma 1.13.13, printed pp. 128–132, supplies the eight-claim nested convex-block induction; its final reference to Lemma 1.13.10 step 6 is expanded here into the exact identity and telescoping calculation. Theorem 1.13.14(b)→(d), printed pp. 132–133, supplies the annihilator inclusion and geometric-weight norm-nonattainment argument. The proof here reindexes all public data from the source's positive integers to the repository's zero-based .
Depends on
- James nonreflexivity sequence separated from an annihilator
- Dominated extension conditional on the relative principle
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- The real dominated-extension principle as an additional hypothesis over ZF
- Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact
- The dual space X^* of a normed space and its dual norm
- Limit superior and limit inferior of a real sequence as $\inf_n \sup_{k \ge n} x_k$ and $\sup_n \inf_{k \ge n} x_k$ in $\overline{\mathbb{R}}$
- The tail suprema of any real sequence are nonincreasing in $\overline{\mathbb{R}}$, so the limit superior exists for every sequence
- $\limsup(x_k + y_k) \le \limsup x_k + \limsup y_k$ whenever the right-hand side is defined in $\overline{\mathbb{R}}$, and dually for $\liminf$
- $\limsup(-x_k) = -\liminf(x_k)$, with the reflection of $\overline{\mathbb{R}}$ exchanging $\pm\infty$
- The limit inferior is the least subsequential limit in $\overline{\mathbb{R}}$
- Every nonempty set bounded below has an infimum
- A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum
- If \(Y\) is Banach then \(\mathcal B(X,Y)\) is Banach
- Series criterion for Banach spaces
- Series and absolute convergence in a normed space
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- A strictly increasing index map satisfies $n_k \ge k$
Used by
- James reflexivity theorem Theorem
Dependency tree · two levels
97 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
- Robert E. Megginson, An Introduction to Banach Space Theory (1998) (standard reference, not scraped)