proposition: Lemma recursive_computation m0 n0 d : n0 \in 'V m0 -> alpha m0 n0 d = \sum_(x = d [~'V m0 :\ n0]) (\delta ('V m0) x)%:R * \prod_(n1 in 'V m0 :\ n0) beta n1 m0 x.
proof: Proof. move=> m0n0. transitivity (\sum_(x = d [~'V(m0, n0) :\ n0]) (\delta ('V m0) x)%:R * W ``(y \# 'V(m0, n0) :\ n0 | x \# 'V(m0, n0) :\ n0) * \prod_(n1 in 'V m0 :\ n0) \prod_(m1 in 'F n1 :\ m0) \prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x)%:R). rewrite /alpha. apply eq_bigr => /= t Ht. rewrite -[in X in _ = X]mulRA -[in X in _ = X]mulRC -[in X in _ = X]mulRA. congr (_ * _)%R. rewrite (bigD1 m0) /=; last by apply Fgraph_m0. rewrite mulRC; congr (_ * _)%R. transitivity (\prod_(i in 'F(m0, n0) :\ m0) (\delta ('V i) t)%:R). apply eq_bigl => /= m1. by rewrite 2![in X in _ = X]inE andbC. rewrite -(cover_Fgraph_part_Fgraph (Tanner.acyclic tanner)) //. rewrite big_trivIset /=; last first. by apply (@trivIset_Fgraph_part_Fgraph _ _ _ (Tanner.acyclic tanner)). rewrite /Fgraph_part_Fgraph. rewrite (filter_out_set0 _ _ (fun x t => (\delta ('V x) t)%:R)). rewrite big_imset /=; last first. move=> n1 /= n2 Hn1 Hn2 n1xn2x. rewrite inE in Hn1; case/andP : Hn1 => Hn1 H1. rewrite inE in Hn2; case/andP : Hn2 => Hn2 H2. by apply: (another_Fgraph_injective (Tanner.acyclic tanner) Hn1 Hn2 H1). transitivity (\prod_(n1 < n | (n1 \in 'V m0 :\ n0) && ('F n1 :\ m0 != set0)) \prod_(m1 in 'F n1 :\ m0) \prod_(m2 in 'F(m1, n1)) (\delta ('V m2) t)%:R); last first. rewrite [in RHS](bigID [pred x | 'F x :\ m0 == set0]) /= [in RHS]big1 ?mul1R //. move=> n1 /andP [] H1 /eqP ->; by rewrite !big_set0. apply eq_big => /= n1; first by rewrite !inE. move=> Hn1. rewrite big_bigcup_partition //= => m1 m2 m1m2. apply: contraNT m1m2. rewrite -setI_eq0 => /set0Pn[m3]; rewrite inE => /andP[H1 H2]. by apply/eqP/(Fgraph_disjoint (Tanner.acyclic tanner) H1 H2). transitivity (\sum_(x = d [~'V(m0, n0) :\ n0]) (\delta ('V m0) x)%:R * \prod_(n1 in 'V m0 :\ n0) (W `(y ``_ n1 | x ``_ n1) * \prod_(m1 in 'F n1 :\ m0) ((W ``(y \# 'V(m1, n1) :\ n1 | x \# 'V(m1, n1) :\ n1)) * \prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x)%:R))). apply eq_bigr => /= t Ht. rewrite -mulRA; congr (_ * _). rewrite DMC_sub_vec_Vgraph // -big_split /=. apply eq_bigr => /= n1 _. by rewrite -mulRA big_split. transitivity (\sum_(x = d [~('V m0) :\ n0]) \sum_(x' = d [~'V(m0, n0) :\ n0] | [pred x' | dproj d ('V m0 :\ n0) x' == x]) (\delta ('V m0) x')%:R * \prod_(n1 in 'V m0 :\ n0) (W (x' ``_ n1) (y ``_ n1) * (\prod_(m1 in 'F n1 :\ m0) (W ``(y \# 'V(m1, n1) :\ n1 | x' \# 'V(m1, n1) :\ n1) * (\prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x')%:R))))). apply partition_big => /= t _. by apply freeon_dproj. apply eq_bigr => /= x Hx. transitivity (\sum_(x' = d [~'V(m0, n0) :\ n0] | [pred x' | dproj d ('V m0 :\ n0) x' == x]) (\delta ('V m0) x)%:R * (\prod_(n1 in 'V m0 :\ n0) (W (x' ``_ n1) y ``_ n1 * (\prod_(m1 in 'F n1 :\ m0) (W ``(y \# 'V(m1, n1) :\ n1 | x' \# 'V(m1, n1) :\ n1) * (\prod_(m2 in 'F(m1, n1)) (\delta ('V m2) x')%:R)))))). apply eq_bigr => /= x' Hx'. congr (_%:R * _)%R. case/andP : Hx' => H1 /eqP <-. by rewrite checksubsum_dprojD1 // (freeon_notin H1) // !inE eqxx. by rewrite -big_distrr /= recursive_computation_helper. 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