\begin{lemma}[Balog-Szemer\'edi-Gowers]\label{entropic-bsg}
  \lean{ent_bsg}\leanok
  Let $A,B$ be $G$-valued random variables on $\Omega$, and set $Z := A+B$.
Then
\begin{equation}\label{2-bsg-takeaway} \sum_{z}  \bbP[Z=z] d[(A | Z = z); (B | Z = z)] \leq 3  \bbI[A:B] + 2 \bbH[Z] - \bbH[A] - \bbH[B]. \end{equation}
\end{lemma}
\begin{proof}
  \uses{cond-indep-exist, cond-trial-ent, conditional-entropy-def,submodularity, copy-ent, relabeled-entropy, add-entropy, ruz-indep}
  \leanok
Let $(A_1, B_1)$ and $(A_2, B_2)$ (and $Z'$, which by abuse of notation we call $Z$) be conditionally independent trials of $(A,B)$ relative to $Z$ as produced by \Cref{cond-indep-exist}, thus $(A_1,B_1)$ and $(A_2,B_2)$ are coupled through the random variable $A_1 + B_1 = A_2 + B_2$, which by abuse of notation we shall also call $Z$.

Observe from \Cref{ruz-indep} that the left-hand side of~\eqref{2-bsg-takeaway} is
\begin{equation}\label{lhs-to-bound}
\bbH[A_1 - B_2| Z] - \bbH[A_1 | Z]/2 - \bbH[B_2 | Z]/2.
\end{equation}
since, crucially, $(A_1 | Z=z)$ and $(B_2 | Z=z)$ are independent for all $z$.

Applying submodularity (\Cref{alt-submodularity}) gives
\begin{equation}\label{bsg-31} \begin{split}
&\bbH[A_1 - B_2] + \bbH[A_1 - B_2, A_1, B_1] \\
&\qquad \leq \bbH[A_1 - B_2, A_1] + \bbH[A_1 - B_2,B_1].
\end{split}\end{equation}
We estimate the second, third and fourth terms appearing here.
First note that, by \Cref{cond-trial-ent} and \Cref{relabeled-entropy} (noting that the tuple $(A_1 - B_2, A_1, B_1)$  determines the tuple $(A_1, A_2, B_1, B_2)$ since $A_1+B_1=A_2+B_2$)
\begin{equation}\label{bsg-24} \bbH[A_1 - B_2, A_1, B_1] = \bbH[A_1, B_1, A_2, B_2,Z] = 2\bbH[A,B] - \bbH[Z].\end{equation}
Next observe that
\begin{equation}\label{bsg-23} \bbH[A_1 - B_2, A_1] = \bbH[A_1, B_2] \leq \bbH[A] + \bbH[B].
\end{equation}
Finally, we have
\begin{equation}\label{bsg-25} \bbH[A_1 - B_2, B_1] = \bbH[A_2 - B_1, B_1] = \bbH[A_2, B_1] \leq \bbH[A] + \bbH[B].\end{equation}
Substituting~\eqref{bsg-24},~\eqref{bsg-23} and~\eqref{bsg-25} into~\eqref{bsg-31} yields
\[\bbH[A_1 - B_2] \leq 2 \bbI[A:B] + \bbH[Z]\] and so by \Cref{cond-reduce}
\[\bbH[A_1 - B_2 | Z]  \leq 2 \bbI[A:B] + \bbH[Z].\]
Since
\begin{align*} \bbH[A_1 | Z] & = \bbH[A_1, A_1 + B_1] - \bbH[Z] \\ & = \bbH[A,B] - \bbH[Z] \\ & = \bbH[Z] -  \bbI[A:B] - 2 \bbH[Z]- \bbH[A]-\bbH[B]\end{align*}
and similarly for $\bbH[B_2 | Z]$, we see that~\eqref{lhs-to-bound} is bounded by
$3 \bbI[A:B] + 2\bbH[Z]-\bbH[A]-\bbH[B]$ as claimed.
\end{proof}
lemma ent_bsg [IsProbabilityMeasure μ] {A B : Ω → G} (hA : Measurable A) (hB : Measurable B)
    [Fintype G] :
    (μ.map (A + B))[fun z ↦ d[A ; μ[|(A + B) ⁻¹' {z}] # B ; μ[|(A + B) ⁻¹' {z}]]]
      ≤ 3 * I[A : B; μ] + 2 * H[A + B ; μ] - H[A ; μ] - H[B ; μ] := by
  let Z := A + B
  have hZ : Measurable Z := hA.add hB
  obtain ⟨Ω', _, AB₁, AB₂, Z', ν, _, hAB₁, hAB₂, hZ', hABZ, hABZ₁, hABZ₂, hZ₁, hZ₂⟩ :=
    condIndep_copies' (⟨A, B⟩) Z (hA.prodMk hB) hZ μ (fun (a, b) c ↦ c = a + b)
    .of_discrete (Eventually.of_forall fun _ ↦ rfl)
  let A₁ := fun ω ↦ (AB₁ ω).1
  let B₁ := fun ω ↦ (AB₁ ω).2
  let A₂ := fun ω ↦ (AB₂ ω).1
  let B₂ := fun ω ↦ (AB₂ ω).2
  replace hZ₁ : Z' = A₁ + B₁ := funext hZ₁
  replace hZ₂ : Z' = A₂ + B₂ := funext hZ₂
  have hA₁ : Measurable A₁ := hAB₁.fst
  have hB₁ : Measurable B₁ := hAB₁.snd
  have hA₂ : Measurable A₂ := hAB₂.fst
  have hB₂ : Measurable B₂ := hAB₂.snd
  have hZZ' : IdentDistrib Z' Z ν μ := hABZ₁.comp measurable_snd
  have :=
    calc
      H[⟨A₁, ⟨B₁, A₁ - B₂⟩⟩ ; ν]
        = H[⟨⟨A₁, B₁⟩, ⟨⟨A₂, B₂⟩, Z'⟩⟩ ; ν] := entropy_of_comp_eq_of_comp _
          (hA₁.prodMk $ hB₁.prodMk $ hA₁.sub hB₂) (hAB₁.prodMk $ hAB₂.prodMk hZ')
            (fun (a, b, c) ↦ ((a, b), (b + c, a - c), a + b))
            (fun ((a, b), (_c, d), _e) ↦ (a, b, a - d))
          (by funext; simpa [sub_add_eq_add_sub, Prod.ext_iff, ← hZ₁, hZ₂, two_nsmul, ← add_sub_assoc,
            add_comm, eq_sub_iff_add_eq] using congr_fun (hZ₂.symm.trans hZ₁) _) rfl
      _ = H[⟨⟨A₁, B₁⟩, Z'⟩ ; ν] + H[⟨⟨A₂, B₂⟩, Z'⟩ ; ν] - H[Z' ; ν] :=
        ent_of_cond_indep _ hAB₁ hAB₂ hZ' hABZ
      _ = 2 * H[⟨⟨A, B⟩, Z⟩ ; μ] - H[Z ; μ] := by
        rw [two_mul]
        congr 1
        congr 1 <;> exact IdentDistrib.entropy_eq ‹_›
        exact hZZ'.entropy_eq
      _ = 2 * H[⟨A, B⟩ ; μ] - H[Z ; μ] := by
        congr 2
        exact entropy_prod_comp (hA.prodMk hB) _ fun x ↦ x.1 + x.2
  have :=
    calc
      H[⟨A₁, A₁ - B₂⟩ ; ν]
        = H[⟨A₁, B₂⟩ ; ν] := entropy_sub_right hA₁ hB₂ _
      _ ≤ H[A₁ ; ν] + H[B₂ ; ν] := entropy_pair_le_add hA₁ hB₂ _
      _ = H[A ; μ] + H[B ; μ] := by
        congr 1
        exact (hABZ₁.comp measurable_fst.fst).entropy_eq
        exact (hABZ₂.comp measurable_fst.snd).entropy_eq
  have :=
    calc
      H[⟨B₁, A₁ - B₂⟩ ; ν]
        = H[⟨A₂, B₁⟩ ; ν] := by
          rw [entropy_comm hB₁ (show Measurable (A₁ - B₂) from hA₁.sub hB₂),
            ← entropy_sub_left' hA₂ hB₁, sub_eq_sub_iff_add_eq_add.2 $ hZ₁.symm.trans hZ₂]
      _ ≤ H[A₂ ; ν] + H[B₁ ; ν] := entropy_pair_le_add hA₂ hB₁ _
      _ = H[A ; μ] + H[B ; μ] := by
        congr 1
        exact (hABZ₂.comp measurable_fst.fst).entropy_eq
        exact (hABZ₁.comp measurable_fst.snd).entropy_eq
  have :=
    calc
     _ ≤ _ := entropy_triple_add_entropy_le ν hA₁ hB₁ (show Measurable (A₁ - B₂) from hA₁.sub hB₂)
     _ ≤ _ := add_le_add ‹_› ‹_›
  have :=
    calc
      H[A₁ - B₂ | Z' ; ν]
        ≤ H[A₁ - B₂ ; ν] := condEntropy_le_entropy _ (hA₁.sub hB₂) hZ'
      _ ≤ _ := le_sub_iff_add_le'.2 ‹_›
      _ = 2 * I[A : B ; μ] + H[Z ; μ] := by
        rw [‹H[⟨A₁, ⟨B₁, A₁ - B₂⟩⟩ ; ν] = _›, mutualInfo_def]; ring
  have hA₁Z :=
    calc
      H[A₁ | Z' ; ν]
      _ = H[⟨A₁, B₁⟩ ; ν] - H[Z' ; ν] := by
        rw [chain_rule'', hZ₁, entropy_add_right, entropy_comm] <;> assumption
      _ = H[⟨A, B⟩ ; μ] - H[Z ; μ] := by
        congr 1
        exact (hABZ₁.comp measurable_fst).entropy_eq
        exact hZZ'.entropy_eq
      _ = H[A ; μ] + H[B ; μ] - I[A : B ; μ] - H[Z ; μ] := by
        rw [← entropy_add_entropy_sub_mutualInfo]
  have hB₂Z :=
    calc
      H[B₂ | Z' ; ν]
      _ = H[⟨A₂, B₂⟩ ; ν] - H[Z' ; ν] := by
        rw [chain_rule'', hZ₂, entropy_add_right', entropy_comm] <;> assumption
      _ = H[⟨A, B⟩ ; μ] - H[Z ; μ] := by
        congr 1
        exact (hABZ₂.comp measurable_fst).entropy_eq
        exact hZZ'.entropy_eq
      _ = H[A ; μ] + H[B ; μ] - I[A : B ; μ] - H[Z ; μ] := by
        rw [← entropy_add_entropy_sub_mutualInfo]
  calc
    (μ.map Z)[fun z ↦ d[A ; μ[|Z ← z] # B ; μ[|Z ← z]]]
      = (ν.map Z')[fun z ↦ d[A₁ ; ν[|Z' ← z] # B₂ ; ν[|Z' ← z]]] := by
        rw [hZZ'.map_eq]
        refine integral_congr_ae $ Eventually.of_forall fun z ↦ ?_
        have hAA₁ : IdentDistrib A₁ A (ν[|Z' ← z]) (μ[|Z ← z]) :=
          (hABZ₁.comp $ measurable_fst.fst.prodMk measurable_snd).cond
            (.singleton z) hZ' hZ
        have hBB₂ : IdentDistrib B₂ B (ν[|Z' ← z]) (μ[|Z ← z]) :=
          (hABZ₂.comp $ measurable_fst.snd.prodMk measurable_snd).cond
            .of_discrete hZ' hZ
        dsimp (config := {zeta := false}) [rdist]
        rw [← hAA₁.entropy_eq, ← hBB₂.entropy_eq, hAA₁.map_eq, hBB₂.map_eq]
    _ = (ν.map Z')[fun z ↦
          H[A₁ - B₂ ; ν[|Z' ← z]] - H[A₁ ; ν[|Z' ← z]]/2 - H[B₂ ; ν[|Z' ← z]]/2] := by
        apply integral_congr_ae
        apply hABZ.mono
        intro z hz
        exact (hz.comp measurable_fst measurable_snd).rdist_eq hA₁ hB₂
    _ = H[A₁ - B₂ | Z' ; ν] - H[A₁ | Z' ; ν] / 2 - H[B₂ | Z' ; ν] / 2 := by
        rw [integral_sub, integral_sub, integral_div, integral_div]
        rfl
        all_goals exact .of_finite
    _ ≤ 2 * I[A : B ; μ] + H[Z ; μ] - H[A₁ | Z' ; ν] / 2 - H[B₂ | Z' ; ν] / 2 :=
        sub_le_sub_right (sub_le_sub_right ‹_› _) _
    _ = _ := by rw [hA₁Z, hB₂Z]; ring

end BalogSzemerediGowers

variable (μ μ') in
/-- Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian
group. Then $$d[X | Z ; Y | W] \leq d[X ; Y] + \tfrac{1}{2} I[X : Z] + \tfrac{1}{2} I[Y : W]$$ -/