proposition: Lemma E_leng_cw_le_Length : @E_leng_cw _ _ P (f (n':=n') P epsilon) <= (IZR L_typ + 1) + epsilon * (IZR L_not_typ + 1) .
proof: Proof. rewrite /E_leng_cw /Ex /=. under eq_bigr do rewrite mulRC. rewrite (rsum_split _ (`TS P n'.+1 epsilon)). rewrite eq_sizef_Lnt eq_sizef_Lt -!(big_morph _ (morph_mulRDl _) (mul0R _)) mulRC. rewrite (_ : \sum_(i | i \in ~: `TS P n epsilon) P `^ n i = 1 - \sum_(i | i \in `TS P n epsilon) P `^ n i); last first. - by rewrite (_ : 1 = 1%mcR)// -(FDist.f1 P`^n) (rsum_split _ (`TS P n epsilon)) addRC addRK. - apply leR_add. + rewrite -[X in _ <= X]mulR1; apply: leR_wpmul2l => //. * by apply: addR_ge0 => //; exact/ltRW/Lt_pos. * rewrite (_ : 1 = 1%mcR)// -(FDist.f1 (P `^ n)); apply: leR_sumRl => // *. by apply/RleP; rewrite Order.POrderTheory.lexx. + apply: leR_wpmul2r => //. * by apply addR_ge0 => //; exact (Lnt_nonneg _ P). * by rewrite leR_subl_addr addRC -leR_subl_addr; exact: Pr_TS_1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code