proposition: Lemma good_code_sufficient_condition P W epsilon (phi : encT A M n -> decT B M n) : \sum_(f : encT A M n) (Wght.d P f * echa(W , mkCode f (phi f))) < epsilon -> exists f, echa(W , mkCode f (phi f)) < epsilon.
proof: Proof. move=> H. apply not_all_not_ex => abs. set x := \sum_(f <- _) _ in H. have : \sum_(f : encT A M n) Wght.d P f * epsilon <= x. rewrite /x; apply leR_sumRl => //= f _. - by apply leR_wpmul2l => //; exact/Rnot_lt_le/abs. - by apply mulR_ge0 => //; exact/RleP/echa_ge0. apply/Rlt_not_le/(@ltR_leR_trans epsilon) => //. rewrite -big_distrl /= (FDist.f1 (Wght.d P)) mul1R. by apply/RleP; rewrite Order.POrderTheory.lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code