proposition: Lemma recursive_computation_helper m0 n0 d : n0 \in 'V m0 -> forall x : 'rV_n, freeon ('V m0 :\ n0) d x -> let A := \sum_(i | freeon ('V( m0, n0) :\ n0) d i && (dproj d ('V m0 :\ n0) i == x)) \prod_(n1 < n | n1 \in 'V m0 :\ n0) ((W i ``_ n1) y ``_ n1 * (\prod_(m1 < m | m1 \in 'F n1 :\ m0) (W ``((y \# 'V( m1, n1) :\ n1) | (i \# 'V( m1, n1) :\ n1)) * (\prod_(m2 < m | m2 \in 'F( m1, n1)) (\delta ('V m2) i)%:R)))) in A = \prod_(n1 < n | n1 \in 'V m0 :\ n0) beta n1 m0 x.
proof: Proof. move=> m0n0 x Hx A; apply/esym. transitivity (\prod_(n1 in 'V m0 :\ n0) ((W x ``_ n1) y ``_ n1 * (\sum_(z | (dprojs_V H x n1 z \in pfamily x ('F n1 :\ m0) (fun m1 => freeon ('V( m1, n1) :\ n1) x)) && (comb_V H x n1 (dprojs_V H x n1 z) == z)) \prod_(m1 in 'F n1 :\ m0) (W ``((y \# 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 z) m1 \# 'V( m1, n1) :\ n1)) * (\prod_(m2 in 'F( m1, n1)) (\delta ('V m2) ((dprojs_V H x n1 z) m1))%:R))))). apply eq_bigr => n1 Hn1. congr (_ * _)%R. rewrite {1}(big_distr_big_dep x) /=. rewrite (reindex_onto (dprojs_V H x n1) (comb_V H x n1)) //. rewrite /= => g Hg. exact: (@dprojs_comb_V _ _ _ (Tanner.acyclic tanner) _ _ (fun x => 'F x :\ m0) _ Hg). transitivity (\prod_(n1 in 'V m0 :\ n0) \sum_(z | (dprojs_V H x n1 z \in pfamily x ('F n1 :\ m0) (fun m1 => freeon ('V( m1, n1) :\ n1) x)) && (comb_V H x n1 (dprojs_V H x n1 z) == z)) (W z ``_ n1) y ``_ n1 * (\prod_(m1 in 'F n1 :\ m0) (W ``((y \# 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 z) m1 \# 'V( m1, n1) :\ n1)) * (\prod_(m2 in 'F( m1, n1)) (\delta ('V m2) ((dprojs_V H x n1 z) m1))%:R)))). apply/esym. apply eq_bigr => /= n1 Hn1. rewrite [RHS]big_distrr /=. apply eq_bigr => /= t' Ht'. congr (W _ _ * _)%R. case/andP : Ht' => X1 X2. move/eqP : X2 => <-. rewrite comb_dprojs_V_not_in_partition // => m1; by rewrite !inE eqxx. transitivity (\sum_(t | (dprojs_V2 H x m0 n0 t \in pfamily x ('V m0 :\ n0) (fun n1 => [pred t0 | (dprojs_V H x n1 t0 \in pfamily x ('F n1 :\ m0) (fun m1 => freeon ('V( m1, n1) :\ n1) x)) && (comb_V H x n1 (dprojs_V H x n1 t0) == t0)])) && (comb_V2 H x m0 n0 (dprojs_V2 H x m0 n0 t) == t)) \prod_(n1 < n | n1 \in 'V m0 :\ n0) (W (((dprojs_V2 H x m0 n0 t) n1) ``_ n1) y ``_ n1 * (\prod_(m1 < m | m1 \in 'F n1 :\ m0) (W ``((y \# 'V( m1, n1) :\ n1) | ((dprojs_V H x n1 ((dprojs_V2 H x m0 n0 t) n1)) m1 \# 'V( m1, n1) :\ n1)) * (\prod_(m2 < m | m2 \in 'F( m1, n1)) (\delta ('V m2) ((dprojs_V H x n1 ((dprojs_V2 H x m0 n0 t) n1)) m1))%:R))))). apply/esym. by rewrite [in RHS](rprod_rsum_commute (Tanner.acyclic tanner)). apply/eq_big. move=> t' /=. move Hlhs : (_ && _) => [|]. apply/esym. case/andP : Hlhs => Hlhs1 Hlhs2. apply/andP; split. apply: (@comb_V2_freeon _ _ _ (Tanner.acyclic tanner) x _ _ m0n0) => //. by rewrite freeon_sym. by apply/eqP. apply (dproj_prop (Tanner.acyclic tanner) (simple_tanner_rel _)) => //; by apply/eqP. apply/esym/negbTE. move/negbT : Hlhs; apply: contra => /andP [] Hlhs1 Hlhs1'. apply/andP; split. apply: (@dprojs_V2_pfamily _ _ _ (Tanner.acyclic tanner) (Tanner.connected tanner) _ _ _ m0n0 _ d) => //. by apply/eqP. apply: (@comb_dprojs_V2 _ _ _ (Tanner.acyclic tanner) _ _ _ m0n0 d) =>//; by apply/eqP. move=> t Ht. apply eq_bigr => n1 Hn1. congr (W _ _ * _). rewrite (dprojs_V2_in (Tanner.acyclic tanner) (simple_tanner_rel _)) //. by case/andP : Ht => _ /eqP. apply eq_bigr => m1 Hm1. rewrite /dprojs_V sub_vec_dprojs // sub_vec_dprojs_V2 //. congr (_ * _). apply eq_bigr => m2 Hm2. congr (_%:R). case/andP : Ht. by move/checksubsum_dprojs_V2 => ->. 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