mutual_of_W_Z_two_le

lemma mutual_of_W_Z_two_le : I[W : Z2] ≤ 2 * (p.m-1) * k := by  rw [mutualInfo_eq_entropy_sub_condEntropy (by fun_prop) (by fun_prop)]  have hm := p.hm  let zero : Fin p.m := ⟨0, by linarith [hm]⟩  have h1 := entropy_of_W_le _ h_mes h_indep hident  have h2 : H[W | Z2] ≥ H[Q zero] := calc    _ ≥ H[W | fun ω (i : Finset.univ.erase zero) ↦ Q (i.val) ω] := by      let f : (Finset.univ.erase zero → G) → G := fun x ↦ ∑ j, j.val.val • (x j)      convert condEntropy_comp_ge _ _ _ f <;> try infer_instance      · ext ω; simp only [Z2_eq, f]        simp only [Finset.sum_apply, Pi.smul_apply, Function.comp_apply]        convert Finset.sum_subtype _ _ _        simp [zero]      all_goals fun_prop    _ = H[Q zero | fun ω (i : Finset.univ.erase zero) ↦ Q (i.val) ω] := by      let f : (Finset.univ.erase zero → G) → G → G := fun x y ↦ y + ∑ j, x j      convert condEntropy_of_injective _ _ _ f _ with ω <;> try infer_instance      all_goals try fun_prop      · simp only [Finset.sum_apply, Finset.univ_eq_attach, f]        rw [Finset.sum_comm]        symm        convert Finset.add_sum_erase (a := zero) _ _ _        · rfl        · convert Finset.sum_attach _ _; rfl        simp      intro _ _ _ h; simpa [f] using h    _ = _ := by      apply IndepFun.condEntropy_eq_entropy _ (by fun_prop) (by fun_prop)      let T : Finset (Fin p.m × Fin p.m) := {q|q.2=zero}      let T' : Finset (Fin p.m × Fin p.m) := Tᶜ      let φ : (T → G) → G := fun f ↦ ∑ i, f ⟨(i,zero), by simp [T]⟩      let φ' (f : T' → G) (j : Finset.univ.erase zero) : G :=        ∑ i, f ⟨(i, j), by obtain ⟨j, hj⟩ := j;  simpa [T, T'] using hj⟩      convert iIndepFun.finsets_comp' _ h_indep (by fun_prop) (show Measurable φ by fun_prop)        (show Measurable φ' by fun_prop) with ω ω <;> try simp [φ,φ']      simp [T', disjoint_compl_right]  have h3 := Q_ent _ h_mes h_indep hident zero  linarith