proposition: Lemma filter_out_set0 m0 t (g : 'I_m -> 'rV['F_2]_n -> R) (s : {set 'I_n}) : \prod_(A in [set \bigcup_(m1 in 'F n1 :\ m0) 'F( m1, n1) | n1 in s]) \prod_(x in A) (g x t) = \prod_(A in [set \bigcup_(m1 in 'F n1 :\ m0) 'F( m1, n1) | n1 in [set n1 in s | 'F n1 :\ m0 != set0]]) \prod_(x in A) (g x t).
proof: Proof. rewrite (bigID [pred x | x == set0]) /= big1 ?mul1R; last first. move=> ms. case/andP => _ /eqP ->; by rewrite big_set0. apply eq_bigl => /= ms. apply/esym/imsetP. case: ifPn. case/andP => /imsetP[n1 Hn1 Hms Hms']. exists n1 => //. rewrite inE Hn1 /=. apply: contra Hms'. rewrite Hms => /eqP ->. by rewrite big_set0. rewrite negb_and negbK. case/orP => [|/eqP ->]. move/imsetP => abs abs'; apply abs => {abs}. case: abs' => n1; rewrite inE =>/andP[abs'1 abs'2] abs''. by exists n1. case=> n1. rewrite inE. case/andP => H1 H2 /esym/eqP/bigcup_succ_set0. by apply/negP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext fdist channel pproba f2 linearcode subgraph_partition tanner tanner_partition hamming binary_symmetric_channel decoding channel_code summary checksum summary_tanner