proposition: Lemma tuple_dist_type t : tuple_of_row t \in T_{P} -> (type.d P) `^ n t = \prod_(a : A) type.d P a ^ (type.f P a).
proof: Proof. move=> Hx. rewrite fdist_rVE. rewrite (_ : \prod_(i < n) type.d P (t ``_ i) = \prod_(a : A) (\prod_(i < n) (if a == t ``_ i then type.d P t ``_ i else 1))); last first. rewrite exchange_big; apply eq_big ; first by []. move=> i _. rewrite (bigID (fun y => y == t ``_ i)) /=. rewrite -/(INR n.+1) big_pred1_eq eqxx big1 ?mulR1 //. by move=> i0 /negbTE ->. apply eq_bigr => a _. rewrite -big_mkcond /= -/(INR n.+1). transitivity (\prod_(i < n | t ``_ i == a) (INR (type.f P a) / INR n)). apply eq_big => // i. move/eqP => ->. by rewrite INR_type_fun. rewrite big_const iter_mulR INR_type_fun. congr (_ ^ _). rewrite /typed_tuples inE in Hx. move/forallP/(_ a)/eqP : Hx. rewrite -INR_type_fun eqR_mul2r; last by apply/invR_neq0; rewrite INR_eq0; exact/eqP. move/INR_eq => ->. rewrite num_occ_alt cardsE /=. apply eq_card => /= n0. by rewrite /in_mem /= tnth_mktuple. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq