proposition: Lemma rsum_rmul_tuple_pmf_tnth {C : finType} n k (Q : {fdist C}) : \sum_(t : {:k.-tuple ('rV[C]_n)}) \prod_(m < k) (Q `^ n) t !_ m = 1.
proof: Proof. transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) Q `^ _ (j m)). rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)]) (fun x => fgraph x)) //=; last first. by move=> f _; apply/ffunP => /= i; rewrite ffunE tnth_fgraph enum_rankK. rewrite (big_tcast (esym (card_ord k))) esymK. apply eq_big => //. - move=> i /=; apply/esym/eqP/eq_from_tnth => j. by rewrite tnth_fgraph ffunE enum_valK. - by move=> i _; apply eq_bigr => j _; rewrite ffunE /= tcastE -enum_rank_ord. rewrite -(bigA_distr_bigA (fun m xn => Q `^ _ xn)) /= big_const. by rewrite FDist.f1 iter_mulR exp1R. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code