\begin{definition}[Ruzsa distance]\label{ruz-dist-def}
  \uses{entropy-def, independent-exist}
  \lean{rdist_def}\leanok
  Let $X,Y$ be $G$-valued random variables (not necessarily on the same sample space).  The \emph{Ruzsa distance} $d[X ;Y]$ between $X$ and $Y$ is defined to be
$$ d[X ;Y] := \bbH[X' - Y'] - \bbH[X']/2 - \bbH[Y']/2$$
where $X',Y'$ are (the canonical) independent copies of $X,Y$ from \Cref{independent-exist}.
\end{definition}
/-- Explicit formula for the Ruzsa distance. -/
lemma rdist_def (X : Ω → G) (Y : Ω' → G) (μ : Measure Ω) (μ' : Measure Ω') :
    d[X ; μ # Y ; μ']
      = H[fun x ↦ x.1 - x.2 ; (μ.map X).prod (μ'.map Y)] - H[X ; μ]/2 - H[Y ; μ']/2 := rfl