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.
Geometric Hahn Banach and Convex Separation
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complex Subspace Realification
- Complexification, Realification and Real Structures
- 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
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Foundations of the Real Numbers for Analysis
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Linear Independence, Bases and Dimension
- 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
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The Analytic Hahn Banach Theorem
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The gauge turns a translated open convex neighbourhood into a real sublinear functional. Under the Axiom of Choice, Hahn–Banach supplies geometric separation, with real parts used over complex scalars. The later results apply separation to subspace closure, complemented finite-dimensional directions, and weak/norm closure of convex sets. The closed-hyperplane theorem has a separate choice-free proof using the coefficient along one complementary vector.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Absorbing, balanced, and absolutely convex sets
Definition
Let be a normed space over , with the real norm definition A norm on a real vector space, the induced metric, and the dictionary with the metric axioms over and the complex norm definition Complex norm and complex normed space over , and let . The set is absorbing if, for every , there is such that . It is balanced if for every with . It is absolutely convex if it is both convex and balanced. No closedness, openness, or positive definiteness is part of these definitions.
Minkowski functional of an absorbing set
Definition
For an absorbing subset of a normed space , its Minkowski functional or gauge is
The defining set is nonempty by absorption, so is finite and nonnegative. It is not asserted to be a norm or a seminorm: those conclusions need additional hypotheses on .
The gauge of a convex absorbing set is sublinear
Statement
If is convex and absorbing, then its gauge satisfies for and . Thus is a real sublinear functional.
Facts & Assumptions
Given: A convex absorbing set and .
The gauge is , and its defining set is nonempty (Minkowski functional of an absorbing set).
Proof
For , holds exactly when ; taking infima gives , while gives .
Absorption and convexity first give . Given and , choose , with , ; convexity with enlarges these to , for some . Then , hence .
Therefore for every such ; letting them decrease to the two infima proves subadditivity.
The gauge of an absolutely convex absorbing set is a seminorm
Statement
If is absolutely convex and absorbing, then for every scalar , and is a seminorm. It need not be positive definite.
Facts & Assumptions
Given: An absolutely convex absorbing , , and .
For convex absorbing , is nonnegative, subadditive, and homogeneous for nonnegative real scalars (The gauge of a convex absorbing set is sublinear).
Proof
If the assertion follows from [F1]. For , balancedness gives : one inclusion is balancedness and the reverse follows by applying it to the inverse scalar.
Hence exactly when , so taking infima yields . Together with [F1] this is precisely the seminorm axioms.
An open convex neighbourhood is recovered from its gauge
Statement
If is open, convex, and , then is absorbing and
Facts & Assumptions
Given: An open convex containing .
The gauge is defined for absorbing sets by an infimum over positive dilates (Minkowski functional of an absorbing set).
Proof
Openness gives for some . For any , , so is absorbing and [F1] applies.
If , openness gives with ; hence .
If , choose with , say . Convexity and imply . Thus both inclusions hold.
Weak, strict, and strong separation
Definition
For nonempty , a nonzero weakly separates and if . It strictly separates them if for every , and strongly separates them if there are with for all . Over , ; over these real parts are essential, since complex values are not ordered.
Separate a point from an open convex set
Statement
Assume the Axiom of Choice. Let be a nonempty open convex subset of a real or complex normed space and let . Then a nonzero satisfies
Facts & Assumptions
Given: The Axiom of Choice, a nonempty open convex and .
If an open convex set contains , it equals the strict unit sublevel set of its gauge (An open convex neighbourhood is recovered from its gauge).
Assuming the Axiom of Choice, a real linear functional dominated by a sublinear functional on a linear subspace extends to the whole real vector space with the same domination (Hahn-Banach dominated extension theorem for real vector spaces).
A real linear functional on a complex space yields the complex-linear functional with real part (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).
The gauge of a convex absorbing set is a real sublinear functional (The gauge of a convex absorbing set is sublinear).
Proof
Choose and put , . Then and is open, convex, contains , and ; by [F1], and for .
By [F1], is absorbing, and [F4] makes sublinear. On the real line define . For , ; for , . Thus [F2] gives a real linear on with and .
Choose with . For one has and , so taking infima gives . Domination applied to both and gives . In the real case take ; in the complex case take , which is continuous by this estimate and has real part by [F3].
For , [F1] and give . Since , is nonzero. Hence the stated strict separation holds.
Separation of disjoint convex sets when one is open
Statement
Assume the Axiom of Choice. If are nonempty disjoint convex sets and is open, then there is a nonzero such that
Facts & Assumptions
Given: The Axiom of Choice and nonempty disjoint convex sets , with open.
An exterior point and a nonempty open convex set admit a strict separating continuous functional (Separate a point from an open convex set).
The Axiom of Choice is used through the Hahn–Banach extension in [F1].
Proof
The difference is open and convex, and because .
Under [A1], apply [F1] to and . It supplies nonzero with for every .
For and , , so . This is the required strict separation.
Strong separation of a closed and a compact convex set
Statement
Assume the Axiom of Choice. Let be disjoint nonempty convex sets, where is closed and is compact. Then they are strongly separated by a nonzero functional in .
Facts & Assumptions
Given: The Axiom of Choice and disjoint nonempty convex , with closed and compact.
Distance to a fixed nonempty set is continuous (indeed -Lipschitz) (, so the distance to a fixed nonempty set is -Lipschitz).
A continuous real-valued function on a compact metric space attains its minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Disjoint convex sets, one open, are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).
The Axiom of Choice supplies the Hahn–Banach premise in [F3].
Proof
By [F1]--[F2], has a minimum on . It is positive: a zero minimum would put some in the closed set . Choose .
The thickening is open and convex and is disjoint from . Under [A1], apply [F3] to to obtain nonzero with for .
For , take the supremum over in the inequalities from step 2.1. Since , this gives for every . Hence , a positive gap.
A closed convex set is an intersection of closed half-spaces
Statement
Assume the Axiom of Choice. Every nonempty closed convex is the intersection of the closed affine half-spaces that contain .
Facts & Assumptions
Given: The Axiom of Choice and a nonempty closed convex set .
Disjoint convex sets with one open are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).
Proof
Since every closed affine half-space in the family contains , their intersection contains .
If , choose with . The set is open and convex and still omits ; [F1], using AC through its open-convex point-separation supplier, gives a nonzero continuous with for every and .
Taking the supremum over in step 1.2 gives for every . Since , the closed half-space contains and excludes . Thus every exterior point is excluded from the intersection, proving equality.
Continuous annihilator of a linear subspace
Definition
Let be a normed space and let be a linear subspace. Its continuous annihilator is
This is an annihilator in the topological dual , not in the unrestricted algebraic dual.
Geometric Hahn--Banach theorem for subspaces
Statement
Assume the Axiom of Choice. For a linear subspace and , there is with .
Facts & Assumptions
Given: The Axiom of Choice, A subspace and .
AC is used through norm-preserving extension [F2] in step 3.1.
exactly when is positive (The closure of a nonempty is , equals together with its limit points, and is the smallest closed superset).
A bounded functional on any subspace extends to the ambient normed space without increasing its norm (A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed).
Proof
By [F1], . On define ; the representation is unique because .
For , , while the case is immediate. Thus .
Extend by [F2] to . Then and , so as required.
The annihilator detects the closure of a subspace
Statement
Assume the Axiom of Choice. For every linear subspace ,
Facts & Assumptions
Given: The Axiom of Choice, A linear subspace .
AC is used through geometric Hahn–Banach [F1] in step 1.2.
Every point outside is sent to by some continuous functional vanishing on (Geometric Hahn--Banach theorem for subspaces).
Proof
If and , continuity of and give . Thus lies in the intersection.
If , [F1] gives with , so is absent from the intersection.
The two inclusions prove the formula.
Density is characterized by a zero annihilator
Statement
Assume the Axiom of Choice. A linear subspace is dense if and only if .
Facts & Assumptions
Given: The Axiom of Choice, A linear subspace .
AC is used through annihilator closure [F1] in step 2.1.
Proof
If is dense, [F1] says every vanishes on , hence is zero.
If , the intersection in [F1] is , so and is dense.
Finite-dimensional subspaces are complemented
Statement
Assume the Axiom of Choice. Every finite-dimensional linear subspace of a normed space is complemented in .
Facts & Assumptions
Given: The Axiom of Choice, A finite-dimensional subspace .
AC is used through functional extension [F2] in step 1.1.
Relative to a fixed finite basis, every coordinate functional on a finite-dimensional normed space is bounded (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space).
A bounded functional on a subspace extends norm-preservingly to the ambient normed space (A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed).
A subspace is complemented exactly when it is the range of a bounded projection (A closed subspace is complemented exactly when it is the range of a bounded projection).
Proof
Choose a basis of , and let be its coordinate maps. By [F1]--[F2], extend each to .
Define by . It is bounded, has range in , and for satisfies .
Thus and ; [F3] makes complemented.
Closed finite-codimensional subspaces are complemented
Statement
Every closed finite-codimensional linear subspace of a normed space is complemented in .
Facts & Assumptions
Given: A closed subspace with finite-dimensional .
The quotient seminorm is a norm exactly when the subspace is closed (The quotient seminorm is a norm exactly when the subspace is closed).
Coordinate functionals for a fixed basis of a finite-dimensional normed space are bounded (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space).
The range of a bounded projection is complemented (A closed subspace is complemented exactly when it is the range of a bounded projection).
Proof
By [F1], is a normed finite-dimensional quotient. Choose a basis of , representatives , and bounded coordinate maps supplied by [F2].
The map , , is bounded and satisfies . Hence is bounded, , and .
By [F3], is complemented.
Linear hyperplane
Definition
Let be a vector space over a field . A linear hyperplane of is a linear subspace such that is finite-dimensional over and . This is algebraic codimension one; closedness is an additional topological property, not part of the definition.
Closed hyperplanes are kernels of nonzero functionals
Statement
A linear hyperplane is closed if and only if for some nonzero .
Facts & Assumptions
Given: A linear hyperplane .
Since a linear hyperplane has codimension one, for any each has a unique decomposition with and (Linear hyperplane).
Since is closed, implies (The closure of a nonempty is , equals together with its limit points, and is the smallest closed superset).
Proof
Suppose is closed and choose . By [F1], define on . Uniqueness of the decomposition makes well defined and linear, with and .
By [F2], . For with , the vector has norm at least , since . Hence ; the same bound is clear for . Thus is bounded and nonzero, so and .
Conversely, if with nonzero, continuity makes closed. The induced nonzero map is injective and onto, so .
Mazur theorem: weak and norm closure agree for convex sets
Statement
Assume the Axiom of Choice. For a convex subset of a normed space , its norm closure equals its weak closure. Here the weak topology is generated by the basic neighbourhoods of
for finitely many and some .
Facts & Assumptions
Given: The Axiom of Choice, a convex set , and .
Disjoint convex sets, one open, are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).
The Axiom of Choice is used through the Hahn–Banach extension behind [F1].
Proof
Every is norm-continuous, so every displayed basic weak neighbourhood is norm-open. Thus every weak-open set is norm-open, and .
If , both closures are empty. Otherwise is nonempty; if , choose with . This latter set is open and convex, so under [A1], [F1] yields with for , .
Taking suprema over gives . The weak neighbourhood therefore misses , hence misses .
Thus is not in the weak closure whenever it is not in , proving the reverse inclusion and equality.
The sequence spaces c_0 and ell-infinity
Definition
Let or , with absolute value in the real case and modulus in the complex case. A scalar sequence here is a function , including index zero. Let
both equipped with . Thus is a specified linear subspace of the bounded-sequence space .
For each bounded sequence, the nonempty real set has a finite supremum by The Cauchy-sequence reals have the least-upper-bound property. This proves that the displayed norm exists, rather than presuming existence in the definition of boundedness. Its uniqueness requires no choice of supremum witnesses.
Here means that for every real there is such that for all . Addition and scalar multiplication are coordinatewise. The scalar triangle inequality makes bounded sequences and null sequences linear spaces and gives the triangle inequality for the displayed supremum norm. Absolute homogeneity follows coordinatewise, and a zero supremum forces every coordinate to vanish.
c_0 is a closed subspace of ell-infinity
Statement
is a closed linear subspace of in the sup norm.
Facts & Assumptions
Given: The sequence spaces .
consists of bounded sequences tending to zero, with the sup norm (The sequence spaces c_0 and ell-infinity).
Proof
Sums and scalar multiples of null sequences are null, so is a linear subspace.
If and , choose with this norm below , then with for . Thus for .
Hence and the subspace is closed.
5 · Examples, counterexamples and false statements
None yet.
Sources
- Gerald Teschl, Topics in Real and Functional Analysis, §5.1
- Gerald Teschl, Topics in Real and Functional Analysis, Lemma 5.1
- Theo Buehler and Dietmar Salamon, Functional Analysis, §2.3.3
- Gerald Teschl, Topics in Real and Functional Analysis, Theorems 5.2--5.3
- Theo Buehler and Dietmar Salamon, Functional Analysis, Theorem 2.41
- Gerald Teschl, Topics in Real and Functional Analysis, Corollary 5.4
- Theo Buehler and Dietmar Salamon, Functional Analysis, Exercise 2.51
- Theo Buehler and Dietmar Salamon, Functional Analysis, Definition 2.52
- Theo Buehler and Dietmar Salamon, Functional Analysis, Theorem 2.53
- Theo Buehler and Dietmar Salamon, Functional Analysis, Corollary 2.55
- Theo Buehler and Dietmar Salamon, Functional Analysis, Corollary 2.56
- Piotr Hajlasz, Functional Analysis, Theorem 10.17(a)
- Piotr Hajlasz, Functional Analysis, Theorem 10.17(b)
- Theo Buehler and Dietmar Salamon, Functional Analysis, Definition 2.46
- Theo Buehler and Dietmar Salamon, Functional Analysis, Exercise 2.47
- Gerald Teschl, Topics in Real and Functional Analysis, Theorem 5.11
- Piotr Hajlasz, Functional Analysis, §10.5