proposition: Lemma fdist_rV_out (W : `Ch(A, B)) (P : {fdist A}) n (b : 'rV_n): `O(P, W) `^ _ b = \sum_(j : 'rV[A]_n) (\prod_(i < n) W j ``_ i b ``_ i) * P `^ _ j.
proof: Proof. rewrite fdist_rVE. under eq_bigr do rewrite fdist_outE. rewrite bigA_distr_big_dep /=. rewrite (reindex_onto (fun p : 'rV_n => [ffun x => p ``_ x]) (fun y => \row_(k < n) y k)) //=; last first. by move=> i _; apply/ffunP => /= n0; rewrite ffunE mxE. apply: eq_big. - move=> a /=; apply/andP; split; first exact/finfun.familyP. by apply/eqP/rowP => a'; rewrite mxE ffunE. - move=> a Ha; rewrite big_split /=; congr (_ * _)%R. + by apply eq_bigr => i /= _; rewrite ffunE. + by rewrite fdist_rVE; apply eq_bigr => i /= _; rewrite ffunE. 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