proposition: Lemma typical_sequence1_JTS x : prod_rV x \in `JTS -> exp2 (- INR n * (`H P + epsilon)) <= P `^ n x.1 <= exp2 (- INR n * (`H P - epsilon)).
proof: Proof. rewrite inE => /and3P[/andP[/RleP JTS11 /RleP JTS12] _ _]. by rewrite prod_rVK in JTS11, JTS12. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext logb ssralg_ext bigop_ext fdist proba entropy aep typ_seq channel