Multidist ruzsa IV

lemma multidist_ruzsa_IV {m : ℕ} (hm : m ≥ 2) {Ω : Type u} [MeasureSpace Ω] (X : Fin m → Ω → G)    (h_indep : iIndepFun X) (hmes : ∀ i, Measurable (X i)) [IsProbabilityMeasure (ℙ : Measure Ω)]    (hfin : ∀ i, FiniteRange (X i)) :    d[∑ i, X i # - ∑ i, X i] ≤ 2 * D[X; fun _ ↦ inferInstance] := by  set mS₂ : Fin 2 × Fin m → MeasurableSpace G := fun _ ↦ inferInstance  set mΩ₂ : (i : Fin 2 × Fin m) → MeasurableSpace Ω := fun _ ↦ inferInstance  obtain ⟨Ω', hΩ', μ', X', hprob', h_indep', hX'⟩ :=    independent_copies'_finiteRange (mS := mS₂) (mΩ := mΩ₂) (fun i ↦ (X i.2)) (fun i ↦ hmes i.2)      (fun _ ↦ volume)  have hX'meas i := (hX' i).1  letI hΩ' : MeasureSpace Ω' := ⟨μ'⟩  set W₀ := ∑ i, X' (0, i)  set W₁ := ∑ i, X' (1, i)  have hW_ident (a: Fin 2) : IdentDistrib (∑ i, X' (a, i)) (∑ i, X i) := by    have : IdentDistrib (fun ω i ↦ X' (a, i) ω) (fun ω i ↦ X i ω) := by      refine IdentDistrib.iprodMk ?_ hprob' inferInstance ?_ h_indep      · intro i; exact (hX' (a,i)).2.1      exact h_indep'.precomp (Prod.mk_right_injective a)    convert IdentDistrib.comp this (u := fun x ↦ ∑ i, x i) (by measurability)    all_goals ext ω; simp  have hW₀_ident : IdentDistrib W₀ (∑ i, X i) := hW_ident 0  have hW₁_ident : IdentDistrib W₁ (∑ i, X i) := hW_ident 1  have hW₀_mes : Measurable W₀ := by fun_prop  have hW₁_mes : Measurable W₁ := by fun_prop  have hW₀W₁ : H[W₁] = H[W₀] := (hW₁_ident.trans hW₀_ident.symm).entropy_congr  have hfin' (i : Fin 2 × Fin m) : FiniteRange (X' i) := (hX' i).2.2  have hmes' (i : Fin 2 × Fin m) : Measurable (X' i) := (hX' i).1  have claim (a b : Fin m) (hab : a ≠ b) : H[W₀ + W₁] ≤ 3 * H[W₀] - H[X a] - H[X b] := by    set W₀' := ∑ i ∈ Finset.univ.erase a, X' (0, i)    set W₁' := ∑ i ∈ Finset.univ.erase b, X' (1, i)    have hW₀' : W₀ = W₀' + X' (0, a) := (Finset.sum_erase_add _ _ (Finset.mem_univ a)).symm    have hW₁' : W₁ = X' (1, b) + W₁' := by      rw [add_comm]      exact (Finset.sum_erase_add _ _ (Finset.mem_univ b)).symm    have hW₀'_mes : Measurable W₀' := by fun_prop    have hW₁'_mes : Measurable W₁' := by fun_prop    have h1a : H[W₀' + X' (0,a)] = H[W₀] := by rw [hW₀']    have h1b : H[W₀ + W₁] = H[W₀' + X' (0, a) + W₁] := by rw [hW₀']    have h1c : H[X' (1, b) + W₁'] = H[W₁] := by rw [hW₁']    have h1d : H[X' (0, a) + W₁] = H[X' (0, a) + X' (1, b) + W₁'] := by rw [hW₁', add_assoc]    have h2a : H[X' (0,a)] = H[X a] := by apply IdentDistrib.entropy_congr (hX' (0,a)).2.1    have h2b : H[X' (1, b)] = H[X b] := by apply IdentDistrib.entropy_congr (hX' (1, b)).2.1    have h2c : H[X' (0, a) + X' (1, b)] = H[X a + X b] := by      apply IdentDistrib.entropy_congr      apply (hX' (0,a)).2.1.add (hX' (1, b)).2.1      · apply h_indep'.indepFun; simp      apply h_indep.indepFun; simp [hab]    have h2d: H[X' (0, a) + X' (0, b)] = H[X a + X b] := by      apply IdentDistrib.entropy_congr      apply (hX' (0,a)).2.1.add (hX' (0, b)).2.1      · apply h_indep'.indepFun; simp [hab]      apply h_indep.indepFun; simp [hab]    have h3: H[X a + X b] ≤ H[W₀] := by      set W := ∑ i ∈ {a, b}ᶜ, X' (0, i)      have : W₀ = X' (0, a) + X' (0, b) + W := by        rw [add_comm]        convert (Finset.sum_compl_add_sum {a, b} (fun a ↦ X' (0,a))).symm using 2        simp [hab]      rw [this, ←h2d]      apply (le_max_left _ _).trans (max_entropy_le_entropy_add _ _ _)      · fun_prop      · fun_prop      set S : Finset (Fin 2 × Fin m) := {(0,a), (0, b)}      set ι : Fin m ↪ Fin 2 × Fin m := Function.Embedding.sectR (0:Fin 2) (Fin m)      set S' : Finset (Fin 2 × Fin m) := Finset.map ι {a, b}ᶜ      have hab' : ((0:Fin 2),a) ≠ (0, b) := by simp [hab]      have h_disjoint : Disjoint S S' := by        rw [Finset.disjoint_left]; intro ⟨i, j⟩ h; simp [S,S',ι] at h ⊢; tauto      set φ : (S → G) → G := fun x ↦ ∑ i, x i      set φ' : (S' → G) → G := fun x ↦ ∑ i, x i      have hφ : Measurable φ := by        apply Finset.measurable_sum        intro i _; exact measurable_pi_apply i      have hφ' : Measurable φ' := by        apply Finset.measurable_sum        intro i _; exact measurable_pi_apply i      convert! iIndepFun.finsets_comp' h_disjoint h_indep' hmes' hφ hφ' using 1      · ext ω        simp only [Fin.isValue, Pi.add_apply, Finset.univ_eq_attach, φ]        rw [Finset.sum_attach S (fun i ↦ X' i ω), Finset.sum_pair hab']      ext ω      simp only [Finset.sum_apply, Finset.univ_eq_attach, W, φ']      rw [Finset.sum_attach S' (fun i ↦ X' i ω)]      simp only [S', Finset.sum_map]      congr    have h4a : H[W₀' + X' (0, a) + W₁] - H[W₀' + X' (0, a)] ≤ H[X' (0, a) + W₁] - H[X' (0,a)] := by      apply kaimanovich_vershik _ hW₀'_mes (hmes' (0,a)) hW₁_mes      set S : Fin 3 → Finset (Fin 2 × Fin m) :=        fun i ↦ match i with        | 0 => Finset.map (Function.Embedding.sectR (0:Fin 2) (Fin m)) (Finset.univ.erase a)        | 1 => {(0,a)}        | 2 => Finset.map (Function.Embedding.sectR (1:Fin 2) (Fin m)) Finset.univ      have h_disjoint01 : Disjoint (S 0) (S 1) := by        rw [Finset.disjoint_iff_ne]        intro (i, b) hb (j, c) hc        simp only [Fin.isValue, Finset.map_erase, Embedding.sectR_apply, Finset.mem_erase, ne_eq,          Prod.mk.injEq, not_and, Finset.mem_map, Finset.mem_univ, true_and, exists_eq_right,          Finset.mem_singleton, S] at hb hc ⊢        intro _        have := hb.1 (hb.2.symm)        rwa [hc.2]      have h_disjoint02 : Disjoint (S 0) (S 2) := by        rw [Finset.disjoint_iff_ne]        intro (i, b) hb (j, c) hc        simp [S] at hb hc ⊢        simp [←hb.2, ←hc]      have h_disjoint12 : Disjoint (S 1) (S 2) := by        rw [Finset.disjoint_iff_ne]        intro (i, b) hb (j, c) hc        simp [S] at hb hc ⊢        simp [hb.1, ←hc]      have h_disjoint : Set.PairwiseDisjoint Set.univ S := by        rw [Set.PairwiseDisjoint, Set.Pairwise]        simp_rw [Fin.forall_fin_three]        simp [h_disjoint01, h_disjoint01.symm, h_disjoint02, h_disjoint02.symm, h_disjoint12,          h_disjoint12.symm]      set φ : (j:Fin 3) → ((i:S j) → G) → G := fun j x ↦ ∑ i, x i      have hφ (j:Fin 3) : Measurable (φ j) := by        simp only [Finset.univ_eq_attach, φ]        apply Finset.measurable_sum        intro i _; exact measurable_pi_apply i      convert! iIndepFun.finsets_comp S h_disjoint h_indep' hmes' φ hφ using 1      ext j ω      fin_cases j <;> simp [φ, Finset.sum_attach _ (fun i ↦ X' i ω), S, W₁, W₀']    have h4b :        H[X' (0, a) + X' (1, b) + W₁'] - H[X' (0, a) + X' (1, b)]          ≤ H[X' (1, b) + W₁'] - H[X' (1, b)] := by      apply kaimanovich_vershik _ (hmes' (0,a)) (hmes' (1, b)) hW₁'_mes      set S : Fin 3 → Finset (Fin 2 × Fin m) :=        fun i ↦ match i with        | 0 => {(0,a)}        | 1 => {(1, b)}        | 2 => Finset.map (Function.Embedding.sectR (1:Fin 2) (Fin m)) (Finset.univ.erase b)      have h_disjoint01 : Disjoint (S 0) (S 1) := by        rw [Finset.disjoint_iff_ne]        intro (i, b) hb (j, c) hc        simp [S] at hb hc ⊢        simp [hb.1, hc.1]      have h_disjoint02 : Disjoint (S 0) (S 2) := by        rw [Finset.disjoint_iff_ne]        intro (i, b) hb (j, c) hc        simp [S] at hb hc ⊢        simp [hb.1, ←hc.2]      have h_disjoint12 : Disjoint (S 1) (S 2) := by        rw [Finset.disjoint_iff_ne]        intro (i,d) hd (j, c) hc        simp only [Fin.isValue, Finset.map_erase, Embedding.sectR_apply, Finset.mem_singleton,          Prod.mk.injEq, Finset.mem_erase, ne_eq, not_and, Finset.mem_map, Finset.mem_univ,          true_and, exists_eq_right, S] at hd hc ⊢        intro _        replace hc := hc.1 hc.2.symm        contrapose! hc        rw [←hc, hd.2]      have h_disjoint : Set.PairwiseDisjoint Set.univ S := by        rw [Set.PairwiseDisjoint, Set.Pairwise]        simp_rw [Fin.forall_fin_three]        simp [h_disjoint01, h_disjoint01.symm, h_disjoint02, h_disjoint02.symm, h_disjoint12,          h_disjoint12.symm]      set φ : (j:Fin 3) → ((i:S j) → G) → G := fun j x ↦ ∑ i, x i      have hφ (j:Fin 3) : Measurable (φ j) := by        simp only [Finset.univ_eq_attach, φ]        apply Finset.measurable_sum        intro i _; exact measurable_pi_apply i      convert! iIndepFun.finsets_comp S h_disjoint h_indep' hmes' φ hφ using 1      ext j ω      fin_cases j <;> simp [φ, Finset.sum_attach _ (fun i ↦ X' i ω), S, W₁']    linarith  replace claim := offDiag_sum_le _ _ claim  have hm' : m ≥ 1 := by linarith  rw [offDiag_sum_sub, offDiag_sum_sub, offDiag_mul_sum, offDiag_sum_const hm',    offDiag_sum_const hm', offDiag_sum_left hm', offDiag_sum_right hm'] at claim  have claim2 : m * (m - 1) * H[W₀+W₁] - m*(m - 1)*H[W₀] ≤    2 * m*(m - 1)*H[W₀] - 2 * (m - 1) * ∑ j, H[X j] := by linarith  have hpos : (m:ℝ) * (m - 1) > 0 := by    have : (0 : ℝ) < m - 1 := by simp; linarith    positivity  apply le_of_mul_le_mul_left _ hpos  convert! claim2 using 1  · rw [← mul_sub_left_distrib]; congr    have hW₁_ident' : IdentDistrib (-W₁) (-∑ i, X i) := hW₁_ident.comp (u := (-·)) (by fun_prop)    rw [IdentDistrib.rdist_congr hW₀_ident.symm hW₁_ident'.symm, IndepFun.rdist_eq _ hW₀_mes _]    · simp only [sub_neg_eq_add]      rw [entropy_neg hW₁_mes]      linarith    · set S : Finset (Fin 2 × Fin m) := .map (.sectR (0:Fin 2) (Fin m)) .univ      set S' : Finset (Fin 2 × Fin m) := .map (.sectR (1:Fin 2) (Fin m)) .univ      have h_disjoint : Disjoint S S' := by        rw [Finset.disjoint_iff_ne]        intro (i,a) ha (j, b) hb        simp [S,S'] at ha hb ⊢        simp [← ha, ←hb]      set φ : (S → G) → G := fun x ↦ ∑ i, x i      set φ' : (S' → G) → G := fun x ↦ - ∑ i, x i      have hφ : Measurable φ := by        apply Finset.measurable_sum        intro i _; exact measurable_pi_apply i      have hφ' : Measurable φ' := by        apply Measurable.neg        apply Finset.measurable_sum        intro i _; exact measurable_pi_apply i      convert! iIndepFun.finsets_comp' h_disjoint h_indep' hmes' hφ hφ' using 1      · ext ω        simp only [Finset.sum_apply, Finset.univ_eq_attach, W₀, φ]        rw [Finset.sum_attach S (fun i ↦ X' i ω)]        simp [S]      ext ω      simp only [Finset.univ_eq_attach, W₁, φ']      rw [Finset.sum_attach S' (fun i ↦ X' i ω)]      simp [S']    exact Measurable.neg hW₁_mes  rw [multiDist_indep _ hmes h_indep]  have : H[∑ i, X i] = H[W₀] := by    apply IdentDistrib.entropy_congr    exact hW₀_ident.symm  rw [this]  field_simp