fact: Definition MAP_decoding := forall y : P.-receivable W, exists m, dec y = Some m /\ P `^^ W (m | y) = \rmax_(m in C) (P `^^ W (m | y)).
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg perm) mathcomp(zmodp matrix vector order) mathcomp(lra mathcomp_extra Rstruct reals) Reals ssrR realType_ext Reals_ext ssr_ext ssralg_ext f2 fdist proba channel_code channel binary_symmetric_channel hamming pproba