\begin{lemma}[Multidistance and Ruzsa distance, IV]\label{multidist-ruzsa-IV}\lean{multidist_ruzsa_IV}\uses{multidist-def}\leanok
  Let $m \ge 2$, and let $X_{[m]}$ be a tuple of independent $G$-valued random variables.  Let $W := \sum_{i=1}^m X_i$. Then
  $$ d[W;-W] \leq 2 D[X_i].$$
\end{lemma}
\begin{proof}\uses{independent-exist, kv, sumset-lower, ruz-indep}
  Take $(X'_i)_{1 \leq i \leq m}$ to be further independent copies of $(X_i)_{1 \leq i \leq m}$ (which exist by \Cref{independent-exist}), and write $W' := \sum_{i=1}^m X'_i$.
  Fix any distinct $a,b \in I$.

  From \Cref{kv} one has
  \begin{equation}\label{7922}
    \bbH[W + W'] \leq  \bbH[W] + \bbH[X_{a} + W'] - \bbH[X_{a}]
   \end{equation}
   and also
   \[ \bbH[X_a + W'] \leq \bbH[X_a + X_b] + \bbH[W'] - \bbH[X'_b].\]
   Combining this with~\eqref{7922} and then applying \Cref{sumset-lower} we have
   \begin{align*}  \bbH[W + W']  & \leq    2\bbH[W] + \bbH[X_a + X_b]  - \bbH[X_a] - \bbH[X_b] \\ & \leq
    3 \bbH[W] - \bbH[X_a] - \bbH[X_b].
  \end{align*}
  Averaging this over all choices of $(a,b)$ gives $\bbH[W] + 2 D[X_{[m]}]$, and the claim follows from \Cref{ruz-indep}.
\end{proof}
lemma multidist_ruzsa_IV {m:ℕ} (hm: m ≥ 2) {Ω : Type*} (hΩ : MeasureSpace Ω) (X : Fin m → Ω → G)
    (h_indep : iIndepFun X) : d[∑ i, X i # ∑ i, X i] ≤ 2 * D[X; fun _ ↦ hΩ] := by sorry

/-- If `D[X_[m]]=0`, then for each `i ∈ I` there is a finite subgroup `H_i ≤ G` such that
`d[X_i; U_{H_i}] = 0`. -/