proposition: Lemma rewrite_HP_with_PN : `H P = - \sum_(m in [set x | PN x != 0]) PN m * (\sum_(a in {: m.-tuple bool}) Pf' m a * (log (Pf' m a) + log (PN m))).
proof: Proof. rewrite rewrite_HP_with_Pf; congr (- _). rewrite (eq_bigl (fun m => m \in [set : 'I_Nmax.+1]) _) => [|?]; last first. by rewrite /= in_setT. rewrite rsum_disjoints_set [Y in Y + _ = _]big1 ?add0R; last first. move=> /= i; rewrite inE. rewrite /pr_eq; unlock. rewrite /Pr ffunE /= => /eqP/psumr_eq0P => H. have {}H : forall j : A, j \in [set x | (size (f x))%:R == i%:R] -> P j = 0. move=> a Ha. apply: H => //. rewrite inE/=. rewrite inE in Ha. by rewrite (eqP Ha) INRE. rewrite big1 // => i0 _. rewrite {1}/Pf. case: pickP => [a /eqP fai0|]; last by rewrite mul0R. by rewrite H ?mul0R // inE fai0 size_tuple. apply : eq_bigr => i. rewrite inE /eqP => Pr_non0. rewrite big_distrr /=. apply : eq_bigr => i0 _. rewrite ffunE. rewrite {1}/Pf'. rewrite ffunE. rewrite [in RHS]mulRC /Rdiv -mulRA -mulRA. case: (Req_dec (Pf i0) 0) => [->| /nesym/eqP Pfi0_non0]; first by rewrite !mul0R. congr (_ * _). rewrite mulRC -mulRA. rewrite {2}/PN. rewrite [in X in _ = _ * (_ * / X)]/= [in X in _ = _ * (_ * / X)]ffunE. rewrite mulRV ?mulR1; last by rewrite /PN /= ffunE in Pr_non0. rewrite /log LogM; last 2 first. apply/RltP; rewrite lt0r eq_sym Pfi0_non0; apply/RleP. rewrite /Pf; case:pickP=>[? _ | ? ]; [exact/RleP/FDist.ge0 | by []]. by apply/invR_gt0/RltP; rewrite -fdist_gt0. rewrite LogV; last by apply/RltP; rewrite -fdist_gt0. by rewrite /PN /= ffunE -addRA Rplus_opp_l addR0. 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