proposition: Lemma log_pow_INR m k : (m > 0)%nat -> log (expn m k)%:R = k%:R * log m%:R.
proof: Proof. move=> m0; elim: k => [|k ih]; first by rewrite expn0 /log Log_1 mul0R. rewrite expnS natRM /log LogM ?ltR0n // ?expn_gt0 ?m0 // -!/(log _) ih. by rewrite -addn1 natRD addRC mulRDl mul1R. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code