fact: Fixpoint sumproduct_loop (lmax : nat) (beta0 beta1 : 'M_(m, n)) : option ('rV['F_2]_n) := match lmax with | O => None | lmax'.+1 => let nalpha m0 n0 x := let K := / (alpha_fun m0 n0 (beta0, beta1) 0 + alpha_fun m0 n0 (beta0, beta1) 1) in (K * alpha_fun m0 n0 (beta0, beta1) x)%R in let alpha0 : 'M_(m, n) := \matrix_(m0 < m, n0 < n) nalpha m0 n0 0 in let alpha1 : 'M_(m, n) := \matrix_(m0 < m, n0 < n) nalpha m0 n0 1 in let nbeta m0 n0 x alpha := let K := / (beta_fun m0 n0 Zp0 alpha + beta_fun m0 n0 Zp1 alpha) in (K * beta_fun m0 n0 x alpha)%R in let beta0 := \matrix_(m0 < m, n0 < n) nbeta m0 n0 0 alpha0 in let beta1 := \matrix_(m0 < m, n0 < n) nbeta m0 n0 1 alpha1 in let estimation x n0 alpha := (W x (y !_ n0) * \prod_(m1 in 'F n0) alpha m1 n0)%R in let gamma0 n0 := estimation Zp0 n0 alpha0 in let gamma1 n0 := estimation Zp1 n0 alpha1 in let chat := \matrix_(i < 1, n0 < n) if (gamma0 n0 >= gamma1 n0)%mcR then 0 else 1 in if H *m chat^T == 0 then Some chat else sumproduct_loop lmax' beta0 beta1 end.
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