[proofplan] We use the Hahn-Banach theorem to construct a norming functional $f_x \in X^*$ with $\|f_x\|_{X^*} = 1$ and $f_x(x) = \|x\|_X$. Evaluating $f_x$ along the weakly convergent sequence gives $f_x(x_n) \to \|x\|_X$. The operator norm bound $|f_x(x_n)| \leq \|x_n\|_X$ then yields the desired inequality upon passing to the $\liminf$. [/proofplan] [step:Construct a norming functional via the Hahn-Banach theorem] By the Hahn-Banach theorem applied to the Banach space $X$, for the element $x \in X$ there exists a functional $f_x \in X^*$ satisfying \begin{align*} \|f_x\|_{X^*} = 1 \quad \text{and} \quad f_x(x) = \|x\|_X. \end{align*} This follows from the Hahn-Banach extension theorem: the linear functional $\ell: \mathbb{R} x \to \mathbb{R}$ defined by $\ell(\alpha x) = \alpha \|x\|_X$ has norm $1$ on the one-dimensional subspace $\operatorname{span}\{x\}$, and Hahn-Banach extends it to all of $X$ without increasing the norm. [guided] The existence of norming functionals is a fundamental consequence of the Hahn-Banach theorem. We construct $f_x$ as follows. On the one-dimensional subspace $\operatorname{span}\{x\}$, define \begin{align*} \ell: \operatorname{span}\{x\} &\to \mathbb{R} \\ \alpha x &\mapsto \alpha \|x\|_X. \end{align*} This functional has norm $1$ on $\operatorname{span}\{x\}$: $|\ell(\alpha x)| = |\alpha|\|x\|_X = \|\alpha x\|_X$. By the Hahn-Banach extension theorem, $\ell$ extends to $f_x \in X^*$ with $\|f_x\|_{X^*} = 1$, and $f_x(x) = \ell(x) = \|x\|_X$. In a Hilbert space $H$, the norming functional is easy to identify: $f_x(v) = (x, v)_H / \|x\|_H$ does the job. In a general [Banach space](/page/Banach%20Space), the construction is non-constructive and relies on the Axiom of Choice. [/guided] [/step] [step:Evaluate the norming functional along the weakly convergent sequence] Since $x_n \rightharpoonup x$ in $X$, the definition of weak convergence gives $f(x_n) \to f(x)$ for every $f \in X^*$. Applying this with $f = f_x$: \begin{align*} f_x(x_n) \to f_x(x) = \|x\|_X. \end{align*} [/step] [step:Bound each term using the operator norm and pass to the $\liminf$] For every $n \in \mathbb{N}$, the definition of the operator norm $\|f_x\|_{X^*} = 1$ gives \begin{align*} |f_x(x_n)| \leq \|f_x\|_{X^*} \cdot \|x_n\|_X = \|x_n\|_X. \end{align*} Combining with the convergence from the previous step: \begin{align*} \|x\|_X = \lim_{n \to \infty} f_x(x_n) = \lim_{n \to \infty} |f_x(x_n)| \leq \liminf_{n \to \infty} \|x_n\|_X, \end{align*} where the equality $\lim f_x(x_n) = \lim |f_x(x_n)|$ holds because the limit $f_x(x_n) \to \|x\|_X \geq 0$ is non-negative, and the final inequality uses $|f_x(x_n)| \leq \|x_n\|_X$ together with the monotonicity of $\liminf$ under pointwise inequalities. [guided] The chain of reasoning is: the norming functional $f_x$ satisfies $\|f_x\|_{X^*} = 1$ and $f_x(x) = \|x\|_X$. The operator norm bound gives $|f_x(x_n)| \leq \|x_n\|_X$ for every $n$. Weak convergence gives $f_x(x_n) \to f_x(x) = \|x\|_X$. Combining: \begin{align*} \|x\|_X = \lim_{n \to \infty} f_x(x_n) = \lim_{n \to \infty} |f_x(x_n)| \leq \liminf_{n \to \infty} \|x_n\|_X. \end{align*} The equality $\lim f_x(x_n) = \lim |f_x(x_n)|$ holds because $f_x(x_n) \to \|x\|_X \geq 0$. The final inequality uses $|f_x(x_n)| \leq \|x_n\|_X$ together with the monotonicity of $\liminf$: if $a_n \leq b_n$ for all $n$, then $\liminf a_n \leq \liminf b_n$. Why is strict inequality possible? Consider the sequence $e_n$ of standard basis vectors in $\ell^2$. This sequence converges weakly to $0$ (since for any $(a_n) \in \ell^2$, $\langle (a_n), e_n \rangle = a_n \to 0$), but $\|e_n\|_{\ell^2} = 1$ while $\|0\|_{\ell^2} = 0$. The energy "escapes to infinity" in the coordinate directions, and the weak limit captures none of it. [/guided] [/step]