multidist_ruzsa_I_indep

lemma multidist_ruzsa_I_indep {m : ℕ} (hm : m ≥ 1) {Ω : Type*} (hΩ : MeasureSpace Ω)    [IsProbabilityMeasure (hΩ.volume)] (X : Fin m → Ω → G) (h_indep : iIndepFun X)    (hmes : ∀ j, Measurable (X j)) (hfin : ∀ j, FiniteRange (X j)) :    ∑ j, ∑ k, (if j = k then (0:ℝ) else d[X j # -X k]) ≤ m * (m - 1) * D[X; fun _ ↦ hΩ] := by  have claim1 {j k : Fin m} (h: j ≠ k) : H[X j + X k] ≤ H[∑ i, X i] := by    set S := ∑ i ∈ {j,k}ᶜ, X i    have : ∑ i, X i = X j + X k + S := by      rw [←Finset.sum_compl_add_sum {j,k} _, add_comm]      congr      simp [h]    rw [this]    apply (le_max_left _ _).trans (max_entropy_le_entropy_add _ _ _)    · exact Measurable.add (hmes j) (hmes k)    · have : ∀ i ∈ ({j,k}: Finset (Fin m))ᶜ, Measurable (X i) := by        intro i _; exact hmes i      convert Finset.measurable_sum _ this with ω      simp only [Finset.sum_apply,S]    set s : Fin 2 → Finset (Fin m) := ![{j,k}, {j,k}ᶜ]    set γ : Fin 2 → Type uG := fun _ ↦ G    set ϕ : (j:Fin 2) → (({ x // x ∈ s j } → G) → γ j) := fun _ x ↦ ∑ i, x i    have hϕ: ∀ a : Fin 2, Measurable (ϕ a) := by      intro _      convert Finset.measurable_sum _ _ with ω      · simp [γ]        infer_instance      measurability    have h_disjoint: Set.univ.PairwiseDisjoint s := by      simp [Set.PairwiseDisjoint, Set.Pairwise, Fin.forall_fin_two, Function.onFun, s]    have hneq : (0:Fin 2) ≠ (1:Fin 2) := by norm_num    replace h_indep := (h_indep.finsets_comp s h_disjoint hmes ϕ hϕ).indepFun hneq    simp [s,ϕ] at h_indep    convert h_indep with ω ω    · calc        _ = ∑ i ∈ {j,k}, X i ω := by simp [Finset.sum_pair h]        _ = _ := by          convert (Finset.sum_attach _ _).symm          simp    simp only [Finset.sum_apply,S]    exact (Finset.sum_attach _ _).symm  have claim2 (j k : Fin m) (h: j ≠ k) : d[X j # -X k] ≤ H[∑ i, X i] - (H[X j] + H[X k]) / 2 := by    rw [IndepFun.rdist_eq _ (hmes j) _]    · simp only [sub_neg_eq_add, tsub_le_iff_right, entropy_neg (hmes k)]      convert claim1 h using 1      ring    · exact (h_indep.indepFun h).neg_right    exact (hmes k).neg  calc    _ ≤ offDiag_sum (fun j k ↦ (H[∑ i, X i] - (H[X j] + H[X k]) / 2)) := offDiag_sum_le _ _ claim2    _ = m * (m - 1) * H[∑ i, X i] - ((m - 1) * ∑ j, H[X j] + (m - 1) * ∑ j, H[X j]) / 2 := by      rw [offDiag_sum_sub, offDiag_sum_div, offDiag_sum_add, offDiag_sum_const hm,        offDiag_sum_left hm, offDiag_sum_right hm]    _ = m * (m - 1) * D[X; fun _ ↦ hΩ] := by      rw [multiDist_indep hΩ hmes h_indep, mul_sub ((m:ℝ) * (m - 1 : ℝ)) _ _]      congr      field_simp      ring