proposition: Lemma card_shell_leq_exp_entropy : #| V.-shell ta |%:R <= exp2 (n%:R * `H(V | P)).
proof: Proof. rewrite cond_entropy_chanE2. apply (@leR_trans (\prod_ ( i < #|A|) card_type_of_row Hta Vctyp i)%:R). - exact/le_INR/leP/card_shelled_tuples_leq_prod_card. - rewrite exp2_pow big_morph_natRM. rewrite (@big_morph _ _ (fun r : R => ((exp2 r) ^ n)%R) 1%R Rmult _ Rplus _); last 2 first. move=> a b /=; rewrite -!exp2_pow mulRDr /exp2 !ExpD; by field. by rewrite -exp2_pow mulR0 /exp2 Exp_0. rewrite (reindex_onto (fun x => enum_rank x) (fun y => enum_val y)) => [|i _]; last by rewrite enum_valK. rewrite (_ : \prod_(j | enum_val (enum_rank j) == j) _ = \prod_(j : A) (card_type_of_row Hta Vctyp (enum_rank j))%:R); last first. apply eq_bigl => a; rewrite enum_rankK; by apply/eqP. apply leR_prodR => a. split; first exact/leR0n. rewrite -exp2_pow mulRA. rewrite /card_type_of_row; case: Bool.bool_dec => [e|/Bool.eq_true_not_negb e]. rewrite -[X in X <= _]exp2_0. apply Exp_le_increasing, mulR_ge0 => //. apply mulR_ge0 => //; exact: leR0n. exact: entropy_ge0. set pta0 := type_of_row Hta Vctyp _. rewrite (_ : exp2 _ = exp2 (N(a | ta)%:R * `H pta0)%R). by rewrite -[in X in _ <= exp2 (X * _)](enum_rankK a); apply card_typed_tuples. congr (exp2 (_ * _)). + by rewrite -type_fun_type // (type_numocc Hta). + rewrite /entropy. apply Ropp_eq_compat, eq_bigr => b _. rewrite /pta0 (JType.c_f V) /= (Vctyp Hta a) -{1 4}(enum_rankK a). by move/negbTE : (e) => ->; rewrite !ffunE /= enum_rankK. 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