\begin{lemma}[Entropy of $W$]\label{ent-w}\lean{entropy_of_W_le}\uses{more-random}\leanok  We have $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$.
\end{lemma}
\begin{proof}\uses{multidist-def, multidist-ruzsa-IV, klm-1} Without loss of generality, we may take $X_1,\dots,X_m$ to be independent. Write $S = \sum_{i=1}^m X_i$.
  Note that for each $j \in \Z/m\Z$, the sum $Q_j$ from~\eqref{pqr-defs} above has the same distribution as $S$.
  By \Cref{klm-1} we have
  \begin{align*}
    \bbH[W] = \bbH[\sum_{j \in \Z/m\Z} Q_j]  & \leq \bbH[S] + \sum_{j=2}^m (\bbH[Q_1+Q_j] - \bbH[S]) \\ & = \bbH[S] + (m-1) d[S;-S].
  \end{align*}
  By \Cref{multidist-ruzsa-IV}, we have
  \begin{equation}
    \label{eq:s-bound}
    d[S; -S] \leq 2 k
  \end{equation}
  and hence
  \[
    \bbH[W] \leq 2 k (m-1) + \bbH[S].
  \]
  From \Cref{multidist-def} we have
  \begin{equation}
    \label{eq:ent-s}
    \bbH[S] = k + \frac1m \sum_{i=1}^m \bbH[X_i],
  \end{equation}
  and the claim follows.
\end{proof}
/-- We have $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$. -/
lemma entropy_of_W_le : H[W] ≤ (2*p.m - 1) * k + (m:ℝ)⁻¹ * ∑ i, H[X i] := sorry