proposition: Lemma hamming_error_rate : Prob.p p < 1/2 -> echa(W, hamming_channel_code) = 1 - ((1 - Prob.p p) ^ n) - n%:R * (Prob.p p) * ((1 - Prob.p p) ^ (n - 1)).
proof: Proof. move=> p05. rewrite /CodeErrRate. eapply eq_trans. apply f_equal. apply eq_bigr => i _; exact: e_hamming. eapply eq_trans. apply f_equal. by rewrite big_const /= iter_addR. rewrite mulRA /=. set den := INR _. have -> : 1 / den * den = 1. by rewrite div1R mulVR // ?INR_eq0' card_mx /= mul1n expn_eq0 negb_and card_F2. rewrite mul1R. have toleft A B C D : A + C + D = B -> A = B - C - D by move => <-; ring. apply toleft. rewrite -addRA -(hamming_01 n (Prob.p p)) //. rewrite -big_union //. rewrite (_ : _ :|: _ = [set: 'rV_n]). by apply binomial_theorem. apply/setP => /= x; by rewrite !inE leqNgt orNb. rewrite -setI_eq0. apply/eqP/setP => /= x; by rewrite !inE leqNgt andNb. 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