proposition: Lemma typ_seq_definition_equiv x : x \in `TS P n epsilon -> exp2 (- n%:R * (`H P + epsilon)) <= P `^ n x <= exp2 (- n%:R * (`H P - epsilon)).
proof: Proof. by rewrite inE /typ_seq => /andP[? ?]; split; apply/RleP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep