proposition: Lemma div_ge0 : 0 <= D(P || Q).
proof: Proof. rewrite /div [X in _ <= X](_ : _ = - \sum_(a | a \in A) P a * (log (Q a / P a))); last first. rewrite big_morph_oppR; apply eq_bigr => a _; rewrite -mulRN. case/boolP : (P a == 0) => [/eqP ->|H0]; first by rewrite !mul0R. congr (_ * _). have Qa0 := dominatesEN P_dom_by_Q H0. by rewrite -logV ?Rinv_div//; apply divR_gt0; apply /RltP; rewrite -fdist_gt0. rewrite leR_oppr oppR0. apply (@leR_trans ((\sum_(a | a \in A) (Q a - P a)) * log (exp 1))). rewrite (big_morph _ (morph_mulRDl _) (mul0R _)). apply leR_sumR => a _; apply div_diff_ub => //. by move/dominatesP : P_dom_by_Q; exact. rewrite -{1}(mul0R (log (exp 1))); apply (leR_wpmul2r log_exp1_Rle_0). by rewrite big_split /= -big_morph_oppR !FDist.f1 addR_opp subRR. Qed.
imports: mathcomp(all_ssreflect ssralg all_algebra reals) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ln_facts logb fdist proba