proposition: Lemma step1 : (1 - esrc(P , sc)) = \sum_(x in no_failure) P `^ k.+1 x.
proof: Proof. rewrite /SrcErrRate /no_failure /Pr. set a := \sum_(_ | _) _. set b := \sum_(_ | _) _. suff : 1 = a + b by move=> ->; field. rewrite /a {a}. have -> : b = \sum_(i in [set i | dec sc (enc sc i) == i]) P `^ k.+1 i. apply eq_big => // i /=; by rewrite inE. rewrite (_ : 1 = 1%mcR)//. rewrite -(FDist.f1 (P `^ k.+1)). rewrite (bigID [pred a | a \in [set i0 | dec sc (enc sc i0) == i0]]) /= addRC. by congr (_ + _); apply eq_bigl => t /=; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep typ_seq source_code