Hahn–Banach extension and separation

In the real algebraic version, a sublinear function p is subadditive and positively homogeneous. If a real-linear functional on a linear subspace satisfies f≤p there, it extends to a real-linear functional with the same domination on the whole vector space. Completeness is not required. Choosing p(x)=C∥x∥ gives the familiar bounded extension theorem, and applying domination to x and −x produces the absolute bound. A maximal-extension argument supplies existence, but generally does not identify a unique extension.

For a complex vector space, the useful domination form uses a seminorm and an absolute-value inequality, not an order comparison of complex values. In particular, a bounded complex-linear functional extends complex-linearly with unchanged norm. One proof extends its real part on the underlying real space, obtaining g, and reconstructs the complex functional as g(x)−ig(ix). Multiplying x by a scalar of modulus one then verifies the full modulus bound. This reconstruction is essential: an arbitrary real-linear extension need not respect multiplication by i.

Given a nonzero vector x, define a functional on its one-dimensional span that takes value ∥x∥ at x and has norm one. Hahn–Banach extends it to the ambient space. Hence the norm of a vector is the supremum of its evaluations by dual unit-ball functionals, and that supremum is attained for each fixed vector. This does not say that every fixed functional attains its own norm on the primal unit ball; the order of the quantifiers is different. Such norm attainment can fail in nonreflexive spaces.

For a closed subspace M and a point outside it, apply the same argument in X/M and pull the functional back through the quotient map. The resulting norm-one functional vanishes on M and evaluates the chosen point at its distance from M, with a suitable phase in the complex case. This gives a lower-bound certificate for every candidate approximation from M. It still does not produce a nearest point in M. A dual certificate can identify an infimum even when no primal representative achieves that infimum.

In a real normed space, a point outside a nonempty closed convex set can be strictly separated from that set by a continuous linear functional with a positive gap. Over a complex space, use the real part of a complex-linear functional. One route separates the convex set from a sufficiently small open ball around the point. More general separation statements have different strengths: two disjoint convex sets with one open admit a separating functional, but two arbitrary disjoint closed convex sets need not admit a uniform positive separating gap.

Convexity and closedness play different roles. Convexity makes supporting linear inequalities describe the set, while closedness keeps an exterior point a positive distance from a small surrounding ball disjoint from the set. As a consequence, a norm-closed convex subset is also weakly closed, a fact used later in weak compactness arguments. None of these statements makes every closed nonconvex set weakly closed. Nor does scalar extension imply that every closed subspace has a bounded complementary projection; that stronger property distinguishes special Banach-space geometry.