proposition: Lemma wght_o_PI m m' P (h : encT A M n) : Wght.d P (o_PI m m' h) = Wght.d P h.
proof: Proof. rewrite 2!Wght.dE /Wght.f 2!ffunE (reindex_onto (tperm m m') (tperm m m')) /=; last first. move=> m0 _; by rewrite tpermK. apply eq_big => m0. - by rewrite tpermK eqxx. - by move=> _; rewrite /o_PI ffunE tpermK. 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