\begin{lemma}[Conditional Gibbs inequality]\label{Conditional-Gibbs}\lean{condKLDiv_nonneg}\leanok  $D_{KL}((X|W)\Vert Y) \geq 0$.
\end{lemma}
\begin{proof}\leanok \uses{Gibbs, ckl-div}  Clear from Definition \ref{ckl-div} and Lemma \ref{Gibbs}.
\end{proof}
/-- `KL(X|Z ‖ Y) ≥ 0`.-/
lemma condKLDiv_nonneg {S : Type*} [MeasurableSingletonClass G] [Fintype G]
    {X : Ω → G} {Y : Ω' → G} {Z : Ω → S}
    [IsZeroOrProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) :
    0 ≤ KL[X | Z; μ # Y ; μ'] := by
  rw [condKLDiv]
  refine tsum_nonneg (fun i ↦ mul_nonneg (by simp) ?_)
  apply KLDiv_nonneg hX hY
  intro s hs
  specialize habs s hs
  rw [Measure.map_apply hX (measurableSet_singleton s)] at habs ⊢
  exact cond_absolutelyContinuous habs