\begin{lemma}[Entropy of $Z_2$]\label{ent-z2}\lean{entropy_of_Z_two_le}\uses{more-random}\leanok  We have $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$.
\end{lemma}
\begin{proof}\uses{sum-dilate-II, klm-1}
  We observe
  \[
    \bbH[Z_2] = \bbH[\sum_{j \in \Z/m\Z} j Q_j].
  \]
  Applying \Cref{klm-1} one has
  \begin{align*}
    \bbH[Z_2] &\leq \sum_{i=2}^{m-1} \bbH[Q_1 + i Q_i]  - (m-2) \bbH[S].
  \end{align*}
  Using \Cref{sum-dilate-II} and~\eqref{eq:s-bound} we get
  \begin{align*}
    \bbH[Z_2]
              &\leq \bbH[S] + 4m (m-2) d[S;-S] \\
              &\leq \bbH[S] + 8m (m-2) k.
  \end{align*}
  Applying~\eqref{eq:ent-s} gives the claim.
\end{proof}
/-- We have $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$. -/
lemma entropy_of_Z_two_le : H[Z2] ≤ (8 * p.m^2 - 16 * p.m + 1) * k + (m:ℝ)⁻¹ * ∑ i, H[X i] := sorry