proposition: Lemma DMC_sub_vec_Vgraph t m0 n0 : n0 \in 'V m0 -> W ``(tb \# ('V(m0, n0) :\ n0) | t \# ('V(m0, n0) :\ n0)) = (\prod_(n1 in 'V m0 :\ n0) (W (t ``_ n1) (tb ``_ n1) * \prod_(m1 in 'F n1 :\ m0) W ``(tb \# 'V(m1, n1) :\ n1 | t \# 'V(m1, n1) :\ n1)))%R.
proof: Proof. move=> m0n0. rewrite DMCE rprod_sub_vec. rewrite -{1}(cover_Vgraph_part_Vgraph (Tanner.acyclic tanner) m0n0). rewrite big_trivIset /=; last by apply trivIset_Vgraph_part_Vgraph => //; by apply (Tanner.acyclic tanner). rewrite /Vgraph_part_Vgraph. rewrite big_imset /=; last first. move=> n1 n2 Hn1 Hn2 /=. apply: Vgraph_injective3 Hn1 Hn2 => //; by apply: Tanner.acyclic tanner. apply eq_bigr => n1 Hn1. set body := BIG_F. transitivity (\prod_(i in [predU (pred1 n1) & [pred x | x \in \bigcup_(m1 in 'F n1 :\ m0) ('V(m1, n1) :\ n1)]]) (body i))%R. apply eq_bigl => x /=. by rewrite !inE. rewrite {}/body bigU /=; last first. apply bigcup_disjoint => m1 Hm1. rewrite (@eq_disjoint1 _ n1) //. by rewrite !inE eqxx /=. rewrite (@big_bigcup_partition _ _ _ _ _ (fun x => ('V(x, n1) :\ n1)) (fun x => (W (t ``_ x)) (tb ``_ x)) ('F n1 :\ m0)) /=; last first. move=> i j ij. rewrite -setI_eq0. apply/set0Pn; case=> n2. rewrite inE. case/andP. rewrite 2!inE. case/andP => n2n1 Hn2. rewrite 2!inE n2n1 /=. apply/negP. move: Hn2. apply disjoint_Vgraph => //; by apply: Tanner.acyclic tanner. rewrite (big_pred1 n1); last first. move=> x /=. by rewrite !inE. congr (_ * _)%R. apply eq_bigr => m1 Hm1. 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