proposition: Lemma log_prodR_sumR_mlog {A : finType} k (f : A -> R) s : (forall a, 0 <= f a)%coqR -> (forall i, 0 < f i)%coqR -> (- Log k (\prod_(i <- s) f i) = \sum_(i <- s) - Log k (f i))%R.
proof: Proof. move=> f0 f0'. elim: s => [|h t ih]. by rewrite !big_nil Log_1 oppR0. rewrite big_cons LogM//; last first. by apply/RltP/prodr_gt0 => a _; exact/RltP. by rewrite [RHS]big_cons oppRD; congr (_ + _)%coqR. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext