\begin{proposition}[Mutual information bound]\label{prop:52}\lean{mutual_information_le_t_12, mutual_information_le_t_13, mutual_information_le_t_23}\uses{more-random}\leanok
  We have
  \[
    \bbI[Z_1 : Z_2\, |\, W],\
    \bbI[Z_2 : Z_3\, |\, W],\
    \bbI[Z_1 : Z_3\, |\, W] \leq t
  \]
  where
  \begin{equation}\label{t-def}
    t :=  4m^2 \eta k.
  \end{equation}
\end{proposition}
\begin{proof}\uses{key, data-process}
  We analyze these variables by \Cref{key} in several different ways.
  In the first application, take $X_{i,j}=Y_{i,j}$.
  Note that each column $(X_{i,j})_{i=1}^m$ is indeed a permutation of $X_1,\dots,X_m$; in fact, the trivial permutation.
  Note also that for each $i \in \Z/m\Z$, the row sum is
  \[
    \sum_{j=1}^m X_{i,j} = \sum_{j \in \Z/m\Z} Y_{i,j} = P_i
  \]
  and for each $j \in \Z/m\Z$, the column sum is
  \[
    \sum_{i=1}^m X_{i,j} = \sum_{i \in \Z/m\Z} Y_{i,j} = Q_j.
  \]
  Finally note that $\sum_{i,j=1}^m X_{i,j} = W$.
  From \Cref{key} we then have
  \[
    \bbI[ (P_i)_{i \in \Z/m\Z} : (Q_j)_{j \in \Z/m\Z } \,\big|\, W ] \leq t,
  \]
  with $t$ as in~\eqref{t-def}.
  Since $Z_1$ is a function of $(P_i)_{i \in \Z/m\Z}$ by~\eqref{pqr-defs}, and similarly $Z_2$ is a function of $(Q_j)_{j \in \Z/m\Z}$, it follows immediately from \Cref{data-process} that
  \[
    \bbI[ Z_1 : Z_2 \,|\, W ] \leq t.
  \]

  In the second application of \Cref{key}, we instead consider $X'_{i,j} = Y_{i-j,j}$.
  Again, for each fixed $j$, the tuple $(X'_{i,j})_{i=1}^m$ is a permutation of $X_1,\dots,X_m$.
  This time the row sums for $i \in \{1,\dots, m\}$ are
  \[
    \sum_{j=1}^m X'_{i,j} = \sum_{j \in \Z/m\Z} Y_{i-j,j} = R_{-i}.
  \]
 Similarly, the column sums for $j \in \{1,\dots, m\}$ are
  \[
    \sum_{i=1}^m X'_{i,j} = \sum_{i \in \Z/m\Z} Y_{i-j,j} = Q_j.
  \]
  As before, $\sum_{i,j=1}^m X'_{i,j} = W$.
  Hence, using~\eqref{pqr-defs} and \Cref{data-process} again, \Cref{key} tells us
  \[
    \bbI[ Z_3 :  Z_2 \,|\, W] \leq \bbI[ (R_i)_{i \in \Z/m\Z} : (Q_j)_{j \in \Z/m\Z } \,\big|\, W ] \leq t.
  \]

  In the third application\footnote{In fact, by permuting the variables $(Y_{i,j})_{i,j \in \Z/m\Z}$, one can see that the random variables $(W, Z_1, Z_2)$ and $(W, Z_1, Z_3)$ have the same distribution, so this is in some sense identical to -- and can be deduced from -- the first application.} of \Cref{key}, take $X''_{i,j} = Y_{i,j-i}$.
  The column and row sums are respectively
  \[
    \sum_{j=1}^m X''_{i,j} = \sum_{j \in \Z/m\Z} Y_{i,j-i} = P_i \] and
\[     \sum_{i=1}^m X''_{i,j} = \sum_{i \in \Z/m\Z} Y_{i,j-i} = R_{-j}.
  \]
  Hence, \Cref{key} and \Cref{data-process} give
  \[
    \bbI[ Z_1 : Z_3 \,|\, W] \leq \bbI[ (P_i)_{i \in \Z/m\Z} : (R_j)_{j \in \Z/m\Z } \,\big|\, W ] \leq t,
  \]
  which completes the proof.
\end{proof}
lemma mutual_information_le_t_23 : I[Z2 : Z3 | W] ≤ 4 * p.m ^ 2 * p.η * k := sorry