proposition: Lemma TS_inf : aep_bound P epsilon <= n.+1%:R -> (1 - epsilon) * exp2 (n.+1%:R * (`H P - epsilon)) <= #| `TS P n.+1 epsilon |%:R.
proof: Proof. move=> k0_k. have H1 : (1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon) <= 1)%mcR. by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_1]. have H2 : (forall x, x \in `TS P n.+1 epsilon -> exp2 (- n.+1%:R * (`H P + epsilon)) <= P `^ n.+1 x <= exp2 (- n.+1%:R * (`H P - epsilon)))%mcR. by move=> x; rewrite inE /typ_seq => /andP[-> ->]. have /RltP H3 := exp2_gt0 (- n.+1%:R * (`H P + epsilon)). have /RltP H5 := exp2_gt0 (- n.+1%:R * (`H P - epsilon)). have := wolfowitz H3 H5 H1 H2. rewrite mulNR exp2_Ropp. rewrite RinvE ?gtR_eqF// invrK => /andP[] /RleP. by rewrite -!RmultE -RminusE -INRE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep