proposition: Lemma DMC_sub_vec_Fnext t n0 : W ``(tb \# [set~ n0] | t \# [set~ n0]) = (\prod_(i in 'F n0) W ``(tb \# 'V(i, n0) :\ n0 | t \# 'V(i, n0) :\ n0))%R.
proof: Proof. rewrite DMCE. transitivity (\prod_(i in setT :\ n0) W (t ``_ i) (tb ``_ i))%R. transitivity (\prod_(i in [set~ n0]) W (t ``_ i) (tb ``_ i))%R; last first. apply eq_bigl => x /=; by rewrite !inE andbT. by rewrite -rprod_sub_vec. rewrite -{1}(cover_Vgraph_part_vnode (Tanner.connected tanner) n0). rewrite big_trivIset /=; last by apply trivIset_Vgraph_part_vnode, (Tanner.acyclic tanner). rewrite /Vgraph_part_vnode. transitivity (\prod_(A in [set 'V(m0, n0) :\ n0 | m0 in 'F n0 & ('V(m0, n0) :\ n0 != set0)]) \prod_(x in A) W (t ``_ x) (tb ``_ x))%R. rewrite (bigID [pred x | x == set0 ]) /=. rewrite big1; last first. move=> i /andP [] Hi1 /eqP ->. rewrite big1 // => j. by rewrite inE. rewrite mul1R. apply eq_bigl => i. move Hrhs : (_ \in _) => [|] /=. case/imsetP : Hrhs => /= m1 Hm1 Hi. move Hrhs' : (_ != _) => [|] /=. apply/esym/imsetP; exists m1 => //. by rewrite inE Hm1 -Hi. apply/esym/imsetP => abs. case: abs => m2 Hm2 Hi2. rewrite inE in Hm2. case/andP : Hm2 => _. by rewrite -Hi2 Hrhs'. apply negbT in Hrhs. apply/esym/negbTE. apply: contra Hrhs. case/imsetP => m1. rewrite inE => /andP [] Hm1 Hm1' Hi. by apply/imsetP; exists m1. rewrite big_imset; last first. move=> /= m0 m1 Hm0 Hm1. rewrite inE /= in Hm0. rewrite inE /= in Hm1. case/andP : Hm0 Hm1 => ? ? /andP [] ? ?. apply Vgraph_injective => //; [ | | ]; try by rewrite -FnextE. by apply tanner. apply/esym. rewrite /= (bigID [pred x | 'V(x, n0) :\ n0 == set0 ]) /=. rewrite [X in (X * _)%R = _](_ : _ = R1); last first. rewrite big1 // => i /andP [] Hi1 /eqP Hi2. rewrite Hi2 DMCE. rewrite big1 //= => j. exfalso. rewrite cards0 /= in j. by case: j. rewrite mul1R. apply eq_big. move=> i /=; by rewrite !inE. move=> i /andP [] Hi1 Hi2. by rewrite DMCE -rprod_sub_vec. 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