\begin{lemma}[Multidistance and Ruzsa distance, III]\label{multidist-ruzsa-III}\lean{multidist_ruzsa_III}\uses{multidist-def}\leanok
  Let $m \ge 2$, and let $X_{[m]}$ be a tuple of $G$-valued random variables. If the $X_i$ all have the same distribution, then $D[X_{[m]}] \leq m d[X_i;X_i]$ for any $1 \leq i \leq m$.
\end{lemma}
\begin{proof}\uses{klm-1, neg-ent, ruz-indep, sumset-lower, ruz-copy, multidist-copy}
  By \Cref{ruz-copy}, \Cref{multidist-copy} we may take the $X_i$ to be jointly independent.    Let $X_0$ be a further independent copy of the $X_i$.
From \Cref{klm-1}, we have
$$ \bbH[-X_0 + \sum_{i=1}^m X_i] - \bbH[-X_0] \leq \sum_{i=1}^m \bbH[X_0 - X_i] - \bbH[-X_0]$$
and hence by \Cref{neg-ent} and \Cref{ruz-indep}
$$ \bbH[-X_0 + \sum_{i=1}^m X_i] - \bbH[X_0] \leq m d[X_i,X_i].$$
On the other hand, by \Cref{sumset-lower} we have
$$ \bbH[\sum_{i=1}^m X_i] \leq \bbH[-X_0 + \sum_{i=1}^m X_i]$$
and the claim follows.
\end{proof}
lemma multidist_ruzsa_III {m:ℕ} (hm: m ≥ 2) {Ω: Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (X : ∀ i, (Ω i) → G) (hidenT : ∀ j k, IdentDistrib (X j) (X k)): ∀ i, D[X; hΩ] ≤ m * d[X i # X i] := by sorry

/-- Let `m ≥ 2`, and let `X_[m]` be a tuple of `G`-valued random
variables. Let `W := ∑ X_i`. Then `d[W;-W] ≤ 2 D[X_i]`. -/