fact: Definition log_sum_stmt {A : finType} (C : {set A}) (f g : {ffun A -> R}) := (forall x, 0 <= f x) -> (forall x, 0 <= g x) -> f `<< g -> \sum_{C} f * log (\sum_{C} f / \sum_{C} g) <= \sum_(a | a \in C) f a * log (f a / g a).
imports: mathcomp(all_ssreflect all_algebra) Reals Lra mathcomp(Rstruct lra) ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts bigop_ext