\begin{lemma}[Rho of subgroup]\label{rho-subgroup}\uses{rho-def}\lean{rho_of_subgroup}\leanok
If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists
$t$ such that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$, and
$|H|/|A|\in[e^{-2r},e^{2r}]$.
\end{lemma}
\begin{proof}\leanok\uses{rhominus-subgroup, rhoplus-subgroup} The first claim is a direct corollary of \Cref{rhominus-subgroup} and \Cref{rhoplus-subgroup}. To see the second claim, observe that \Cref{rhominus-nonneg} and \Cref{rhoplus-subgroup} imply $\rho^-(U_H),\rho^+(U_H)\ge 0$. Therefore $$|H(U_A)-H(U_H)|=|\rho^+(U_H)-\rho^-(U_H)|\le \rho^-(U_H)+\rho^+(U_H)= 2\rho(U_H)\le 2r,$$
  which implies the second claim.
\end{proof}
lemma rho_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G}
    (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U)
    (r : ℝ) (hr : ρ[U ; μ # A] ≤ r) :
    ∃ t : G,
      exp (-r) * Nat.card A ^ (1/2 : ℝ) * Nat.card H ^ (1/2 : ℝ) ≤
        Nat.card ↑(↑A ∩ (t +ᵥ (H : Set G)))
      ∧ Nat.card A ≤ exp (2 * r) * Nat.card H
      ∧ Nat.card H ≤ exp (2 * r) * Nat.card A := by
  have hr' : ρ[U ; μ # A] ≤ r := hr
  have Hpos : 0 < (Nat.card H : ℝ) := by exact_mod_cast Nat.card_pos
  have : Nonempty A := hA.to_subtype
  have Apos : 0 < (Nat.card A : ℝ) := by exact_mod_cast Nat.card_pos
  simp only [rho] at hr
  rw [rhoMinus_of_subgroup hunif hA hU, rhoPlus_of_subgroup hunif hA hU] at hr
  rcases exists_card_inter_add_eq_sSup (A := A) H hA with ⟨t, ht, hpos⟩
  rw [← ht] at hr
  have Rm : 0 ≤ ρ⁻[U ; μ # A] := rhoMinus_nonneg hU
  have RM : 0 ≤ ρ⁺[U ; μ # A] := by
    rw [rhoPlus_of_subgroup hunif hA hU, ← ht, sub_nonneg]
    apply log_le_log (mod_cast hpos)
    norm_cast
    have : Nat.card (t +ᵥ (H : Set G) : Set G) = Nat.card H := by
      apply Nat.card_image_of_injective (add_right_injective t)
    rw [← this]
    exact Nat.card_mono (toFinite _) inter_subset_right
  have I : |log (Nat.card H) - log (Nat.card A)| ≤ 2 * r := calc
    |log (Nat.card H) - log (Nat.card A)|
    _ = |H[U ; μ] - log (Nat.card A)| := by rw [hunif.entropy_eq' (toFinite _) hU]; rfl
    _ = |ρ⁺[U ; μ # A] - ρ⁻[U ; μ # A]| := by congr 1; simp [rhoPlus]; abel
    _ ≤ ρ⁺[U ; μ # A] + ρ⁻[U ; μ # A] :=
      (abs_sub _ _).trans_eq (by simp [abs_of_nonneg, Rm, RM])
    _ = 2 * ρ[U ; μ # A] := by simp [rho]; ring
    _ ≤ 2 * r := by linarith
  refine ⟨t, ?_, ?_, ?_⟩
  · have : - r + (log (Nat.card A) + log (Nat.card H)) * (1 / 2 : ℝ) ≤
      log (Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G)) := by linarith
    have := exp_monotone this
    rwa [exp_add, exp_log (mod_cast hpos), exp_mul, exp_add,
      exp_log Hpos, exp_log Apos, mul_rpow, ← mul_assoc] at this <;> positivity
  · have : log (Nat.card A) ≤ 2 * r + log (Nat.card H) := by
      linarith [(abs_sub_le_iff.1 I).2]
    have := exp_monotone this
    rwa [exp_log Apos, exp_add, exp_log Hpos] at this
  · have : log (Nat.card H) ≤ 2 * r + log (Nat.card A) := by
      linarith [(abs_sub_le_iff.1 I).1]
    have := exp_monotone this
    rwa [exp_log Hpos, exp_add, exp_log Apos] at this

/-- If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists $t$ such
that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$. -/