proposition: Lemma hamming_01 m p : \sum_(u in 'rV['F_2]_m| u \in [set v |(1 >= wH v)%nat]) (1 - p) ^ (m - wH u) * p ^ wH u = (1 - p) ^ m + m%:R * p * (1 - p) ^ (m - 1).
proof: Proof. rewrite (bigID [pred i | wH i == O]) /=. rewrite (big_pred1 (GRing.zero _)) /=; last first. by move=> i /=; rewrite !inE -wH_eq0 andb_idl // => /eqP ->. rewrite wH0 pow_O subn0 mulR1; congr (_ + _). transitivity (\sum_(i | wH (i : 'rV['F_2]_m) == 1%nat) ((1 - p) ^ (m - 1) * p ^ 1)). transitivity (\sum_(i|(wH (i : 'rV['F_2]_m) == 1)%nat) ((1 - p) ^ (m - wH i) * p ^ wH i)). apply eq_bigl => /= i. rewrite !inE. case/boolP : (wH i == 1)%nat => [/eqP -> //|wH_1]. case wH_0 : (wH i) => [|n1]; first by rewrite eqxx. rewrite /= andbT. case n1_0 : n1 => [|? //]. by rewrite wH_0 n1_0 in wH_1. by apply/eq_bigr => /= v /eqP ->. by rewrite big_const iter_addR pow_1 /= -(mulRC p) mulRA -cardsE wH_m_card bin1. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext