mutual_information_le_t_12

lemma mutual_information_le_t_12 : I[Z1 : Z2 | W] ≤ p.m * (4*p.m+1) * p.η * k := by  have hm := p.hm  let zero : Fin p.m := ⟨0, by linarith [hm]⟩  have hindep_j (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_j zero) ?_ h_mes h_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] 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 [Finset.smul_sum]      · ext ω        simp only [natCast_zsmul, Finset.sum_apply, Pi.smul_apply, Function.comp_apply,          Finset.smul_sum]        rw [Finset.sum_comm]      simp    all_goals try fun_prop  · 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_j zero)  intro i  exact (hident i j).trans (hident i zero).symm