\begin{lemma}[Distance controls entropy difference]\label{ruzsa-diff}
  \uses{ruz-dist-def}
  \lean{diff_ent_le_rdist}\leanok
  If $X,Y$ are $G$-valued random variables, then
$$|\bbH[X]-H[Y]| \leq 2 d[X ;Y].$$
\end{lemma}
\begin{proof} \uses{sumset-lower, neg-ent} \leanok Immediate from \Cref{sumset-lower} and \Cref{ruz-dist-def}, and also \Cref{neg-ent}.
\end{proof}
/-- `|H[X] - H[Y]| ≤ 2 d[X ; Y]`. -/
lemma diff_ent_le_rdist [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) :
    |H[X ; μ] - H[Y ; μ']| ≤ 2 * d[X ; μ # Y ; μ'] := by
  obtain ⟨ν, X', Y', _, hX', hY', hind, hIdX, hIdY, _, _⟩ := independent_copies_finiteRange hX hY μ μ'
  rw [← hIdX.rdist_eq hIdY, hind.rdist_eq hX' hY', ← hIdX.entropy_eq, ← hIdY.entropy_eq, abs_le]
  have := max_entropy_le_entropy_sub hX' hY' hind
  constructor
  · linarith[le_max_right H[X'; ν] H[Y'; ν]]
  · linarith[le_max_left H[X'; ν] H[Y'; ν]]