proposition: Lemma card_typed_tuples : INR #| T_{ P } | <= exp2 (INR n * `H P).
proof: Proof. rewrite -(invRK (exp2 (INR n * `H P))%R) -exp2_Ropp -mulNR. set aux := - INR n * `H P. rewrite -div1R leR_pdivl_mulr // {}/aux. case/boolP : [exists x, x \in T_{P}] => x_T_P. - case/existsP : x_T_P => ta Hta. rewrite -(row_of_tupleK ta) in Hta. rewrite -(tuple_dist_type_entropy Hta). rewrite [X in X <= _](_ : _ = Pr (type.d P) `^ n (@row_of_tuple A n @: T_{P})). by apply Pr_1. symmetry. rewrite /Pr. transitivity (\sum_(a| (a \in [finType of 'rV[A]_n]) && [pred x in (@row_of_tuple A n @: T_{P})] a) exp2 (- INR n * `H P)). apply eq_big => // ta'/= Hta'. rewrite -(@tuple_dist_type_entropy ta') //. case/imsetP : Hta' => x Hx ->. by rewrite row_of_tupleK. rewrite big_const iter_addR tuple_dist_type_entropy //. do 2 f_equal. by rewrite card_imset //; exact: row_of_tuple_inj. - rewrite (_ : (INR #| T_{P} | = 0)%R); first by rewrite mul0R; exact/Rle_0_1. rewrite (_ : 0%R = INR 0) //; congr INR; apply/eqP. rewrite cards_eq0; apply/negPn. by move: x_T_P; apply contra => /set0Pn/existsP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq