proposition: Lemma tuple_dist_type_entropy t : tuple_of_row t \in T_{P} -> (type.d P) `^ n t = exp2 (- INR n * `H P).
proof: Proof. move/(@tuple_dist_type t) => ->. rewrite (_ : \prod_(a : A) type.d P a ^ (type.f P) a = \prod_(a : A) exp2 (type.d P a * log (type.d P a) * INR n)); last first. apply eq_bigr => a _. case/boolP : (0 == type.d P a) => H; last first. have {}H : 0 < type.d P a. have := FDist.ge0 (type.d P) a. move/RleP. case/Rle_lt_or_eq_dec => // abs. rewrite (_ : 0%mcR = 0)// in abs. by rewrite abs eqxx in H. rewrite -{1}(logK H) -exp2_pow. congr exp2. rewrite -mulRA [X in _ = X]mulRC -mulRA mulRC. congr (_ * _). by rewrite type_fun_type. - move/eqP : (H) => <-. rewrite -(_ : O = type.f P a); first by rewrite !mul0R exp2_0 /pow. apply INR_eq. rewrite {1}/INR. rewrite -(@eqR_mul2r ( / INR n)); last by apply/invR_neq0; rewrite INR_eq0; exact/eqP. by rewrite type_fun_type // -(eqP H) mulR0. rewrite -(big_morph _ morph_exp2_plus exp2_0) -(big_morph _ (morph_mulRDl _) (mul0R _)). by rewrite /entropy Rmult_opp_opp mulRC. 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