proposition: Lemma JTS_sup : INR #| `JTS P W n epsilon| <= exp2 (INR n * (`H(P , W) + epsilon)).
proof: Proof. have : INR #|`JTS P W n epsilon| <= INR #|`TS ((P `X W)) n epsilon|. suff : `JTS P W n epsilon \subset `TS ((P `X W)) n epsilon. by move/subset_leq_card/leP/le_INR. apply/subsetP => tab. by rewrite /set_jtyp_seq inE /jtyp_seq inE => /and3P[]. move/leR_trans; apply; exact: (@TS_sup _ ((P `X W)) epsilon n). 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