proposition: Lemma joint_dominates : P |- V << W -> (P `X V) `<< (P `X W).
proof: Proof. move=> V_dom_by_W /=; apply/dominatesP => ab Hab. case/RleP/leR_eqVlt : (FDist.ge0 P ab.1) => [/esym|] Hab1. - by rewrite fdist_prodE Hab1 -RmultE mul0R. - rewrite fdist_prodE in Hab. rewrite fdist_prodE (dominatesE (V_dom_by_W _ _)) -?RmultE ?mulR0 //. + exact/gtR_eqF. + move: Hab; rewrite mulR_eq0 => -[|//]. by move: (gtR_eqF _ _ Hab1) => /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