\begin{lemma}[Convexity of Kullback--Leibler]\label{kl-div-convex}\lean{KLDiv_of_convex}\leanok  If $S$ is a finite set, $\sum_{s \in S} w_s = 1$ for some non-negative $w_s$, 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).$$
\end{lemma}
\begin{proof}\leanok
  \uses{kl-div,log-sum}
For each $x$, replace $\log \frac{\mathbf{P}(X_s=x)}{\mathbf{P}(Y_s=x)}$ in the definition with $\log \frac{w_s\mathbf{P}(X_s=x)}{w_s\mathbf{P}(Y_s=x)}$ for each $s$, and apply \Cref{log-sum}.
\end{proof}
lemma KLDiv_of_convex [Fintype G] [IsFiniteMeasure μ''']
    {ι : Type*} {S : Finset ι} {w : ι → ℝ} (hw : ∀ s ∈ S, 0 ≤ w s)
    (X' : ι → Ω'' → G) (Y' : ι → Ω''' → G)
    (hconvex : ∀ x, (μ.map X {x}).toReal = ∑ s ∈ S, (w s) * (μ''.map (X' s) {x}).toReal)
    (hconvex' : ∀ x, (μ'.map Y {x}).toReal = ∑ s ∈ S, (w s) * (μ'''.map (Y' s) {x}).toReal)
    (habs : ∀ s ∈ S, ∀ x, μ'''.map (Y' s) {x} = 0 → μ''.map (X' s) {x} = 0) :
    KL[X ; μ # Y ; μ'] ≤ ∑ s ∈ S, w s * KL[X' s ; μ'' # Y' s ; μ'''] := by
  conv_lhs => rw [KLDiv_eq_sum]
  have A x : (μ.map X {x}).toReal * log ((μ.map X {x}).toReal / (μ'.map Y {x}).toReal)
    ≤ ∑ s ∈ S, (w s * (μ''.map (X' s) {x}).toReal) *
        log ((w s * (μ''.map (X' s) {x}).toReal) / (w s * (μ'''.map (Y' s) {x}).toReal)) := by
    rw [hconvex, hconvex']
    apply sum_mul_log_div_leq (fun s hs ↦ ?_) (fun s hs ↦ ?_) (fun s hs h's ↦ ?_)
    · exact mul_nonneg (by simp [hw s hs]) (by simp)
    · exact mul_nonneg (by simp [hw s hs]) (by simp)
    · rcases mul_eq_zero.1 h's with h | h
      · simp [h]
      · simp only [ENNReal.toReal_eq_zero_iff, measure_ne_top, or_false] at h
        simp [habs s hs x h]
  have B x : (μ.map X {x}).toReal * log ((μ.map X {x}).toReal / (μ'.map Y {x}).toReal)
    ≤ ∑ s ∈ S, (w s * (μ''.map (X' s) {x}).toReal) *
        log ((μ''.map (X' s) {x}).toReal / (μ'''.map (Y' s) {x}).toReal) := by
    apply (A x).trans_eq
    apply Finset.sum_congr rfl (fun s _ ↦ ?_)
    rcases eq_or_ne (w s) 0 with h's | h's
    · simp [h's]
    · congr 2
      rw [mul_div_mul_left _ _ h's]
  apply (Finset.sum_le_sum (fun x _ ↦ B x)).trans_eq
  rw [Finset.sum_comm]
  simp_rw [mul_assoc, ← Finset.mul_sum, KLDiv_eq_sum]