\begin{lemma}[Distance bound]\label{xi-z2-w-dist}\lean{sum_of_conditional_distance_le}\leanok We have $\sum_{i=1}^m d[X_i;Z_2|W] \leq 8(m^3-m^2) k$.
\end{lemma}
\begin{proof}\uses{klm-3, cond-dist-fact, mutual-w-z2, ent-z2, multidist-ruzsa-II}
  For each $i \in \{1,\dots, m\}$, using \Cref{klm-3} (noting the sum $Z_2$ contains $X_i$ as a summand) we have
  \begin{equation}\label{in-a-bit-6}
    d[X_i;Z_2] \leq d[X_i;X_i] + \tfrac12 (\bbH[Z_2] - \bbH[X_i])
  \end{equation}
  and using \Cref{cond-dist-fact} we have
  \[
    d[X_i;Z_2 | W] \leq d[X_i;Z_2] + \tfrac12 \bbI[W : Z_2].
  \]
 Combining with~\eqref{in-a-bit-6} and \Cref{mutual-w-z2} gives
 \[ d[X_i;Z_2 | W] \leq d[X_i;X_i] + \tfrac12 (\bbH[Z_2] - \bbH[X_i]) + (m-1)k.\]
 Summing over $i$ and applying \Cref{ent-z2} gives
 \[ \sum_{i = 1}^m d[X_i;Z_2 | W] \leq \sum_{i = 1}^m d[X_i;X_i] + m(8m^2-16m+1) k + m(m-1) k.\]
Finally, applying \Cref{multidist-ruzsa-II} (and dropping some lower order terms) gives the claim.
\end{proof}
/-- We have $\sum_{i=1}^m d[X_i;Z_2|W] \leq 8(m^3-m^2) k$. -/
lemma sum_of_conditional_distance_le : ∑ i, d[ X i # Z2 | W] ≤ 8 * (p.m^3 - p.m^2)*k := sorry


/-- Let $G$ be an abelian group, let $(T_1,T_2,T_3)$ be a $G^3$-valued random variable such that $T_1+T_2+T_3=0$ holds identically, and write
  \[
    \delta := \bbI[T_1 : T_2] + \bbI[T_1 : T_3] + \bbI[T_2 : T_3].
  \]
  Let $Y_1,\dots,Y_n$ be some further $G$-valued random variables and let $\alpha>0$ be a constant.
  Then there exists a random variable $U$ such that
$$  d[U;U] + \alpha \sum_{i=1}^n d[Y_i;U] \leq \Bigl(2 + \frac{\alpha n}{2} \Bigr) \delta + \alpha \sum_{i=1}^n d[Y_i;T_2].
$$
-/