proposition: Lemma sum_messages_types f : \sum_(P : P_ n ( A )) (\sum_(m |m \in enc_pre_img c P) f m) = \sum_ (m : M) (f m).
proof: Proof. transitivity (\sum_ (m in [set: M]) (f m)); last by apply eq_bigl => b; rewrite in_set. rewrite -(cover_enc_pre_img c) /enc_pre_img_partition sum_messages_types'. symmetry. by apply big_trivIset, trivIset_enc_pre_img. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq