\begin{lemma}\label{app-ent-pfr}\lean{app_ent_PFR}\leanok
Let $G=\mathbb{F}_2^n$ and $\alpha\in (0,1)$ and let $X,Y$ be $G$-valued
random variables such that
\[\mathbb{H}(X)+\mathbb{H}(Y)> \frac{20}{\alpha} d[X;Y].\]
There is a non-trivial subgroup $H\leq G$ such that
\[\log \lvert H\rvert <\frac{1+\alpha}{2}(\mathbb{H}(X)+\mathbb{H}(Y))\] and
\[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))< \alpha (\mathbb{H}(X)+\mathbb{H}(Y))\]
where $\psi:G\to G/H$ is the natural projection homomorphism.
\end{lemma}
\begin{proof}
\uses{entropy-pfr-improv, ruzsa-diff, dist-projection, ruzsa-nonneg}\leanok
By \Cref{entropy-pfr-improv} there exists a subgroup $H$ such that
$d[X;U_H] + d[Y;U_H] \leq 10 d[X;Y]$. Using \Cref{dist-projection} we
deduce that $\mathbb{H}(\psi(X)) + \mathbb{H}(\psi(X)) \leq 20 d[X;Y]$. The
second claim follows adding these inequalities and using the assumption on
$\mathbb{H}(X)+\mathbb{H}(Y)$.

Furthermore we have by \Cref{ruzsa-diff}
\[\log \lvert H \rvert-\mathbb{H}(X)\leq 2d[X;U_H]\]
and similarly for $Y$ and thus
\begin{align*}
\log \lvert  H\rvert
&\leq
\frac{\mathbb{H}(X)+\mathbb{H}(Y)}{2}+d[X;U_H] + d[Y;U_H] \leq
\frac{\mathbb{H}(X)+\mathbb{H}(Y)}{2}+ 10d[X;Y]
\\& <
\frac{1+\alpha}{2}(\mathbb{H}(X)+\mathbb{H}(Y)).
\end{align*}
Finally note that if $H$
were trivial then $\psi(X)=X$ and $\psi(Y)=Y$ and hence
$\mathbb{H}(X)+\mathbb{H}(Y)=0$, which contradicts \Cref{ruzsa-nonneg}.
\end{proof}
lemma app_ent_PFR (α : ℝ) (hent : 20 * d[X ;μ # Y;μ'] < α * (H[X ; μ] + H[Y; μ'])) (hX : Measurable X)
    (hY : Measurable Y) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) < (1 + α) / 2 * (H[X ; μ] + H[Y;μ']) ∧
    H[H.mkQ ∘ X ; μ] + H[H.mkQ ∘ Y; μ'] < α * (H[ X ; μ] + H[Y; μ']) :=
  app_ent_PFR' (mΩ := .mk μ) (mΩ' := .mk μ') X Y hent hX hY

set_option maxHeartbeats 300000 in
/-- If $G=\mathbb{F}_2^d$ and `X, Y` are `G`-valued random variables and $\alpha < 1$ then there is
a subgroup $H\leq \mathbb{F}_2^d$ such that
\[\log \lvert H\rvert \leq (1 + α) / (2 * (1 - α)) * (\mathbb{H}(X)+\mathbb{H}(Y))\]
and if $\psi:G \to G/H$ is the natural projection then
\[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 20/\alpha * d[\psi(X);\psi(Y)].\] -/