proposition: Lemma card_le_Xn_Lnt' : INR #| [set: n.-tuple X]| <= INR #| [set: (Z.abs_nat L_not_typ).-tuple bool]|.
proof: Proof. have fact : log (INR (expn #|X| n)) <= IZR (ceil (log (INR (expn #|X| n)))). exact: (proj1 (ceilP _)). rewrite /L_not_typ cardsT card_tuple. rewrite {1}(_ : INR (expn #|X| n) = exp2 (log (INR (expn #|X| n)))). - rewrite cardsT card_tuple card_bool -natRexp2. apply: Exp_le_increasing => //. rewrite /L_not_typ INR_Zabs_nat //. apply: le_IZR; apply: (Rle_trans _ (log (INR (expn #|X| n)))) => //. rewrite /= -(Log_1 2); apply: Log_increasing_le => //. rewrite -natRexp. by apply: pow_R1_Rle; apply: fdist_support_LB. - rewrite logK //; last rewrite -natRexp. exact/pow_lt/(Rlt_le_trans _ 1 _ _ fdist_support_LB). 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