proposition: Lemma card_shelled_tuples : #| V.-shell ta |%:R <= exp2 (n%:R * `H(V | P)).
proof: Proof. case: (tuple_exist_perm_sort (@le_rank A) ta) => /= s Hta'. have H : sort (@le_rank _) ta = perm_tuple (s^-1) ta by rewrite {2}Hta' perm_tuple_comp mulVg perm_tuple_id. have {}Hta': ta = perm_tuple s (sort_tuple (@le_rank _) ta) by rewrite {1}Hta'. rewrite (card_shelled_tuples_perm V ta (s^-1)). rewrite Hta' perm_tuple_comp mulVg perm_tuple_id. apply card_shell_leq_exp_entropy => //. - rewrite in_set. apply/forallP => a /=. rewrite H num_occ_perm. move: a; apply/forallP. move: Hta; by rewrite in_set. - apply cond_type_equiv. move: (Vctyp); by rewrite in_set. - exact/sort_sorted/le_rank_total. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types