proposition: Lemma log_sum1 {A : finType} (C : {set A}) (f g : {ffun A -> R}) : (forall a, a \in C -> 0 < f a) -> log_sum_stmt C f g.
proof: Proof. move=> fspos f0 g0 fg. case/boolP : (C == set0) => [ /eqP -> | Hc]. by apply/RleP; rewrite !big_set0 mul0R lexx. have gspos : forall a, a \in C -> 0 < g a. move=> a a_C. case (g0 a) => //. move=>/esym/(dominatesE fg) abs. by move: (fspos _ a_C); rewrite abs => /ltRR. have Fnot0 : \sum_{ C } f != 0. apply/eqP => /psumr_eq0P abs. case/set0Pn : Hc => a aC. move: (fspos _ aC); rewrite abs //. by move=> /RltP; rewrite ltxx. by move=> i iC; exact/RleP. have Gnot0 : \sum_{ C } g != 0. apply/eqP => /psumr_eq0P abs. case/set0Pn : Hc => a aC. move: (gspos _ aC); rewrite abs //. by move=> /RltP; rewrite ltxx. by move=> i iC; exact/RleP. wlog : Fnot0 g g0 Gnot0 fg gspos / \sum_{ C } f = \sum_{ C } g. move=> Hwlog. set k := (\sum_{ C } f / \sum_{ C } g). have Fspos : 0 < \sum_{ C } f. suff Fpos : 0 <= \sum_{ C } f by apply/RltP; rewrite lt0r Fnot0; exact/RleP. by apply/RleP/sumr_ge0 => ? ?; exact/RleP/ltRW/fspos. have Gspos : 0 < \sum_{ C } g. suff Gpocs : 0 <= \sum_{ C } g by apply/RltP; rewrite lt0r Gnot0; exact/RleP. by apply/RleP/sumr_ge0 => ? ?; exact/RleP/ltRW/gspos. have kspos : 0 < k by exact: divR_gt0. set kg := [ffun x => k * g x]. have kg_pos : forall a, 0 <= kg a. by move=> a; rewrite /kg /= ffunE; apply mulR_ge0 => //; exact: ltRW. have kabs_con : f `<< kg. apply/dominates_scale => //; exact/gtR_eqF. have kgspos : forall a, a \in C -> 0 < kg a. by move=> a a_C; rewrite ffunE; apply mulR_gt0 => //; exact: gspos. have Hkg : \sum_{C} kg = \sum_{C} f. transitivity (\sum_(a in C) k * g a). by apply eq_bigr => a aC; rewrite /= ffunE. by rewrite -big_distrr /= /k /Rdiv -mulRA mulRC mulVR // mul1R. have Htmp : \sum_{ C } kg != 0. rewrite /=. evar (h : A -> R); rewrite (eq_bigr h); last first. by move=> a aC; rewrite ffunE /h; reflexivity. rewrite {}/h (_ : \sum_(i in C) _ = \sum_{C} f) // -Hkg. by apply eq_bigr => a aC /=; rewrite ffunE. symmetry in Hkg. move: {Hwlog}(Hwlog Fnot0 kg kg_pos Htmp kabs_con kgspos Hkg) => /= Hwlog. rewrite Hkg {1}/Rdiv mulRV // /log Log_1 mulR0 in Hwlog. set rhs := \sum_(_ | _) _ in Hwlog. rewrite (_ : rhs = \sum_(a | a \in C) (f a * log (f a / g a) - f a * log k)) in Hwlog; last first. rewrite /rhs. apply eq_bigr => a a_C. rewrite /Rdiv /log LogM; last 2 first. exact/fspos. rewrite ffunE; apply/invR_gt0/mulR_gt0 => //; exact/gspos. rewrite LogV; last first. rewrite ffunE; apply mulR_gt0 => //; exact: gspos. rewrite ffunE LogM //; last exact: gspos. rewrite LogM //; last 2 first. exact/fspos. by apply invR_gt0 => //; apply gspos. by rewrite LogV; [field | apply gspos]. rewrite big_split /= -big_morph_oppR -big_distrl /= in Hwlog. by rewrite -subR_ge0. move=> Htmp; rewrite Htmp. rewrite /Rdiv mulRV; last by rewrite -Htmp. rewrite /log Log_1 mulR0. suff : 0 <= \sum_(a | a \in C) f a * ln (f a / g a). move=> H. rewrite /log /Rdiv. set rhs := \sum_( _ | _ ) _. have -> : rhs = \sum_(H | H \in C) (f H * (ln (f H / g H))) / ln 2. rewrite /rhs. apply eq_bigr => a a_C; by rewrite /Rdiv -mulRA. rewrite -big_distrl /=. by apply mulR_ge0 => //; exact/invR_ge0. apply (@leR_trans (\sum_(a | a \in C) f a * (1 - g a / f a))). apply (@leR_trans (\sum_(a | a \in C) (f a - g a))). rewrite big_split /= -big_morph_oppR Htmp addRN. by apply/RleP; rewrite lexx. apply/Req_le/eq_bigr => a a_C. rewrite mulRDr mulR1 mulRN. case: (Req_EM_T (g a) 0) => [->|ga_not_0]. by rewrite div0R mulR0. by field; exact/eqP/gtR_eqF/(fspos _ a_C). apply: leR_sumR => a C_a. apply leR_wpmul2l; first exact/ltRW/fspos. rewrite -[X in _ <= X]oppRK leR_oppr -ln_Rinv; last first. apply divR_gt0; by [apply fspos | apply gspos]. rewrite invRM; last 2 first. exact/gtR_eqF/(fspos _ C_a). by rewrite invR_neq0' // gtR_eqF //; exact/(gspos _ C_a). rewrite invRK mulRC; apply: leR_trans. by apply/ln_id_cmp/divR_gt0; [apply gspos | apply fspos]. apply Req_le. by field; exact/eqP/gtR_eqF/(fspos _ C_a). Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals Lra mathcomp(Rstruct lra) ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts bigop_ext