Theorem: Banach-Dieudonné Theorem

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $B_{X^\ast}^-$ be the closed unit ball in $X^\ast$.
Let $w^\ast$ be the weak-$\ast$ topology in $X^\ast$.
Let $A$ be a convex set in $X^\ast$ such that:
:$A \cap n B_{X^\ast}^-$ is $w^\ast$-closed for each $n \in \N$.
Then $A$ is $w^\ast$-closed.

Proof:
We first consider the case $\GF = \R$.
Note that the conclusion is entirely independent of whether $\R$ or $\C$ is used, so this is unproblematic.
Throughout we work in the dual system $\innerprod X {X^\ast}$ over $\R$, where:
:$\innerprod x f = \map f x$ for each $\tuple {x, f} \in X \times X^\ast$.
We are assured that this is a dual system from Normed Vector Space with Normed Dual Space is Dual System.
We take absolute polars, one-sided polars and so forth in this dual system.
We first argue that for each $f_0 \in A$, we have that:
:$A \cap \paren {f + n B_{X^\ast}^-}$ is $w^\ast$-closed for each $n \in \N$.
Let $M \in \N$ be such that $\norm f_{X^\ast} \le M$. 
Note that for each $g \in B_{X^\ast}$, we have:
{{begin-eqn}}
{{eqn	| l = \norm {f + n g}_{X^\ast}
		| o = \le
		| r = \norm f_{X^\ast} + n \norm g_{X^\ast}
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| o = \le
		| r = M + n
		| c = since $g \in B_{X^\ast}^-$
}}
{{end-eqn}}
Hence:
:$f + n B_{X^\ast}^- \subseteq \paren {M + n} B_{X^\ast}$ for each $n \in \N$. 
From Closed Unit Ball in Normed Dual Space is Weak-* Closed, we have that:
:$f + n B_{X^\ast}^-$ is $w^\ast$-closed.
Further by hypothesis:
:$A \cap \paren {\norm f_{X^\ast} + n} B_{X^\ast}$ is $w^\ast$-closed.
Hence:
:$A \cap \paren {\norm f_{X^\ast} + n} B_{X^\ast} \cap \paren {f + n B_{X^\ast}^-}$ is $w^\ast$-closed.
By Intersection is Associative and Intersection with Subset is Subset, we therefore have:
:$A \cap \paren {f + n B_{X^\ast}^-}$ is $w^\ast$-closed.
Let $f \in A$.
Then we have that:
:$A \cap \paren {f + n B_{X^\ast}^-}$ is $w^\ast$-closed.
By Translation of Intersection of Subsets of Vector Space and Translation of Closed Set in Topological Vector Space is Closed Set, we have that:
:$A \cap \paren {f + n B_{X^\ast}^-} - f = \paren {A - f} \cap n B_{X^\ast}$ is $w^\ast$-closed for each $n \in \N$.
By Translation of Convex Set in Vector Space is Convex, $A - f$ is convex and contains ${\mathbf 0}_{X^\ast}$.
{{WLOG}}, by replacing $A$ with $A - f$ (with $f \in A$) if necessary, suppose that ${\mathbf 0}_{X^\ast} \in A$.
Note that the conclusion will remain the same, from Translation of Closed Set in Topological Vector Space is Closed Set.
We now show that $A$ is (norm) closed.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a convergent sequence valued in $A$ with limit $f$. 
We aim to show that $f \in A$.
From Convergent Sequence in Normed Vector Space is Bounded, there exists $N \in \N$ such that:
:$f_n \in A \cap N B_{X^\ast}^-$ for each $n \in \N$.
From Convergence in Normed Dual Space implies Weak-* Convergence, we have that $\sequence {f_n}_{n \mathop \in \N}$ converges weak-$\ast$ to $f$. 
Since $A \cap N B_{X^\ast}^-$ is $w^\ast$-closed, we have that $f \in A \cap N B_{X^\ast}^- \subseteq A$.
Since $\sequence {f_n}_{n \mathop \in \N}$ was an convergent sequence valued in $A$, we have that $A$ is (norm) closed.
Now, for each $n \in \N$ set:
:$A_n = A \cap 2^n B_{X^\ast}^-$ 
From Closed Unit Ball is Convex Set, $B_{X^\ast}^-$ is convex.
From Dilation of Convex Set in Vector Space is Convex, $2^n B_{X^\ast}^-$ is convex.
From Intersection of Convex Sets is Convex Set (Vector Spaces), $A_n$ is convex.
Further, since ${\mathbf 0}_{X^\ast} \in n B_{X^\ast}^-$ for each $n \in \N$, we have:
:${\mathbf 0}_{X^\ast} \in A_n$ 
Let $\paren {A_n}_\odot$ be the one-sided prepolar of $A_n$.
Let $\paren {\paren {A_n}_\odot}^\odot$ be the one-sided polar of $A_n$.
Let $\cl_{w^\ast}$ be the closure taken in $\struct {X^\ast, w^\ast}$. 
From Bipolar Theorem: Corollary: One Sided Polar, we have:
:$\paren {\paren {A_n}_\odot}^\odot = \map {\cl_{w^\ast} } {\map {\operatorname {conv} } {A_n} }$
Since $A_n$ is convex, we have:
:$\map {\operatorname {conv} } {A_n} = A_n$
from Convex Hull is Smallest Convex Set containing Set: Corollary.
From Set is Closed iff Equals Topological Closure, we have $\map {\cl_{w^\ast} } {A_n} = A_n$ .
We have:
:$\paren {\paren {A_n}_\odot}^\odot = A_n$
Let:
:$\ds G = \bigcap_{n \mathop = 1}^\infty \paren {A_n}_\odot$
Our goal is now to show that $A = G^\odot$, where $G^\odot$ is the one-sided polar of $G$.
From One-Sided Polar is Closed in Weak-* Topology, we will have that $G^\odot$, and hence $A$, is $w^\ast$-closed.
Note that we have:
:$G \subseteq \paren {A_n}_\odot$ for each $n \in \N$.
Hence from One-Sided Polar Reverses Subset Relation, we have:
:$\paren {\paren {A_n}_\odot}^\odot \subseteq G^\odot$ for each $n \in \N$.
We have already established that:
:$\paren {\paren {A_n}_\odot}^\odot = A_n$ for each $n \in \N$.
Hence:
:$A_n \subseteq G^\odot$ for each $n \in \N$. 
Hence we have:
:$\ds \bigcup_{n \mathop = 1}^\infty A_n \subseteq G^\odot$
That is:
:$A \subseteq G^\odot$
It remains to show that $G^\odot \subseteq A$.