proposition: Lemma entropy_log_div : entropy p = log #|A|%:R - D(p || u).
proof: Proof. rewrite /entropy /div. evar (RHS : A -> R). have H a : p a * log (p a / u a) = RHS a. have /RleP[H|H] := FDist.ge0 p a. - rewrite fdist_uniformE. change (p a * log (p a / / #|A|%:R)) with (p a * log (p a * / / #|A|%:R)). have H0 : 0 < #|A|%:R by rewrite An1 ltR0n. have /eqP H1 : #|A|%:R <> 0 by apply/eqP/gtR_eqF. rewrite -RinvE ?An1; last first. by rewrite -INRE// INR_eq0'. rewrite /Rdiv invRK// logM //; last first. by rewrite -INRE ltR0n. rewrite mulRDr -INRE. rewrite -An1. by instantiate (RHS := fun a => p a * log (p a) + p a * log #|A|%:R). - by rewrite /RHS -H /= 3!mul0R add0R. have -> : \sum_(a in A) p a * log (p a / u a) = \sum_(a in A) RHS a. by move : H; rewrite /RHS => H; exact: eq_bigr. rewrite /RHS big_split /= -big_distrl /= (FDist.f1 p) mul1R. by rewrite -addR_opp oppRD addRC -addRA Rplus_opp_l addR0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(mathcomp_extra Rstruct reals) Reals Ranalysis_ext Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist jfdist_cond entropy convex binary_entropy_function log_sum divergence