\begin{lemma}[Converse Gibbs inequality]\label{Gibbs-converse}\lean{KLDiv_eq_zero_iff_identDistrib}\leanok  If $D_{KL}(X\Vert Y) = 0$, then $Y$ is a copy of $X$.
\end{lemma}
\begin{proof}\leanok
  \uses{converse-log-sum}
  Apply \Cref{converse-log-sum}.
\end{proof}
/-- `KL(X ‖ Y) = 0` if and only if `Y` is a copy of `X`. -/
lemma KLDiv_eq_zero_iff_identDistrib [Fintype G] [MeasurableSingletonClass G]
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) :
    KL[X ; μ # Y ; μ'] = 0 ↔ IdentDistrib X Y μ μ' := by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [KLDiv, h.map_eq]⟩
  let νY := μ'.map Y
  have : IsProbabilityMeasure νY := isProbabilityMeasure_map hY.aemeasurable
  let νX := μ.map X
  have : IsProbabilityMeasure νX := isProbabilityMeasure_map hX.aemeasurable
  obtain ⟨r, hr⟩ : ∃ (r : ℝ), ∀ x ∈ Finset.univ, (νX {x}).toReal = r * (νY {x}).toReal := by
    apply sum_mul_log_div_eq_iff (by simp) (by simp) (fun i _ hi ↦ ?_)
    · rw [KLDiv_eq_sum] at h
      simpa using h
    · simp only [ENNReal.toReal_eq_zero_iff, measure_ne_top, or_false] at hi
      simp [habs i hi, νX]
  have r_eq : r = 1 := by
    have : r * ∑ x, (νY {x}).toReal = ∑ x, (νX {x}).toReal := by
      simp only [Finset.mul_sum, Finset.mem_univ, hr]
    simpa using this
  have : νX = νY := by
    apply Measure.ext_iff_singleton.mpr (fun x ↦ ?_)
    simpa [r_eq, ENNReal.toReal_eq_toReal] using hr x (Finset.mem_univ _)
  exact ⟨hX.aemeasurable, hY.aemeasurable, this⟩

/-- If $S$ is a finite set, $w_s$ is non-negative,
and ${\bf P}(X=x) = \sum_{s\in S} w_s {\bf P}(X_s=x)$, ${\bf P}(Y=x) =
  \sum_{s\in S} w_s {\bf P}(Y_s=x)$ for all $x$, then
$$D_{KL}(X\Vert Y) \le \sum_{s\in S} w_s D_{KL}(X_s\Vert Y_s).$$ -/