proposition: Lemma alpha_def_sub m0 n1 n0 (x y : 'F_2) (l : seq 'I_n) d : n1 \notin l -> uniq l -> n0 != n1 -> n0 \notin l -> n1 \in 'V m0 :\ n0 -> {subset l <= 'V m0 :\ n0} -> beta' n1 m0 (d`[n1 := x]) * foldr (fun n2 (F : 'rV_n -> R) t => \sum_(x in 'F_2) F (t`[n2 := x])) (fun t => INR (t ``_ n0 != \delta [set x in l] t) * (\prod_(n3 in [set x in l]) beta' n3 m0 t)) l (d`[n0 := x + y])%R = foldr (fun n2 (F : 'rV_n -> R) t => \sum_(x in 'F_2) F (t`[n2 := x])) (fun t => INR (t ``_ n0 != \delta [set x in n1 :: l] t) * (\prod_(n3 in [set x in n1 :: l]) beta' n3 m0 t)) l ((d`[n0 := y])`[n1 := x]).
proof: Proof. move=> n1_l Hun n0_n1 n0_l Hn1 Hsub. have d' := d. have n1_Vm0 : n1 \in 'V m0 by move: Hn1; rewrite in_setD1; case/andP. rewrite {1}/beta'. rewrite (@beta_inva _ _ _ _ _ _ _ _ _ (d'`[n1 := x])) => //; last first. by rewrite !mxE eqxx. rewrite rmul_foldr_rsum. pose l' := l. rewrite -{3 6}/l'. have n1_l' := n1_l. have n0_l' := n0_l. rewrite -/l' in n1_l' n0_l'. elim: l' => [|hd tl IH] /= in d n1_l' n0_l' *. rewrite [X in _ = _ * X](bigD1 n1) /=; last by rewrite !inE eqxx. rewrite (@beta_inva _ _ _ _ W _ _ m0 _ ((d`[n0 := y])`[n1 := x])) //; last first. by rewrite !mxE eqxx. rewrite mulRA mulRA [X in _ = X * _]mulRC. congr (_ * _). congr (_ * INR _). rewrite row_setC; last by rewrite eq_sym. by rewrite !mxE eqxx (@checksubsum_add n1). apply congr_big => // i. rewrite !inE. move: n1_l. case/boolP : (i == n1) => [/eqP -> |] /=. by move/negbTE. by rewrite andbT. rewrite inE => i_l. apply beta_inva. by move: (Hsub _ i_l); rewrite in_setD1; case/andP. rewrite !mxE. move: i_l. case/boolP : (i == n0) => [/eqP -> |]. by rewrite (negbTE n0_l). case/boolP : (i == n1) => [/eqP -> |//]. by rewrite (negbTE n1_l). apply eq_bigr => i _. rewrite row_setC; last first. by move: n0_l'; rewrite in_cons eq_sym; case/norP. rewrite IH; last 2 first. by rewrite in_cons in n1_l'; case/norP: n1_l'. by rewrite in_cons in n0_l'; case/norP: n0_l'. congr (foldr _ _ _ _). rewrite (row_setC y i); last first. by rewrite in_cons in n0_l'; case/norP: n0_l'. rewrite (row_setC x i) //. by rewrite in_cons in n1_l'; case/norP: n1_l'. 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