proposition: Lemma exp_cdiv_left (H : P |- V << W) : exp_cdiv = exp2 (-INR n * D(V || W | P)).
proof: Proof. rewrite /exp_cdiv. suff : (type.d P) |- V <<b W by move=> ->. apply/forallP => a; apply/implyP => Pa0. apply/forall_inP => b /eqP Wab; by rewrite (dominatesE (H _ Pa0)). 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