proposition: Lemma log_sum_inequality_ord_add1' : (\sum_(i < n) f i.+1) * (log (\sum_(i < n) f i.+1) - log (\sum_(i < n) g i.+1)) <= \sum_(i < n) f i.+1 * (log (f i.+1) - log (g i.+1)).
proof: Proof. rewrite [X in _ <= X] (_ : _ = \sum_(i < n) f i.+1 * log (f i.+1 / (g i.+1))). rewrite [X in X <= _](_ : _ = (\sum_(i < n) f i.+1) * (log ((\sum_(i < n)f i.+1) / (\sum_(i < n) g i.+1)))). exact: log_sum_inequality_ord_add1. have : 0 <= \sum_(i in 'I_n) f i.+1. by apply/RleP/sumr_ge0 => ? _; exact/RleP/nneg_f_ge0. case=>[Hf | <-]; last by rewrite !mul0R. have : 0 <= \sum_(i in 'I_n) g i.+1. by apply/RleP/sumr_ge0 => ? _; exact/RleP/nneg_f_ge0. case => [Hg |]. by rewrite /log LogM // ?LogV //; last exact: invR_gt0. have Rle0g_add1 : forall x : 'I_n, 0 <= g x.+1 by move=> ?; apply nneg_f_ge0. move=> H. have eq_g_0 : forall i : 'I_n, 0 = g i.+1. move/esym/psumr_eq0P : H => H i; rewrite H//. by move=> /= j _; exact/RleP. have : 0 = \sum_(i < n) f i.+1. apply/esym/eqP; rewrite psumr_eq0 /=; last first. move=> i _. exact/RleP/nneg_f_ge0. apply/allP => i _; apply/eqP. by move/dominatesP : f_dom_by_g; apply; rewrite -eq_g_0. by move => tmp; move: Hf; rewrite -tmp; move/Rlt_not_eq. apply: eq_bigr => i _. case: (nneg_f_ge0 f i.+1) => [fpos|<-]; last by rewrite !mul0R. case: (nneg_f_ge0 g i.+1); last first. move/esym => g0; move/dominatesP : f_dom_by_g => /(_ _ g0) ->. by rewrite !mul0R. by move=>gpos; rewrite /log LogM // ?LogV //; exact: invR_gt0. 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