proposition: Lemma rewrite_HP_with_Pf : `H P = - \sum_(m in 'I_Nmax.+1) \sum_(a in {: m.-tuple bool}) Pf a * log (Pf a).
proof: Proof. move: (uniq_dec_inj f_uniq) => f_inj; congr (- _). rewrite [in LHS](partition_big (inordf (size \o f)) (fun i => i \in 'I_Nmax.+1))//=. apply: eq_bigr => i _. rewrite (eq_bigr (fun i0 => Pf (f i0) * log (Pf (f i0)))) =>[|a]; last first. rewrite /Pf. case: (pickP _) => [x0 /eqP /f_inj->|] //. move/(_ a); by rewrite eqxx. rewrite (eq_bigl (fun x => size (f x) == i) _) =>[|x]; last first. apply/eqP/eqP => [<-| H]; first by rewrite inordfE. by apply/ord_inj; rewrite inordfE. rewrite (@big_seq_tuple _ i _ f_inj (fun a => Pf a * log (Pf a)) (fdist_card_neq0 P))//. rewrite /Pf; move=> i0. case: (pickP ) => // x; first by move/eqP <-; rewrite codom_f. by case: ifP; rewrite mul0R. 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