An equivalent definition of a compact operator How can I show, that the following definitions of a compact operator are equivalent?
Definition 1:

An operator $A$ on a Hilbert space $H$ is called compact if for every bounded sequence $(x_n)$ in $H$, the sequence $(Ax_n)$ contains a convergent subsequence.

Definition 2:

An operator $A$ on a Hilbert space $H$ is called compact if $x_n \rightharpoonup x$ and $y_n \rightharpoonup y$ implies $(Ax_n, y_n) \to (Ax, y)$.

I managed to prove, that Definition 1. is equivalent to ($x_n \rightharpoonup x$ implies $Ax_n \to Ax$). Can I apply this result somehow?
 A: This is too large for a comment, but it is not a complete answer. Please see below for an explanation.
What you've shown is a good intermediate step.  Using this we can go from defintion 1. to definition 2., but we need one more (easy to prove) ingredient, which is that weakly convergent sequences are norm-bounded.
Suppose $x_n \rightharpoonup x$ and $y_n \rightharpoonup y$, and let $\varepsilon>0$ be given. For any $n\in\mathbb{N}$ we have
\begin{align}
|\langle Ax_n,y_n\rangle-\langle Ax,y\rangle|
&\leq |\langle Ax_n,y_n\rangle-\langle Ax,y_n\rangle|+|\langle Ax,y_n\rangle-\langle Ax,y\rangle| \\
&\leq\|Ax_n-Ax\|\|y_n\|+|\langle Ax,y_n\rangle-\langle Ax,y\rangle|
\end{align}
Since $y_n \rightharpoonup y$, the sequence $\{y_n\}$ is norm-bounded, so there is some $M>0$ with $\|y_n\|<M$ for all $n$. If $A$ satisfies definition 1., then there is some $N_1\in\mathbb N$ such that $\|Ax_n-Ax\|<\varepsilon/2M$ for $n\geq N_1$.  Since $y_n \rightharpoonup y$, there is some $N_2\in\mathbb N$ such that $|\langle Ax,y_n\rangle-\langle Ax,y\rangle|<\varepsilon/2$ for all $n\geq N_2$.  Then for $n\geq\max\{N_1,N_2\}$ we have
\begin{align}
|\langle Ax_n,y_n\rangle-\langle Ax,y\rangle|
&\leq\|Ax_n-Ax\|\|y_n\|+|\langle Ax,y_n\rangle-\langle Ax,y\rangle| \\
&<M\varepsilon/2M+\varepsilon/2=\varepsilon,
\end{align}
and thus $(Ax_n, y_n) \to (Ax, y)$. 
This shows definition 1. implies definition 2.  At the moment, the only way I can prove the reverse implication relies on some machinery you may not be familiar with (the Banach-Alaoglu and the Eberlein-Smulian theorems), but I will consider this some more and edit.
