proposition: Lemma cond_relative_entropy_compat : R `X P `<< R `X Q -> cond_relative_entropy (R, P) (R, Q) = D(P || Q | R).
proof: Proof. move=> PQ. rewrite /cond_relative_entropy cdiv_is_div_joint_dist; last exact/dom_by_cdom_by. rewrite /div. under eq_bigr do rewrite big_distrr /=. rewrite pair_big /=; apply eq_bigr => -[a b] _ /=. rewrite (_ : (R `X P) (a, b) = (R `X P) (a, b)); last by rewrite fdist_prodE. rewrite (_ : (R `X Q) (a, b) = (R `X Q) (a, b)); last by rewrite fdist_prodE. rewrite mulRA. rewrite {1}/jcPr. rewrite fdistX2 fdist_prod1 Pr_set1. have [H|H] := eqVneq (R a) 0. by rewrite H mul0R fdist_prodE H -RmultE !mul0R/=. congr (_ * log _). by rewrite setX1 Pr_set1 fdistXE fdist_prodE /=; field; exact/eqP. rewrite /jcPr !setX1 !Pr_set1 !fdistXE !fdistX2. have [H'|H'] := eqVneq ((R `X Q) (a, b)) 0. have : (R `X P) (a, b) = 0 by move/dominatesP : PQ => ->. rewrite fdist_prodE /= mulR_eq0 => -[| -> ]. by move/eqP : H; tauto. rewrite -RmultE. by rewrite !(mulR0,mul0R,div0R). by rewrite 2!fdist_prod1 /=; field; split; exact/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg finset matrix) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb ln_facts num_occ fdist entropy channel divergence types jtypes proba jfdist_cond