proposition: Lemma log_sum {A : finType} (C : {set A}) (f g : {ffun A -> R}) : log_sum_stmt C f g.
proof: Proof. move=> f0 g0 fg. set D := [set a | (a \in C) && (f a != 0)]. suff : \sum_{D} f * log (\sum_{D} f / \sum_{D} g) <= \sum_(a | a \in D) f a * log (f a / g a). move=> H. set D' := [set a in C | f a == 0]. have DUD' : C = D :|: D'. apply/setP => a. move Hlhs : (a \in C) => lhs. destruct lhs => //. symmetry. rewrite in_setU /C1 /C1 !in_set Hlhs /=. by destruct (f a == 0). by rewrite in_setU in_set Hlhs /= /C1 in_set Hlhs. have DID' : [disjoint D & D']. rewrite -setI_eq0. apply/eqP/setP => a. rewrite in_set0 /C1 /C1 in_setI !in_set. by destruct (a \in C) => //=; rewrite andNb. have H1 : \sum_{C} f = \sum_{D} f. rewrite setUC in DUD'. rewrite DUD' (big_union _ f DID') /=. rewrite (_ : \sum_{D'} f = \sum_(a | a \in D') 0); last first. apply eq_bigr => a. rewrite /D' in_set. by case/andP => _ /eqP. by rewrite big_const iter_addR mulR0 add0R. rewrite -H1 in H. have pos_F : 0 <= \sum_{C} f by apply/RleP/sumr_ge0 => ? ?; exact/RleP. apply (@leR_trans (\sum_{C} f * log (\sum_{C} f / \sum_{D} g))). case/Rle_lt_or_eq_dec : pos_F => pos_F; last first. by rewrite -pos_F !mul0R. have H2 : 0 <= \sum_(a | a \in D) g a by apply/RleP/sumr_ge0 => ? _; exact/RleP. case/Rle_lt_or_eq_dec : H2 => H2; last first. have : 0 = \sum_{D} f. transitivity (\sum_(a | a \in D) 0). by rewrite big_const iter_addR mulR0. apply: eq_bigr => a a_C1. rewrite (dominatesE fg) //. apply/(@psumr_eq0P _ _ (mem D) g) => // i _. exact/RleP. move=> abs; rewrite -abs in H1; rewrite H1 in pos_F. by move/ltRR : pos_F. have H3 : 0 < \sum_(a | a \in C) g a. rewrite setUC in DUD'. rewrite DUD' (big_union _ g DID') /=. by apply: addR_gt0wr => //; apply/RleP/sumr_ge0=> ? _; exact/RleP. apply/(leR_wpmul2l (ltRW pos_F))/Log_increasing_le => //. by apply divR_gt0 => //; rewrite -HG. apply/(leR_wpmul2l (ltRW pos_F))/leR_inv => //. rewrite setUC in DUD'. rewrite DUD' (big_union _ g DID') /= -[X in X <= _]add0R; apply leR_add2r. by apply/RleP/sumr_ge0 => ? ?; exact/RleP. apply: (leR_trans H). rewrite setUC in DUD'. rewrite DUD' (big_union _ (fun a => f a * log (f a / g a)) DID') /=. rewrite (_ : \sum_(_ | _ \in D') _ = 0); last first. transitivity (\sum_(a | a \in D') 0). apply eq_bigr => a. by rewrite /D' in_set => /andP[a_C /eqP ->]; rewrite mul0R. by rewrite big_const iter_addR mulR0. by apply/RleP; rewrite add0R lexx. apply: log_sum1 => // a. rewrite /C1 in_set. case/andP => a_C fa_not_0. case (f0 a) => // abs. by rewrite abs eqxx in fa_not_0. Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals Lra mathcomp(Rstruct lra) ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts bigop_ext