proposition: Lemma entropy_TupleFDist : `H (P `^ n) = n%:R * `H P.
proof: Proof. elim:n=>[|n0 IH]. rewrite mul0R /entropy /= big1 ?oppR0 // => i _. by rewrite fdist_rV0 /log Log_1 mulR0. rewrite S_INR mulRDl mul1R -IH /entropy -(big_rV_cons_behead _ xpredT xpredT). rewrite /= -oppRD; congr (- _). rewrite [LHS](_ :_ = \sum_(i | i \in A) P i * log (P i) * (\sum_(j in 'rV[A]_n0) (\prod_(i0 < n0) P j ``_ i0)) + \sum_(i | i \in A) P i * \sum_(j in 'rV[A]_n0) (\prod_(i0 < n0) P j ``_ i0) * log (\prod_(i0 < n0) P j ``_ i0)); last first. rewrite -big_split /=; apply: eq_bigr => i _. rewrite -mulRA -mulRDr (mulRC (log (P i))) (big_distrl (log (P i)) _ _) /=. rewrite -big_split /= big_distrr /=. apply: eq_bigr => i0 _. rewrite fdist_rVE. rewrite big_ord_recl (_ : _ ``_ ord0 = i); last first. by rewrite mxE; case: splitP => // j Hj; rewrite mxE. rewrite -mulRA. case/RleP : (FDist.ge0 P i) => [pi_pos| <-]; last by rewrite !mul0R. congr (P i * _). rewrite -mulRDr. rewrite (@eq_bigr _ _ _ _ _ _ (fun x => P ((row_mx (\row_(_ < 1) i) i0) ``_ (lift ord0 x))) (fun x => P i0 ``_ x)) => [|i1 _]; last first. congr (P _). rewrite mxE. case: splitP => j; first by rewrite (ord1 j). by rewrite lift0 add1n; case=> /eqP /val_eqP ->. case: (Req_dec 0 (\prod_(i' < n0) P i0 ``_ i')) => [<-|rmul_non0]. by rewrite !mul0R. have rmul_pos : 0 < \prod_(i1<n0) P i0 ``_ i1. move/eqP in rmul_non0. apply/RltP; rewrite lt0r eq_sym rmul_non0; apply/RleP/prodR_ge0 => ?. exact/RleP/FDist.ge0. by rewrite /log LogM // !mulRDr mulRA mulRA. rewrite (_ : \sum_(j in 'rV_n0) _ = 1); last first. by rewrite (_ : 1 = 1%mcR)// -(FDist.f1 (P `^ n0)); apply eq_bigr => i _; rewrite fdist_rVE. rewrite -big_distrl /= mulR1 [in RHS]addRC; congr (_ + _). rewrite -big_distrl /= FDist.f1 mul1R; apply eq_bigr => i _. by rewrite fdist_rVE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code