proposition: Lemma eq_sizef_Lnt: \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_not_typ + 1) .
proof: Proof. apply: eq_bigr => ? H. apply: Rmult_eq_compat_l. move: H; rewrite in_setC. rewrite /f; move /negbTE ->. rewrite /= -addn1 size_tuple plus_INR INR_Zabs_nat. - by []. - by apply: le_IZR; apply: (Lnt_nonneg _ P). 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