\begin{lemma}[Rho and conditioning]\label{rho-cond}\lean{condRhoMinus_le, condRhoPlus_le, condRho_le}\leanok  If $X,Z$ are defined on the same space, one has
  $$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$
  $$ \rho^+(X|Z) \leq \rho^+(X)$$
and
  $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z] ).$$
\end{lemma}
\begin{proof}\leanok
  \uses{kl-cond}
  The first inequality follows from \Cref{kl-cond}. The second and third inequalities are direct corollaries of the first.
\end{proof}
/-- $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z] )$$ -/
lemma condRho_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Fintype S] [MeasurableSingletonClass S]
    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :
    ρ[X | Z ; μ # A] ≤ ρ[X ; μ # A] + (H[X ; μ] - H[X | Z ; μ]) / 2 := by
  rw [condRho_eq, rho]
  linarith [condRhoMinus_le hX hZ hA (μ := μ), condRhoPlus_le hX hZ hA (μ := μ)]

omit [Fintype G] [DiscreteMeasurableSpace G] in