proposition: Lemma pmf1_Pf' m : PN m <> 0 -> \sum_(a in {: m.-tuple bool}) Pf' m a = 1.
proof: Proof. move: (uniq_dec_inj f_uniq) => f_inj PNnon0. rewrite /Pf'. under eq_bigr do rewrite ffunE. rewrite -big_distrl /=. apply: (Rmult_eq_reg_r (PN m)) => //; rewrite mul1R. rewrite -mulRA mulVR ?mulR1; last exact/eqP. rewrite /= ffunE. rewrite /pr_eq; unlock. rewrite /Pr (eq_bigr (fun x => Pf (f x))) => [|a ain]; last first. rewrite /Pf. case:pickP; first by move =>x /eqP/ f_inj ->. by move/(_ a); rewrite eqxx. rewrite (eq_bigl (fun x => size (f x) == m) _) => [|a]; last first. rewrite inE /X /= -INRE. by apply/eqP/eqP => [/INR_eq | ->]. rewrite (big_seq_tuple m f_inj (fdist_card_neq0 P)) /Pf => [//|i0]. case: pickP => // ?; first by move/eqP <-; rewrite codom_f. by case: ifP. 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