proposition: Lemma log_pow r : 0 < r -> log (r ^ n) = n%:R * log r.
proof: Proof. elim:n=> [|n' IH lt_0_r]; first by rewrite /log Log_1 mul0R. rewrite /log LogM //;last exact: pow_lt. rewrite /log in IH; by rewrite IH // -addn1 addRC plus_INR mulRDl mul1R. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code