proposition: Lemma big_seq_tuple (F : seq bool -> R) : (0 < #|A|)%nat -> (forall i, F i = if i \in codom f then F i else 0)-> \sum_(i in {: n.-tuple bool}) F i = \sum_(a| size (f a) == n) F (f a).
proof: Proof. move=> Anon0 Fi0. rewrite big_seq_tuple' //. rewrite (eq_bigr (fun a => if (tval a \in codom f) then F a else 0)) => [|i _]. by rewrite -big_mkcondr. by rewrite {1}Fi0. 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