Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

James convex-block norm-attainment criterion

Statement

Assume the Axiom of Dependent Choice (DC) and the relative Hahn–Banach principle HB. Let X be a real Banach space, let 0<θ<1, and let (xn)nN be a sequence in BX. For every bounded sequence s=(sn) in X put

L(s)={wX:w(x)lim supnsn(x) for every xX}.

Suppose

dist ⁣(L(x),co{xn:nN})θ,

where co is the finite convex hull. If (βn)nN is any sequence of positive reals with n=0βn=1, then there are α[θ,2] and a sequence (yn) in BX such that, for every wL(y),

j=0βj(yjw)=α

and, for every nN,

j=0nβj(yjw)<α(1θj>nβj).

In addition, assume the ultrafilter lemma. If X is nonreflexive, then some zX does not attain its norm on BX.

Facts & Assumptions

Given: DC, HB, a real Banach space X, 0<θ<1, a dual-ball sequence (xn) satisfying the displayed separation, and positive weights (βn) of sum one. The ultrafilter lemma is assumed only for the final nonreflexive consequence.

[F2]

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

[F3]

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

[F4]

The dual norm is the supremum of absolute values on the closed unit ball. Since the scalar field is complete, X=B(X,R) 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).

[F5]

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 N-indexed chain).

[F6]

A strictly increasing subsequence index map satisfies knn, and the real geometric-series formula holds for every ratio of absolute value less than one (A strictly increasing index map satisfies nkk, For r<1, k0rk=1/(1r), and for r1 the series diverges).

[F7]

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

technique · nested convex-block induction and a geometric series argument
1.1

We first record two elementary properties of L. For a bounded sequence s=(sn), say snC, the function p(u)=lim supnsn(u) is finite, positively homogeneous, and subadditive: homogeneity follows directly from tail suprema and subadditivity from [F1]. Apply [F2] to the zero functional on {0} dominated by p. The extension w satisfies w(u)p(u), while applying this inequality at u and using [F1] gives w(u)lim infnsn(u). Hence w(u)Cu, so wL(s) and wC. Thus L(s) is nonempty and, when sBX, lies in BX.

F1F2F4
1.2

Let V(s) be the set of sequences v=(vn) for which vnco{sj:jn} at every n. It is nonempty because sV(s). For each u, every such convex combination satisfies vn(u)supjnsj(u), so the receding-tail definition gives lim supnvn(u)lim supnsn(u) and therefore L(v)L(s). Flattening two finite convex combinations proves V(v)V(s) when vV(s). A subsequence of s also belongs to V(s): its nth index is at least n by [F6].

F1F6construct
1.3

Reindex the weights by positive integers, bm=βm1 for m1. Extend the corresponding reindexing of the dual sequence to a genuine zero-based library sequence by setting x^0=x0 and x^m=xm1 for m1. The duplicate initial term does not change any scalar limsup, so L(x^)=L(x), and {x^m:m1}={xn:nN}. Put Tm=j=mbj, so T1=1, Tm=bm+Tm+1, every Tm>0, and Tm0. Choose explicitly εm=min{1/(m+1),(1θ)2m1TmTm+1/bm}>0. Then εm0 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}

givenF6algebra
1.4

Now additionally assume the ultrafilter lemma and that X is nonreflexive. Apply [F7] with the same θ to obtain M and (xn)BX, pointwise null on M, with its convex hull at distance at least θ from M. If wL(x), then for mM the defining inequality at m and m gives w(m)0 and w(m)0. Hence L(x)M, and the separation hypothesis of the technical criterion holds.

F1F7
2.1

Set x(0)=x^. Suppose that y1,,ym1 and the sequences x(0),,x(m1) have been constructed. For yco{xj(m1):jm} and vV(x(m1)), define Sm(y,v)={j<mbjyj+Tmyw:wL(v)}, and let αm be the infimum, over all such (y,v), of supSm(y,v). Step 1.1 makes every Sm nonempty. All displayed functionals have norm at most two, because all the convex blocks and all members of L(v) lie in the dual unit ball; hence 0αm2 and [F3] makes the infimum legitimate.

step 1.1step 1.2F3F4
3.1

For m=1, any admissible y is in the convex hull of the original sequence and L(v)L(x^)=L(x) by steps 1.2–1.3. The separation hypothesis therefore gives ywθ for every admissible w, so α1θ.

step 1.2step 1.3step 2.1given
4.1

Suppose m2. The induction will arrange that x(m1) is a subsequence of some z(m1)V(x(m2)). Consequently x(m1)V(x(m2)) by step 1.2. For an admissible y at stage m, both ym1 and y lie in co{xk(m2):km1}, and so does u=bm1ym1+TmyTm1. Also vV(x(m2)) by flattening. Since j<m1bjyj+Tm1uw=j<mbjyj+Tmyw, every stage-m candidate supplies a stage-(m1) candidate of the same supremum. Hence αm1αm. Together with step 3.1, θαm2 for all m.

step 1.2step 2.1step 3.1algebra
5.1

The definition of the positive number αm supplies ymco{xj(m1):jm} and z(m)V(x(m1)) such that \alpha_m\le\sup S_m(y_m^*,z^{(m)})<\alpha_m(1+\varepsilon_m).\tag{2} Because 0<εm<1, choose wmL(z(m)) for which the norm inside (2) is greater than αm(1εm). By [F4] and the balance of BX, there is umBX on which the same functional, without absolute-value signs, has value greater than that number. The bounded scalar sequence zj(m)(um) has a subsequence converging to its liminf by [F1]; denote the corresponding dual sequence by x(m).

step 1.3step 2.1step 4.1F1F3F4
6.1

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 x(0)=x^, 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 ym,z(m),wm,um,x(m) with (2) and the strict lower inequality. No simultaneous selection outside this DC application is being hidden.

step 5.1F5
7.1

The induction has produced the positive-indexed family (ym)m1. Make it a genuine sequence by putting y~0=y1 and y~m=ym for m1. For fixed n0 and every j>n, repeated flattening of the relations in steps 4.1–5.1 gives yjco{xk(n):kj}. Ignoring the single duplicated initial term in y~, 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, x(n) is a subsequence of z(n).

step 1.2step 4.1step 5.1step 6.1
8.1

Fix wL(y~). Since wL(x(m)) by (3) and the um-evaluations of x(m) converge to the liminf of those of z(m), w(um)lim infjzj(m)(um)wm(um). The last inequality follows by applying the definition wmL(z(m)) at um and using limsup reflection. Replacing wm by w therefore preserves the strict lower evaluation chosen in step 5.1. The upper estimate follows from wL(z(m)) 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}

step 5.1step 7.1F1F4
9.1

By steps 2.1 and 4.1, (αm) is nondecreasing and bounded above by 2, so [F3] gives a limit α[θ,2]. The series j1bjyj is absolutely convergent and hence convergent in the Banach space X by [F4]. If q=j1bjyjw and the functional inside (4) is qm, then qqmjmbjyjym2Tm0. Since εm0, (4) gives q=α. Because bj=1, this is j1bj(yjw)=α.

step 1.3step 4.1step 8.1F3F4
10.1

It remains to prove the strict prefix estimate. Put Pn=j=1nbj(yjw), P0=0, and Qn=Pn1+Tn(ynw). The upper half of (4) and αnα give Qn<α(1+εn). The exact identity Pn=bnTnQn+Tn+1TnPn1 and induction yield Pn<αTn+1k=1nbk(1+εk)TkTk+1. Since bk=TkTk+1, k=1nbk/(TkTk+1)=1/Tn+11/T1. Using T1=1 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 n=1, where P0=0.

step 1.3step 8.1step 9.1algebrainduction
11.1

Define the asserted zero-based sequence by ynout=yn+1. It and y~ differ only by a one-place shift and a duplicated first term, so their scalar limsups agree and L(yout)=L(y~). Step 9.1 is therefore the asserted infinite-series equality for every wL(yout), while (5) with n replaced by n+1 is exactly j=0nβj(yjoutw)<α(1θj>nβj). Relabeling yout as y proves the technical criterion, including the first term n=0 and every positive weight sequence.

step 1.3step 7.1step 9.1step 10.1
12.1

Put Δ=θ2/4 and r=Δ/2, and take the positive zero-based weights βj=(1r)rj. By [F6] they sum to one; their tails Rk=jkβj satisfy Rk+1=rRk<ΔRk. Apply the technical criterion to obtain α, y, and choose one wL(y), which is possible by step 1.1. The absolutely convergent series z=j=0βj(yjw) has z=αθ>0.

step 1.1step 11.1step 1.4F4F6
13.1

Fix uBX. Step 1.1 gives w1 and lim infjyj(u)w(u). Since θ22Δ=θ2/2>0, there is an arbitrarily late k, and in particular one with k1, such that (ykw)(u)<θ22Δαθ2Δ. Split z(u) before k, at k, and after k. The prefix estimate at k1, the displayed scalar inequality, and yjw2 give z(u)<α(1θRk)+(αθ2Δ)βk+2Rk+1<α(1θRk)+(αθ2Δ)βk+2ΔRk=α(αθ2Δ)Rk+1<α, because αθ2Δθ22Δ>0. Applying the same argument to u gives z(u)<α. Therefore z(u)<α=z for every uBX: z is nonzero but attains its norm nowhere on the closed unit ball.

step 1.1step 11.1step 12.1F1F4
14.1

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 0<θ<1 are used in (1) and step 13.1.

step 1.1step 1.3step 3.1step 6.1step 11.1step 1.4step 13.1

Source notes

Megginson's Lemma 1.13.12 proves nonemptiness of L(s). 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 Pn,Qn,Tn 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 N.

Depends on

Used by

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