\begin{lemma}[Rho minus of subgroup]\label{rhominus-subgroup}\lean{rhoMinus_of_subgroup}\uses{rhominus-def}\leanok If $H$ is a finite subgroup of $G$, then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$.
\end{lemma}
\begin{proof}\leanok
  \uses{log-sum}
  For every $G$-valued random variable $T$ that is independent of $Y$,
  $$D_{KL}(U_H \Vert U_A+T) = \sum_{h\in H} \frac{1}{|H|}\log\frac{1/|H|}{\mathbf{P}[U_A+T=h]}\ge -\log(\mathbf{P}[U_A+T\in H]),$$
  by \Cref{log-sum}. Then observe that $$-\log(\mathbf{P}[U_A+T\in H])=-\log(\mathbf{P}[U_A\in H-T])\ge -\log(\max_{t\in G} \mathbf{P}[U_A\in H+t]).$$ This proves $\ge$.

  To get the equality, let $t^*:=\arg\max_t |A \cap (H+t)|$ and observe that $$\rho^-(U_H)\le D_{KL}(U_H \Vert  U_A+(U_H-t^*))= \log |A| - \log \max_t|A \cap (H+t)|.$$
\end{proof}
lemma rhoMinus_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G}
    {U : Ω → G} (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) :
    ρ⁻[U ; μ # A] = log (Nat.card A) -
      log (sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} : ℕ) := by
  apply le_antisymm _ (le_rhoMinus_of_subgroup hunif hA hU)
  rcases exists_card_inter_add_eq_sSup (A := A) H hA with ⟨t, ht, hpos⟩
  rw [← ht]
  have : Nonempty (A ∩ (t +ᵥ (H : Set G)) : Set G) :=  (Nat.card_pos_iff.1 hpos).1
  exact rhoMinus_le_of_subgroup t hunif hA .of_subtype hU

/-- If $H$ is a finite subgroup of $G$, then
$\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$. -/