[proofplan]
We test sequential weak lower semicontinuity on an arbitrary bounded weakly convergent sequence $(u_k)$ in $X$. The compactness of the embedding $j:X\to Y$ converts boundedness in $X$ into strong subsequential convergence in $Y$, and the [weak convergence](/page/Weak%20Convergence) identifies the only possible strong $Y$-limit as $j u$. We then choose a subsequence realizing the liminf of $I[u_k]$, pass to a compactly convergent further subsequence, use continuity of $J$, and combine this with the weak lower semicontinuity of $I_0$.
[/proofplan]
[step:Fix a bounded weakly convergent sequence and name the liminf]
Let $(u_k)_{k=1}^{\infty}$ be a bounded sequence in $X$, and suppose that $u_k\rightharpoonup u$ in $X$. Define
\begin{align*}
L=\liminf_{k\to\infty} I[u_k]\in[-\infty,\infty].
\end{align*}
We prove that $I[u]\le L$.
If $L=+\infty$, the inequality is immediate because $I[u]\in(-\infty,\infty]$. Hence assume $L<+\infty$. By the defining property of the liminf, there exists a strictly increasing sequence of indices $(k_m)_{m=1}^{\infty}$ such that
\begin{align*}
I[u_{k_m}]\to L
\end{align*}
in the extended real sense as $m\to\infty$.
[/step]
[step:Extract strong convergence in $Y$ from compactness of the embedding]
Since $(u_{k_m})_{m=1}^{\infty}$ is bounded in $X$ and $j:X\to Y$ has the compactness property stated in the theorem, there are a further strictly increasing sequence of indices $(m_\ell)_{\ell=1}^{\infty}$ and an element $y\in Y$ such that
\begin{align*}
j u_{k_{m_\ell}}\to y
\end{align*}
strongly in $Y$.
We claim that $y=j u$. Indeed, because $u_{k_{m_\ell}}\rightharpoonup u$ in $X$ and $j:X\to Y$ is continuous and linear, every functional $\varphi\in Y^*$ gives a functional $\varphi\circ j\in X^*$. Therefore
\begin{align*}
\varphi(j u_{k_{m_\ell}})=(\varphi\circ j)(u_{k_{m_\ell}})\to(\varphi\circ j)(u)=\varphi(j u).
\end{align*}
Thus $j u_{k_{m_\ell}}\rightharpoonup j u$ weakly in $Y$. Strong convergence in $Y$ also implies weak convergence in $Y$ to the same limit $y$, so uniqueness of weak limits in the [Banach space](/page/Banach%20Space) $Y$ gives $y=j u$. Hence
\begin{align*}
j u_{k_{m_\ell}}\to j u
\end{align*}
strongly in $Y$.
[guided]
The compactness hypothesis is used only after we have a bounded sequence. Since $(u_k)$ is bounded in $X$, its subsequence $(u_{k_m})$ is also bounded in $X$. Compactness of the continuous linear embedding
\begin{align*}
j:X\to Y
\end{align*}
means precisely that the image under $j$ of every bounded sequence in $X$ has a strongly convergent subsequence in $Y$. Therefore there are indices $(m_\ell)_{\ell=1}^{\infty}$ and some element $y\in Y$ such that
\begin{align*}
j u_{k_{m_\ell}}\to y
\end{align*}
with respect to the norm of $Y$.
The remaining point is to identify the limit $y$. Compactness alone only gives a limit in $Y$; it does not immediately say that the limit is $j u$. The weak convergence in $X$ supplies the identification. Let $\varphi:Y\to\mathbb R$ be any bounded linear functional, so $\varphi\in Y^*$. Since $j:X\to Y$ is continuous and linear, the composition
\begin{align*}
\varphi\circ j:X\to\mathbb R
\end{align*}
is a bounded linear functional on $X$, hence belongs to $X^*$. From $u_{k_{m_\ell}}\rightharpoonup u$ in $X$, we obtain
\begin{align*}
(\varphi\circ j)(u_{k_{m_\ell}})\to(\varphi\circ j)(u).
\end{align*}
Equivalently,
\begin{align*}
\varphi(j u_{k_{m_\ell}})\to\varphi(j u).
\end{align*}
This is exactly the statement that $j u_{k_{m_\ell}}\rightharpoonup j u$ weakly in $Y$.
On the other hand, the same sequence converges strongly in $Y$ to $y$. Strong convergence implies weak convergence to the same strong limit: for each $\varphi\in Y^*$, continuity of $\varphi$ gives
\begin{align*}
\varphi(j u_{k_{m_\ell}})\to\varphi(y).
\end{align*}
The scalar limit is unique, so $\varphi(y)=\varphi(j u)$ for every $\varphi\in Y^*$. By the [Hahn-Banach separation theorem](/theorems/974), bounded linear functionals separate points in a Banach space, so this implies $y=j u$. Therefore the compact subsequence satisfies
\begin{align*}
j u_{k_{m_\ell}}\to j u
\end{align*}
strongly in $Y$.
[/guided]
[/step]
[step:Pass the compact perturbation to the limit]
Because $J:Y\to\mathbb R$ is continuous in the norm topology and
\begin{align*}
j u_{k_{m_\ell}}\to j u
\end{align*}
strongly in $Y$, we have
\begin{align*}
J(j u_{k_{m_\ell}})\to J(j u).
\end{align*}
[/step]
[step:Combine weak lower semicontinuity of $I_0$ with continuity of $J$]
Since $u_{k_{m_\ell}}\rightharpoonup u$ in $X$ and $I_0$ is sequentially weakly lower semicontinuous on $X$,
\begin{align*}
I_0[u]\le \liminf_{\ell\to\infty} I_0[u_{k_{m_\ell}}].
\end{align*}
Using the convergence of $J(j u_{k_{m_\ell}})$ to the finite number $J(j u)$, and the extended-real identity $\liminf_{\ell\to\infty}(a_\ell+b_\ell)=\liminf_{\ell\to\infty}a_\ell+b$ whenever $b_\ell\to b\in\mathbb R$, we get
\begin{align*}
I_0[u]+J(j u)\le \liminf_{\ell\to\infty}\bigl(I_0[u_{k_{m_\ell}}]+J(j u_{k_{m_\ell}})\bigr).
\end{align*}
The expression on the right is
\begin{align*}
\liminf_{\ell\to\infty} I[u_{k_{m_\ell}}].
\end{align*}
Since the subsequence $(u_{k_m})$ was chosen so that $I[u_{k_m}]\to L$, every further subsequence has the same extended-real limit $L$. Therefore
\begin{align*}
I[u]\le L.
\end{align*}
Substituting the definition of $L$ gives
\begin{align*}
I[u]\le \liminf_{k\to\infty} I[u_k].
\end{align*}
This proves that $I$ is sequentially weakly lower semicontinuous on bounded subsets of $X$.
[/step]
