\begin{lemma}[Gibbs inequality]\label{Gibbs}\uses{kl-div}\lean{KLDiv_nonneg}\leanok  $D_{KL}(X\Vert Y) \geq 0$.
\end{lemma}
\begin{proof}\leanok
  \uses{log-sum}
  Apply \Cref{log-sum} on the definition.
\end{proof}
/-- `KL(X ‖ Y) ≥ 0`.-/
lemma KLDiv_nonneg [Fintype G] [MeasurableSingletonClass G] [IsZeroOrProbabilityMeasure μ]
    [IsZeroOrProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) : 0 ≤ KL[X ; μ # Y ; μ'] := by
  rw [KLDiv_eq_sum]
  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
  · simp
  rcases eq_zero_or_isProbabilityMeasure μ' with rfl | hμ'
  · simp
  apply le_trans ?_ (sum_mul_log_div_leq (by simp) (by simp) ?_)
  · have : IsProbabilityMeasure (μ'.map Y) := isProbabilityMeasure_map hY.aemeasurable
    have : IsProbabilityMeasure (μ.map X) := isProbabilityMeasure_map hX.aemeasurable
    simp
  · intro i _ hi
    simp only [ENNReal.toReal_eq_zero_iff, measure_ne_top, or_false] at hi
    simp [habs i hi]