\begin{lemma}\label{pfr-projection'}\lean{PFR_projection'}\leanok
If $G=\mathbb{F}_2^d$ and $\alpha\in (0,1)$ and $X,Y$ are $G$-valued random
variables then there is a subgroup $H\leq \mathbb{F}_2^d$ such that
\[\log \lvert H\rvert \leq \frac{1+\alpha}{2(1-\alpha)} (\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 \frac{20}{\alpha} d[\psi(X);\psi(Y)].\]
\end{lemma}
\begin{proof}
\uses{app-ent-pfr}\leanok
Let $H\leq \mathbb{F}_2^d$ be a maximal subgroup such that
\[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))> \frac{20}{\alpha} d[\psi(X);\psi(Y)]\]
and such that there exists $c \ge 0$ with
\[\log \lvert H\rvert \leq \frac{1+\alpha}{2(1-\alpha)}(1-c)(\mathbb{H}(X)+\mathbb{H}(Y))\]
and
\[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq c (\mathbb{H}(X)+\mathbb{H}(Y)).\]
Note that this exists since $H=\{0\}$ is an example of such a subgroup or we are done with this choice of $H$.

We know that $G/H$ is a $2$-elementary group and so by Lemma
\ref{app-ent-pfr} there exists some non-trivial subgroup $H'\leq G/H$ such
that
\[\log \lvert H'\rvert < \frac{1+\alpha}{2}(\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\]
and
\[\mathbb{H}(\psi' \circ\psi(X))+\mathbb{H}(\psi' \circ \psi(Y))< \alpha(\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y)))\]
where $\psi':G/H\to (G/H)/H'$. By group isomorphism theorems we know that
there exists some $H''$ with $H\leq H''\leq G$ such that $H'\cong H''/H$ and
$\psi' \circ \psi(X)=\psi''(X)$ where $\psi'':G\to G/H''$ is the projection
homomorphism.

Since $H'$ is non-trivial we know that $H$ is a proper subgroup of $H''$. On the other hand we know that
\[\log \lvert H''\rvert=\log \lvert H'\rvert+\log \lvert H\rvert< \frac{1+\alpha}{2(1-\alpha)}(1-\alpha c)(\mathbb{H}(X)+\mathbb{H}(Y))\]
and
\[\mathbb{H}(\psi''(X))+\mathbb{H}(\psi''(Y))< \alpha (\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y)))\leq \alpha c (\mathbb{H}(X)+\mathbb{H}(Y)).\]
Therefore (using the maximality of $H$) it must be the first condition that fails, whence
\[\mathbb{H}(\psi''(X))+\mathbb{H}(\psi''(Y))\leq \frac{20}{\alpha}d[\psi''(X);\psi''(Y)].\]
\end{proof}
lemma PFR_projection'
    (α : ℝ) (hX : Measurable X) (hY : Measurable Y) (αpos : 0 < α) (αone : α < 1) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) ≤ (1 + α) / (2 * (1 - α)) * (H[X ; μ] + H[Y ; μ']) ∧
    α * (H[H.mkQ ∘ X ; μ] + H[H.mkQ ∘ Y ; μ']) ≤
      20 * d[H.mkQ ∘ X ; μ # H.mkQ ∘ Y ; μ'] := by
  let S := {H : Submodule (ZMod 2) G | (∃ (c : ℝ), 0 ≤ c ∧
      log (Nat.card H) ≤ (1 + α) / (2 * (1 - α)) * (1 - c) * (H[X ; μ] + H[Y;μ']) ∧
    H[H.mkQ ∘ X ; μ] + H[H.mkQ ∘ Y; μ'] ≤ c * (H[X ; μ] + H[Y;μ'])) ∧
    20 * d[H.mkQ ∘ X ; μ # H.mkQ ∘ Y ; μ'] < α * (H[H.mkQ ∘ X ; μ ] + H[H.mkQ ∘ Y; μ'])}
  have : 0 ≤ H[X ; μ] + H[Y ; μ'] := by linarith [entropy_nonneg X μ, entropy_nonneg Y μ']
  have : 0 < 1 - α := sub_pos.mpr αone
  by_cases hE : ⊥ ∈ S
  · classical
    obtain ⟨H, ⟨⟨c, hc, hlog, hup⟩, hent⟩, hMaxl⟩ :=
      S.toFinite.exists_maximal_wrt id S (Set.nonempty_of_mem hE)
    set G' := G ⧸ H
    set ψ : G →ₗ[ZMod 2] G' := H.mkQ
    have surj : Function.Surjective ψ := Submodule.Quotient.mk_surjective H

    obtain ⟨H', hlog', hup'⟩ := app_ent_PFR _ _ _ _ α hent (.comp .of_discrete hX)
      (.comp .of_discrete hY)
    have H_ne_bot : H' ≠ ⊥ := by
      by_contra!
      rcases this with rfl
      have inj : Function.Injective (Submodule.mkQ (⊥ : Submodule (ZMod 2) G')) :=
        QuotientAddGroup.quotientBot.symm.injective
      rw [entropy_comp_of_injective _ (.comp .of_discrete hX) _ inj,
          entropy_comp_of_injective _ (.comp .of_discrete hY) _ inj] at hup'
      nlinarith [entropy_nonneg (ψ ∘ X) μ, entropy_nonneg (ψ ∘ Y) μ']
    let H'' := H'.comap ψ
    use H''

    rw [← (Submodule.map_comap_eq_of_surjective surj _ : H''.map ψ = H')] at hup' hlog'
    set H' := H''.map ψ

    have Hlt :=
      calc
        H = (⊥ : Submodule (ZMod 2) G').comap ψ := by simp [ψ]; rw [Submodule.ker_mkQ]
        _ < H'' := by rw [Submodule.comap_lt_comap_iff_of_surjective surj]; exact H_ne_bot.bot_lt

    let φ : (G' ⧸ H') ≃ₗ[ZMod 2] (G ⧸ H'') := Submodule.quotientQuotientEquivQuotient H H'' Hlt.le
    set ψ' : G' →ₗ[ZMod 2] G' ⧸ H' := H'.mkQ
    set ψ'' : G →ₗ[ZMod 2] G ⧸ H'' := H''.mkQ
    have diag : ψ' ∘ ψ = φ.symm ∘ ψ'' := rfl
    rw [← Function.comp_assoc, ← Function.comp_assoc, diag, Function.comp_assoc,
        Function.comp_assoc] at hup'

    have cond : log (Nat.card H'') ≤
        (1 + α) / (2 * (1 - α)) * (1 - α * c) * (H[X ; μ] + H[Y;μ']) := by
      have cardprod : Nat.card H'' = Nat.card H' * Nat.card H := by
        have hcard₀ := Nat.card_congr <| (Submodule.comapSubtypeEquivOfLe Hlt.le).toEquiv
        have hcard₁ := Nat.card_congr <| (ψ.domRestrict H'').quotKerEquivRange.toEquiv
        have hcard₂ := (H.comap H''.subtype).card_eq_card_quotient_mul_card
        rw [ψ.ker_domRestrict H'', Submodule.ker_mkQ, ψ.range_domRestrict H''] at hcard₁
        simpa only [← Nat.card_eq_fintype_card, hcard₀, hcard₁, mul_comm] using hcard₂
      calc
          log (Nat.card H'')
      _ = log (Nat.card H' * Nat.card H) := by rw [cardprod]; norm_cast
      _ = log (Nat.card H') + log (Nat.card H) := by
        rw [Real.log_mul (Nat.cast_ne_zero.2 (@Nat.card_pos H').ne')
              (Nat.cast_ne_zero.2 (@Nat.card_pos H).ne')]
      _ ≤ (1 + α) / 2 * (H[ψ ∘ X ; μ] + H[ψ ∘ Y ; μ']) + log (Nat.card H) := by gcongr
      _ ≤ (1 + α) / 2 * (c * (H[X ; μ] + H[Y;μ'])) +
            (1 + α) / (2 * (1 - α)) * (1 - c) * (H[X ; μ] + H[Y ; μ']) := by gcongr
      _ = (1 + α) / (2 * (1 - α)) * (1 - α * c) * (H[X ; μ] + H[Y ; μ']) := by
        field_simp; ring

    have HS : H'' ∉ S := λ Hs => Hlt.ne (hMaxl H'' Hs Hlt.le)
    simp only [S, Set.mem_setOf_eq, not_and, not_lt] at HS
    refine ⟨?_, HS ⟨α * c, by positivity, cond, ?_⟩⟩
    · calc
      log (Nat.card H'')
      _ ≤ (1 + α) / (2 * (1 - α)) * (1 - α * c) * (H[X ; μ] + H[Y;μ']) := cond
      _ ≤ (1 + α) / (2 * (1 - α)) * 1 * (H[X ; μ] + H[Y;μ']) := by gcongr; simp; positivity
      _ = (1 + α) / (2 * (1 - α)) * (H[X ; μ] + H[Y;μ']) := by simp only [mul_one]
    · calc
      H[ ψ'' ∘ X ; μ ] + H[ ψ'' ∘ Y; μ' ]
      _ = H[ φ.symm ∘ ψ'' ∘ X ; μ ] + H[ φ.symm ∘ ψ'' ∘ Y; μ' ] := by
        simp_rw [← entropy_comp_of_injective _ (.comp .of_discrete hX) _ φ.symm.injective,
                 ← entropy_comp_of_injective _ (.comp .of_discrete hY) _ φ.symm.injective]
      _ ≤ α * (H[ ψ ∘ X ; μ ] + H[ ψ ∘ Y; μ' ]) := hup'.le
      _ ≤ α * (c * (H[X ; μ] + H[Y ; μ'])) := by gcongr
      _ = (α * c) * (H[X ; μ] + H[Y ; μ']) := by ring
  · use ⊥
    constructor
    · simp only [AddSubgroup.mem_bot, Nat.card_eq_fintype_card, Fintype.card_ofSubsingleton,
        Nat.cast_one, log_one]
      positivity
    · simp only [S, Set.mem_setOf_eq, not_and, not_lt] at hE
      exact hE ⟨1, by norm_num, by
        norm_num; exact add_le_add (entropy_comp_le μ hX _) (entropy_comp_le μ' hY _)⟩

/-- If $G=\mathbb{F}_2^d$ and `X, Y` are `G`-valued random variables then there is
a subgroup $H\leq \mathbb{F}_2^d$ such that
\[\log \lvert H\rvert \leq 2 * (\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 34 * d[\psi(X);\psi(Y)].\] -/