\begin{proposition}[Bounding mutual information]\label{key}\lean{mutual_information_le}\leanok
Suppose that $X_{i,j}$, $1 \leq i,j \leq m$, are jointly independent $G$-valued random variables, such that for each $j = 1,\dots,m$, the random variables $(X_{i,j})_{i = 1}^m$ coincide in distribution with some permutation of $X_{[m]}$.
  Write
  \[
    {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m  X_{i,j} ].
  \]
Then
  \begin{equation}\label{I-ineq}
    {\mathcal I} \leq 4 m^2 \eta k.
  \end{equation}
\end{proposition}
\begin{proof}\uses{cor-multid, multidist-perm, cond-multidist-lower-II, first-useful, klm-3, sumset-lower, ruzsa-triangle, compare-sums, multidist-ruzsa-II}
  For each $j \in \{1,\dots,m\}$ we call the tuple $(X_{i,j})_{i = 1}^m$ a \emph{column} and for each $i \in \{1,\dots, m\}$ we call the tuple $(X_{i,j})_{j = 1}^m$ a \emph{row}. Hence, by hypothesis, each column is a permutation of $X_{[m]} = (X_i)_{i=1}^m$.

From \Cref{cor-multid} we have
\begin{equation}\label{441} {\mathcal I} \leq \sum_{j=1}^{m-1} A_j + B,\end{equation}
where
\[
  A_j := D[ (X_{i, j})_{i = 1}^m] - D[ (X_{i, j})_{i = 1}^m  \; \big| \; (X_{i,j} + \cdots + X_{i,m})_{i =1}^m  ]
\]
and
\[
  B := D[ (X_{i,m})_{i=1}^m ] - D[ \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i=1}^m ].
\]
We first consider the $A_j$, for fixed $j \in \{1,\dots, m-1\}$.
By \Cref{multidist-perm} and and our hypothesis on columns, we have
\[
  D[ (X_{i, j})_{i = 1}^m ]= D[ (X_i)_{i=1}^m ] = k.
\]
Let $\sigma = \sigma_j \colon I \to I$ be a permutation such that $X_{i,j} = X_{\sigma(i)}$, and write $X'_i := X_{i,j}$ and $Y_i := X_{i,j} + \cdots + X_{i,m}$.
\Cref{cond-multidist-lower-II}, we have
\begin{align}
  A_j & \leq \eta \sum_{i = 1}^m d[X_{i,j}; X_{i, j}|X_{i, j} + \cdots + X_{i,m}].\label{54a}
\end{align}
We similarly consider $B$.  By \Cref{multidist-perm} applied to the $m$-th column,
\[
  D[ (X_{i, m})_{i = 1}^m ] = D[X_{[m]}] = k.
\]
For $1 \leq i \leq m$, denote the sum of row $i$ by
\[
  V_i := \sum_{j=1}^m X_{i,j};
\]
if we apply \Cref{cond-multidist-lower-II} again, now with $X_{\sigma(i)} = X_{i,m}$, $X'_i := V_i$, and with the variable $Y_i$ being trivial, we obtain
\begin{equation}\label{55a}
  B \leq \eta \sum_{i = 1}^m d[X_{i,m}; V_i].
\end{equation}

It remains to bound the distances appearing in~\eqref{54a} and~\eqref{55a} further using Ruzsa calculus.
For $1 \leq j \leq m-1$ and $1 \leq i \leq m$, by \Cref{first-useful} we have
\begin{align*} &d[ X_{i,j}; X_{i,j}| X_{i,j}+\cdots+X_{i,m}]
\leq d[X_{i,j}; X_{i,j}] \\
&\quad + \tfrac{1}{2} \bigl(\bbH[X_{i,j}+\cdots+X_{i,m}] - \bbH[X_{i,{j+1}}+\cdots+X_{i,m}]\bigr).
\end{align*}
For each $i$, summing over $j = 1,\dots, m-1$ gives
\begin{align}
  \nonumber
  &\sum_{j=1}^{m-1} d[X_{i,j}; X_{i,j}| X_{i,j}+\cdots+X_{i,m}] \\
  &\qquad \leq \sum_{j=1}^{m-1} d[X_{i,j}; X_{i,j}] + \frac12 \bigl( \bbH[V_i] - \bbH[X_{i,m}] \bigr).
  \label{eq:distbnd1}
\end{align}
On the other hand, by \Cref{klm-3} (since $X_{i,m}$ appears in the sum $V_i$) we have
\begin{align}
  d[X_{i,m}; V_i]
  &\leq d[X_{i,m}; X_{i,m}] + \frac12 \bigl( \bbH[V_i] - \bbH[X_{i,m}] \bigr).
  \label{eq:distbnd2}
\end{align}
Combining~\eqref{441},~\eqref{54a} and~\eqref{55a} with~\eqref{eq:distbnd1} and~\eqref{eq:distbnd2} (the latter two summed over $i$), we get
\begin{align}
  \nonumber
  \frac1{\eta} {\mathcal I} &\leq \sum_{i,j=1}^m d[X_{i,j};X_{i,j}] + \sum_{i=1}^m (\bbH[V_i] - \bbH[X_{i,m}]) \\
      &= m \sum_{i=1}^m d[X_i; X_i] + \sum_{i=1}^m \bbH[V_i] - \sum_{i=1}^m \bbH[X_i].
      \label{eq:distbnd3}
\end{align}
By \Cref{compare-sums} (with $f$ taking each $j$ to the index $j'$ such that $X_{i,j}$ is a copy of $X_{j'}$) we obtain the bound
\[
  \bbH[V_i] \leq \bbH[\sum_{j=1}^m X_j] + \sum_{j=1}^m d[X_{i,j}; X_{i,j}].
\]
Finally, summing over $i$ and using $D[X_{[m]}] = k$ gives
\begin{align*}
  \sum_{i=1}^m \bbH[V_i] - \sum_{i=1}^m \bbH[X_i] & \leq \sum_{i,j=1}^m d[X_{i,j}; X_{i,j}] + m k \\ & = m\sum_{i = 1}^m d[X_i; X_i] + mk,
\end{align*}
where in the second step we used the permutation hypothesis. Combining this with~\eqref{eq:distbnd3} gives the
$$
{\mathcal I} \leq 2\eta m \biggl( \sum_{i=1}^m d[X_i;X_i] \biggr).$$
The claim \eqref{I-ineq} is now immediate from \Cref{multidist-ruzsa-II}.
\end{proof}
lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ]
  (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → G)
  (h_indep : iIndepFun X)
  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω']
  (X' : Fin p.m × Fin p.m → Ω' → G) (h_indep': iIndepFun X')
  (hperm : ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω))
    (fun ω ↦ (fun i ↦ X (e i) ω))) :
  I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) |
    fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ 4 * p.m^2 * p.η * D[ X; (fun _ ↦ hΩ)] := sorry