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 be a nonempty closed bounded convex subset of a real Banach space . For every and every there are and such that
In fact, the construction below gives the strict bound .
Facts & Assumptions
Given: DC, HB, and as in the statement.
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).
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 -indexed chain).
Every bounded monotone real sequence converges, and every nonempty subset of 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, Every nonempty set bounded below has an infimum).
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).
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.
Choose a real number with . The restriction is continuous and bounded above because is bounded. By [F1], with its norm metric is complete. Fix one , possible because is nonempty, and for define Each is nonempty because it contains , and it is closed because is continuous in .
If and , then Thus and . Since is bounded above and is nonempty, its supremum is a real number. For every and every , the defining approximation property of the supremum supplies with
Let a state be a nonempty finite sequence in which starts at the fixed and, at each earlier index , has and 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 with both displayed properties for every .
The ascent condition gives Consequently the partial sums of are nondecreasing and bounded above by . By [F3] the series converges, hence its tails tend to zero and is Cauchy. Completeness gives a limit .
Transitivity in step 2.1 makes every tail point , , belong to ; closedness gives for every . If , then transitivity also puts in every , and the approximate-supremum condition gives Letting and using continuity yields . But also gives , so . Therefore and the corresponding non-strict inequality holds for every .
Put Because is convex and contains zero, is a convex cone: for the sum is zero if , and otherwise equals . Step 5.1 and real linearity give This includes .
For define The set being infimized is nonempty because . Step 6.1 and the reverse triangle inequality give every one of its terms at least , while gives a term equal to . Thus [F3] makes a finite real and -\eta\|x\|\le p(x)\le\eta\|x\|.\tag{1} Both bounds are uniform in the choice of .
The cone identities imply for , and (1) gives . If , then and Taking infima first over and then over proves . Hence is sublinear.
Apply [F4] to the zero functional on , dominated by , to obtain a real-linear with . Applying this at and and using (1) gives , so and by [F5]. For , the candidate in the infimum gives , whence and . Thus the extension dominates on the support cone.
Set . Then and . For every , the vector lies in , so step 9.1 gives Thus attains its supremum on at . The proof permits a singleton , , and the closed-boundary cases; DC is used only in step 3.1 and HB only in step 9.1.
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
- Banach space
- 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
- Dominated extension conditional on the relative principle
- Closed subspaces of complete metric spaces are complete; the converse under countable choice
- A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum
- Every nonempty set bounded below has an infimum
- The dual space X^* of a normed space and its dual norm
Used by
- Bishop phelps Theorem
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
- Philip D. Loewen and Xianfu Wang, A Generalized Variational Principle, Canadian Journal of Mathematics 53 (2001), 1174–1193 (standard reference, not scraped)