proposition: Lemma MAP_implies_ML : MAP_decoding W C dec P -> ML_decoding W C dec P.
proof: Proof. move=> HMAP. rewrite /ML_decoding => /= tb. have Hunpos : (#| [set cw in C] |%:R)^-1 > 0 :> R. by rewrite invr_gt0 ltr0n; exact/vspace_not_empty. move: (HMAP tb) => [m [tbm]]. rewrite /fdist_post_prob. unlock. simpl. set tmp := \rmax_(_ <- _ | _) _. rewrite /tmp. under [in X in _ = X -> _]eq_bigr do rewrite ffunE. move=> H. evar (h : 'rV[A]_n -> R); rewrite (eq_bigr h) in H; last first. by move=> v vC; rewrite /h; reflexivity. rewrite -bigmaxR_distrl in H; last first. by apply/RleP; rewrite invr_ge0; exact/fdist_post_prob_den_ge0. rewrite {2 3}/P in H. set r := index_enum _ in H. move: H. under [in X in _ = X -> _]eq_bigr. move=> i iC. rewrite fdist_uniform_supp_in; last by rewrite inE. over. move=> H. rewrite -bigmaxR_distrr in H; last exact/RleP/ltW/Hunpos. exists m; split; first exact tbm. rewrite ffunE in H. set x := (X in _ * _ / X) in H. have x0 : x^-1 <> 0 by apply/eqP/invr_neq0; rewrite -receivable_propE receivableP. move/(eqR_mul2r x0) in H. rewrite /= fdist_uniform_supp_in ?inE // in H; last first. move/subsetP : dec_img; apply. by rewrite inE; apply/existsP; exists (receivable_rV tb); apply/eqP. move/lt0r_neq0/eqP: Hunpos. move/eqR_mul2l : H; move/[apply] ->. by rewrite bigmaxRE. Qed.
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