ent_sub_zsmul_sub_ent_le

lemma ent_sub_zsmul_sub_ent_le {Y : Ω → G} [IsProbabilityMeasure μ] [Finite 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_congr_left (Y := -Y') hY'.aemeasurable.neg, iX₁Y.rdist_eq hX₁' hY',      iX₂nY.rdist_eq hX₂' hY'.neg, entropy_neg hY', idX₁X₂'.entropy_congr.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]    simp only [sub_sub, neg_sub, add_sub_right_comm, sub_neg_eq_add, add_comm X₂']    linear_combination h1  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_congr <|          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_sub_zsmul_le 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_congr <|          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_congr  simp_rw [idX₁.rdist_congr idY, this] at h4 h4'  set n := |a| with ha  clear_value n  have hn : 0 ≤ n := by simp [ha]  lift n to ℕ using hn with n  induction n generalizing a with  | zero => simp [abs_eq_zero.mp ha.symm]  | succ n ih =>  have : a ≠ 0 := by rw [ne_eq, ← abs_eq_zero, ← ha]; norm_cast  have : n = |a - 1| ∨ n = |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]      · norm_num      · exact Int.sub_nonneg_of_le h  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        rw [← h]        exact ih h      _ = 4 * |a| * d[X ; μ # Y ; μ] := by        nth_rw 2 [← mul_one 4]        rw [← add_mul, ← mul_add, ← ha, ← h]        norm_num      _ = _ := by rw [← ha]  · 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        rw [← h]        exact ih h      _ = 4 * |a| * d[X ; μ # Y ; μ] := by        nth_rw 2 [← mul_one 4]        rw [← add_mul, ← mul_add, ← ha, ← h]        norm_num      _ = _ := by rw [← ha]