proposition: Lemma eq_sizef_Lt : \sum_(x| x \in `TS P n epsilon) P `^ n (x) * (INR (size (f P epsilon x)) ) = \sum_(x| x \in `TS P n epsilon) P `^ n (x) * (IZR L_typ + 1).
proof: Proof. apply: eq_bigr=> i H. apply: Rmult_eq_compat_l. rewrite /f H /= size_pad_seqL -INR_Zabs_nat. - by rewrite -addn1; rewrite plus_INR. - by apply: le_IZR;apply: ltRW; apply: Lt_pos. 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