proposition: Lemma step2 : 1 - (esrc(P , sc)) = \sum_(x in 'rV[A]_k.+1 | x \in no_failure :&: ~: `TS P k.+1 delta) P `^ k.+1 x + \sum_(x in 'rV[A]_k.+1 | x \in no_failure :&: `TS P k.+1 delta) P `^ k.+1 x.
proof: Proof. rewrite step1 (bigID [pred x | x \in `TS P k.+1 delta]) /= addRC. f_equal. - apply eq_bigl => x; by rewrite in_setI in_setC. - apply eq_bigl => x; by rewrite in_setI. 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