proposition: Lemma typ_seq_definition_equiv2 x : x \in `TS P n.+1 epsilon -> `H P - epsilon <= - (1 / n.+1%:R) * log (P `^ n.+1 x) <= `H P + epsilon.
proof: Proof. rewrite inE /typ_seq. case/andP => H1 H2; split; apply/RleP; rewrite -(@ler_pM2r _ n.+1%:R) ?ltr0n//. - rewrite div1R -[in leRHS]RmultE mulRAC mulNR INRE mulVR; last first. by rewrite mulrn_eq0/= oner_eq0. rewrite mulN1R; apply/RleP. rewrite leR_oppr. apply/(@Exp_le_inv 2) => //. rewrite LogK //; last by apply/(ltR_leR_trans (exp2_gt0 _)); apply/RleP: H1. rewrite mulrC -mulNR -INRE. exact/RleP. - rewrite div1R -[in leLHS]RmultE mulRAC mulNR INRE mulVR; last first. by rewrite mulrn_eq0/= oner_eq0. rewrite mulN1R; apply/RleP. rewrite leR_oppl. apply/(@Exp_le_inv 2) => //. rewrite LogK //; last by apply/(ltR_leR_trans (exp2_gt0 _)); apply/RleP: H1. rewrite mulrC -mulNR -INRE. exact/RleP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep