proposition: Lemma K949_lemma df n0 : K949 n0 df = marginal_post_prob_den y * post_prob_uniform_cst [set cw in C] y.
proof: Proof. rewrite /K949 /marginal_post_prob_den /post_prob_uniform_cst -invRM; last 2 first. - by rewrite FDist.f1; apply: lt0r_neq0. - by rewrite -not_receivable_prop_uniform receivableP. congr (/ _). transitivity (\sum_(t in 'rV['F_2]_n) if t \in kernel H then W ``(y | t) else 0); last first. rewrite big_distrl /=. apply eq_bigr => /= t Ht. case: ifP => HtH. rewrite fdist_post_probE fdist_uniform_supp_in ?inE //. have HH : (#|[set cw in kernel H]|%:R)%mcR != 0. have->: 0 = GRing.natmul 1 0 by []. apply/eqP => /mulrIn /eqP. rewrite -unitfE unitr1 => /(_ erefl); apply/negP. rewrite cards_eq0. by apply/set0Pn; exists t; rewrite inE. rewrite -(mulrC (W ``(y | t))) -[X in X = _]mulr1. rewrite !coqRE -!mulrA. congr (_ * _). rewrite fdist_uniform_supp_restrict /= fdist_uniform_supp_distrr /=; last first. rewrite invrM; last 2 first. exact/invr_neq0. rewrite (eq_bigl (fun x => x \in [set cw in C])); last by move=> i; rewrite inE. by rewrite unitfE -not_receivable_prop_uniform receivableP. rewrite invrK [X in _ = _ * X]mulrAC mulVr ?mul1r ?coqRE ?mulVr //. by rewrite unitfE -not_receivable_prop_uniform receivableP. rewrite fdist_post_probE fdist_uniform_supp_notin; last by rewrite inE; exact/negbT. by rewrite !coqRE !mul0r. rewrite -big_mkcond /=. rewrite /alpha. transitivity (W Zp0 (y ``_ n0) * (\sum_(ta = df `[ n0 := Zp0 ] [~ setT :\ n0]) \prod_(m1 in 'F n0) (W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0) * (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R))) + W Zp1 (y ``_ n0) * (\sum_(ta = df `[ n0 := Zp1 ] [~ setT :\ n0]) \prod_(m1 in 'F n0) (W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0) * (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R)))). congr (_ * _ + _ * _). rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y (fun m x y => W ``(x | y))) // => m1 m0 t Hm1 tdf. by rewrite checksubsum_dprojs_V. rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y (fun m x y => W ``(x | y))) // => m1 m0 t Hm1 tdf. by rewrite checksubsum_dprojs_V. transitivity (\sum_(ta : 'rV_n) W (ta ``_ n0) (y ``_ n0) * \prod_(m1 in 'F n0) (W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0) * (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R))). rewrite big_distrr big_distrr /=. rewrite [in X in _ = X] (bigID [pred x : 'rV_n | x ``_ n0 == Zp0]) /=. congr (_ + _). + rewrite (eq_bigl [pred x : 'rV_n | x ``_ n0 == Zp0]) /=. by apply eq_bigr => ta /eqP ->. move=> ta /=. by rewrite -freeon_all mxE eqxx. + rewrite (eq_bigl [pred x : 'rV_n | x ``_ n0 != Zp0]) /=. apply eq_bigr => ta. by rewrite -F2_eq1 => /eqP ->. move=> v /=; by rewrite -freeon_all mxE eqxx F2_eq1. transitivity (\sum_(ta : 'rV_n) W (ta ``_ n0) (y ``_ n0) * (\prod_(m1 in 'F n0) W ``(y \# 'V(m1, n0) :\ n0 | ta \# 'V(m1, n0) :\ n0)) * (\prod_(m1 in 'F n0) (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R))). apply eq_bigr => ta _. rewrite -mulRA. congr (_ * _). by apply big_split. transitivity (\sum_(ta : 'rV_n) (\prod_(k < n) W (ta ``_ k) (y ``_ k)) * (\prod_(m1 in 'F n0) \prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R)). apply eq_bigr => t /= _. congr (_ * _). rewrite -DMC_sub_vec_Fnext // (bigID (pred1 n0)) /= (big_pred1 n0) //. congr (_ * _). rewrite DMC_sub_vecE. apply eq_bigl => ? /=. by rewrite in_setC in_set1. transitivity (\sum_(ta : 'rV_n) (\prod_(k < n) (W ta ``_ k) y ``_ k) * (\prod_(m2 < m) (\delta ('V m2) ta)%:R)). apply eq_bigr => t /= _. congr (_ * _). by rewrite -(rprod_Fgraph_part_fnode (Tanner.connected tanner) (Tanner.acyclic tanner) (fun m0 => (\delta ('V m0) t)%:R)). rewrite [in X in X = _](bigID [pred x | x \in kernel H]) /=. rewrite addRC (eq_bigr (fun=> 0)); last first. by move=> ta /negbTE Hta; rewrite checksubsum_in_kernel Hta mulR0. rewrite big_const iter_addR mulR0 add0R. apply eq_bigr => ta Ha. by rewrite checksubsum_in_kernel Ha mulR1 -DMCE. 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