mutual_information_le_t_13

lemma mutual_information_le_t_13 : I[Z1 : Z3 | W] ≤ p.m * (4*p.m+1) * p.η * k := by  have hm := p.hm  have _ : NeZero p.m := by rw [neZero_iff]; linarith  let zero : Fin p.m := ⟨0, by linarith [hm]⟩  let X' : Fin p.m × Fin p.m → Ω' → G := fun (i, j) ω ↦ Y (i, j-i) ω  have hX'_indep : iIndepFun X' := by    let S : Fin p.m × Fin p.m → Finset (Fin p.m × Fin p.m) := fun (i,j) ↦ {(i,j-i)}    let φ : (q:Fin p.m × Fin p.m) → ((_: S q) → G) → G := fun q x ↦ x ⟨(q.1,q.2-q.1), by simp [S]⟩    convert iIndepFun.finsets_comp S _ h_indep (by fun_prop) φ (by fun_prop) with i ω    rw [Finset.pairwiseDisjoint_iff]; rintro ⟨i,j⟩ _ ⟨i',j'⟩ _ ⟨⟨i₀, j₀⟩, hij⟩    simp only [Finset.mem_inter, Finset.mem_singleton, Prod.mk.injEq, S] at hij    obtain ⟨⟨rfl, rfl⟩, rfl, h2⟩ := hij    simpa using h2  have hindep_j (j: Fin p.m) : iIndepFun (fun i ↦ X' (i, j)) := by    let S : Fin p.m → Finset (Fin p.m × Fin p.m) := fun i ↦ {(i,j)}    let φ : (i:Fin p.m) → ((_: S i) → G) → G := fun i x ↦ x ⟨(i,j), by simp [S]⟩    convert iIndepFun.finsets_comp S _ hX'_indep (by fun_prop) φ (by fun_prop) with i ω    rw [Finset.pairwiseDisjoint_iff]; rintro _ _ _ _ ⟨⟨_, _⟩, hij⟩    simp [S] at hij; omega  have hindep_yj (j: Fin p.m) : iIndepFun (fun i ↦ Y (i, j)) := indep_yj h_mes h_indep j  have := mutual_information_le (by fun_prop) (hindep_yj zero) ?_ (by fun_prop) hX'_indep ?_  · have k_eq : k = D[fun i ω ↦ Y (i, zero) ω ; fun x ↦ hΩ'] := by      apply multiDist_copy; intro i; exact (hident i zero).symm    rw [←k_eq,condMutualInfo_comm (by fun_prop) (by fun_prop)] at this    refine .trans ?_ this    convert! condMutual_comp_comp_le _ _ _ _ (fun (x: Fin p.m → G) ↦ ∑ i, i.val • x i)      (fun (x: Fin p.m → G) ↦ -∑ i, i.val • x i) _ with ω <;> try infer_instance    all_goals try fun_prop    · ext ω      simp only [natCast_zsmul, Finset.sum_apply, Pi.smul_apply, Function.comp_apply,        Finset.smul_sum, X']      congr! 1 with j      symm; convert Equiv.sum_comp (Equiv.subRight j) _ with i _      simp    · ext ω      simp only [Finset.sum_apply, Pi.smul_apply, ← Finset.sum_neg_distrib, Function.comp_apply,        Finset.smul_sum, X']      nth_rewrite 2 [Finset.sum_comm]      congr! 1 with j _      symm; convert Equiv.sum_comp (Equiv.subRight j) _ with i _      simp only [← natCast_zsmul, Equiv.subRight_apply]      rw [←neg_zsmul]      apply torsion_mul_eq (p := p)      simp only [Lean.Omega.Fin.ofNat_val_sub, Fin.is_le', Nat.cast_sub, Int.emod_def,        Int.modEq_iff_add_fac]      use ((↑p.m - ↑↑j + ↑↑i) / ↑p.m) - 1      ring    simp only [Finset.sum_apply, X']    apply Finset.sum_congr rfl; intro i _    convert Equiv.sum_comp (Equiv.subRight i) _ with j _    simp  · apply multiTauMinimizes_of_ident p _ _ _ h_min    intro i; exact (hident i zero).symm  intro j; use Equiv.refl _  apply IdentDistrib.iprodMk _ hΩ'_prob hΩ'_prob (hindep_j j) (hindep_yj zero)  intro i  exact (hident i (j-i)).trans (hident i zero).symm