\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) + \bbH[X] - \bbH[X|Z]$$ -/
lemma condRhoMinus_le [IsZeroOrProbabilityMeasure μ] {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 ; μ] := by
  have : IsProbabilityMeasure (uniformOn (A : Set G)) := by
    apply uniformOn_isProbabilityMeasure A.finite_toSet hA
  suffices ρ⁻[X | Z ; μ # A] - H[X ; μ] + H[X | Z ; μ] ≤ ρ⁻[X ; μ # A] by linarith
  apply le_csInf (nonempty_rhoMinusSet hA)
  rintro - ⟨μ', hμ', habs, rfl⟩
  rw [condRhoMinus, tsum_fintype]
  let _ : MeasureSpace (G × G) := ⟨μ'.prod (uniformOn (A : Set G))⟩
  have hP : (ℙ : Measure (G × G)) = μ'.prod (uniformOn (A : Set G)) := rfl
  have : IsProbabilityMeasure (ℙ : Measure (G × G)) := by rw [hP]; infer_instance
  have : ∑ b : S, (μ (Z ⁻¹' {b})).toReal * ρ⁻[X ; μ[|Z ← b] # A]
      ≤ KL[ X | Z ; μ # (Prod.fst + Prod.snd : G × G → G) ; ℙ] := by
    rw [condKLDiv, tsum_fintype]
    apply Finset.sum_le_sum (fun i hi ↦ ?_)
    gcongr
    apply rhoMinus_le_def hX (fun y hy ↦ ?_)
    have T := habs y hy
    rw [Measure.map_apply hX (measurableSet_singleton _)] at T ⊢
    exact cond_absolutelyContinuous T
  rw [condKLDiv_eq hX hZ (by exact habs)] at this
  rw [← hP]
  linarith