proposition: Lemma le_entroPN_logeEX' : `H PN <= `E X * log (`E X) - (`E X - 1) * log((`E X ) - 1).
proof: Proof. move/Rle_lt_or_eq_dec:le_1_EX=>[lt_EX_1| eq_E_0]; last first. rewrite -eq_E_0 /Rminus Rplus_opp_r mul0R Ropp_0 addR0 mul1R /log Log_1. by move/esym/entroPN_0 : eq_E_0 ->. have lt_0_EX_1 : 0 < `E X - 1 by rewrite subR_gt0. pose alp := (`E X - 1) / `E X . have gt_alp_1 : alp < 1. rewrite -(ltR_pmul2r EX_gt0) // mul1R. rewrite /alp -mulRA mulVR ?mulR1; last exact/gtR_eqF/EX_gt0. by rewrite -ltR_subr_addl subRR -ltR_oppl oppR0. have lt_0_alp : 0 < alp by rewrite /alp; exact/divR_gt0/EX_gt0. have EX_pos' : 0 < 1 - (`E X - 1) / `E X . rewrite divRDl divRR; last exact/gtR_eqF/EX_gt0. rewrite divN1R addR_opp subRB subRR add0R; exact/invR_gt0/EX_gt0. have max_pos: (0 < \max_(a in A) size (f a))%coq_nat. apply/ltP. move/card_gt0P : (fdist_card_neq0 P) => [a _]. apply: (bigmax_sup a)=> //. by move: (Xpos a); rewrite /X /= (_ : 0 = INR 0) // => /INR_lt/ltP. rewrite [X in _ <= X](_ :_ = log ( alp / (1 - alp)) - (log alp) * `E X); last first. rewrite /alp /Rdiv /log !LogM //; last 2 first. exact/invR_gt0/EX_gt0. exact/invR_gt0. rewrite ![in RHS](LogV _ EX_gt0) // mulRDl [in RHS]/Rminus. rewrite [in RHS]addRC (addRC _ (- log (`E X ) * `E X )) oppRD. rewrite [in RHS]mulNR oppRK -addRA. rewrite [in LHS]mulRC -addR_opp; congr (_ + _). rewrite [in LHS]mulRDl mulRC oppRD mulN1R oppRK; congr (_ + _). rewrite -[in RHS]addRA -[LHS]addR0; congr (_ + _). rewrite mulRDl mulRV; last exact/gtR_eqF/EX_gt0. by rewrite mulN1R !addR_opp subRB subRR add0R invRK ?Rplus_opp_l. apply: (@leR_trans (log (alp * (1 - (alp ^ (\max_(a | a \in A) size (f a)))) / (1 - alp)) - log alp * `E X ) _); last first. rewrite leR_add2r. apply: Log_increasing_le => //. apply/mulR_gt0; last by apply/invR_gt0; rewrite subR_gt0. apply/mulR_gt0 => //; rewrite subR_gt0. have : 0 <= alp < 1 by split => //; exact/ltRW. by case/(pow_lt_1_compat _ _)/(_ max_pos). rewrite /Rdiv -mulRA; apply/(leR_wpmul2l (ltRW lt_0_alp)). rewrite -{2}(mul1R (/ (1 - alp))). apply/leR_wpmul2r; first by apply/invR_ge0; rewrite subR_gt0. rewrite -addR_opp addRC -leR_subr_addr subRR leR_oppl oppR0. exact/expR_ge0/ltRW. rewrite EX_ord -big_pow1; last exact/eqP/ltR_eqF. rewrite mulRC (big_morph _ (morph_mulRDl _) (mul0R _)). rewrite -(@leR_add2r (\sum_(i < Nmax.+1) i%:R * `Pr[ X = i%:R ] * log alp)). rewrite -addRA (_ : - _ + _ = 0) ?addR0; last first. rewrite addRC addR_opp subR_eq0; apply eq_bigr => i _; rewrite ffunE. by rewrite -INRE. rewrite (@eq_bigr _ _ _ 'I_Nmax.+1 _ _ _ (fun i => `Pr[ X = i%:R ] * log (alp ^ i)))=>[|i _]; last first. by rewrite log_pow // [in RHS]mulRC -mulRA (mulRC _ (log alp)) mulRA. rewrite /entropy addRC; move: oppRB; rewrite/Rminus; move<-. rewrite -(oppRK (log _)) leR_oppl oppRK big_morph_oppR -big_split /=. rewrite [X in _ <= X](_ : _ = \sum_(i < Nmax.+1) `Pr[ X = i%:R] * (log (`Pr[ X = i%:R ]) - log (alp ^ i))); last first. by apply: eq_bigr => i _; rewrite ffunE addR_opp -INRE -mulRBr. rewrite -sub0R -(mul1R (0 - _)). have pmf1' : \sum_(i < Nmax) `Pr[X = i.+1%:R] = 1. rewrite (_ : 1 = 1%mcR)// -PN_sum1 /=. under [in RHS]eq_bigr do rewrite ffunE. rewrite big_ord_recl. rewrite -RplusE. rewrite -subR_eq. rewrite [LHS](_ : _ = 0); last first. apply/eqP; rewrite GRing.subr_eq0; apply/eqP/eq_bigr => i _ /=. by rewrite INRE. apply/esym. rewrite /pr_eq; unlock. rewrite /Pr big1 // => i. rewrite inE; move/eqP => Xi_0. by move/gtR_eqF: (Xpos i); rewrite Xi_0 => /eqP. rewrite -{1}(Log_1 2) -pmf1'. have Pr_ge0' (i : nat) : 0 <= `Pr[ X = i%:R] by []. have alpi_ge0 (i : nat) : 0 <= alp ^ i by exact/pow_le/ltRW. pose h := mkNNFun Pr_ge0'. pose g := mkNNFun alpi_ge0. have dom_by_hg : h `<< g. apply/dominatesP => i. rewrite /g /= => alp0. move: lt_0_alp. have -> : alp = 0 by move: (pow_nonzero alp i); tauto. by move/ltRR. rewrite big_ord_recl [X in _ <= X + _](_ : _ = 0) ?add0R; last first. rewrite /pr_eq; unlock. rewrite /Pr. have -> : [set x | X x == INR 0] = set0; last by rewrite big_set0 mul0R. apply/setP => i; rewrite inE /= in_set0. by apply/negbTE; rewrite gtR_eqF //; exact: Xpos. exact: (log_sum_inequality_ord_add1' Nmax dom_by_hg). 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