User:Caliburn/s/fa/Normed Vector Space with Separable Dual is Separable

Theorem

Let $\struct {X, \norm \cdot_X}$ be a normed vector space.

Let $\struct {X^\ast, \norm \cdot_{X^\ast} }$ be the normed dual space of $X$.

Then, if $X^\ast$ is separable:

$X$ is separable.

Proof

From Characterization of Separable Normed Vector Space, we have that:

$S_{X^\ast} = \set {f \in X^\ast : \norm f_{X^\ast} = 1}$ is separable.

Let $\mathcal S_{X^\ast} = \set {f_n : n \in \N}$ be a countable everywhere dense subset of $S_{X^\ast}$.

For each $n \in \N$, pick $x_n \in X$ such that $\norm {x_n}_X = 1$ and:

$\ds \size {\map {f_n} {x_n} } \ge \frac 1 2$

Let:

$M = \span \set {x_1, x_2, \ldots}$

From Characterization of Separable Normed Vector Space, it suffices to show that:

$M^- = X$

Suppose that $M^- \ne X$.

From Closed Linear Span is Closed Linear Subspace, we have that:

$M^-$ is a closed linear subspace.

So, from Existence of Distance Functional, there exists $f \in X^\ast$ such that:

$\map f x = 0$ for each $x \in M^-$ and $\norm f_{X^\ast} = 1$.

That is, $f \in S_{X^\ast}$.

Then we have:

$\map f {x_n} = 0$ for each $n \in \N$

and so:

\(\ds \size {\map {f_n} {x_n} }\)

\(=\)

\(\ds \size {\map {f_n} {x_n} - \map f {x_n} }\)

\(\ds \)

\(\le\)

\(\ds \norm {f_n - f}_{X^\ast} \norm {x_n}_X\)

Definition of Norm on Bounded Linear Functional

\(\ds \)

\(=\)

\(\ds \norm {f_n - f}_{X^\ast}\)

However since:

$\ds \size {\map {f_n} {x_n} } \ge \frac 1 2$

for each $n \in \N$, we have:

$\ds \norm {f_n - f}_{X^\ast} \ge \frac 1 2$

for each $n \in \N$.

So there does not exist $g \in \mathcal S_{X^\ast}$ such that:

$\ds \norm {g - f}_{X^\ast} < \frac 1 3$

while $f \in S_{X^\ast}$.

This contradicts that $\mathcal S_{X^\ast}$ is everywhere dense in $S_{X^\ast}$.

So we must have $M^- = X$.

So, from Characterization of Separable Normed Vector Space, we have:

$X$ is separable.