Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Quantitative Bishop–Phelps support functional construction

Statement

Assume the Axiom of Dependent Choice (DC) and the relative Hahn–Banach principle HB. Let C be a nonempty closed bounded convex subset of a real Banach space X. For every fX and every ε>0 there are vC and gX such that

gfεandg(c)g(v)(cC).

In fact, the construction below gives the strict bound gf<ε.

Facts & Assumptions

Given: DC, HB, X,C,f and ε as in the statement.

[F1]

A closed subset of a complete metric space is complete, without a choice axiom (Closed subspaces of complete metric spaces are complete; the converse under countable choice, claim 2, Banach space).

[F2]

DC produces a sequence along an entire relation from a specified initial state (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

[F4]

Under HB, a real linear functional dominated by a sublinear functional on a subspace has a dominated real-linear extension (Dominated extension conditional on the relative principle, The real dominated-extension principle as an additional hypothesis over ZF).

[F5]

The dual norm is the supremum of the absolute values on the closed unit ball (The dual space X^* of a normed space and its dual norm).

Proof

Proof technique: maximizing variational construction followed by a support-cone Hahn–Banach argument.

1.1

Choose a real number η with 0<η<ε. The restriction F=fC is continuous and bounded above because C is bounded. By [F1], C with its norm metric is complete. Fix one x0C, possible because C is nonempty, and for xC define S(x)={yC:F(y)F(x)+ηyx}. Each S(x) is nonempty because it contains x, and it is closed because F(y)F(x)ηyx is continuous in y.

givenF1construct
2.1

If yS(x) and zS(y), then F(z)F(y)+ηzyF(x)+η(yx+zy)F(x)+ηzx. Thus zS(x) and S(y)S(x). Since F is bounded above and S(x) is nonempty, its supremum is a real number. For every n and every xC, the defining approximation property of the supremum supplies yS(x) with F(y)>supzS(x)F(z)2n.

step 1.1algebra
3.1

Let a state be a nonempty finite sequence (x0,,xn) in C which starts at the fixed x0 and, at each earlier index k<n, has xk+1S(xk) and F(xk+1)>supzS(xk)F(z)2k. Relate each state to every valid one-term extension. Step 2.1 proves that this relation is entire, so one application of DC gives a compatible infinite sequence (xn) with both displayed properties for every n.

step 2.1F2choose
4.1

The ascent condition gives ηxn+1xnF(xn+1)F(xn). Consequently the partial sums of nxn+1xn are nondecreasing and bounded above by (supCFF(x0))/η. By [F3] the series converges, hence its tails tend to zero and (xn) is Cauchy. Completeness gives a limit vC.

step 1.1step 3.1F3algebra
5.1

Transitivity in step 2.1 makes every tail point xk, kn, belong to S(xn); closedness gives vS(xn) for every n. If zS(v), then transitivity also puts z in every S(xn), and the approximate-supremum condition gives F(z)<F(xn+1)+2n. Letting n and using continuity yields F(z)F(v). But zS(v) also gives F(z)F(v)+ηzv, so z=v. Therefore F(c)<F(v)+ηcv(cC, cv), and the corresponding non-strict inequality holds for every cC.

step 1.1step 2.1step 3.1step 4.1algebra
6.1

Put D={t(cv):t0, cC}. Because Cv is convex and contains zero, D is a convex cone: for t,s0 the sum t(cv)+s(cv) is zero if t+s=0, and otherwise equals (t+s)(tt+sc+st+scv). Step 5.1 and real linearity give f(d)ηd(dD). This includes d=0.

step 5.1givenalgebra
7.1

For xX define p(x)=infdD(ηx+df(d)). The set being infimized is nonempty because 0D. Step 6.1 and the reverse triangle inequality give every one of its terms at least ηx, while d=0 gives a term equal to ηx. Thus [F3] makes p(x) a finite real and -\eta\|x\|\le p(x)\le\eta\|x\|.\tag{1} Both bounds are uniform in the choice of d.

step 6.1F3algebra
8.1

The cone identities imply p(tx)=tp(x) for t>0, and (1) gives p(0)=0. If d1,d2D, then d1+d2D and ηx+y+d1+d2f(d1+d2)ηx+d1f(d1)+ηy+d2f(d2). Taking infima first over d1,d2 and then over D proves p(x+y)p(x)+p(y). Hence p is sublinear.

step 6.1step 7.1algebra
9.1

Apply [F4] to the zero functional on {0}, dominated by p, to obtain a real-linear h:XR with h(x)p(x). Applying this at x and x and using (1) gives h(x)ηx, so hX and hη by [F5]. For dD, the candidate d in the infimum gives p(d)f(d), whence h(d)=h(d)p(d)f(d) and h(d)f(d). Thus the extension dominates f on the support cone.

step 7.1step 8.1F4F5
10.1

Set g=fh. Then gX and gf=hη<ε. For every cC, the vector cv lies in D, so step 9.1 gives g(c)g(v)=f(cv)h(cv)0. Thus g attains its supremum on C at v. The proof permits a singleton C, f=0, X={0} and the closed-boundary cases; DC is used only in step 3.1 and HB only in step 9.1.

step 6.1step 9.1given

Source notes

Loewen–Wang Theorem 2.2 proves a generalized variational principle and derives the Ekeland inequality in (2.14). Proposition 5.1(i) applies that principle to a coercive function, and Theorem 5.2 states Bishop–Phelps for nonempty closed bounded convex sets. The proof above derives exactly the maximizing inequality needed here and then spells out the support-cone/sublinear-gauge argument.

Depends on

Used by

Dependency tree · two levels

44 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