proposition: Lemma e_hamming m0 : e(W, hamming_channel_code) m0 = \sum_(e0 in [set e0 : 'rV['F_2]_n | (2 <= wH e0)%nat]) (1 - Prob.p p) ^ (n - wH e0) * (Prob.p p) ^ wH e0.
proof: Proof. rewrite /ErrRateCond /Pr /=. transitivity ( \sum_(a | a \in preimC (dec hamming_channel_code) m0) let d := dH ((enc hamming_channel_code) m0) a in (1 - Prob.p p) ^ (n - d) * (Prob.p p) ^ d). apply eq_bigr => t Ht. rewrite dH_sym. rewrite -(DMC_BSC_prop p (enc hamming_channel_code) m0 t). by rewrite [X in BSC.c X _](_ : _ = card_F2). transitivity ( \sum_(a|a \in [set tb | if dec hamming_channel_code tb is Some m1 then m1 != m0 else true]) (let d := dH ((enc hamming_channel_code) m0) a in (1 - Prob.p p) ^ (n - d) * (Prob.p p) ^ d)). apply eq_bigl => t /=. rewrite !inE. case_eq (dec hamming_channel_code t) => [m1 Hm1|]; last first. by move=> ->. by case: ((dec hamming_channel_code) t). set y0 := (enc hamming_channel_code) m0. Local Close Scope R_scope. set f := fun y => (y0 + y). Local Open Scope R_scope. transitivity ( \sum_(y | f y \in [set e1 | (1 < wH e1)%nat]) (1 - Prob.p p) ^ (n - wH (f y)) * (Prob.p p) ^ wH (f y)). apply eq_big. move=> y. simpl in y, f, m0. rewrite !inE. have H : y0 \in lcode m'. move/subsetP : (Encoder.enc_img (Lcode.enc (lcode m'))); apply. apply/imsetP; by exists m0. move/(@repair_failure _ y y0) : H => /= H. rewrite /f /= ffunE. move: H. move H : ((@hamming_repair m') y) => [h|//]. rewrite /= in h H * => <-. rewrite /y0 /=. apply/idP/idP. apply: contra => /eqP ->. rewrite ffunE /Hamming'.discard. rewrite -mulmxA. move: (Hamming'.mx_discard_GEN m'). move/(congr1 trmx). rewrite trmx_mul trmxK => ->. by rewrite trmx1 mulmx1. rewrite ffunE; apply: contra => /= /eqP <-. have : h \in Hamming.code m. rewrite mem_kernel_syndrome0. move: H. rewrite /hamming_repair ffunE => -[<-]. by rewrite syndromeD syndrome_hamming_err F2_addmx. move/(@Lcode.compatible _ _ _ _ (lcode m') h). by rewrite /= ffunE => ->. move=> /= y; rewrite inE => Hy. by rewrite /dH !F2_mx_opp. apply/esym/reindex. exists f; move=> /= x _; by rewrite /f addrA F2_addmx add0r. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel Reals Reals_ext