\begin{lemma}[Rho invariant]\label{rho-invariant}\lean{rho_of_translate}\leanok\uses{rho-def}  For any $s \in G$, $\rho(X+s) = \rho(X)$.
\end{lemma}
\begin{proof}\leanok\uses{kl-div-inj} Observe that by \Cref{kl-div-inj}, $$\inf_T D_{KL}(X\Vert U_A+T)=\inf_T D_{KL}(X+s\Vert U_A+T+s)=\inf_{T'} D_{KL}(X+s\Vert U_A+T').$$
\end{proof}
lemma rho_of_translate [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hA : A.Nonempty) (s : G) :
    ρ[(fun ω ↦ X ω + s) ; μ # A] = ρ[X ; μ # A] := by
  apply le_antisymm (rho_le_translate hX hA s)
  convert rho_le_translate (X := fun ω ↦ X ω + s) (by fun_prop) hA (-s) (μ := μ) with ω
  abel

-- This may not be the optimal spelling for condRho, feel free to improve
/-- We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$. -/
noncomputable def condRho {S : Type*}
    (X : Ω → G) (Y : Ω → S) (A : Finset G) (μ : Measure Ω): ℝ :=
  ∑' s, (μ (Y ⁻¹' {s})).toReal * ρ[X ; μ[|Y ← s] # A]

/-- Average of rhoMinus along the fibers-/
noncomputable def condRhoMinus {S : Type*}
    (X : Ω → G) (Y : Ω → S) (A : Finset G) (μ : Measure Ω) : ℝ :=
  ∑' s, (μ (Y ⁻¹' {s})).toReal * ρ⁻[X ; μ[|Y ← s] # A]

/-- Average of rhoPlus along the fibers-/
noncomputable def condRhoPlus {S : Type*}
    (X : Ω → G) (Y : Ω → S) (A : Finset G) (μ : Measure Ω) : ℝ :=
  ∑' s, (μ (Y ⁻¹' {s})).toReal * ρ⁺[X ; μ[|Y ← s] # A]

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

@[inherit_doc condRho]
notation3:max "ρ[" X " | " Z " # " A "]" => condRho X Z A volume

@[inherit_doc condRhoMinus]
notation3:max "ρ⁻[" X " | " Z " ; " μ " # " A "]" => condRhoMinus X Z A μ

@[inherit_doc condRhoPlus]
notation3:max "ρ⁺[" X " | " Z " ; " μ " # " A "]" => condRhoPlus X Z A μ