[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$.[/step]

[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: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]