proposition: Lemma aep : aep_bound P epsilon <= n.+1%:R -> Pr (P `^ n.+1) [set t | (0 < P `^ n.+1 t)%mcR && (`| (`-- (`log (P `^ n.+1)) `/ n.+1) t - `H P | >= epsilon)%mcR ] <= epsilon.
proof: Proof. move=> Hbound. apply (@leR_trans (aep_sigma2 P / (n.+1%:R * epsilon ^ 2))); last first. rewrite /aep_bound in Hbound. apply (@leR_wpmul2r (epsilon / n.+1%:R)) in Hbound; last first. apply divR_ge0; [exact/ltRW/Hepsilon | exact/ltR0n]. rewrite [in X in _ <= X]mulRCA mulRV ?INR_eq0' // ?mulR1 in Hbound. apply/(leR_trans _ Hbound)/Req_le; field. by split; [by rewrite INR_eq0 | exact/eqP/gtR_eqF]. have Hsum := sum_mlog_prod_sum_map_mlog P n. have H1 k i : `E ((\row_(i < k.+1) `-- (`log P)) ``_ i) = `H P. by rewrite mxE entropy_Ex. have H2 k i : `V ((\row_(i < k.+1) `-- (`log P)) ``_ i) = aep_sigma2 P. by rewrite mxE V_mlog. have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon). move/(leR_trans _); apply. apply/Pr_incl/subsetP => ta; rewrite 2!inE => /andP[H1]. rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /= /scalel_RV /log_RV /neg_RV. rewrite fdist_rVE. rewrite log_prodR_sumR_mlog //. move=> i; apply/RltP. move: i; apply/prod_gt0_inv. by move=> x; exact: FDist.ge0. by move: H1; rewrite fdist_rVE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb fdist proba entropy