proposition: Lemma convex_div : convex_function (uncurry_dom_pair (@div A)).
proof: Proof. move=> [x Hx] [y Hy] p /=; rewrite /uncurry_dom_pair /=. rewrite /convex_function_at/= avgRE 2!big_distrr /= -big_split /= /div. apply leR_sumR => a _; rewrite 2!fdist_convE. have [y2a0|y2a0] := eqVneq (y.2 a) 0. rewrite y2a0 (_ : y.1 a = 0) ?(mulR0,addR0,mul0R); last first. by move/dominatesP : Hy; exact. have [x2a0|x2a0] := eqVneq (x.2 a) 0. rewrite (_ : x.1 a = 0). by rewrite -!RmultE -!RplusE ?(mul0R,mulR0,addR0). exact/((dominatesP _ _).1 Hx). have [p0|p0] := eqVneq p 0%:pr. by rewrite p0 -!RmultE -!RplusE ?(mul0R,mulR0,addR0). apply/Req_le; rewrite -!RmultE -!RplusE mulRA ?(mulR0,addR0); congr (_ * _ * log _). simpl. by field; split; exact/eqP. have [x2a0|x2a0] := eqVneq (x.2 a) 0. rewrite x2a0 (_ : x.1 a = 0)// -?RplusE -?RmultE ?(mulR0,add0R,mul0R); last first. by move/dominatesP : Hx; exact. have [->|t0] := eqVneq (Prob.p p).~ 0; first by rewrite !mul0R. apply/Req_le; rewrite mulRA; congr (_ * _ * log _). simpl. by field; split; exact/eqP. set h : {fdist A} -> {fdist A} -> {ffun 'I_2 -> R} := fun p1 p2 => [ffun i => [eta (fun=> 0) with ord0 |-> Prob.p p * p1 a, lift ord0 ord0 |-> (Prob.p p).~ * p2 a] i]. have hdom : h x.1 y.1 `<< h x.2 y.2. apply/dominatesP => i; rewrite /h /= !ffunE; case: ifPn => _. by rewrite mulR_eq0 => -[->|/eqP]; [rewrite mul0R | rewrite (negbTE x2a0)]. case: ifPn => // _. by rewrite mulR_eq0 => -[->|/eqP]; [rewrite mul0R | rewrite (negbTE y2a0)]. have h0 p1 p2 : [forall i, (0 <= h p1 p2 i)%mcR]. apply/forallPP; first by move=> ?; exact/RleP. move=> ?; rewrite /h /= ffunE. case: ifPn => [_ | _]; first exact/mulR_ge0. case: ifPn => [_ |//]. by apply/mulR_ge0 => //; exact/onem_ge0/prob_le1. have h01 (x0 : 'I_2) : 0 <= mkNNFinfun (h0 x.1 y.1) x0. rewrite /= /h ffunE/=; case: ifPn => _; first exact: mulR_ge0. by case: ifPn => // _; exact: mulR_ge0. have h02 (x0 : 'I_2) : 0 <= mkNNFinfun (h0 x.2 y.2) x0. rewrite /= /h ffunE/=; case: ifPn => _; first exact: mulR_ge0. by case: ifPn => // _; exact: mulR_ge0. have := log_sum setT (mkNNFinfun (h0 x.1 y.1)) (mkNNFinfun (h0 x.2 y.2)) h01 h02 hdom. rewrite /= -!sumR_ord_setT !big_ord_recl !big_ord0 !addR0. rewrite /h /= !ffunE => /leR_trans; apply. rewrite !eqxx eq_sym (negbTE (neq_lift ord0 ord0)) -!mulRA; apply/Req_le. congr (_ + _ ). have [->|t0] := eqVneq p 0%:pr; first by rewrite !mul0R. by congr (_ * (_ * log _)); field; split; exact/eqP. have [->|t1] := eqVneq (Prob.p p).~ 0; first by rewrite !mul0R. by congr (_ * (_ * log _)); field; split; exact/eqP. 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