proposition: Lemma chain_rule_rV (A : finType) (n : nat) (P : {fdist 'rV[A]_n.+1}) : `H P = \sum_(i < n.+1) if i == O :> nat then `H (head_of_fdist_rV P) else cond_entropy (fdistX (fdist_belast_last_of_rV (fdist_take P (lift ord0 i)))).
proof: Proof. elim: n P => [P|n IH P]. by rewrite big_ord_recl /= big_ord0 addR0 -entropy_head_of1. rewrite entropy_rV chain_rule {}IH [in RHS]big_ord_recr /=. rewrite fdist_take_all; congr (_ + _); apply eq_bigr => i _. case: ifP => i0; first by rewrite head_of_fdist_rV_belast_last. congr (cond_entropy (fdistX (fdist_belast_last_of_rV _))). rewrite /fdist_take /fdist_fst /fdist_belast_last_of_rV !fdistmap_comp. congr (fdistmap _ P); rewrite boolp.funeqE => /= v. apply/rowP => j; rewrite !mxE !castmxE /= !mxE /= cast_ord_id; congr (v _ _). exact: val_inj. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence