Does weak $L^2$ convergence $+$ (uniform) $H^1$ boundedness imply weak $H^1$ convergence on bounded domains?

I'm really surprised I can't seem to find this statement anywhere, even though it seems to follow from compactness theorems, I'm therefore wondering whether I made a mistake in my proof below.

Claim: Let $$\Omega$$ be a sufficiently nice bounded domain. Let $$u_n \in H^1(\Omega)$$ with $$u_n \rightharpoonup u$$ in $$L^2$$, where $$\rightharpoonup$$ denotes weak convergence. Assume further that $$\| \nabla u_n\|_{L^2} \leq C$$ for some $$C > 0$$ independent of $$n$$. Then $$u_n \rightharpoonup u$$ in $$H^1$$.

Proof: Since $$u_n$$ is bounded in $$H^1$$, it must have a $$H^1$$-weakly convergent subsequence to some $$\tilde u \in H^1$$ by the sequential Banach-Alaoglu theorem. Since this subsequence is also $$L^2$$-weakly convergent and weak limits are unique, it is true that $$u = \tilde u$$ and in particular $$u \in H^1$$. Now assume that the sequence $$u_n$$ does not converge weakly to $$u$$. Then there must be some subsequence that is completely outside of a neighborhood $$U$$ of $$u$$. By the same compactness argument, this subsequence again has a $$H^1$$-weakly convergent subsequence which must converge to $$u$$, and hence be in $$U$$ infinitely often, a contradiction.

The result is true and your argument is correct. A slightly better phrasing might be to show that every subsequence of $$u_n$$ has a further subsequence that converges weakly to $$u$$ in $$H^1$$. It is then a standard topological result that this implies that $$u_n \rightharpoonup u$$. In fact, the last part of your argument would essentially prove the general topological result.
• thanks! Since strong $L^2$ convergence implies weak $L^2$ convergence, this in particular implies that the $H^1$-unit ball is $L^2$ closed? Moreover, by the Rellich-Kondrachev theorem, a similar argument should give that the $u_n \rightarrow u$ in $L^2$ (or, as a corollary: sequential weak $H^1$ convergence implies strong $L^2$ convergence). I guess I'm just surprised I haven't come across any of these results, but only versions that deal with subsequences and not the whole sequence. Jul 25, 2019 at 10:51