mutual_information_le_t_23

lemma mutual_information_le_t_23 : I[Z2 : 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, j) ω  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,j)}    let φ : (q:Fin p.m × Fin p.m) → ((_: S q) → G) → G := fun q x ↦ x ⟨(q.1-q.2,q.2), 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⟩, h1, rfl⟩ := hij    simpa using h1  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 := mutual_information_le (by fun_prop) (indep_yj h_mes h_indep 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] at this    apply LE.le.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']      nth_rewrite 1 [Finset.sum_comm]      apply Finset.sum_congr rfl; intro 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 1 [Finset.sum_comm]; nth_rewrite 2 [Finset.sum_comm]      apply Finset.sum_congr rfl; intro 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, neg_sub,        Int.modEq_iff_add_fac]      use ((↑p.m - ↑↑j + ↑↑i) / ↑p.m) - 1      ring    simp only [Finset.sum_apply, X']    nth_rewrite 1 [Finset.sum_comm]    nth_rewrite 2 [Finset.sum_comm]    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.subRight j  apply IdentDistrib.iprodMk _ hΩ'_prob hΩ'_prob (hindep_j j)  · exact iIndepFun.precomp (Equiv.injective (Equiv.subRight j)) (indep_yj h_mes h_indep zero)  intro i  exact (hident (i-j) j).trans (hident (i-j) zero).symm