proposition: Lemma f1 x : (\sum_(y in 'rV_n) f x y = 1)%R.
proof: Proof. set f' := fun i b => W (x ``_ i) b. suff H : (\sum_(g : {ffun 'I_n -> B}) \prod_(i < n) f' i (g i) = 1)%R. rewrite -{}[RHS]H /f'. rewrite (reindex_onto (fun vb : 'rV_n => [ffun x => vb ``_ x]) (fun g => \row_(k < n) g k)) /=; last first. move=> g _; apply/ffunP => /= i; by rewrite ffunE mxE. apply eq_big => vb. - rewrite inE. apply/esym/eqP/rowP => a; by rewrite mxE ffunE. - move=> _; rewrite ffunE; apply eq_bigr => i _; by rewrite ffunE. by rewrite -bigA_distr_bigA /= /f' big1 // => i _; rewrite FDist.f1. Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy jfdist_cond