fact: Definition aep_sigma2 := `E ((`-- (`log P)) `^2) - (`H P)^2.
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