proposition: Lemma aep_sigma2E : aep_sigma2 = \sum_(a in A) P a * (log (P a))^2 - (`H P)^2.
proof: Proof. rewrite /aep_sigma2 /Ex [in LHS]/log_RV /sq_RV /comp_RV. by under eq_bigr do rewrite mulRC /ambient_dist -mulRR Rmult_opp_opp mulRR. 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