\begin{corollary}[Rho plus of subgroup]\label{rhoplus-subgroup}\lean{rhoPlus_of_subgroup}\uses{rhoplus-def}\leanok If $H$ is a finite subgroup of $G$, then $\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$.
\end{corollary}
\begin{proof}\leanok \uses{rhominus-subgroup} Straightforward by definition and \Cref{rhominus-subgroup}.
\end{proof}
lemma rhoPlus_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 H) -
      log (sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} : ℕ) := by
  have : H[U ; μ] = log (Nat.card H) := hunif.entropy_eq' (toFinite _) hU
  rw [rhoPlus, rhoMinus_of_subgroup hunif hA hU, this]
  abel

/-- We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$. -/
noncomputable def rho (X : Ω → G) (A : Finset G) (μ : Measure Ω ) : ℝ :=
  (ρ⁻[X ; μ # A] + ρ⁺[X ; μ # A]) / 2

@[inherit_doc rho] notation3:max "ρ[" X " ; " μ " # " A "]" => rho X A μ

@[inherit_doc rho] notation3:max "ρ[" X " # " A "]" => rho X A volume