The Hahn-Banach Theorem in functional analysis is the theorem saying more or less that normed vector spaces have many bounded linear functionals. The theorem is usually proven via Zorn’s lemma, giving the impression that Hahn-Banach uses the full power of choice. I’ll here give a proof based on the ultrafilter lemma, that every filter can be extended to an ultrafilter. One of the benefits of this approach, besides relying on a (strictly) weaker assumption, is that we get a little more information about how the functionals are constructed. The idea is that the ultrafilters allow us to “glue” functionals together. A latex’ed version can be found here.
Let’s start off with reviewing what Hahn-Banach is actually saying. First of all, say that a seminorm on a vector space is a function such that
- (Non-negative) ;
- (Subadditivity) ;
- (Absolute homogeneity) .
A functional is simply a linear function from a vector space to its underlying field.
Hahn-Banach Theorem. Let be a normed space, a subspace, a functional on , a seminorm on such that for every . Then there is a linear functional on such that for every and for every .
To prove this we first show a weaker version, which can be proven in ZF.
Finite Extension Lemma (ZF). Let , , and be as in the Hahn-Banach Theorem. Then for any there is a linear functional on which extends and satisfies that for every .
The proof is roughly that in this finite case we get a closed interval of possible values of , so we can simply pick one of those. For more details see e.g. my note. We will prove Hahn-Banach in the case where is a real vector space, as the transition to the complex case is standard. Define the set as
iff is a linear functional extending , defined on a subspace that contains , and which is absolutely bounded by .
Then to any set to be all those with . The finite extension lemma implies that all the ‘s are non-empty and furthermore that finite intersections of them are non-empty as well. The ‘s then form a “subbasis” for a filter :
Use the ultrafilter lemma to extend to an ultrafilter on . It then holds that given any , for -a.e. . Now form the (ill-founded) ultrapower with associated ultrapower embedding
Then setting we see that given any , , giving us a candidate for an extension! But note that is a function into the hyperreals (inside the ultrapower), so it’s not really a functional. But the hyperreals has the nifty feature that there is a homomorphism called the standard part. This is basically by the completeness of the reals, so that to any hyperreal we can associate a unique real such that their difference is infinitesimal. Then set to be the functional on defined as
As extends for -a.e. , we get that . This means that
for every , so does in fact extend . Furthermore, note that for every , so that
showing that is absolutely bounded by as well. QED
Note that the function in the proof was defined as , so that really it corresponds to all the functionals that we’re interested in, at the same time. The ultrafilters are thus used for this sort of “gluing”, that if we can just make sure that a given property holds for many partial functionals, there is a canonical functional with the property as well.
This note was inspired by Asaf Karagila’s note on Hahn-Banach and the Axiom of Choice.