proposition: Theorem get_esti_ok : get_esti_spec vb.
proof: Proof. rewrite /get_esti_spec /esti_spec. move=> n0. rewrite computed_tree_ok. rewrite estimation_alpha //; last 2 first. by rewrite card0 subn0 card_sum !card_ord. rewrite -computed_tree_ok labels_sumprod_down labels_sumprod_up. by apply build_tree_full. congr (_ :: _). rewrite -(row_setK (n0 : 'I_n) 0%R d). rewrite -(row_setK (n0 : 'I_n) 1%R d). rewrite !estimation_correctness; last 2 first. by apply tanner. by apply tanner. rewrite -!(K949_lemma vb tanner d n0). rewrite /K949 /normalize. rewrite beta_map big_beta_mul /=. rewrite /Rdiv. congr pair. rewrite mulRC /alpha' !mxE. by rewrite eqxx mulRA. rewrite mulRC /alpha' !mxE. by rewrite eqxx mulRA. 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