proposition: Lemma apply_max_HPN : `H P <= `E X + `H PN.
proof: Proof. have f_inj := uniq_dec_inj f_uniq. rewrite rewrite_HP_with_HPN addRC (addRC _ (`H _)) leR_add2l EX_ord. rewrite (eq_bigl (fun m => m \in [set : 'I_Nmax.+1]) (fun x=> INR x * _ ))=>[|?]; last first. by rewrite /= in_setT. rewrite rsum_disjoints_set. rewrite [Y in _ <= Y + _ ](_ :_ = 0). rewrite add0R; apply: leR_sumR => i. rewrite mulRC inE; move/eqP => H. apply/leR_wpmul2r; first by rewrite /PN /= ffunE. pose pmf_Pf' := mkNNFinfun (Rle0Pf' H). have pmf1'_Pf' : ([forall a, (0 <= pmf_Pf' a)%mcR] && ((\sum_(a in {: i.-tuple bool}) pmf_Pf' a)%mcR == 1%mcR)). apply/andP; split. apply/forallP => x. rewrite /pmf_Pf'/= /Pf'; rewrite ffunE. apply/RleP/divR_ge0 => //. exact: Rle0Pf. by apply/RltP/fdist_gt0/eqP. by apply/eqP; apply: (pmf1_Pf' H). pose distPf := FDist.mk pmf1'_Pf'. move: (entropy_max distPf). rewrite card_tuple /= card_bool -natRexp log_pow (_ : INR 2 = 2) //. by rewrite /log Log_n // mulR1. rewrite big1 //= => i. by rewrite inE /PN /= => /eqP ->; rewrite mulR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code