\begin{lemma}[Kaimonovich--Vershik--Madiman inequality, III]\label{klm-3}\lean{kvm_ineq_III}\leanok  If $n \geq 1$ and $X, Y_1, \dots, Y_n$ are jointly independent $G$-valued random variables, then
  $$d\left[X; \sum_{i=1}^n Y_i\right] \leq d\left[X; Y_1\right] + \frac{1}{2}\left(\bbH\left[ \sum_{i=1}^n Y_i\right] - \bbH[Y_1]\right).$$
\end{lemma}
\begin{proof}\uses{kv, ruz-indep}\leanok
  From \Cref{kv} one has
  $$ \bbH\left[-X + \sum_{i=1}^n Y_i\right] \leq \bbH[ - X + Y_1 ] + \bbH\left[ \sum_{i=1}^n Y_i \right] - \bbH[Y_1].$$
  The claim then follows from \Cref{ruz-indep} and some elementary algebra.
\end{proof}
lemma kvm_ineq_III {I : Type*} {i₀ i₁ : I} {s : Finset I}
    (hs₀ : ¬ i₀ ∈ s) (hs₁ : ¬ i₁ ∈ s) (h01 : i₀ ≠ i₁)
    (Y : I → Ω → G) [∀ i, FiniteRange (Y i)]
    (hY : ∀ i, Measurable (Y i)) (h_indep : iIndepFun Y μ) :
    d[Y i₀; μ # Y i₁ + ∑ i ∈ s, Y i; μ]
      ≤ d[Y i₀; μ # Y i₁; μ] + (2 : ℝ)⁻¹ * (H[Y i₁ + ∑ i ∈ s, Y i; μ] - H[Y i₁; μ]) := by
  let J := Fin 3
  let S : J → Finset I := ![{i₀}, {i₁}, s]
  have h_dis : Set.univ.PairwiseDisjoint S := by
    intro j _ k _ hjk
    change Disjoint (S j) (S k)
    fin_cases j <;> fin_cases k <;> try exact (hjk rfl).elim
    all_goals
      simp_all [Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
        Finset.disjoint_singleton_right, S, hs₀, hs₁, h01, h01.symm]
  let φ : (j : J) → ((_ : S j) → G) → G
    | 0 => fun Ys ↦ Ys ⟨i₀, by simp [S]⟩
    | 1 => fun Ys ↦ Ys ⟨i₁, by simp [S]⟩
    | 2 => fun Ys ↦ ∑ i : s, Ys ⟨i.1, i.2⟩
  have hφ : (j : J) → Measurable (φ j) := fun j ↦ .of_discrete
  have h_indep' : iIndepFun ![Y i₀, Y i₁, ∑ i ∈ s, Y i] μ := by
    convert iIndepFun.finsets_comp S h_dis h_indep hY φ hφ with j x
    fin_cases j <;> simp [φ, (s.sum_attach _).symm]
  exact kvm_ineq_III_aux (hY i₀) (hY i₁) (by fun_prop) h_indep'


open Classical in
/-- Let `X₁, ..., Xₘ` and `Y₁, ..., Yₗ` be tuples of jointly independent random variables (so the
`X`'s and `Y`'s are also independent of each other), and let `f: {1,..., l} → {1,... ,m}` be a
function, then `H[∑ j, Y j] ≤ H[∑ i, X i] + ∑ j, H[Y j - X f(j)] - H[X_{f(j)}]`.-/