proposition: Lemma V_mlog : `V (`-- (`log P)) = aep_sigma2.
proof: Proof. rewrite aep_sigma2E /Var E_trans_RV_id_rem -entropy_Ex. transitivity (\sum_(a in A) ((- log (P a))^2 * P a - 2 * `H P * - log (P a) * P a + `H P ^ 2 * P a))%R. apply eq_bigr => a _. rewrite /scalel_RV /log_RV /neg_RV /trans_add_RV /sq_RV /comp_RV /= /sub_RV. by rewrite /ambient_dist; field. rewrite big_split /= big_split /= -big_distrr /= (FDist.f1 P) mulR1. rewrite (_ : \sum_(a in A) - _ = - (2 * `H P ^ 2))%R; last first. rewrite -{1}big_morph_oppR; congr (- _)%R. rewrite [X in X = _](_ : _ = \sum_(a in A) (2 * `H P) * (- (P a * log (P a))))%R; last first. by apply eq_bigr => a _; rewrite -!mulRA (mulRC (P a)) mulNR. rewrite -big_distrr [in LHS]/= -{1}big_morph_oppR. by rewrite -/(entropy P) -mulRA /= mulR1. set s := ((\sum_(a in A ) _)%R in LHS). rewrite (_ : \sum_(a in A) _ = s)%R; last by apply eq_bigr => a _; field. rewrite RpowE GRing.expr2 -!RmultE mulR1. field. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb fdist proba entropy