proposition: Lemma estimation_correctness (d : 'rV_n) n0 : let b := d ``_ n0 in let P := `U C_not_empty in P '_ n0 `^^ W (b | y) = marginal_post_prob_den y * post_prob_uniform_cst [set cw in C] y * W `(y ``_ n0 | b) * \prod_(m0 in 'F n0) alpha m0 n0 d.
proof: Proof. move=> b P. rewrite fdist_marginal_post_probE -2!mulRA; congr (_ * _). transitivity (post_prob_uniform_cst [set cw in C] y * (\sum_(x = d [~ setT :\ n0]) W ``(y | x) * \prod_(m0 < m) (\delta ('V m0) x)%:R))%R. rewrite [RHS]big_distrr [in RHS]/=. apply eq_big => t; first by rewrite -freeon_all. rewrite inE andTb => td_n0. rewrite post_prob_uniform_kernel -mulRA; congr (_ * _)%R. rewrite mulRC; congr (_ * _)%R. by rewrite checksubsum_in_kernel inE mem_kernel_syndrome0. congr (_ * _)%R. transitivity (W `(y ``_ n0 | b) * (\sum_(x = d [~ setT :\ n0]) W ``(y \# ~: [set n0] | x \# ~: [set n0]) * \prod_(m0 < m) (\delta ('V m0) x)%:R)). rewrite big_distrr /=; apply eq_bigr => t Ht. rewrite mulRA; congr (_ * _)%R. rewrite /b (freeon_notin Ht); last by rewrite !inE eqxx. rewrite DMCE (bigD1 n0) //=; congr (_ * _). rewrite DMCE rprod_sub_vec; apply eq_big => i //=. by rewrite in_setC in_set1. congr (_ * _). transitivity ( \sum_(x = d [~ setT :\ n0]) W ``(y \# ~: [set n0] | x \# ~: [set n0]) * \prod_(m0 in 'F n0) \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R). apply eq_bigr => /= t Ht. congr (_ * _)%R. by rewrite -(rprod_Fgraph_part_fnode (Tanner.connected tanner) (Tanner.acyclic tanner) (fun m0 => (\delta ('V m0) t)%:R)). transitivity ( \sum_(x = d [~ setT :\ n0]) \prod_(m0 in 'F n0) (W ``(y \# 'V(m0, n0) :\ n0 | x \# 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R)). apply: eq_bigr => /= t Ht. rewrite [in X in _ = X]big_split /=; congr (_ * _). by apply DMC_sub_vec_Fnext. rewrite (@rmul_rsum_commute0 _ _ _ (Tanner.connected tanner) (Tanner.acyclic tanner) d n0 _ y (fun m x y => W ``(x | y))) //. move=> /= m1 m0 t m1m0n0 tn0dn0; by rewrite checksubsum_dprojs_V. 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