proposition: Lemma dom_conv p (x y u v : {fdist A}) : x `<< y -> u `<< v -> x <| p |> u `<< y <| p |> v.
proof: Proof. move=> /dominatesP xy /dominatesP uv; apply/dominatesP => a. rewrite !fdist_convE. rewrite paddR_eq0; [|exact/mulR_ge0 |exact/mulR_ge0]. rewrite !mulR_eq0 => -[[->|/xy ->]]; last first. by rewrite -RplusE -!RmultE mulR0 add0R => -[->|/uv ->]; rewrite !(mul0R,mulR0). by rewrite -RplusE -!RmultE mul0R add0R => -[|/uv ->]; [rewrite onem0 => /R1_neq_R0 | rewrite mulR0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(mathcomp_extra Rstruct reals) Reals Ranalysis_ext Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist jfdist_cond entropy convex binary_entropy_function log_sum divergence