\begin{lemma}[Sums of dilates II]\label{sum-dilate-II}\lean{ent_of_sub_smul_le}\leanok  Let $X,Y$ be independent $G$-valued random variables, and let $a$ be an integer.  Then
  $$\bbH[X-aY] - \bbH[X] \leq 4 |a| d[X;Y].$$
\end{lemma}
\begin{proof}\uses{kv, ruz-indep, sign-flip, sum-dilate-I}\leanok From \Cref{kv} one has
  $$\bbH[Y-X+X'] - \bbH[Y-X] \leq \bbH[Y+X'] - \bbH[Y] = \bbH[Y+X] - \bbH[Y]$$
  which by \Cref{ruz-indep} gives
  $$\bbH[X-Y-X'] -\bbH[X] \leq d[X;Y] + d[X;-Y]$$
  and hence by \Cref{sign-flip}
  $$\bbH[X-Y-X'] - \bbH[X] \leq 4d[X;Y].$$
  From \Cref{sum-dilate-I} we then have
  $$\bbH[X-(a\pm 1)Y] \leq \bbH[X-aY] + 4 d[X;Y]$$
and the claim now follows by an induction on $|a|$.
\end{proof}
lemma ent_of_sub_smul_le {Y : Ω → G} [IsProbabilityMeasure μ] [Fintype G]
    (hX : Measurable X) (hY : Measurable Y) (h_indep : IndepFun X Y μ) {a : ℤ} :
    H[X - a • Y; μ] - H[X; μ] ≤ 4 * |a| * d[X ; μ # Y ; μ] := by
  obtain ⟨Ω', mΩ', μ', X₁', Y', X₂', hμ', h_indep', hX₁', hY', hX₂', idX₁, idY, idX₂⟩
    := independent_copies3_nondep hX hY hX μ μ μ
  have iX₁Y : IndepFun X₁' Y' μ' := h_indep'.indepFun (show 0 ≠ 1 by simp)
  have iYX₂ : IndepFun Y' X₂' μ' := h_indep'.indepFun (show 1 ≠ 2 by simp)
  have iX₂nY : IndepFun X₂' (-Y') μ' := iYX₂.symm.comp measurable_id measurable_neg
  have inX₁YX₂ : iIndepFun ![-X₁', Y', X₂'] μ' := by
    convert h_indep'.comp ![-id, id, id] (by fun_prop) with i
    match i with | 0 => rfl | 1 => rfl | 2 => rfl
  have idX₁X₂' : IdentDistrib X₁' X₂' μ' μ' := idX₁.trans idX₂.symm
  have idX₁Y : IdentDistrib (⟨X, Y⟩) (⟨X₁', Y'⟩) μ μ' :=
    IdentDistrib.prodMk idX₁.symm idY.symm h_indep iX₁Y
  have h1 : H[Y' - X₁' + X₂'; μ'] - H[Y' - X₁'; μ'] ≤ H[Y' + X₂'; μ'] - H[Y'; μ'] := by
    simp_rw [sub_eq_add_neg Y', add_comm Y' (-X₁')]
    exact kaimanovich_vershik inX₁YX₂ hX₁'.neg hY' hX₂'
  have h2 : H[X₁' - Y' - X₂'; μ'] - H[X₁'; μ'] ≤ d[X₁' ; μ' # Y' ; μ'] + d[X₁' ; μ' # -Y' ; μ'] := by
    rw [idX₁X₂'.rdist_eq (IdentDistrib.refl hY'.aemeasurable).neg, iX₁Y.rdist_eq hX₁' hY',
      iX₂nY.rdist_eq hX₂' hY'.neg, entropy_neg hY', idX₁X₂'.entropy_eq.symm]
    rw [show H[X₁' - Y' - X₂'; μ'] = H[-(X₁' - Y' - X₂'); μ']
      from entropy_neg (hX₁'.sub hY' |>.sub hX₂') |>.symm]
    rw [show H[X₁' - Y'; μ'] = H[-(X₁' - Y'); μ'] from entropy_neg (hX₁'.sub hY') |>.symm]
    ring_nf
    rw [sub_eq_add_neg, add_comm, add_assoc, sub_neg_eq_add]
    gcongr
    convert sub_le_iff_le_add'.mp h1 using 1
    · simp [sub_eq_add_neg, add_comm]
    · simp only [sub_eq_add_neg, neg_add_rev, neg_neg, add_comm, add_assoc]
      linarith
  have h3 : H[X₁' - Y' - X₂' ; μ'] - H[X₁'; μ'] ≤ 4 * d[X₁' ; μ' # Y' ; μ'] :=
    calc
      _ ≤ d[X₁' ; μ' # Y' ; μ'] + d[X₁' ; μ' # -Y' ; μ'] := h2
      _ ≤ d[X₁' ; μ' # Y' ; μ'] + 3 * d[X₁' ; μ' # Y' ; μ'] := by
        gcongr
        exact rdist_of_neg_le hX₁' hY'
      _ = _ := by ring_nf
  have h4 (a : ℤ) : H[X - (a + 1) • Y; μ] ≤ H[X₁' - a • Y'; μ'] + 4 * d[X₁' ; μ' # Y' ; μ'] := by
    calc
      _ = H[X₁' - (a + 1) • Y'; μ'] :=
        IdentDistrib.entropy_eq <|
          idX₁Y.comp (show Measurable (fun xy ↦ (xy.1 - (a + 1) • xy.2)) by fun_prop)
      _ ≤ H[X₁' - a • Y'; μ'] + H[X₁' - Y' - X₂'; μ'] - H[X₁'; μ'] :=
        ent_of_sub_smul hX₁' hY' hX₂' h_indep' idX₁X₂'
      _ ≤ H[X₁' - a • Y'; μ'] + 4 * d[X₁' ; μ' # Y' ; μ'] := by
        rw [add_sub_assoc]
        gcongr
  have h4' (a : ℤ) : H[X - (a - 1) • Y; μ] ≤ H[X₁' - a • Y'; μ'] + 4 * d[X₁' ; μ' # Y' ; μ'] := by
    calc
      _ = H[X₁' - (a - 1) • Y'; μ'] :=
        IdentDistrib.entropy_eq <|
          idX₁Y.comp (show Measurable (fun xy ↦ (xy.1 - (a - 1) • xy.2)) by fun_prop)
      _ ≤ H[X₁' - a • Y'; μ'] + H[X₁' - Y' - X₂'; μ'] - H[X₁'; μ'] :=
        ent_of_sub_smul' hX₁' hY' hX₂' h_indep' idX₁X₂'
      _ ≤ H[X₁' - a • Y'; μ'] + 4 * d[X₁' ; μ' # Y' ; μ'] := by
        rw [add_sub_assoc]
        gcongr
  have (a : ℤ) : H[X₁' - a • Y'; μ'] = H[X - a • Y; μ] :=
    idX₁Y.symm.comp (show Measurable (fun xy ↦ (xy.1 - a • xy.2)) by fun_prop) |>.entropy_eq
  simp_rw [IdentDistrib.rdist_eq idX₁ idY, this] at h4 h4'
  set! n := |a| with ha
  have hn : 0 ≤ n := by simp [ha]
  lift n to ℕ using hn with n
  induction' n with n ih generalizing a
  · rw [← ha, abs_eq_zero.mp ha.symm]
    simp
  · rename_i m _
    have : a ≠ 0 := by
      rw [ne_eq, ← abs_eq_zero, ← ha]
      exact NeZero.natCast_ne (m + 1) ℤ
    have : m = |a - 1| ∨ m = |a + 1| := by
      rcases lt_or_gt_of_ne this with h | h
      · right
        rw [abs_of_neg h] at ha
        rw [abs_of_nonpos (by exact h), neg_add, ← ha]
        norm_num
      · left
        rw [abs_of_pos h] at ha
        rw [abs_of_nonneg ?_, ← ha]
        swap; exact Int.sub_nonneg_of_le h
        norm_num
    rcases this with h | h
    · calc
        _ ≤ H[X - (a - 1) • Y; μ] - H[X; μ] + 4 * d[X ; μ # Y ; μ] := by
          nth_rw 1 [(a.sub_add_cancel 1).symm, sub_add_eq_add_sub _ H[X; μ]]
          gcongr
          exact h4 (a - 1)
        _ ≤ 4 * |a - 1| * d[X ; μ # Y ; μ] + 4 * d[X ; μ # Y ; μ] := by
          gcongr
          exact ih h h
        _ = 4 * |a| * d[X ; μ # Y ; μ] := by
          nth_rw 2 [← mul_one 4]
          rw [← add_mul, ← mul_add, ← ha, ← h]
          norm_num
    · calc
        _ ≤ H[X - (a + 1) • Y; μ] - H[X; μ] + 4 * d[X ; μ # Y ; μ] := by
          nth_rw 1 [(a.add_sub_cancel 1).symm, sub_add_eq_add_sub _ H[X; μ]]
          gcongr
          exact h4' (a + 1)
        _ ≤ 4 * |a + 1| * d[X ; μ # Y ; μ] + 4 * d[X ; μ # Y ; μ] := by
          gcongr
          exact ih h h
        _ = 4 * |a| * d[X ; μ # Y ; μ] := by
          nth_rw 2 [← mul_one 4]
          rw [← add_mul, ← mul_add, ← ha, ← h]
          norm_num