[proofplan] The proof has two parts. First, the tightness theorem for couplings gives tightness of $\Pi(\mu,\nu)$, and [Prokhorov's theorem](/theorems/1172) turns this tightness into relative compactness because $X \times Y$ is Polish. Second, we prove that the marginal constraints are weakly closed by testing [weak convergence](/page/Weak%20Convergence) against bounded continuous functions pulled back along the coordinate projections. A relatively compact subset that is also closed is compact. [/proofplan]

[step:Use tightness and Prokhorov's theorem to obtain relative compactness] Let $p_X: X \times Y \to X$ and $p_Y: X \times Y \to Y$ denote the coordinate projections. Since $X$ and $Y$ are Polish spaces, their product $X \times Y$, equipped with the [product topology](/page/Product%20Topology), is also Polish. By the tightness of the coupling set, $\Pi(\mu,\nu)$ is tight as a family of probability measures on $X \times Y$ (citing a result not yet in the wiki: Tightness of the coupling set). Prokhorov's theorem applies on the Polish space $X \times Y$ and says that every tight family in $\mathcal{P}(X \times Y)$ is relatively compact for weak convergence (citing a result not yet in the wiki: Prokhorov theorem). Hence the weak closure \begin{align*} \overline{\Pi(\mu,\nu)} \subset \mathcal{P}(X \times Y) \end{align*} is compact. [/step]

[step:Show that weak limits preserve the first marginal]Let $\pi \in \overline{\Pi(\mu,\nu)}$. By definition of closure, there is a net $(\pi_\lambda)_{\lambda \in \Lambda}$ in $\Pi(\mu,\nu)$ such that $\pi_\lambda \Rightarrow \pi$ weakly in $\mathcal{P}(X \times Y)$. We prove that $(p_X)_\#\pi = \mu$. Let $f: X \to \mathbb{R}$ be a bounded [continuous function](/page/Continuous%20Function). Define the pulled-back [test function](/page/Test%20Function) \begin{align*} F: X \times Y &\to \mathbb{R}, \quad F(x,y) := f(p_X(x,y)) = f(x). \end{align*} Since $p_X$ is continuous and $f$ is bounded and continuous, $F$ is bounded and continuous on $X \times Y$. Weak convergence of $\pi_\lambda$ to $\pi$ gives \begin{align*} \int_{X \times Y} F \, d\pi_\lambda \to \int_{X \times Y} F \, d\pi. \end{align*} For each $\lambda \in \Lambda$, the identity $(p_X)_\#\pi_\lambda = \mu$ gives, by the defining property of pushforward measures, \begin{align*} \int_{X \times Y} F \, d\pi_\lambda = \int_X f \, d\mu. \end{align*} Taking the limit in $\lambda$ therefore yields \begin{align*} \int_{X \times Y} F \, d\pi = \int_X f \, d\mu. \end{align*} Again using the defining property of the pushforward measure, \begin{align*} \int_X f \, d((p_X)_\#\pi) = \int_X f \, d\mu. \end{align*} Because bounded continuous functions determine Borel probability measures on the Polish space $X$, it follows that $(p_X)_\#\pi = \mu$.[/step]

[guided]We want to prove that the condition on the first marginal survives passage to a weak limit. Let $\pi \in \overline{\Pi(\mu,\nu)}$. By the definition of topological closure, there exists a net $(\pi_\lambda)_{\lambda \in \Lambda}$ in $\Pi(\mu,\nu)$ such that $\pi_\lambda \Rightarrow \pi$ weakly in $\mathcal{P}(X \times Y)$. We use a net rather than a sequence so that the argument proves closedness directly in the [weak topology](/page/Weak%20Topology). The first marginal is tested by bounded continuous functions on $X$. Let $f: X \to \mathbb{R}$ be bounded and continuous. To connect this test function on $X$ with weak convergence on $X \times Y$, pull it back along the first projection. Define \begin{align*} F: X \times Y &\to \mathbb{R}, \quad F(x,y) := f(p_X(x,y)) = f(x). \end{align*} The projection $p_X$ is continuous for the product topology, and $f$ is bounded and continuous, so $F = f \circ p_X$ is bounded and continuous on $X \times Y$. Therefore weak convergence of $\pi_\lambda$ to $\pi$ applies to this particular test function and gives \begin{align*} \int_{X \times Y} F \, d\pi_\lambda \to \int_{X \times Y} F \, d\pi. \end{align*} Now we use the fact that every $\pi_\lambda$ belongs to $\Pi(\mu,\nu)$. By definition of the coupling set, $(p_X)_\#\pi_\lambda = \mu$ for every $\lambda \in \Lambda$. The defining property of the pushforward measure says that integrating $f$ against the pushed-forward measure is the same as integrating $f \circ p_X$ against the original measure. Hence \begin{align*} \int_{X \times Y} F \, d\pi_\lambda = \int_X f \, d((p_X)_\#\pi_\lambda) = \int_X f \, d\mu. \end{align*} The left-hand side converges to $\int_{X \times Y} F \, d\pi$, while the right-hand side is independent of $\lambda$. Thus \begin{align*} \int_{X \times Y} F \, d\pi = \int_X f \, d\mu. \end{align*} Applying the pushforward identity once more, now to $\pi$, gives \begin{align*} \int_X f \, d((p_X)_\#\pi) = \int_X f \, d\mu. \end{align*} This equality holds for every bounded continuous function $f: X \to \mathbb{R}$. Since $X$ is Polish, bounded continuous functions determine Borel probability measures on $X$. Therefore $(p_X)_\#\pi = \mu$.[/guided]

[step:Show that weak limits preserve the second marginal] We prove analogously that $(p_Y)_\#\pi = \nu$. Let $g: Y \to \mathbb{R}$ be a bounded continuous function, and define \begin{align*} G: X \times Y &\to \mathbb{R}, \quad G(x,y) := g(p_Y(x,y)) = g(y). \end{align*} Since $p_Y$ and $g$ are continuous and $g$ is bounded, $G$ is bounded and continuous on $X \times Y$. Weak convergence gives \begin{align*} \int_{X \times Y} G \, d\pi_\lambda \to \int_{X \times Y} G \, d\pi. \end{align*} For every $\lambda \in \Lambda$, the marginal condition $(p_Y)_\#\pi_\lambda = \nu$ gives \begin{align*} \int_{X \times Y} G \, d\pi_\lambda = \int_Y g \, d\nu. \end{align*} Passing to the limit and using the pushforward identity for $\pi$ gives \begin{align*} \int_Y g \, d((p_Y)_\#\pi) = \int_Y g \, d\nu. \end{align*} Since bounded continuous functions determine Borel probability measures on the Polish space $Y$, we conclude that $(p_Y)_\#\pi = \nu$. [/step]

[step:Conclude that the coupling set is closed and therefore compact] The preceding two steps show that every $\pi \in \overline{\Pi(\mu,\nu)}$ satisfies \begin{align*} (p_X)_\#\pi = \mu \quad \text{and} \quad (p_Y)_\#\pi = \nu. \end{align*} Hence $\pi \in \Pi(\mu,\nu)$, so \begin{align*} \overline{\Pi(\mu,\nu)} \subset \Pi(\mu,\nu). \end{align*} The reverse inclusion holds for every set, and therefore $\Pi(\mu,\nu)$ is weakly closed in $\mathcal{P}(X \times Y)$. From the first step, $\overline{\Pi(\mu,\nu)}$ is compact. Since $\Pi(\mu,\nu) = \overline{\Pi(\mu,\nu)}$, the coupling set itself is compact for weak convergence in $\mathcal{P}(X \times Y)$. This proves the theorem. [/step]