proposition: Lemma chain_rule_multivar (A : finType) (n : nat) (P : {fdist 'rV[A]_n.+1}) (i : 'I_n.+1) : i != ord0 -> (`H P = `H (fdist_col' P i) + cond_entropy (fdist_prod_of_rV (fdist_perm P (put_front_perm i))))%R.
proof: Proof. move=> i0; rewrite fdist_col'_put_front // -fdistX1. rewrite -{2}(fdistXI (fdist_prod_of_rV _)) -chain_rule joint_entropyC fdistXI. by rewrite entropy_fdist_prod_of_rV entropy_fdist_perm. 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