\begin{lemma}[Rho and sums]\label{rho-sums}\lean{rhoMinus_of_sum, rhoPlus_of_sum, rho_of_sum}\leanok  If $X,Y$ are independent, one has
  $$ \rho^-(X+Y) \leq \rho^-(X)$$
  $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$
and
  $$ \rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X] ).$$
\end{lemma}
\begin{proof}\leanok
  \uses{kl-sums}
The first inequality follows from \Cref{kl-sums}. The second and third inequalities are direct corollaries of the first.
\end{proof}
lemma rho_of_sum [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X + Y ; μ # A] ≤ ρ[X ; μ # A] + (H[X+Y ; μ] - H[X ; μ])/2 := by
  simp [rho, rhoPlus]
  have := rhoMinus_of_sum hX hY hA h_indep
  linarith

private lemma rho_le_translate [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hA : A.Nonempty) (s : G) :
    ρ[(fun ω ↦ X ω + s) ; μ # A] ≤ ρ[X ; μ # A] := by
  have : ρ[(fun ω ↦ X ω + s) ; μ # A] ≤ ρ[X ; μ # A] + (H[fun ω ↦ X ω + s ; μ] - H[X ; μ]) / 2 :=
    rho_of_sum (Y := fun ω ↦ s) hX measurable_const hA (indepFun_const s)
  have : H[fun ω ↦ X ω + s ; μ] = H[X ; μ] := entropy_add_const hX _
  linarith