Proposition 5 — strong duality and a primal optimizer on compact $S$ with continuous cost

Let $S$ be a compact Polish space, $\mu$ a Borel probability measure on $S$, $c$ a cost satisfying (A1) that is in addition continuous on $S\times S$, $f:S\to\mathbb R$ upper semicontinuous and $\mu$-integrable (A2), and $\delta>0$. Then

and there is a primal optimizer $\pi^*\in\Phi_{\mu,\delta}$ with $I(\pi^*)=I$.

This is the first step of the proof of Theorem 1, obtained from Fenchel duality on $C_b(S\times S)$.

Formalization Note The space $S$ is a Polish space with its Borel σ-algebra; the cost $c$ is real-valued and written curried, $c\,x\,y = c(x,y)$; (A1) is the structure AssumptionA1; (A2) is the pair of hypotheses UpperSemicontinuous f and Integrable f μ. Values that can be infinite ($I$, $J$, $I(\pi)$, $J(\lambda,\varphi)$, $\varphi_\lambda$) live in EReal; an integral of an extended-real function is $\int\varphi^+ - \int\varphi^-$ with lower Lebesgue integrals, and $\infty-\infty$ evaluates to $-\infty$, so a coupling with $\int f^-\,d\pi=\infty$ never raises the primal supremum (the paper's footnote 2 reading).