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.
The Analytic Hahn Banach Theorem
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Set Theory Beyond Choice: Recorded, Not Proved Here
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
This page follows the analytic route through Hahn-Banach. It starts with sublinear domination, isolates the one-step interval calculation and the chain-union upper bound needed for Zorn, and then proves the real dominated extension theorem. It next packages the normed-space consequences: the dual space, norm-preserving extension in the real and complex cases, norming functionals, separation by the dual, and recovery of the norm from the dual unit ball.
The page also keeps one boundary explicit: the norm-preserving extension theorem does not require the domain subspace to be closed. Seminorms, geometric separation, and finite-dimensional complementation are deliberately left to the next functional-analysis page.
3 · Logical flowchart
4 · Definitions, theorems and proofs
A sublinear functional on a real vector space
Definition
Remarks
- Taking shows .
- No condition is imposed for negative scalars beyond what follows from the two displayed axioms.
- A norm on a real vector space is sublinear, but a sublinear functional need not be symmetric: in general one can have .
The admissible values in a one-step Hahn-Banach extension form a nonempty interval
Statement
Let be a real vector space, let be a linear subspace, let be sublinear, and let be linear with for every . Fix and put .
For define
This is well defined, and with
one has . Moreover, for every if and only if . In particular the admissible values of form the nonempty interval .
Facts & Assumptions
Given: A real vector space , a linear subspace , a sublinear functional , a linear functional with on , and a point .
A sublinear functional satisfies and for every real (A sublinear functional on a real vector space).
A linear functional is additive and homogeneous over the scalar field (Linear functionals and the algebraic dual ).
A linear subspace is closed under addition and scalar multiplication (Linear subspace of a vector space).
Proof
If with and , then . If , closure under scalar multiplication from [L3] gives , contradicting the hypothesis. So and then . Therefore every element of has a unique representation , and is well defined.
For , one has Therefore and
Let . Since by [L3], linearity and domination on give Also so subadditivity from [L1] yields Combining these inequalities gives Hence every lower endpoint is at most every upper endpoint.
Suppose first that the two inequalities from step 1.2 hold for every . Let . If , then so by linearity and positive homogeneity, If , then so the lower-bound half of step 1.2 applied to gives If , then , so the hypothesis gives . Thus on . Conversely, if on , then applying that inequality to and yields the two inequalities in step 1.2.
Step 1.3 shows that the set of lower endpoints is bounded above by every upper endpoint, and the set of upper endpoints is bounded below by every lower endpoint. Completeness of therefore gives real numbers with the displayed formulas in the statement. By step 2.1, a real number is admissible exactly when it lies between every lower endpoint and every upper endpoint, that is, exactly when . Therefore the admissible values form the nonempty interval .
The union of a chain of dominated extensions is a well-defined dominated linear functional
Statement
Let be a real vector space and let be sublinear. Let be a nonempty chain, ordered by extension, of pairs such that is a linear subspace and is linear with for every .
Put
Then is a linear subspace of , and the pointwise union defined by whenever is a well-defined linear functional with for every .
If every extends the same linear functional , then also extends .
Facts & Assumptions
Given: A real vector space , a sublinear functional , and a nonempty chain of dominated linear functionals ordered by extension.
A linear functional is additive and homogeneous over the scalar field (Linear functionals and the algebraic dual ).
A chain is a subset in which any two elements are comparable (Chain in a poset).
Proof
If for , then [L2] gives comparability. Suppose . Since the chain order is extension, , so . The other inclusion case is the same. Therefore is well defined on overlaps.
Let and . Choose with and . By [L2], one of the domains contains the other; after relabeling, assume . Then , so and because is a linear subspace. Hence . Thus is a linear subspace.
With the same choice of as in step 1.2, one has and by [L1]. Therefore is linear.
If , choose with . Then by the defining property of the chain element, so is dominated by . If every chain element extends the same , then every lies in each domain and all values there equal , so .
Hahn-Banach dominated extension theorem for real vector spaces
Statement
Assume the Axiom of Choice. Let be a real vector space, let be a linear subspace, let be sublinear, and let be linear with for every . Then there exists a linear functional such that and for every .
Facts & Assumptions
Given: The Axiom of Choice, a real vector space , a linear subspace , a sublinear functional , and a linear functional with on .
The one-step extension problem over has a nonempty interval of admissible values for (The admissible values in a one-step Hahn-Banach extension form a nonempty interval).
The union of a chain of dominated extensions is again a well-defined dominated extension (The union of a chain of dominated extensions is a well-defined dominated linear functional).
Assuming the Axiom of Choice, a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).
Proof
Let be the set of all pairs such that , the set is a linear subspace of , the map is linear, , and on . Order by extension: The pair lies in , so this poset is nonempty.
Let be a chain. If , then is an upper bound for it. If , [L2] applies to the union of its domains and yields a well-defined linear functional dominated by ; because every chain element extends , that union functional still extends . Hence every chain in has an upper bound in .
By [L3], choose a maximal element of . If , choose . Applying [L1] to the dominated functional on the subspace produces a dominated linear extension on . Then , contradicting maximality. Therefore .
Since the maximal domain is all of , the corresponding functional is the required dominated extension of .
The dual space X^* of a normed space and its dual norm
Definition
Let be a normed space over the scalar field , where in the literal definition and by the convention of Real and complex scalar conventions for normed spaces. The dual space of is
the space of bounded linear functionals on (The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).
Each is in particular a linear functional in the algebraic sense, so is a subspace of the algebraic dual from Linear functionals and the algebraic dual .
The dual norm on is the operator norm:
Remarks
- The pairing between and is evaluation: .
- In this library, means the topological dual unless the phrase "algebraic dual" is written explicitly.
A bounded real linear functional on a subspace of a real normed space extends with the same norm
Statement
Let be a real normed space, let be a linear subspace, and let be a bounded linear functional. Then there exists a bounded linear functional such that and .
Facts & Assumptions
Given: A real normed space , a linear subspace , and a bounded real linear functional .
A dominated real linear functional extends to the whole real vector space (Hahn-Banach dominated extension theorem for real vector spaces).
A bounded linear operator has some constant with for every (A bounded linear operator between normed spaces).
The operator norm is the least such bound: (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).
A normed subspace carries the restricted norm from the ambient space (Normed subspace).
Proof
Define by The triangle inequality and real homogeneity of the norm make sublinear. For , [L3] and [L4] give so on .
By [L1], there exists a linear functional extending and satisfying for every .
Apply step 2.1 to and to . Since , one gets hence So is bounded in the sense of [L2], and [L3] gives .
Since , for every with one has . Taking the supremum over the unit ball of the normed subspace and using [L3] and [L4] yields .
Steps 3.1 and 3.2 give , so is the required norm-preserving extension.
A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)
Statement
Let be a complex vector space.
If is complex linear and , then is real linear on the underlying real vector space and
Conversely, if is real linear on the underlying real vector space, then
defines a complex linear functional with . In particular a complex linear functional is uniquely determined by its real part.
Facts & Assumptions
Given: A complex vector space , a complex linear functional , and a real linear functional on the underlying real vector space.
A linear functional is additive and homogeneous over the relevant scalar field (Linear functionals and the algebraic dual ).
On this page, complex vector-space language is read by the scalar convention recorded in Real and complex scalar conventions for normed spaces.
Proof
Let . For and , and So is real linear.
Write with . Since is complex linear, so and . Therefore
Conversely, let be real linear and define . Additivity is immediate from real linearity of . Also Now for with , Hence is complex linear.
Taking real parts in the definition of gives for every . Together with step 1.2, this shows that a complex linear functional is uniquely determined by its real part.
A bounded complex linear functional on a subspace of a complex normed space extends with the same norm
Statement
Let be a complex normed space, let be a linear subspace, and let be a bounded complex linear functional. Then there exists a bounded complex linear functional such that and .
Facts & Assumptions
Given: A complex normed space , a linear subspace , and a bounded complex linear functional .
A bounded real linear functional on a real normed subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).
A complex linear functional is recovered from its real part by , and conversely every such formula defines a complex linear functional (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).
The complex case uses the scalar convention from Real and complex scalar conventions for normed spaces.
Proof
Let . By [L2], is real linear on the underlying real subspace . Also so is bounded with .
Apply [L1] to the underlying real normed spaces. This yields a bounded real linear functional extending and satisfying . Define By [L2], is complex linear and .
For , the equality and [L2] give So extends .
Fix . Choose so that is a nonnegative real number. Since and is complex linear, Therefore where the last inequality uses step 1.1 and . Hence .
Since , every with satisfies . Taking the supremum over the unit ball of gives . Combined with step 3.2, this yields .
Every nonzero vector has a norming functional
Statement
Let be a normed space over or , and let be nonzero. Then there exists such that
Facts & Assumptions
Given: A normed space over or and a vector with .
The dual space is the space of bounded linear functionals on (The dual space X^* of a normed space and its dual norm).
In the real case, a bounded linear functional extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).
In the complex case, a bounded linear functional extends with the same norm (A bounded complex linear functional on a subspace of a complex normed space extends with the same norm).
Proof
Let . Define or by Because , each vector of has a unique representation . Moreover, so is bounded and .
If the scalar field is , [L2] extends to a bounded real linear functional on with . Since , .
If the scalar field is , [L3] extends to a bounded complex linear functional on with . Again .
In either scalar case, the extension produced in step 2.1 or step 2.2 is a bounded linear functional on , hence an element of by [L1], with norm and value at .
The dual space separates points of a normed space
Statement
Let be a normed space over or . If with , then there exists such that .
Facts & Assumptions
Given: A normed space over or and two vectors with .
Every nonzero vector admits a norming functional (Every nonzero vector has a norming functional).
Proof
Since , the vector is nonzero.
By [L1], there exists with In particular .
If , then linearity would give , contradicting step 2.1. Therefore , so the dual space separates and .
The norm of a vector is the supremum of |f(x)| over the dual unit ball
Statement
Let be a normed space over or . Then for every ,
Facts & Assumptions
Given: A normed space over or and a vector .
The dual norm on is the operator norm, so for every (The dual space X^* of a normed space and its dual norm).
Every nonzero vector admits a norming functional (Every nonzero vector has a norming functional).
Proof
If and , then [L1] gives So the displayed supremum is at most .
If , step 1.1 already shows that the supremum is , so the formula holds. Assume now that . By [L2], choose with and . Then the displayed supremum is at least .
Step 1.1 gives an upper bound of , and step 2.1 gives equality. So
A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed
Statement
Let be a normed space over or , let be a linear subspace, and let or be a bounded linear functional over the ambient scalar field. Then there exists a bounded linear extension of to all of such that .
No closedness hypothesis on is needed.
Facts & Assumptions
Given: A normed space over or , a linear subspace , and a bounded linear functional on .
In the real case, a bounded linear functional on a subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).
In the complex case, a bounded linear functional on a subspace extends with the same norm (A bounded complex linear functional on a subspace of a complex normed space extends with the same norm).
The page's normed-space language is read over either scalar field by the convention of Real and complex scalar conventions for normed spaces.
Proof
If the scalar field is , then [L1] applies exactly as stated to the given subspace and produces a norm-preserving extension of to .
If the scalar field is , then [L2] applies exactly as stated to the given subspace and produces a norm-preserving extension of to .
Neither step 1.1 nor step 1.2 uses or requires that be closed; each cited theorem assumes only that is a linear subspace. Therefore every bounded linear functional on an arbitrary subspace extends with the same norm.
The set-theoretic cost of Hahn-Banach
Remark
The proof of Hahn-Banach dominated extension theorem for real vector spaces on this page is a Zorn proof, so that proof route uses the Axiom of Choice through Zorn's lemma. That is a proof cost, not the exact cost of the theorem itself.
The sharper ledger is recorded in The set-theoretic cost of Hahn-Banach ‡. For the reader of this page, the key points are these:
- the Boolean prime ideal theorem implies Hahn-Banach;
- relative to the consistency of ZF, Hahn-Banach does not imply the Boolean prime ideal theorem, so Hahn-Banach is strictly weaker than full choice by Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡;
- Hahn-Banach already implies the existence of a non-Lebesgue measurable set and the Banach-Tarski paradox.
So later pages should cite Hahn-Banach itself when they use the extension theorem, and should cite Zorn only when they really use this maximal-extension implementation.
5 · Examples, counterexamples and false statements
None yet.
Sources
- Daniel Daners, Introduction to Functional Analysis, Theorem 26.1
- Gerald Teschl, Topics in Real and Functional Analysis, Section 4.2
- Daniel Daners, Introduction to Functional Analysis, Theorem 26.1(a)
- Gerald Teschl, Topics in Real and Functional Analysis, Theorem 4.13
- Daniel Daners, Introduction to Functional Analysis, Definition 25.1
- Gerald Teschl, Topics in Real and Functional Analysis, Corollary 4.15
- Daniel Daners, Introduction to Functional Analysis, Theorem 26.4
- Gerald Teschl, Topics in Real and Functional Analysis, Theorem 4.14
- Daniel Daners, Introduction to Functional Analysis, Corollary 26.5
- Gerald Teschl, Topics in Real and Functional Analysis, Corollary 4.16
- Daniel Daners, Introduction to Functional Analysis, Remark 26.6
- Daniel Daners, Introduction to Functional Analysis, Remark 25.2(c)
- Daniel Daners, Introduction to Functional Analysis, Theorem 26.7
- Gerald Teschl, Topics in Real and Functional Analysis, Corollary 4.15 and Theorem 4.14
- W. A. J. Luxemburg, Two applications of the method of construction by ultrapowers to analysis
- D. Pincus, The strength of the Hahn-Banach theorem
- M. Foreman and F. Wehrung, The Hahn-Banach theorem implies the existence of a non-Lebesgue measurable set
- J. Pawlikowski, The Hahn-Banach theorem implies the Banach-Tarski paradox