\begin{lemma}[Kaimonovich--Vershik--Madiman inequality, II]\label{klm-2}\lean{kvm_ineq_II}\leanok  If $n \geq 1$ and $X, Y_1, \dots, Y_n$ are jointly independent $G$-valued random variables, then
  $$ d[X; \sum_{i=1}^n Y_i] \leq 2 \sum_{i=1}^n d[X; Y_i].$$
\end{lemma}
\begin{proof}\uses{klm-1, neg-ent, ruz-indep, sumset-lower, ruzsa-diff}\leanok
  Applying \Cref{klm-1} with all the $Y_i$ replaced by $-Y_i$, and using \Cref{neg-ent} and \Cref{ruz-indep}, we obtain after some rearranging
$$ d[X; \sum_{i=1}^n Y_i] + \frac{1}{2} (\bbH[\sum_{i=1}^n Y_i] - \bbH[X]) \leq \sum_{i=1}^n \left(d[X;Y_i] + \frac{1}{2} (\bbH[Y_i] - \bbH[X])\right).$$
From \Cref{sumset-lower} we have
$$ \bbH[\sum_{i=1}^n Y_i] \geq \bbH[Y_i]$$
for all $i$; subtracting $\bbH[X]$ and averaging, we conclude that
$$ \bbH[\sum_{i=1}^n Y_i] - \bbH[X] \geq \frac{1}{n} \sum_{i=1}^n \bbH[Y_i] - \bbH[X]$$
and thus
$$ d[X; \sum_{i=1}^n Y_i] \leq \sum_{i=1}^n d[X;Y_i] + \frac{n-1}{2n} (\bbH[Y_i] - \bbH[X]).$$
From \Cref{ruzsa-diff} we have
$$ \bbH[Y_i] - \bbH[X] \leq 2 d[X;Y_i].$$
Since $0 \leq \frac{n-1}{2n} \leq \frac{1}{2}$, the claim follows.
\end{proof}
lemma kvm_ineq_II {I : Type*} {i₀ : I} {s : Finset I} (hs : ¬ i₀ ∈ s)
    (hs' : Finset.Nonempty s) {Y : I → Ω → G} [∀ i, FiniteRange (Y i)]
    (hY : (i : I) → Measurable (Y i)) (h_indep : iIndepFun Y μ) :
    d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ] := by
  classical
  have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
  let φ i : G → G := if i = i₀ then id else - id
  have hφ i : Measurable (φ i) := .of_discrete
  let Y' i : Ω → G := φ i ∘ Y i
  have mnY : (i : I) → Measurable (Y' i) := fun i ↦ (hφ i).comp (hY i)
  have h_indep2 : IndepFun (Y i₀) (∑ i ∈ s, Y i) μ :=
    iIndepFun.indepFun_finset_sum_of_not_mem h_indep (fun i ↦ hY i) hs |>.symm
  have ineq4 : d[Y i₀; μ # ∑ i ∈ s, Y i; μ] + 1/2 * (H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ])
      ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ])) := by
    calc
      _ = H[Y i₀ - ∑ i ∈ s, Y i ; μ] - H[Y i₀ ; μ] := by
        rw [IndepFun.rdist_eq h_indep2 (hY i₀) (by fun_prop)]
        ring
      _ = H[Y' i₀ + ∑ x ∈ s, Y' x ; μ] - H[Y' i₀ ; μ] := by
        simp [Y', φ, sub_eq_add_neg, ← Finset.sum_neg_distrib]
        congr! 3 with i hi
        simp [ne_of_mem_of_not_mem hi hs, Pi.neg_comp]
      _ ≤ ∑ x ∈ s, (H[Y' i₀ + Y' x ; μ] - H[Y' i₀ ; μ]) := kvm_ineq_I hs mnY (h_indep.comp φ hφ)
      _ = ∑ i ∈ s, (H[Y i₀ - Y i ; μ] - H[Y i₀ ; μ]) := by
        congr! 1 with i hi; simp [Y', φ, ne_of_mem_of_not_mem hi hs, Pi.neg_comp, sub_eq_add_neg]
      _ = _ := by
        refine Finset.sum_congr rfl fun i hi ↦ ?_
        rw [IndepFun.rdist_eq (h_indep.indepFun (ne_of_mem_of_not_mem hi hs).symm) (hY i₀) (hY i)]
        ring
  replace ineq4 : d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ]
      + 1/2 * (H[Y i; μ] - H[Y i₀; μ])) - 1/2 * (H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ]) :=
    le_tsub_of_add_le_right ineq4
  have ineq5 (j : I) (hj : j ∈ s) : H[Y j ; μ] ≤ H[∑ i ∈ s, Y i; μ] :=
    max_entropy_le_entropy_sum hj hY h_indep
  have ineq6 : (s.card : ℝ)⁻¹ * ∑ i ∈ s, (H[Y i; μ] - H[Y i₀; μ]) ≤ H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ] := by
    rw [inv_mul_le_iff₀ (by exact_mod_cast Finset.card_pos.mpr hs'), ← smul_eq_mul,
      Nat.cast_smul_eq_nsmul, ← Finset.sum_const]
    refine Finset.sum_le_sum fun i hi ↦ ?_
    gcongr
    exact ineq5 i hi
  have ineq7 : d[Y i₀; μ # ∑ i ∈ s, Y i; μ]
    ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / (2 * s.card) * (H[Y i; μ] - H[Y i₀; μ])) := by
    calc
      _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ]))
          - 1/2 * (H[∑ i ∈ s, Y i; μ] - H[Y i₀; μ]) := ineq4
      _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ]))
          - 1/2 * ((s.card : ℝ)⁻¹ * ∑ i ∈ s, (H[Y i; μ] - H[Y i₀; μ])) := by gcongr
      _ = ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + 1/2 * (H[Y i; μ] - H[Y i₀; μ])
          - 1/2 * ((s.card : ℝ)⁻¹ * (H[Y i; μ] - H[Y i₀; μ]))) := by
        rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_sub_distrib]
      _ = ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / (2 * s.card) * (H[Y i; μ] - H[Y i₀; μ])) := by
        refine Finset.sum_congr rfl fun i _ ↦ ?_
        rw [add_sub_assoc, ← mul_assoc, ← sub_mul]
        field_simp
  have ineq8 (i : I) : H[Y i; μ] - H[Y i₀; μ] ≤ 2 * d[Y i₀; μ # Y i; μ] := by
    calc
      _ ≤ |H[Y i₀ ; μ] - H[Y i ; μ]| := by
        rw [← neg_sub]
        exact neg_le_abs _
      _ ≤ 2 * d[Y i₀; μ # Y i; μ] := diff_ent_le_rdist (hY i₀) (hY i)
  calc
    _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / (2 * s.card) * (H[Y i; μ] - H[Y i₀; μ])) :=
      ineq7
    _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + (s.card - 1) / s.card * d[Y i₀; μ # Y i; μ]) := by
      simp_rw [div_eq_mul_inv, mul_inv, mul_comm (2 : ℝ)⁻¹, mul_assoc]
      gcongr ∑ i ∈ s, (d[Y i₀ ; μ # Y i ; μ] + (s.card - 1) * ((s.card : ℝ)⁻¹ * ?_))
      · simp only [sub_nonneg, Nat.one_le_cast]
        exact Nat.one_le_iff_ne_zero.mpr <| Finset.card_ne_zero.mpr hs'
      · exact (inv_mul_le_iff₀ zero_lt_two).mpr (ineq8 _)
    _ ≤ ∑ i ∈ s, (d[Y i₀; μ # Y i; μ] + d[Y i₀; μ # Y i; μ]) := by
      gcongr ∑ i ∈ s, (d[Y i₀ ; μ # Y i ; μ] + ?_) with i
      refine mul_le_of_le_one_left (rdist_nonneg (hY i₀) (hY i)) ?_
      exact (div_le_one (Nat.cast_pos.mpr <| Finset.card_pos.mpr hs')).mpr (by simp)
    _ = 2 * ∑ i ∈ s, d[Y i₀ ; μ # Y i ; μ] := by
      ring_nf
      exact (Finset.sum_mul _ _ _).symm