proposition: Lemma rewrite_HP_with_HPN : `H P = \sum_(m in [set x : 'I_Nmax.+1 | PN x != 0]) PN m * (- \sum_(a in {: m.-tuple bool}) Pf' m a * (log ((Pf' m a)))) + `H PN.
proof: Proof. rewrite {2}/entropy. rewrite (eq_bigl (fun m => m \in [set : 'I_Nmax.+1]) (fun x=> _ * log _))=>[|?]; last first. by rewrite /= in_setT. rewrite rsum_disjoints_set [Y in _ = _ + - (Y + _)]big1; last first. by move => /= i; rewrite inE /PN /= => /eqP ->; rewrite mul0R. rewrite add0R rewrite_HP_with_PN !big_morph_oppR -big_split /=. apply: eq_bigr => i. rewrite inE => /eqP Pr_non0. rewrite mulRN -oppRD; congr (- _). rewrite -mulRDr. congr (_ * _). rewrite -[Y in _ = _ + Y]mul1R -(pmf1_Pf' Pr_non0) big_distrl /= -big_split /=. by under eq_bigr do rewrite mulRDr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code