proposition: Lemma MD_implies_ML : Prob.p p < 1/2 :> R-> MD_decoding [set cw in C] f -> (forall y, f y != None) -> ML_decoding W C f P.
proof: Proof. move=> p05 MD f_total y. have codebook_not_empty : {c | c \in [set cw in C] }. move: (mem0v C); set x := (X in X \in C) => _. exists x; by rewrite inE mem0v. have {}MD : MD_decoding_alt f codebook_not_empty. apply MD_decoding_equiv => //. apply/subsetP => y' Hy'. move/subsetP : f_img => /(_ _ Hy'); by rewrite inE. move Hoc : (f y) => oc. case: oc Hoc => [c|] Hc; last first. by move: (f_total y); rewrite Hc. exists c; split; first by reflexivity. pose dH_y c := dH y c. pose g : nat -> R := fun d : nat => ((1 - Prob.p p) ^ (n - d) * (Prob.p p) ^ d)%R. have -> : W ``(y | c) = g (dH_y c). move: (DMC_BSC_prop p enc (discard c) y). rewrite [X in BSC.c X _](_ : _ = card_F2) //. rewrite -/W compatible //. move/subsetP : f_img; apply. by rewrite inE; apply/existsP; exists (receivable_rV y); apply/eqP. transitivity (\big[Order.max/0]_(c in C) (g (dH_y c))); last first. apply eq_bigr => /= c' Hc'. move: (DMC_BSC_prop p enc (discard c') y). rewrite [X in BSC.c X _](_ : _ = card_F2) //. by rewrite -/W compatible. rewrite (@bigmaxR_bigmin_vec_helper _ _ _ _ _ _ _ _ _ _ codebook_not_empty) //. - by rewrite bigmaxRE; apply eq_bigl => /= i; rewrite inE. - by apply bsc_prob_prop. - move=> r; rewrite /g !coqRE. apply/RleP/mulr_ge0; apply/exprn_ge0; last exact/prob_ge0. exact/onem_ge0/prob_le1. - rewrite inE; move/subsetP: f_img; apply. rewrite inE; apply/existsP; by exists (receivable_rV y); apply/eqP. - by move=> ? _; rewrite /dH_y max_dH. - by rewrite /dH_y MD. 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