Minimum of a coercive convex functional on a Hilbert space (source code)

= Minimum of a coercive convex functional on a Hilbert space
{title2=$\min_{x\in K}F(x)$}

Let $K$ be a nonempty norm-closed <convex set> in a real <Hilbert space>, and let $F:K\to\mathbb R$ be continuous and a <convex function>. If $K$ is bounded, or $F(x)\to\infty$ as $x\in K$ tends to infinity in <norm>, then $F$ attains its <infimum>. Every <sublevel set> is bounded, norm-closed, and convex, hence contains the weak limits of its sequences by <norm-closed convex set is weakly closed>. A <minimizing sequence> in one fixed <sublevel set> has a <weakly convergent> subsequence by <weak sequential compactness in a Hilbert space>. Its limit lies in every <sublevel set> above the <infimum>. Since $F$ is real-valued, this also rules out <infimum> $-\infty$ and proves attainment. This is an instance of the <direct method in the calculus of variations>.