\begin{lemma}[Ruzsa distance in independent case]\label{ruz-indep}
  \uses{ruz-dist-def}
  \lean{ProbabilityTheory.IndepFun.rdist_eq}\leanok
  If $X,Y$ are independent $G$-random variables then
  $$ d[X ;Y] := \bbH[X - Y] - \bbH[X]/2 - \bbH[Y]/2.$$
\end{lemma}
\begin{proof} \uses{relabeled-entropy, copy-ent}\leanok Immediate from \Cref{ruz-dist-def} and Lemmas \ref{relabeled-entropy}, \ref{copy-ent}.
\end{proof}
/-- If `X, Y` are independent `G`-random variables then `d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2`. -/
lemma ProbabilityTheory.IndepFun.rdist_eq [IsFiniteMeasure μ]
    {Y : Ω → G} (h : IndepFun X Y μ) (hX : Measurable X) (hY : Measurable Y) :
    d[X ; μ # Y ; μ] = H[X - Y ; μ] - H[X ; μ]/2 - H[Y ; μ]/2 := by
  rw [rdist_def]
  congr 2
  have h_prod : (μ.map X).prod (μ.map Y) = μ.map (⟨X, Y⟩) :=
    ((indepFun_iff_map_prod_eq_prod_map_map hX.aemeasurable hY.aemeasurable).mp h).symm
  rw [h_prod, entropy_def, Measure.map_map (measurable_fst.sub measurable_snd) (hX.prodMk hY)]
  rfl