\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 rhoPlus_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 ; μ] := by
  simp [rhoPlus]
  have := rhoMinus_of_sum hX hY hA h_indep
  linarith

/-- If $X,Y$ are independent, one has
  $$ \rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X] ).$$
  -/