proposition: Lemma log_sum_inequality_ord_add1 : (\sum_(i < n) f i.+1) * (log ((\sum_(i < n) f i.+1) / (\sum_(i < n) g i.+1))) <= \sum_(i < n) f i.+1 * (log (f i.+1 / g i.+1)).
proof: Proof. have Rle0f_1 : forall x : 'I_n, 0 <= f x.+1 by move=> ?; apply nneg_f_ge0. have Rle0g_1 : forall x : 'I_n, 0 <= g x.+1 by move=> ?; apply nneg_f_ge0. have newRle0f_1 : [forall x : 'I_n, (0 <= [ffun x : 'I_n => f x.+1] x)%mcR]. apply/forallPP; first by move=> x; apply/RleP. by move=> ?/=; rewrite ffunE. have newRle0g_1: [forall x : 'I_n, (0 <= [ffun x : 'I_n => g x.+1] x)%mcR]. apply/forallPP; first by move=> x; apply/RleP. by move=> ?/=; rewrite ffunE. have f_dom_by_g1 : mkNNFinfun newRle0f_1 `<< mkNNFinfun newRle0g_1. apply/dominatesP => a; move/dominatesP : f_dom_by_g. by rewrite /= !ffunE; exact. have H : forall h, \sum_(a | a \in [set: 'I_n]) h a.+1 = \sum_(a | a \in 'I_n) h a.+1. by move=> ?; under eq_bigl do rewrite in_setT. rewrite -!H -(H (fun i => f i * log (f i / g i))). have H1 : (forall x : 'I_n, 0 <= mkNNFinfun newRle0f_1 x). by move=> x//=; rewrite ffunE. have H2 : (forall x : 'I_n, 0 <= mkNNFinfun newRle0g_1 x). by move=> x//=; rewrite ffunE. have := (log_sum [set: 'I_n] (mkNNFinfun newRle0f_1) (mkNNFinfun newRle0g_1) H1 H2 f_dom_by_g1). rewrite /=. under eq_bigr do rewrite ffunE. under [in X in _ * log (_ / X) <= _ -> _]eq_bigr do rewrite ffunE. under [in X in _ <= X -> _]eq_bigr do rewrite ffunE. move/leR_trans; apply. rewrite leR_eqVlt; left. by under eq_bigr do rewrite ffunE. 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