multidist_ruzsa_III'

lemma multidist_ruzsa_III' {m : ℕ} (hm : m ≥ 2) {Ω : Type*} {hΩ : MeasureSpace Ω}    {X : Fin (m + 1) → Ω → G} (hmes : ∀ i, Measurable (X i))    (hident : ∀ j k, IdentDistrib (X j) (X k)) (hindep : iIndepFun X)    (hfin : ∀ i, FiniteRange (X i)) [IsProbabilityMeasure (ℙ : Measure Ω)] (i₀ : Fin m) :    D[Fin.init X ; fun _ ↦ hΩ] ≤ m * d[X i₀.castSucc # X i₀.castSucc] := by  set m' : Fin (m + 1) := Fin.last _  set X₀ := X m'  set S := ∑ i : Fin m, X i.castSucc  have hent (i : Fin (m + 1)) : H[X i] = H[X₀] := (hident _ _).entropy_congr  have hind' (i : Fin m) : IndepFun (X i.castSucc) X₀ ℙ := hindep.indepFun <| by simp [m']  have hind_S : IndepFun S X₀ ℙ := by    set s : Finset (Fin (m + 1)) := .Iio m'    set s' : Finset (Fin (m + 1)) := {m'}    have h_disjoint : Disjoint s s' := by aesop    have hm': m' ∈ s' := Finset.mem_singleton.mpr rfl    let φ (x : s → G) : G := ∑ i, x i    let φ' (x : s' → G) : G := x ⟨m', hm'⟩    have hφ : Measurable φ := by fun_prop    have hφ' : Measurable φ' := by fun_prop    convert hindep.finsets_comp' h_disjoint hmes hφ hφ' with ω    simp only [Finset.sum_apply, Finset.univ_eq_attach, s.sum_attach (X · ω), S, φ]    exact Fin.sum_univ_castSucc' (X · ω)  have hmes_S : Measurable S := by fun_prop  calc    _ = H[S] - (∑ i : Fin m, H[X i.castSucc])/m :=       multiDist_indep _ (X := Fin.init X) (by simp [Fin.init]; fun_prop) <|         (hindep.precomp <| Fin.castSucc_injective m:)    _ ≤ H[-X₀ + S] - (∑ i : Fin m, H[X i.castSucc])/m := by      gcongr      rw [neg_add_eq_sub]      exact (le_max_left _ _).trans (max_entropy_le_entropy_sub hmes_S (hmes _) hind_S)    _ = (H[-X₀ + S] - H[-X₀]) - (∑ i : Fin m, H[X i.castSucc])/m + H[-X₀] := by abel    _ ≤ ∑ i : Fin m, (H[-X₀ + X i.castSucc] - H[-X₀])        - (∑ i : Fin m, H[X i.castSucc]) / m + H[-X₀] := by      gcongr      set Y : Fin (m + 1) → Ω → G := fun i ↦ if (i = m') then - X₀ else X i      have hYfin (i : Fin (m + 1)) : FiniteRange (Y i) := by        by_cases h : i = m' <;> simp [Y, h]        all_goals infer_instance      have hYfin (i : Fin (m + 1)) : Measurable (Y i) := by        by_cases h : i = m' <;> simp [Y, h]        · exact (hmes _).neg        · exact hmes i      have : H[Y m' + ∑ i < m', Y i] - H[Y m'] ≤ ∑ i < m', (H[Y m' + Y i] - H[Y m']) := by        apply kvm_ineq_I Finset.notMem_Iio_self hYfin _        set f : Fin (m + 1) → G → G := fun i g ↦ if i = m' then -g else g        convert iIndepFun.comp hindep f _ with i        · ext ω          by_cases h : i = m' <;> simp [f, h, Y, X₀]        intro i        by_cases h : i = m' <;> simp [f, h]        all_goals measurability      convert! this using 1      · congr        · simp [Y, X₀]        · convert Fin.sum_univ_castSucc' Y using 2 with i _          have : i.castSucc ≠ m' := by simp [m']          simp [Y, this]        simp [Y,X₀]      rw [← Fin.sum_univ_castSucc' _]      congr; ext i      have : i.castSucc ≠ m' := by simp [m']      congr      all_goals simp [Y,this,X₀]    _ = ∑ i : Fin m, d[X i.castSucc # X₀] - (∑ i : Fin m, H[X₀])/m + H[-X₀] := by      congr 2      · apply Finset.sum_congr rfl        intro i _        rw [(hind' i).rdist_eq (hmes _) (hmes _), hent, entropy_neg (hmes _), neg_add_eq_sub]        linarith      congr 1; apply Finset.sum_congr rfl      intro i _; exact hent _    _ = ∑ i : Fin m, d[X i.castSucc # X₀] := by simp [X₀, entropy_neg (hmes _)]; field_simp; ring    _ = ∑ i : Fin m, d[X i₀.castSucc # X i₀.castSucc] := by      congr; ext i      exact (hident _ _).rdist_congr (hident _ _)    _ = _ := by simp