= Solution
For each real $a$, define the <sublevel set> $K_a=\{u\in K:F(u)\leq a\}$. Continuity of $F$ and closure of $K$ make $K_a$ a <closed set> in $X$; the <convex function> inequality makes it a <convex set>. The preceding result therefore makes every $K_a$ a <sequentially weakly closed set>. Equivalently, $F$ has <weak lower semicontinuity> along sequences in $K$.
Every $K_a$ is bounded. This is immediate if $K$ is bounded. Otherwise, an unbounded $K_a$ would contain $u_n$ with $\|u_n\|\geq n$, contradicting the assumed <coercive function> condition $F(u_n)\to\infty$.
Choose $z\in K$ and put $\ell=\inf_KF\in[-\infty,F(z)]$. Choose a <minimizing sequence> $(u_n)$ entirely in $K_{F(z)}$, with $F(u_n)\to\ell$; when $\ell=-\infty$, require $F(u_n)\leq-n$ for sufficiently large $n$. It is bounded by the previous paragraph.
The <weak subsequence of a bounded Hilbert-space sequence> theorem gives $u_{n_j}\rightharpoonup u_0$. This applies even if $X$ is not separable: the closed <linear span> of the sequence is a <separable Hilbert space>; successive extraction makes every coefficient in a countable <Hilbertian basis> converge, the common <norm> bound gives square-summable limiting coefficients by the <Bessel inequality>, and approximation by finite <linear combinations> proves <weak convergence>. <Orthogonal decomposition> extends that conclusion to all test vectors in $X$. Since $K$ is a <sequentially weakly closed set>, $u_0\in K$.
For any real $a>\ell$, a tail of $(u_{n_j})$ lies in $K_a$, so $u_0\in K_a$. If $\ell=-\infty$, this would give $F(u_0)\leq a$ for every real $a$, impossible because $F$ is real-valued. Thus $\ell$ is finite; letting $a\downarrow\ell$ gives $F(u_0)\leq\ell$, while the definition of <infimum> gives the reverse inequality. Therefore
$$
\boxed{u_0\in K,\qquad F(u_0)=\min_{u\in K}F(u).}
$$
This proves <minimum of a coercive convex functional on a Hilbert space> by the <direct method in the calculus of variations>, with bounded <sublevel sets> supplying the required <weak sequential compactness in a Hilbert space>.
Back to article page
