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.
Milman–Pettis theorem
Statement
Assume the relative Hahn–Banach principle HB and the Axiom of Countable Choice . Every real or complex uniformly convex Banach space is reflexive.
The ultrafilter lemma is not assumed.
Facts & Assumptions
Given: HB, , and a real or complex uniformly convex Banach space , with canonical map .
For every , uniform convexity supplies such that unit-ball vectors separated by at least have midpoint norm at most (Uniformly convex Banach space).
Under HB, if , a finite list and are fixed, some satisfies for every (Goldstine finite-data approximation, equivalently Goldstine's theorem).
The norm on a real or complex dual space is (The dual space X^* of a normed space and its dual norm).
Under HB, is scalar-linear and isometric (Relative Hahn–Banach makes the canonical bidual map an isometry); HB is the explicitly named relative dominated-extension principle (The real dominated-extension principle as an additional hypothesis over ZF).
Under , a complete normed subspace of a normed space is closed (A complete normed subspace is closed under countable choice); Countable Choice is the countable-family selection principle (The Axiom of Countable Choice ()).
A Banach space is reflexive exactly when its canonical map onto the bidual is surjective (Reflexivity is surjectivity of the canonical map).
Proof
We first transfer uniform convexity to . Fix and take from [F1] a number for the separation threshold . Let satisfy . By [F3], choose with . In the complex case multiply by a scalar of modulus one, and in the real case change its sign if necessary, to obtain with .
Fix an arbitrary and , and put and . Apply [F2] separately to and , each time with the two tests and tolerance , obtaining . Then , so . By [F1], . Approximation at therefore gives If the left side exceeded , taking to be half that positive gap would contradict this inequality. Hence . Taking the supremum over by [F3] yields .
Thus , with its given dual norm, is uniformly convex: the modulus at may be taken to be any modulus of at . Notice that step 2.1 used two finite-data witnesses only after were fixed; it selected no sequence or family of witnesses.
Let have norm one and let . Put and let be the bidual modulus established in step 3.1. Set . By [F3] choose with , and rotate or change its sign to get with . By [F2], choose with . Hence , and The contrapositive of the bidual uniform-convexity estimate gives .
It follows that is norm dense in . Indeed, the zero vector is . For nonzero and a prescribed , apply step 4.1 to with tolerance , obtaining ; then and .
By [F4], is an isometry, so its range is a normed subspace isometric to the complete space . Under the assumed , [F5] makes this range norm closed in . Step 5.1 puts every element of in its norm closure and hence in the range. Scaling then gives : the zero element is already in the range, and a nonzero element is its norm times an element of the bidual unit sphere. Thus is surjective, and [F6] says that is reflexive.
HB is used exactly in [F2] for Goldstine finite-data approximation and in [F4] for the canonical isometry. Countable Choice is used exactly through the complete-subspace closedness statement [F5]. No compactness theorem and no ultrafilter principle occurs. If , then and step 6.1 is immediate. All scalar inequalities use real parts, so the proof covers both real and complex scalars.
Depends on
- Uniformly convex Banach space
- Goldstine's theorem
- Relative Hahn–Banach makes the canonical bidual map an isometry
- A complete normed subspace is closed under countable choice
- Reflexivity is surjectivity of the canonical map
- The real dominated-extension principle as an additional hypothesis over ZF
- Goldstine finite-data approximation
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The dual space X^* of a normed space and its dual norm
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
29 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
- Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (standard reference, not scraped)
- Harald Hanche-Olsen, Topological vector spaces (standard reference, not scraped)