proposition: Lemma alpha_def m0 n0 (d : 'rV['F_2]_n) : n0 \in 'V m0 -> let d0 := d`[n0 := 0%R] in let d1 := d`[n0 := 1%R] in alpha [seq (beta' n1 m0 (d`[n1 := 0%R]), beta' n1 m0 (d`[n1 := 1%R])) | n1 in 'V m0 :\ n0] = (alpha' m0 n0 d0, alpha' m0 n0 d1).
proof: Proof. move=> Hn0. rewrite /alpha' !recursive_computation /alpha //; first last. by apply tanner. by apply tanner. rewrite (eq_bigr (fun t : 'rV_n => INR ((t ``_ n0) != \delta ('V m0 :\ n0) t) * (\prod_(n1 in 'V m0 :\ n0) beta' n1 m0 t))); last first. by move=> i _; rewrite (checksubsum_D1 _ Hn0) eq_sym. rewrite [in X in _ = (_, X)](eq_bigr (fun t : 'rV_n => INR ((t ``_ n0) != \delta ('V m0 :\ n0) t) * (\prod_(n1 in 'V m0 :\ n0) beta' n1 m0 t))); last first. move=> i _; by rewrite (checksubsum_D1 _ Hn0) eq_sym. rewrite !summary_powersetE !summary_foldE /summary_fold /=. rewrite /image_mem. set f := 'V m0 :\ n0. rewrite {2 3 5 6}(set_mem f). have {}Hn0 : n0 \notin enum f by rewrite mem_enum setD11. have Hl : {subset enum f <= f} by move=> ?; rewrite mem_enum. elim: (enum (mem _)) (enum_uniq (mem f)) => [|a l IH] /= Hun in Hn0 Hl *. rewrite /checksubsum. rewrite !big_pred0 /=; try by move=> i /=; rewrite !inE in_nil. by rewrite !mxE !eqxx /= !mulR1. case/andP: Hun => a_l Hun. rewrite in_cons in Hn0. case/norP: Hn0 => Hn0a Hn0. have Haf: a \in f by apply Hl; rewrite in_cons eqxx. have Hlf : {subset l <= f}. by move=> x Hx; apply Hl; rewrite in_cons Hx orbT. rewrite {}IH //. congr pair. rewrite (bigD1 (0%R : 'F_2)) => //=. rewrite (bigD1 (1%R : 'F_2)) => //=. rewrite big_pred0; last by case/F2P. congr (_ + _). rewrite -[in X in _ * foldr _ _ _ X = _](GRing.add0r 0)%R. by apply alpha_def_sub. rewrite -[in X in _ * foldr _ _ _ X = _](GRing.addr0 1%R). by rewrite alpha_def_sub // addR0. rewrite (bigD1 (0%R : 'F_2)) //=. rewrite (bigD1 (1%R : 'F_2)) //=. rewrite big_pred0; last by case/F2P. congr (_ + _). rewrite -[in X in _ * foldr _ _ _ X = _](GRing.add0r 1%R). by apply alpha_def_sub. rewrite -[in X in _ * foldr _ _ _ X = _](GRing.addrr_char2 (@char_Fp 2 erefl) 1%R). by rewrite alpha_def_sub // addR0. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo