proposition: Lemma TS_sup : #| `TS P n epsilon |%:R <= exp2 (n%:R * (`H P + epsilon)).
proof: Proof. suff Htmp : #| `TS P n epsilon |%:R * exp2 (- n%:R * (`H P + epsilon)) <= 1. by rewrite -(mulR1 (exp2 _)) mulRC -leR_pdivr_mulr // /Rdiv -exp2_Ropp -mulNR. rewrite (_ : 1 = 1%mcR)// -(FDist.f1 (P `^ n)). rewrite (_ : _ * _ = \sum_(x in `TS P n epsilon) (exp2 (- n%:R * (`H P + epsilon)))); last first. by rewrite big_const iter_addR. by apply/leR_sumRl => //= i; rewrite inE; case/andP => /RleP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep